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