Learning path

Full curriculum

Full curriculum

Unit content

Linear and affine type disciplines

Ordinary type systems usually allow a variable to be copied or ignored freely. Linear and affine type systems control those structural operations.

A linear value must be used exactly once. An affine value may be used at most once. This changes the typing context from an unrestricted set of reusable assumptions into resources whose consumption matters.

If $x:R$ is linear, an expression may not both pass $x$ to one function and retain another usable copy. Likewise, a linear value cannot simply disappear without being consumed.

This discipline can encode real invariants. A file handle can be required to have one owner, a protocol token can represent one permitted transition, and a resource can be made impossible to duplicate accidentally.

The distinction between resource-sensitive and unrestricted data is important. Copying an immutable integer is harmless, while duplicating exclusive authority over a mutable resource may violate safety guarantees. Practical systems therefore combine values that may be copied freely with values whose use is restricted.

By controlling whether assumptions may be discarded or duplicated, the type system can reason statically about ownership, resource use and aliasing properties that ordinary value types cannot express.