Linear and Affine Types

Use-after-free, double-free, data races - three classes of bugs that have destroyed the reputation of C and C++. Mozilla found that 70% of CVEs in Chrome and Firefox are memory safety bugs. Rust solved them not through GC, not through runtime checks, but through a type system. The foundation is linear logic from 1987. Theory finally met industry.

• **Rust in the Linux kernel (2022):** the first language besides C accepted into the kernel. The borrow checker was the primary reason for adoption.
• **Android (Google):** new code written in Rust. Memory safety bugs dropped from 76% to 24% of security vulnerabilities over three years.
• **Haskell LinearTypes (GHC 9.0+):** safe handling of files, networks, and CUDA without resource leaks

Girard's Linear Logic

In classical logic, a proof of P can be used as many times as needed: duplicated or discarded freely. **Linear logic**, proposed by Jean-Yves Girard in 1987, removes this assumption: every resource must be used *exactly once*.

Linear logic models **resources**: money, file descriptors, access tokens, memory. Unlike classical logic, "use" means "consume". This provides the foundation for type systems that track resource lifecycles.

**Affine types** are a relaxation of linear types: a resource can be used *at most once* (it can be discarded, but not duplicated). Rust uses affine types through its ownership system.

Resource Management Through Types

A file descriptor is a classic resource with a lifecycle: open, use, close exactly once. Forgetting to close causes a leak. Closing twice is undefined behavior. Linear types encode this protocol in the type system: the compiler tracks usage.

The key point: the compiler statically guarantees that every `Handle` will be closed *exactly once* - without runtime checks, without GC finalizers, without relying on developer discipline. This is **protocol compliance through types**.

Rust Borrow Checker as Linear Types

Rust does not call its system "linear types", but its semantics are a direct embodiment of affine types. Every value has exactly one **owner**. When the owner goes out of scope, the value is destroyed. Passing a value is a **move**: the original is no longer accessible.

The rule "either N shared or 1 exclusive" is an **aliasing** restriction: two mutable references to the same value cannot coexist. Aliasing is the root cause of most data races and use-after-free bugs. The borrow checker eliminates them statically.

**Lifetimes in Rust** add another layer: the compiler verifies that a reference does not outlive the object it points to. `'a` in `&'a str` is a lifetime annotation that allows the compiler to prove the absence of dangling references.

Uniqueness Types in Clean and Idris

**Uniqueness types** are the dual of linear types, developed for functional languages. The idea: a type is marked *unique* if it is guaranteed that no other references to it exist at that moment. A unique object can safely be mutated in-place - like in imperative languages, but with a static guarantee.

Uniqueness types and linear types solve the same problem from different angles. Linear types constrain the consumer: "use exactly once". Uniqueness types constrain the producer: "no other references exist". In Clean, uniqueness enables O(1) destructive array updates in a functional language - without breaking purity.

**Linearity in Haskell GHC 9.0+:** the `LinearTypes` extension adds `%1 ->` syntax. These are not full linear types, but allow writing safe resource handling protocols in ordinary Haskell code.

Linear and Affine Types

• Girard's linear logic (1987): each resource used exactly once - the foundation for type systems managing resource lifecycles
• Linear types in code: a handle must be both opened and closed - the compiler verifies this, not tests
• Rust borrow checker: affine types + aliasing rule = no data races or use-after-free statically
• Uniqueness types (Clean, Idris): O(1) mutation in a functional language without breaking purity

Related Topics

Linear types intersect with memory management, concurrency, and type theory.

• Dependent Types — Another approach to static guarantees - types encode value properties
• Ownership and Memory Management — Rust ownership is a practical embodiment of affine types
• IO Monads — Haskell's IO monad uses a similar idea: World-token to sequence effects

Вопросы для размышления

• Linear types guarantee "exactly once"; affine types guarantee "at most once". In what cases does the lower bound (mandatory use) matter?
• The borrow checker allows multiple `&T` simultaneously but only one `&mut T`. How does this rule relate to the concept of aliasing in linear logic?
• Uniqueness types allow mutation in a functional language. How does this affect testability and reasoning about invariants?

Связанные уроки

• plt-13-ownership — Rust ownership is linear types made practical: each value is used exactly once unless explicitly cloned
• plt-09-dependent-types — Linear and dependent types represent orthogonal axes of type expressiveness; pairing them gives the full picture
• plt-06-lambda-calculus — Linear logic is a substructural extension of lambda calculus; the lambda abstraction rules are directly modified
• plt-02-type-systems — Substructural type systems modify the structural rules (weakening, contraction) - baseline type system knowledge is needed
• os-07-memory