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.
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.”
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!
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
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.