8 ms·

Higher RAII and the seven arcane uses of linear types

99 points by agluszak 2y ago

verdagon 2y ago
Cool to see this on HN! This is my favorite part of language design: you get to play with weird ideas and see how the implications cascade through the rest of the program. It kind of blew my mind when a linear type solved a caching problem. Now it's kind of a curse, because any time I code in a normal language (even the modern ones like Scala and Rust) I see places (concurrency, coroutines, etc) where we could have statically prevented these bugs.
- spartanatreyu 2y ago
  I didn't know you were back. I always love reading your posts and now I find out I've got 3 new ones to read! It's going to be a good few days. ^_^
  - verdagon 2y ago
    Thank you, my friend =) So glad to hear you enjoy the articles!
- thoasdfwdas 2y ago
  I know that feeling, living life without affine types is awful. How far are you with variants? Have you looked at Hare's union types?
  - verdagon 2y ago
    I've got some weird plans for variants. Basically, we'd represent an enum as a non-heap-allocated sealed interface with a struct for each "case". Basically, think of a Scala case class. Then, depending on where we put it (heap vs local/member/element), it will be compiled differently (a traditional interface vs a tagged variant, respectively). ...I don't expect that to make any sense. Alas, I haven't started on sealed interfaces yet. Right now I'm occupied with the Rust interop; I'm hoping we can be able to seamlessly e.g. `import rust.std.collections.Vec<i32>;` and have it work. A lot of pieces have to fall into place for that to work though, especially since that's generic and Rust doesn't even have a stable ABI. It's kicking my ass, and I'm having a lot of fun with it!
- 3836293648 2y ago
  Have you considered that the whole destructors with multiple arguments thing is more elegantly done with just making the zero argument destructor private and having a wrapper function in the proper module as the only way of accessing it. Based more on the linked podcast than the current article
  - verdagon 2y ago
    You're exactly right, and that's kind of what Vale's `destruct` is, if you squint.
- amluto 2y ago
  I think all of this is great, except that you’re triggering my biggest pet peeve about linear types: the name :) Seriously, though, every time I hear it, I think “hehe, ‘linear’ is like ‘affine’ but even more restrictive. Math is great!” (I hope there’s some better justification for the name.) Maybe a more descriptive name like “must_consume” would be better? I very much appreciate how Rust took the concepts of covariant and contravariant types (and invariant types, which are not the same as what programmers think of as “invariants”) and made the user-facing feature be “phantom” instead. It’s much, much easier to remember what a phantom does than to remember which style of variance is “co” and which is “contra.”
  - glandium 2y ago
    Simple uses of phantom are easy to remember, but the obscure ones are just as hard as remembering what type of variance co and contra are. https://doc.rust-lang.org/nomicon/phantom-data.html#table-of-phantomdata-patterns https://doc.rust-lang.org/nomicon/phantom-data.html#table-of...
  - dullcrisp 2y ago
    I could be wrong but I’m pretty sure affine types were named after linear types, not vice versa.
NeutralForest 2y ago
Is there a reason we're not seeing linear types in more languages? I'm not familiar with how difficult it is to implement or if there are usage issues that end up showing only after a while?
- lmm 2y ago
  Plenty of new research languages are coming out with linear types. Building a mainstream language is extremely expensive these days, to the point that probably only a handful of companies can attempt it. I work in Scala which teeters on the edge of mainstream, and it's not the language itself that needs major backing, it's all the other stuff - IDEs, library repositories, build tools, profilers. I would love to leap into e.g. Idris, which does have linear types, but who's going to write an IDE for it? Even Rust struggles with this. And it's very hard to retrofit linear types onto an existing language, if you can even get a quorum in favour of doing so. Haskell is trying, and I wish them well, but it's not going to be easy, and again they're barely mainstream.
  - nequo 2y ago
    > Even Rust struggles with this. The Rust language server seems really good. What have you been missing there?
    - thoasdfwdas 2y ago
      It was years before we had rust-analyzer.
      - shepmaster 2y ago
        A year and a half doesn't seem like bad turnaround time to me. shrug On June 27, 2016, Microsoft announced a collaboration with Red Hat and Codenvy to standardize [Language Server Protocol]'s specification — https://en.wikipedia.org/wiki/Language_Server_Protocol https://en.wikipedia.org/wiki/Language_Server_Protocol vs initial Date: 2017-12-21 22:25:45 +0300 — https://github.com/rust-lang/rust-analyzer/commit/a63222cd240d9b5405826783603f3b391c90885d https://github.com/rust-lang/rust-analyzer/commit/a63222cd24...
IcyWindows 2y ago
Don't private destructors in c++ enable this?
- jandrewrogers 2y ago
  To some extent, yes. It creates issues for stack allocated types.
  - slaymaker1907 2y ago
    You can sort of work around it by placement new, but it’s still hugely inconvenient in the general case since the thing could have strict alignment requirements. Oh and not just stack, it also breaks global variables because destructors often get run for those when something gets unloaded or the program stops. Finally, because C++ gives you tons of control over how assignment works, it’ll probably break being able to use things within other objects unless you give those mark those classes as friend.
  - IcyWindows 2y ago
    Ah, I forgot that moved-from types in C++ still call the destructor.
- verdagon 2y ago
  They almost work like this. std::move doesn't actually move an object; it leaves an intact instance... which we still don't know how to destroy (because its destructor is private). This also means that if we have an e.g. Outer struct whose constructor takes some kind of linear type, that Outer has no way to ever relinquish it again, which is a prerequisite of all those desirable linear type / higher RAII patterns. This godbolt hopefully illustrates: https://godbolt.org/z/qqMnnKbnd https://godbolt.org/z/qqMnnKbnd though apologies if it's not too clear. If C++ didn't have its quirks, you'd fundamentally be correct. Higher RAII can almost completely be implemented by this one sentence: make destruction private. (In fact, that's why Vale's `destruct` keyword is file-private)
kccqzy 2y ago
In the transaction example, if this were C++, we could probably make the actual destructor private, and then have commit() and rollback() functions take the transaction object by rvalue reference (needs a layer of unique_ptr here). What am I missing? Is this a problem because it forces unique_ptr?
- verdagon 2y ago
  Almost, but see the replies to IcyWindows' comment for why this unfortunately doesn't work in C++. Also, I would love it if C++ had a way to actually move. That would unlock all sorts of interesting possibilities.
  - deleted 2y ago
    [deleted]
two_handfuls 2y ago
One thing I’m missing: how does the compiler check that the “destruct” function is called? Can’t the program just accidentally stash the linear type in some list and forget about it?
- throwaway17_17 2y ago
  The simplest method, omitting the type checking that would be required to verify that any ‘usage’ pre-destruction, any time the type checker encounters an expression that creates a value of linear type the ID (in whatever representation the compiler uses) could be stored in a list of linear object, then when the explicit destruction function is called on a linear object that ID is removed from the list. At the end of compilation (or more likely type checking) if the list is not empty the programmer clearly did not destruct some linear object and an error is issued.
  - two_handfuls 2y ago
    But you’re allowed to destroy in a different function. How does the compiler recognize which ID the variable has? Also, consider: for i in range(100): array[i] = mylinearvariable for j in range(100): x=complicated(j) destroy array[x] In this case it seems potentially extremely difficult for the compiler to know statically that the array will be empty in the end.
    - throwaway17_17 2y ago
      As to recognizing what ID a variable has, compilers often associate a global unique ID with each variable that exists in the translation unit. So when some variable x (or really any semantic object) is initialized to whatever its value is the compiler maps that source code x with ID 16373 (or whatever encoding the compiler is using for the mapping). This ID is what would be held in a ‘linear context’, probably in the type checker, and that ID is removed from the context when it is passed to an appropriate ‘destruction’ function. As to the pseudo-code, it seems like the ‘mylinearvariable’ is being copied 100 times and placed in the array slots. This is probably not possible for most descriptions of linear types, a key component of said types are that only one can exist. I have some qualms with TFA’s description of their types as linear, although I am pretty sure I understand the usage and acknowledge it is somewhat accepted terminology. Even in TFA I don’t think they would accept such semantics for their linear type. If ‘mylinesrvariable’ is a constructor of sorts creating unique linear objects in each slot, each of those would have an ID in the compiler that would be independently removing each of those IDs when said object is handed to the destroy statement. This sort of simple list/map between objects and IDs only works because the types are linear which means only one exists and there must be a single explicit usage of that object (which is the destruction in the semantics proposed in TFA).
miki123211 2y ago
You can implement a weaker version of this in any language that has either destructors or finalizers. Have every linear struct contain a private `was_consumed` field, false by default. Every method that consumes such a struct should set that field to true. If your language doesn't have single-owner references, such methods should also panic if the field is already true. Depending on how closely you subscribe to the "let it crash" philosophy, your destructor should do anything from writing a log to outright panicking and crashing your program when encountering a false value. You can even put all of this under an #ifdef so that it only runs in debug. This isn't as good as actual linear types, as errors will only appear at runtime and only for the code paths you actually hit in development, but it's better than nothing.
gpderetta 2y ago
Great article, but I thought that linear types already implied "named destructors", hence the "Higher RAII" moniker is redundant. If not, how do languages with linear types handle a linearly typed object lifetime?

99 points by agluszak 2y ago

Cool to see this on HN! This is my favorite part of language design: you get to play with weird ideas and see how the implications cascade through the rest of the program. It kind of blew my mind when a linear type solved a caching problem. Now it's kind of a curse, because any time I code in a normal language (even the modern ones like Scala and Rust) I see places (concurrency, coroutines, etc) where we could have statically prevented these bugs.

spartanatreyu 2y ago
I didn't know you were back. I always love reading your posts and now I find out I've got 3 new ones to read! It's going to be a good few days. ^_^
- verdagon 2y ago
  Thank you, my friend =) So glad to hear you enjoy the articles!
thoasdfwdas 2y ago
I know that feeling, living life without affine types is awful. How far are you with variants? Have you looked at Hare's union types?
- verdagon 2y ago
  I've got some weird plans for variants. Basically, we'd represent an enum as a non-heap-allocated sealed interface with a struct for each "case". Basically, think of a Scala case class. Then, depending on where we put it (heap vs local/member/element), it will be compiled differently (a traditional interface vs a tagged variant, respectively). ...I don't expect that to make any sense. Alas, I haven't started on sealed interfaces yet. Right now I'm occupied with the Rust interop; I'm hoping we can be able to seamlessly e.g. `import rust.std.collections.Vec<i32>;` and have it work. A lot of pieces have to fall into place for that to work though, especially since that's generic and Rust doesn't even have a stable ABI. It's kicking my ass, and I'm having a lot of fun with it!
3836293648 2y ago
Have you considered that the whole destructors with multiple arguments thing is more elegantly done with just making the zero argument destructor private and having a wrapper function in the proper module as the only way of accessing it. Based more on the linked podcast than the current article
- verdagon 2y ago
  You're exactly right, and that's kind of what Vale's `destruct` is, if you squint.
amluto 2y ago
I think all of this is great, except that you’re triggering my biggest pet peeve about linear types: the name :) Seriously, though, every time I hear it, I think “hehe, ‘linear’ is like ‘affine’ but even more restrictive. Math is great!” (I hope there’s some better justification for the name.) Maybe a more descriptive name like “must_consume” would be better? I very much appreciate how Rust took the concepts of covariant and contravariant types (and invariant types, which are not the same as what programmers think of as “invariants”) and made the user-facing feature be “phantom” instead. It’s much, much easier to remember what a phantom does than to remember which style of variance is “co” and which is “contra.”
- glandium 2y ago
  Simple uses of phantom are easy to remember, but the obscure ones are just as hard as remembering what type of variance co and contra are. https://doc.rust-lang.org/nomicon/phantom-data.html#table-of-phantomdata-patterns https://doc.rust-lang.org/nomicon/phantom-data.html#table-of...
- dullcrisp 2y ago
  I could be wrong but I’m pretty sure affine types were named after linear types, not vice versa.

NeutralForest 2y ago

Is there a reason we're not seeing linear types in more languages? I'm not familiar with how difficult it is to implement or if there are usage issues that end up showing only after a while?

lmm 2y ago
Plenty of new research languages are coming out with linear types. Building a mainstream language is extremely expensive these days, to the point that probably only a handful of companies can attempt it. I work in Scala which teeters on the edge of mainstream, and it's not the language itself that needs major backing, it's all the other stuff - IDEs, library repositories, build tools, profilers. I would love to leap into e.g. Idris, which does have linear types, but who's going to write an IDE for it? Even Rust struggles with this. And it's very hard to retrofit linear types onto an existing language, if you can even get a quorum in favour of doing so. Haskell is trying, and I wish them well, but it's not going to be easy, and again they're barely mainstream.
- nequo 2y ago
  > Even Rust struggles with this. The Rust language server seems really good. What have you been missing there?
  - thoasdfwdas 2y ago
    It was years before we had rust-analyzer.
    - shepmaster 2y ago
      A year and a half doesn't seem like bad turnaround time to me. shrug On June 27, 2016, Microsoft announced a collaboration with Red Hat and Codenvy to standardize [Language Server Protocol]'s specification — https://en.wikipedia.org/wiki/Language_Server_Protocol https://en.wikipedia.org/wiki/Language_Server_Protocol vs initial Date: 2017-12-21 22:25:45 +0300 — https://github.com/rust-lang/rust-analyzer/commit/a63222cd240d9b5405826783603f3b391c90885d https://github.com/rust-lang/rust-analyzer/commit/a63222cd24...

IcyWindows 2y ago

Don't private destructors in c++ enable this?

jandrewrogers 2y ago
To some extent, yes. It creates issues for stack allocated types.
- slaymaker1907 2y ago
  You can sort of work around it by placement new, but it’s still hugely inconvenient in the general case since the thing could have strict alignment requirements. Oh and not just stack, it also breaks global variables because destructors often get run for those when something gets unloaded or the program stops. Finally, because C++ gives you tons of control over how assignment works, it’ll probably break being able to use things within other objects unless you give those mark those classes as friend.
- IcyWindows 2y ago
  Ah, I forgot that moved-from types in C++ still call the destructor.
verdagon 2y ago
They almost work like this. std::move doesn't actually move an object; it leaves an intact instance... which we still don't know how to destroy (because its destructor is private). This also means that if we have an e.g. Outer struct whose constructor takes some kind of linear type, that Outer has no way to ever relinquish it again, which is a prerequisite of all those desirable linear type / higher RAII patterns. This godbolt hopefully illustrates: https://godbolt.org/z/qqMnnKbnd https://godbolt.org/z/qqMnnKbnd though apologies if it's not too clear. If C++ didn't have its quirks, you'd fundamentally be correct. Higher RAII can almost completely be implemented by this one sentence: make destruction private. (In fact, that's why Vale's `destruct` keyword is file-private)

kccqzy 2y ago

In the transaction example, if this were C++, we could probably make the actual destructor private, and then have commit() and rollback() functions take the transaction object by rvalue reference (needs a layer of unique_ptr here). What am I missing? Is this a problem because it forces unique_ptr?

verdagon 2y ago
Almost, but see the replies to IcyWindows' comment for why this unfortunately doesn't work in C++. Also, I would love it if C++ had a way to actually move. That would unlock all sorts of interesting possibilities.
- deleted 2y ago
  [deleted]

two_handfuls 2y ago

One thing I’m missing: how does the compiler check that the “destruct” function is called? Can’t the program just accidentally stash the linear type in some list and forget about it?

throwaway17_17 2y ago
The simplest method, omitting the type checking that would be required to verify that any ‘usage’ pre-destruction, any time the type checker encounters an expression that creates a value of linear type the ID (in whatever representation the compiler uses) could be stored in a list of linear object, then when the explicit destruction function is called on a linear object that ID is removed from the list. At the end of compilation (or more likely type checking) if the list is not empty the programmer clearly did not destruct some linear object and an error is issued.
- two_handfuls 2y ago
  But you’re allowed to destroy in a different function. How does the compiler recognize which ID the variable has? Also, consider: for i in range(100): array[i] = mylinearvariable for j in range(100): x=complicated(j) destroy array[x] In this case it seems potentially extremely difficult for the compiler to know statically that the array will be empty in the end.
  - throwaway17_17 2y ago
    As to recognizing what ID a variable has, compilers often associate a global unique ID with each variable that exists in the translation unit. So when some variable x (or really any semantic object) is initialized to whatever its value is the compiler maps that source code x with ID 16373 (or whatever encoding the compiler is using for the mapping). This ID is what would be held in a ‘linear context’, probably in the type checker, and that ID is removed from the context when it is passed to an appropriate ‘destruction’ function. As to the pseudo-code, it seems like the ‘mylinearvariable’ is being copied 100 times and placed in the array slots. This is probably not possible for most descriptions of linear types, a key component of said types are that only one can exist. I have some qualms with TFA’s description of their types as linear, although I am pretty sure I understand the usage and acknowledge it is somewhat accepted terminology. Even in TFA I don’t think they would accept such semantics for their linear type. If ‘mylinesrvariable’ is a constructor of sorts creating unique linear objects in each slot, each of those would have an ID in the compiler that would be independently removing each of those IDs when said object is handed to the destroy statement. This sort of simple list/map between objects and IDs only works because the types are linear which means only one exists and there must be a single explicit usage of that object (which is the destruction in the semantics proposed in TFA).

miki123211 2y ago

You can implement a weaker version of this in any language that has either destructors or finalizers. Have every linear struct contain a private `was_consumed` field, false by default. Every method that consumes such a struct should set that field to true. If your language doesn't have single-owner references, such methods should also panic if the field is already true. Depending on how closely you subscribe to the "let it crash" philosophy, your destructor should do anything from writing a log to outright panicking and crashing your program when encountering a false value. You can even put all of this under an #ifdef so that it only runs in debug. This isn't as good as actual linear types, as errors will only appear at runtime and only for the code paths you actually hit in development, but it's better than nothing.

gpderetta 2y ago

Great article, but I thought that linear types already implied "named destructors", hence the "Higher RAII" moniker is redundant. If not, how do languages with linear types handle a linearly typed object lifetime?