# what precisely do linear types prevent?

"A theory of type polymorphism in programming" introduced the Hindly-Milner type system whose punchline can be summarized "well-typed terms don’t get stuck". They do this by creating a relatively simple language with just enough features that an untyped stuck expression is possible. For instance, true false is stuck (true is not a function, so it cannot take the argument false). Stuck expressions would not be possible without non-functions in the language.

Linear Types can encode some additional practical properties. They are often justified with examples using references, memory or file handles. Has anyone constructed a minimal system with a pithy summary like “Linearly-typed terms don’t ___”? If so, what is the simplest additional construct that makes linear types relevant (as bool does in the Hindly-Milner case)?

Linear types don’t prevent anything problematic in pure systems. My impression is that linear typing only makes sense relative to some effect system, but it is unclear to me exactly what that effect system looks like. References, file handles and memory are fairly complicated constructs, is there a simpler linear construct? I think a minimal dynamic system that could fail would help clear that up.

A way of conceptualizing what is going on in this sort of framework is that the non-linear (exponential) parts have some stable, copyable representation. An $$\mathsf{Int}$$ is just a few bits that may be copied or discarded. And a function with type $$A → B$$ is given by some code that may be copied, or a reference thereto.
However, the continuations, which must be used linearly, are ephemeral things that actually represent particular control flow points in a running program. You can conjure a continuation with type $$A \multimap ⊥$$ together with an $$A$$, and send them to separate portions of the program that may run concurrently. When one portion applies the continuation, it specifies the corresponding $$A$$ value in the other portion. It is important for this to happen linearly, because if a continuation is applied twice, then the specification of the correpsonding value is ambiguous, and may depend on evaluation order, and if the continuation is not used at all, then the corresponding value is never specified, and the portion of the program that uses it will be essentially deadlocked.