[_dain_]

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

Affine types give a safety guarantee: you can't use it more than once. The bad thing (double free, use after free) does not happen.

Linear types give that same safety guarantee, plus a liveness guarantee: you must use it, possibly in some nontrivial way.

A function that takes an affine value as an argument is enforcing a contract about the past behaviour of the caller, leading up to the call: having the affine value is proof that certain other functions were called in the right way to produce it. But returning an affine value gives you weaker guarantees about future behaviour, because you can use it zero times. At most you know that it will get Dropped. But maybe you want to enforce more interesting things than the Drop trait can express. Returning a linear value lets you do this: maybe the linear Foo you return can only be disposed of in conjunction with a linear Bar, like

    fn consume(x: Foo, y: Bar) -> Baz

And perhaps now Baz itself is linear, which has to be consumed in some other way ... at any rate, returning a linear value is proof that in the future, the program will advance through a particular state machine of function calls, where the states and transitions are defined by the available signatures. If Foo is linear but there's no simple function like

    fn drop(x: Foo) -> Unit

then buckle in, the compiler says you're not getting off the ride until it's over.

[skybrian]

It seems like a language could support both. That is, a type could either be automatically droppable or not.

[dgreensp]

Yes, this. The notable thing in Austral is not that linear types are used somewhere, it’s that it’s all linear, even when destruction is just deallocation and could easily be done by the compiler (even in the presence of exceptions).

[_dain_]

You might want finer-grained control over when deallocation happens.