[Rusky]

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.

[treyd]

One thing with explicit drops that Rust is having is that the thread can get SIGKILLed at any point without running destructors, which can complicate sync primitives and cause deadlocks in other threads if RAII is used for that. People do use it for that effectively but even if you have support for explicit drops it's really hard to ensure they actually run.

[crabmusket]

I can't quite parse your first line or two. Are you saying that explicit drops make SIGKILL a problem because the compiler can't automatically add in the right cleanups? Whereas if the compiler is in charge of adding all the drops, it can insert those into a signal handler?

[Rusky]

Rust certainly doesn't insert automatic cleanup in signal handlers. I don't think there's actually any meaningful difference between linear types and automatic drop here.

[throwup238]

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

Couldn't the language allow something like Zig's `defer` op except tie that explicit destructor to the type?

[Rusky]

Sure, this would just desugar to normal control flow and be checked for linearity in the usual way.

I'm not sure what you mean exactly by "tie to the type," though? Just some kind of standard name for it? The benefit of linearity here is that you can change its signature while still getting the compiler to enforce its usage, so you probably wouldn't want it to look like e.g. Rust's Drop trait.

[_dain_]

Because it doesn't have to be something you'd ordinarily think of as a "destructor". e.g. you might have multiple possible functions that consume the value, because you're modelling a state machine with several outgoing edges from the type-state. You get to choose the one you call.

[throwup238]

`defer` allows for executing arbitrary expressions based on scope (the "destructor" called depends on the code path)

[aatd86]

Curious, aren't lifetimes and borrowing there in order to control aliasing that linear type preclude?

I was seeing linear types as a kind of: manual ssa + definite assignment analysis + unused variable analysis with the goal to facilitate some typestate analysis by the compiler.

I know barely anything on the subject, just wondering.

[Rusky]

Lifetimes and borrowing are a convenient thing to have together with linear or affine types, but you can use them on their own as well- e.g. Rust lets you borrow Copy types.

At their core, the definition of linear and affine type systems don't reference SSA or dataflow analysis either. Type systems are generally described using the notation of logic (see this intro if you're unfamiliar: https://langdev.stackexchange.com/a/2693/910), and then to get linearity you define the inference rules such that a use of a resource removes it from the context (one way to write this: https://plato.stanford.edu/entries/logic-linear/#SeqCal).

Things like definite assignment are more user-facing convenience features that are also built on top of the core linear logic.

[aatd86]

Oops, I still don't understand. With linear types, you don't have any aliasing so I don't see the value for borrowing. (maybe I'm misunderstanding the idea behind linear types?)

Seems to me, perhaps wrongly, that since there is no aliasing and values are always used, once a value is not returned by a function to be consumed, it's lifetime has effectively ended. So it's automatic?

The point I was making about ssa, dfa, etc. was that it was putting these aspects into userland via the type system.

[Rusky]

With linear types alone you don't have any aliasing. Borrowing is a controlled way to recover some aliasing while retaining the benefits of linearity.

[galangalalgol]

I believe I read australs borrow checker is rusts old version, possibly verbatim?

[crabmusket]

I haven't seen anything like that. I don't think Rust ever had linear types. This blog post has an explanation of Austral's linear type checking:

https://borretti.me/article/how-australs-linear-type-checker...