Higher RAII, and the Seven Arcane Uses of Linear Types

submited by
Style Pass
2024-05-14 13:00:09

We'd love a way to guarantee that we remember to do something. Unfortunately, today's compilers and languages can't really solve this problem for us.

But hark! We can change that, with Higher RAII, a technique where we use linear types that can only be destroyed in certain places.

If you look up linear types online, you'll find a lot of unhelpful definitions, like a linear type is a type that can't be aliased, can't be cloned, and must be "used" exactly once. 0

So for now, let's use a less correct but more helpful definition: A linear struct must eventually be explicitly destroyed. 1

In other words, a linear struct can't just go out of scope. When the user lets a linear struct go out of scope, the compiler gives an error.

Other languages might automatically clean it up, or call a destructor or drop() method, but here we've opted into the compiler error instead.

This might seem like a weird restriction, but if we use it in a certain way, it can unlock some rather amazing capabilities:

Leave a Comment