what precisely do linear types prevent?

Question

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

Answer 1

It's somewhat misleading to say that linear types don't prevent anything in 'pure' systems, because some things that are not considered pure become so when restricted with linear types. An example would be Fillinski's Linear Continuations. Normally, control operators are considered effectful, and results are non-deterministic depending on evaluation order. However, putting linearity restrictions on the use of continuations restores determinism, and makes the control operators an additional way of decomposing the control flow of the program.

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.

So, in some sense, continuations are a way of treating ephemeral control flow points of the program as if they were first class values, and linearity is preventing you from doing things that might make sense for normal, stable values (copying and discarding), but don't make sense for particular program control flows. This perspective can also be applied to other uses of linearity. For instance, if you have linearly typed mutable arrays, the discipline is covering for the fact that it is not a stably specified array of values, but an ephemeral memory region. It is not a fixed value, but a reification of the operations of reading from/writing to a runtime location at a particular point in time, which doesn't make sense to occur more than once.