THE LINEAR TYPE use it exactly once — the type tracks the resource
A linear type demands its value be used exactly once — not dropped, not duplicated. That sounds restrictive until you see what it buys: a file handle that must be closed, memory that cannot be used-after-free, a protocol that must follow its steps. Linearity, from Girard's linear logic, turns resource discipline into a type the compiler enforces. The affine relaxation (use at most once) is exactly Rust's ownership model — move semantics, no aliasing, memory safety without a garbage collector. The type system becomes a resource accountant.
THE TECHNIQUE exactly-once (linear) / at-most-once (affine); count the uses
A linear variable must be used exactly once. The demo counts uses of a variable in a small program and flags the linearity violation: live demo
HISTORY & CREDIT Girard 1987 · Wadler 1990
“Owning a value means you can use it as often as you like.” — for a resource, the second use is the bug: the double-free, the closed-handle read, the reused nonce. A linear type makes the second use unsayable. Restriction is safety. cited
1987 · Jean-Yves Girard — linear logic: propositions as consumable resources. 1990 · Philip Wadler — “Linear types can change the world!”: linearity for safe in-place update. now · Rust's ownership (affine), linear types in Haskell/Idris, session types for protocols.
Exactly-once is conservation for computation: the resource is neither created by duplication nor lost by dropping. Track it in the type and use-after-free becomes a type error. Girard 1987
RECOMMEND FOR I-13 linear use-count checked, computed
On the canonical compiler, a variable used once passes the linear check (1); used twice it violates it (2 ≠ 1):
$ i13 run t_linear.i13 # count uses of a linear variable
linear_uses = 1 -- used exactly once: OK
affine_violation = 2 -- used twice: linear violation
Recommend: i13 already has linearity's payoff without its type. Its arrays are value-semantic: a write yields a new array, there is no aliasing, and a value cannot be captured-and-mutated elsewhere — the same “no shared mutable state” guarantee Rust gets from affine ownership (dart 242's escape analysis is the flip side). What i13 lacks is the exactly-once obligation: nothing forces you to consume a resource. So i13 gets aliasing-safety by construction but not use-once accounting — a partial, un-typed shadow of linearity.