Higher RAII and the seven arcane uses of linear types
verdagon.dev
verdagon.dev
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 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. ^_^
How far are you with variants? Have you looked at Hare's union types?
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!
Based more on the linked podcast than the current article
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.”
Also, consider:
for i in range(100):
array[i] = mylinearvariable
for j in range(100):
x=complicated(j)
destroy array[x]
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).
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.
The emptying could be in a completely different function, called under some arbitrarily complex condition.
1. drop_into(list, func): It consumes the list, calling the given `func` for each element.
2. expect_empty(list): Consumes the list, panicking if the list isn't empty.
fn expect_empty(list) {
drop_into(list, () => panic());
}
If you want to discourage runtime checks, you could even make the programmer do the above themselves since it's a one-liner anyway.
(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)
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.
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.
The Rust language server seems really good. What have you been missing there?
On June 27, 2016, Microsoft announced a collaboration with Red Hat and Codenvy to standardize [Language Server Protocol]'s specification
vs
initial
Date: 2017-12-21 22:25:45 +0300
* 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.
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!
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.
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.
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!
PS. Congrats! https://verdagon.dev/blog/easter-egg-notes
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.
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 godbolt hopefully illustrates: 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)