# Linear types Linear and substructural type systems constrain not what a value *is* but *how it is used*: how many times, and in what order. A **linear** type must be used exactly once; an **affine** type at most once. From that single rule the compiler proves, at compile time, that a resource is released exactly once, that a value is never used after it is consumed, and that no two live paths mutate the same data at once. **Rust's borrow checker** is the flagship. Its affine ownership (each value has one owner, moved rather than copied) eliminates use-after-free, double-free, iterator invalidation, and data races in the safe subset of the language. Memory safety is the sharpest *application* of the discipline, not its whole extent. The family is defined by which of ordinary logic's *structural rules* it drops: **weakening** (discard an unused value), **contraction** (duplicate a value), and **exchange** (reorder). Ordinary logic keeps all three; each discipline *removes* some, and the remaining freedom is the usage rule: | Discipline | Forbids (rule removed) | Usage | Where | | --- | --- | --- | --- | | **Linear** | discarding and duplicating (weakening, contraction) | exactly once | Girard's linear logic; Linear Haskell (`%1 ->`); Clean; ATS; Austral; Move / Cadence resources | | **Affine** | duplicating (contraction) | at most once | Rust ownership + lifetimes; Swift `~Copyable`; C++ move-only (`unique_ptr`, unenforced) | | **Relevant** | discarding (weakening) | at least once | rarer; "must-use" disciplines (`#[must_use]`-style) | | **Ordered** | discarding, duplicating, reordering (all three) | exactly once, in sequence | ordered logic; session-typed channels; stack and region layout | A second style, **reference capabilities** (Pony), types each reference by the aliasing, mutation, and sharing it permits rather than by counting uses. The same machine-checked usage discipline pays back as maintainability: a refactor that breaks an ownership or lifetime assumption fails to compile instead of surfacing at runtime. ## What it catches - **Resource-lifecycle bugs.** A file, socket, lock, connection, or transaction typed linearly must be released exactly once; the compiler catches the missing close and the double close. - **Use-after-consume.** Using a value after it has been moved, freed, or handed off fails to type-check. In Rust this is use-after-free; in general it is use-after-consume. - **Double-free and double-release.** Consuming a value twice is a type error (an owner moved out of scope twice, a lock released twice). - **Data races.** Concurrent access to mutable state without synchronization is rejected. Rust's `Send` / `Sync` bounds and Pony's reference capabilities make sharing a type-level question. - **Aliasing and iterator invalidation.** Two live paths to the same mutable data are forbidden by construction (Rust) or controlled by capabilities (Pony); mutating a container while iterating it is rejected at compile time. - **Protocol violations.** A session-typed channel enforces that a protocol's steps run once, in order; an out-of-order or skipped step is a type error. - **Asset non-conservation.** A linear resource type cannot be copied or silently dropped, so a modeled coin cannot be duplicated (counterfeited) or lost (burned by accident). What linear types do **not** catch: bugs that respect the usage rules but are still logically wrong (integer overflow, business-logic errors), bugs inside `unsafe` blocks (Rust) or explicit allocator misuse (Zig), and panics. The proven bug class is *named and scoped*; what falls outside it is what tests and other methods are for. Affine typing is one attack on memory errors among several: [verifying memory safety](https://quality.stereobooster.com/memory.md) classifies the error space and maps each class to the methods and tools that close it. ## Categories of substructural type system - **Ownership and borrowing** (Rust). References are tracked with lifetimes, and a mutable reference excludes shared references at the same scope. - **Reference capabilities** (Pony). Six capabilities on every reference (`iso`, `trn`, `ref`, `val`, `box`, `tag`) describe the aliasing, mutation, and sharing the holder is permitted (Clebsch et al. 2015)[^clebsch2015]. `iso` (isolated, unique) is the linear corner; `val` (immutable, shareable) and `tag` (opaque identity) express sharing that a pure use-count cannot. Designed for actor concurrency: safe data sharing without locks. - **Region-based memory management** (Cyclone, historical; a research influence on Rust). Allocate into a region, freed as a unit; the type system tracks region lifetimes. ## Tools ### Ownership and affine (systems) - **Rust**: the most widely deployed production example. Adoption in Android, the Linux kernel (drivers and core paths), Windows kernel components, Firefox, Cloudflare, and AWS Firecracker. - **Swift**: noncopyable types (`~Copyable`) add affine ownership with explicit consuming and borrowing; automatic reference counting (ARC) handles the rest at runtime, outside weak/unowned-reference cycles. ### Linear and uniqueness (functional) - **[Linear Haskell](https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/linear_types.html)**: a linear arrow (`a %1 -> b`) layered on GHC; used for safe mutable arrays (mutate a unique array in place, then freeze it) and safe resource APIs. - **[Clean](https://clean.cs.ru.nl/Clean)**: uniqueness types; the design ancestor of ATS-style linearity. - **[ATS](https://www.ats-lang.org/)**, **[Austral](https://austral-lang.org/)**: linear types for low-level and systems code. - **[Idris 2](https://www.idris-lang.org/)**: multiplicity quantifiers (`0` / `1` / unrestricted), linear and dependent at once. - **[Mercury](https://mercurylang.org/)**: unique `di` / `uo` modes thread the I/O world state linearly, giving a pure logic language deterministic I/O. ### Reference capabilities - **[Pony](https://www.ponylang.io/)**: actor language; six reference capabilities. Niche but the cleanest production example of capability-based aliasing control, and garbage-collected, so the capabilities buy data-race freedom rather than memory reclamation. ### Linear resources and digital assets - **[Move](https://move-language.github.io/move/)** (Aptos, Sui) and **[Cadence](https://cadence-lang.org/)** (Flow) make a `resource` linear: it cannot be copied or dropped, only moved, so an on-chain asset is conserved by construction. The largest public deployment of *true* linearity. ### Adjacent - **Granule**, **Alms**: research languages with graded / quantitative resource types (the semiring generalization of "how many times"). ## When to use, when not **Use:** - For resource-lifecycle-heavy code. Files, sockets, locks, connections, and transactions typed linearly turn "released exactly once" into a compile-time guarantee. - For systems and security code where memory bugs are the risk profile. Rust's affine ownership eliminates the category; the Microsoft Security Response Center and Linux/Android maintainers both cite memory bugs as 70%+ of CVE-class issues. - For concurrent code where data races are a real risk. Rust's `Send` / `Sync` and Pony's capabilities make sharing safe by construction. - For protocol conformance (session types) and conserved resources or digital assets (linear resource types, Move and Cadence). **Don't:** - For business-logic-heavy code where usage and memory bugs are not the risk profile. The fight-the-compiler cost may exceed the benefit; consider a garbage-collected language with strong types ([type systems](https://quality.stereobooster.com/static-types.md)). - As a substitute for testing the *logic*. Usage safety is a named bug class; logic errors are not covered. - For throwaway prototypes. The cost-to-iteration tax shows up most at the exploratory phase. ## Evidence - **Industrial adoption of Rust.** Linux kernel (since 6.1), Windows kernel components, Firefox, Android. Per the Android team's 2022 report, memory-safety bugs in new C/C++ code accounted for the majority of high-severity Android CVEs, and Rust adoption is part of the response. Controlled empirical comparisons of "team writing Rust" vs "team writing C++" do not exist in the published literature. The case for linear types rests on the *definitional* point: a value used against its usage type cannot occur, not "has not yet been seen". ## Classification - **Quality dimensions:** Functionality (resources used correctly by construction: acquired and released exactly once, never after consumption; protocols and asset conservation enforced in the type), Security (memory safety in the affine case (Rust): no use-after-free, double-free, or data race in the safe subset), Maintainability (fearless refactoring: a broken ownership or lifetime assumption is a compile error, not a runtime bug). - **Area:** Resource-lifecycle code (files, sockets, locks, connections, transactions); systems and security programming where memory bugs are the risk; concurrency; protocol conformance; conserved digital assets. - **Guarantee:** Exhaustive within the discipline: by construction, a value used against its usage type cannot occur. ## Referenced by - [Effect scope](https://quality.stereobooster.com/effect.md) · The axes - [Systematic concurrency testing](https://quality.stereobooster.com/systematic-concurrency-testing.md) · Methods - [Types and effects](https://quality.stereobooster.com/types.md) · Methods - [Verifying concurrency](https://quality.stereobooster.com/concurrency.md) · Methods - [Verifying memory safety](https://quality.stereobooster.com/memory.md) · Methods - [How AI fits into software quality](https://quality.stereobooster.com/ai.md) · AI ## References [^clebsch2015]: Clebsch, Sylvan, Sophia Drossopoulou, Sebastian Blessing, and Andy McNeil. 2015. "[Deny Capabilities for Safe, Fast Actors](https://www.doc.ic.ac.uk/~scd/fast-cheap-AGERE.pdf)." *Proceedings of the 5th International Workshop on Programming Based on Actors, Agents, and Decentralized Control (AGERE! 2015)*, 1–12. .