Interview about Austral, a systems programming language with linear types

As someone working on a language myself, I found this to be very high-quality material! It aligns with a lot of my thinking, and it’s educational.

A random part of interest: I followed the link about how linear types and exceptions don’t mix: https://borretti.me/article/linear-types-exceptions In it, the author explains how linear types always need to be explicitly destroyed, and if you end up in a “catch” block, you can’t easily go back and destroy things that are now out of scope, which control flow got interrupted while doing things with. “Why not just destroy things when they go out of scope?” I thought. The author addresses this, saying that types that you have to “consume” “at most once” are called affine types, and the compiler can clean them up for you, and it solves the problem with exceptions. Rust has affine types, and you don’t have to explicitly “destruct” every string/object/resource using the appropriate destructor for that type, manually, as you do with linear types (of course, the compiler will make sure you do it, but you have to do it).

So why does Austral use linear types, not affine types? The reasons given do not really resonate with me (but I’m not a systems programmer); it’s that the compiler would have to insert hidden function calls, and secondarily, for temporary/intermediate values, the order of invocation might not be obvious; plus, maybe the programmer not doing something with a value is a mistake. I’m really glad the reasons are written out, however.

In other areas I feel very aligned with the author, such as on the value of required type annotations and local inference rather than global inference, and I’ve saved the link to refer back to the way the opinion is stated.

> So why does Austral use linear types, not affine types?

Because linear types are simpler. The major reason here is that you don't need a "fancy" inference engine of lifetimes like the Rust borrow checker.

You don't need lifetimes or lifetime inference for affine types, either. Lifetimes/regions/borrowing are an orthogonal extension that you can add on top of either affine or linear types.

(In fact Austral includes a region/borrowing system as well! It is a bit more explicit than Rust, along the lines of Rust's pre-NLL borrow checker, and with concrete binding forms instead of inference for regions, but this is also unrelated to the affine/linear distinction.)

One reason for linear types over automatic scope-based destruction is that the final destruction can take arguments and produce results in a more streamlined way. This is nice for e.g. handling errors on file close.

Linear and uniqueness types sort of collapse into the same thing when an object is required to stay linear or unique for its entire life cycle.

They become distinct, and sort of dual to each other, when you relax this restriction: linearity ensures that no copies or aliases are produced going forward, while uniqueness ensures that no copies or aliases have ever been produced in the past.

In other words, if you call a function that is linear in its parameter, you know it won't form any additional copies of the argument, but the function can't assume it has the only reference to that argument, so it can't e.g. update it destructively. Conversely, a function that takes a unique parameter can make that assumption, but its caller can no longer assume that the argument it passed in is unique.

See also this recent paper on the two: https://granule-project.github.io/papers/esop22-paper.pdf

It’s exciting seeing new languages popup offering memory safety.