Linear Types

Linear types are a substructural type system in which every value must be consumed exactly once — no duplication, no discarding. They are the formal mechanism by which Rust achieves memory safety without garbage collection: ownership is linearity in disguise. When a value is bound to a variable, that variable is the sole owner; when the variable goes out of scope, the value is destroyed; when the value is moved to another variable, the original variable becomes inaccessible. The compiler enforces these rules not as conventions but as type errors.

The concept originates in Jean-Yves Girard's linear logic, a refinement of classical logic that distinguishes between resources that can be duplicated (exponentials) and those that cannot (linear). The Curry-Howard correspondence translates this distinction into programming: linear propositions correspond to linear types, and linear proofs correspond to programs that manage resources without waste or duplication.

Linear types have applications beyond memory management. They enforce protocol compliance in concurrent systems (a channel must be closed exactly once), prevent data races (a mutable reference cannot be aliased), and enable zero-cost abstractions (resources are managed at compile time, not runtime). The cost is cognitive: programmers must reason about ownership explicitly, and the compiler rejects programs that violate linearity even when the violation is harmless.

The significance of linear types is not that they prevent bugs. It is that they make resource management a first-class concern of the type system, forcing the programmer to confront what every C programmer ignores: that memory is a resource with a lifecycle, and mismanaging that lifecycle is not an implementation detail but a type error.