> 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.
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.
(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.
Couldn't the language allow something like Zig's `defer` op except tie that explicit destructor to the type?
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.
https://borretti.me/article/how-australs-linear-type-checker...
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.
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.
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.
Do they look simpler in cheesy anecdotes? Sure.
But again, graphs and linked structures come in the to fray and it’s immediately noticeable that there’s be some problems here. Or maybe I am crazy in thinking that “being forced to update every single link just cause one node updated” is a problem.
Even if this is only superficial, I foresee there being not insignificantly annoying issues in how one needs to manage graph and linked structures.
> Is it simple? Yes: the type system rules fit in a napkin. There’s no need to use an SMT solver, or to prove theorems about the code, or do symbolic execution and explore the state space of the program. The linearity checks are simple: we go over the code and count the number of times a variable appears, taking care to handle loops and if statements correctly. And also we ensure that linear values can’t be discarded silently.
https://austral-lang.org/spec/spec.html#rationale-linear-typ...