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