Substructural Type System

A substructural type system is a type system that restricts the structural rules of conventional type theory — the rules that permit variables to be duplicated, discarded, or reordered arbitrarily. In standard type systems, a value of type A can be used as many times as needed (contraction), can be ignored if irrelevant (weakening), and can be used in any order (exchange). Substructural type systems remove one or more of these privileges, creating a family of disciplines: linear types (no contraction, no weakening), affine types (no contraction, weakening permitted), and relevant types (contraction permitted, no weakening).

The removal of structural rules is not a limitation but a feature. It enables the type system to track resources, enforce protocols, and prevent leaks. A linear type ensures a file handle is closed exactly once. An affine type ensures a socket is closed at most once. A relevant type ensures a function's argument is used at least once. These guarantees are not runtime checks; they are compile-time proofs derived from the absence of structural rules.

Substructural type systems bridge the gap between type theory and process calculi, between functional programming and concurrent systems. They are the formal foundation of Rust's ownership model, of session types in concurrent programming, and of region-based memory management. The insight is that computation is not merely the transformation of values but the consumption of resources, and type systems that ignore this fact are type systems that permit leaks.

Substructural type systems are the type-theoretic recognition that computation has a physical substrate — that memory, time, and communication channels are not infinite and that programs which pretend otherwise are not abstract but ignorant.