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
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?
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.
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).
It could, but then that List would have to be linear itself, and then the program would make sure that you eventually drain the list and destroy each element.
(One caveat is for linears in globals, which aren't implemented in Vale yet. We haven't decided which strategy we're going with there, but TFA talks about some)
> Can’t the program just accidentally stash the linear type in some list and forget about it?
No, because the type of the list elements would have to be that linear type (and that linear type is not a subtype of any normal type, not even an "Any" type if you have one). So you can only put linear-typed values into a list type that obeys the rules of linear typing (so e.g. you might be able to split the list into head and tail, but you can't just drop n elements from it - and of course the type of the list itself will be linear, or maybe polymorphic in the linearness of its element type), and if you want to implement a more general-purpose list implementation you won't be able to add linear-typed values to that list.
Depends on the rest of your type system. If your language is capable of tracking whether a list is empty then it can allow dropping empty lists without a runtime check.
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?
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.
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.
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?
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?
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.
1. In RC and tracing GC languages, a linear object would need exactly one special "linear" reference to it, which would be responsible for eventually "consuming" (though not deleting) the object by handing it to its final destination function. (You can tell, I'm trying real hard to not say destructor here)
2. In single-ownership languages like C++, Rust, etc. we've been conflating the destructor to handle two things: fulfilling the object's final purpose, and handling exceptions/panics. It seemed convenient at the time, but it also prevented linear types.
But honestly, I think we were just stuck in a local maximum. There was no reason to change those points because we didn't know about higher RAII, and we didn't know about higher RAII because those two points prevented linear types.
But with more of us exploring this new area (Vale, Austral, maybe even Mojo!), I daresay we'll one day see linear types and higher RAII entering the mainstream. Especially if someone can come up with a better name!
> In single-ownership languages like C++, Rust, etc. we've been conflating the destructor to handle two things: fulfilling the object's final purpose, and handling exceptions/panics.
Well, from a transactional point of view, a good design for C++ classes is to have implicit destructors (i.e. a conventional C++ destructor) rollback any change, while explicit ones would commit. This works very well with exceptions.
What C++ lacks is the ability to statically prevent you from calling an explicit destructor twice, but should be doable, for example, in rust.
Thanks for the answer! Not gonna lie, I don't have the background to understand all your articles, just enough to see that you're pushing the boundary on what's possible and it's really cool!
Thanks! And yeah I get that a lot >_> You're always welcome to swing by the discord where I can give a less arcane explanation! (https://discord.gg/SNB8yGH)
Besides the question of usability, there are at least 3 major problems that come up in the vicinity of linear types (some also apply to ownership in general):
* Do you assume trivial moves? Because that's not a safe assumption. Related, many examples only really work for local variables, and otherwise rely on special language object holders or something, which even if they can also be implemented in user code often break safety elsewhere.
* What, exactly, happens to your objects when a task unwinds?
* What do you do about leaked cycles?
* Inheritance is no longer a simple part of the language. And trust me, you do want inheritance.
It's not that these questions don't have possible answers (a few of which are touched on in the linked article), but there are no easy answers.
I'm glad you brought inheritance up! This rule has solved it nicely in my experience: if a struct is linear, then it can only inherit linear interfaces. And implementation inheritance works because it's really just a combination of interface inheritance + composition + method forwarding, none of which seem to have any particular trouble with linear types.
Even if a language really wanted to have linear types in reference-counted objects, I don't think we'd see cycles in practice. Generally, for a reference-counted object to contain a linear type, we'd need exactly one reference to be the special "linear reference" (think a linear flavor of unique_ptr) which has ultimate responsibility for "consuming" (albeit not deleting) the contents. Making a unique_ptr cycle is much harder than making a regular RC cycle, so I'm not too worried, even if it is theoretically possible.
Re: trivial moves, I'm not sure what you mean. The system works through the entire program, not just local variables. Also, the `onException` method would also handle panics. Hope that helps!
As for inheritance - I'm increasingly convinced that it is a useful idea to have an explicit `Object` (or `BaseObject`, to deal with languages where primitives are special) class at the root of the hierarchy, rather than relying on some nebulous type-checker-only `Top` type (sometimes called `Any`, though that usually has additional footguns). One thing I do think is a mistake in languages that have an `Object` class is that it is often not abstract. In particular it is often used for sentinel-like objects (with no contents - the lack of a name is annoying), to say nothing of Javascript's mess. Is "top-most interface" really a sufficient concept? As much as I've come to love late-defined traits (among others, no more PIMPL), I'm not convinced we can really afford to stop thinking in terms of an OO tree, or even to give up on multiple inheritance
You don't need RC to have a cycle - it already occurs with a pair of structs that refer to each other using `mut Option[Unique[T]]`. Rust seems to have settled for "document it aggressively, and otherwise ignore it" ... yet code very similar to this is actually very useful, so (with a few extra layers of nesting) it often does appear spontaneously in the wild. But the whole point of linear types is that you can no longer just say "leaks are okay I guess".
Moving even a small 64KB buffer isn't actually trivial even if your type system thinks it is by composition, but most linear-ish type systems seem to aggressively use destructuring (possibly via pattern-matching) which relies on moving the members. Not to mention all the other actually-useful things C++ move constructors can do (update peer objects, for example). While "move-by-default" is a definite winner, "trivial-move-only" is not. The question of "what exactly happens so I can move out of a language-defined Option[T], leaving None ... vs how can a user-defined variant type choose to do something similar" is significantly complicated by nontrivial moves.
> Inheritance is no longer a simple part of the language. And trust me, you do want inheritance.
I don't miss it.
> languages where primitives are special
Isn't the object-primitive separation a design flaw? (e.g. c++ can have lists of int, but Java cannot. In Java, sometimes a boolean has two values and sometimes 3, etc.)
> root of the hierarchy
Why a hierarchy? All beginner Java devs at some point attempt to put their domain objects into some kind of hierarchy before realising the futility of it. Especially in game dev.
Sometimes I want to operate on objects which can quack(), and sometimes I want to operate on objects which can toBytes(), and sometimes I want to operate on objects which can do both those those things. But why must they have a common ancestor? Why can't they simply exist in disjoint families?
> I'm increasingly convinced that it is a useful idea to have an explicit `Object` (or `BaseObject`, to deal with languages where primitives are special) class at the root
This is one of those things I dislike about Java. Object has a bunch of included behaviours that I do not want. equals() and hashCode() have the wrong default behaviour, and toString() isn't much better. I would much prefer the compiler to block me if I try to equate two things which haven't defined equality, rather than slip in its own implementation.
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.
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)
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.
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.