Skip to content

Software Quality

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 enforces affine ownership (each value has one owner, moved rather than copied), which eliminates use-after-free, double-free, iterator invalidation, and data races in the safe subset of the language. Memory safety is one 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; session-typed channels
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; stack and region layout

The same machine-checked usage discipline protects 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.
  • 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 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)1. 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). Allocate into a region, freed as a unit; the type system tracks region lifetimes.

Tools

Ownership and affine (systems)

  • Rust: adopted in Android, the Linux kernel (since 6.1), 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, except reference cycles, which weak or unowned references break.

Linear and uniqueness (functional)

  • Linear Haskell: 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: uniqueness types.
  • ATS, Austral: linear types for low-level and systems code.
  • Idris 2: multiplicity quantifiers (0 / 1 / unrestricted), linear and dependent at once.
  • Mercury: unique di / uo modes thread the I/O world state linearly, giving a pure logic language deterministic I/O.

Reference capabilities

  • Pony: actor language; six reference capabilities; garbage-collected, so the capabilities buy data-race freedom rather than memory reclamation.

Linear resources and digital assets

  • Move (Aptos, Sui) and Cadence (Flow) make a resource linear: it cannot be copied or dropped, only moved, so an on-chain asset is conserved by construction.

Adjacent

  • Granule: a research language 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 in the safe subset.
  • 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).
  • For throwaway prototypes. The slowdown to iteration shows up most at the exploratory phase.

Evidence

  • Rust in Android. Per the Android team's 2022 report, memory-safety bugs fell from 76% of Android's vulnerabilities in 2019 to 35% in 2022, a drop that coincides with most new code moving to memory-safe languages, and none had been found in Android's Rust code.

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

References

  1. Clebsch, Sylvan, Sophia Drossopoulou, Sebastian Blessing, and Andy McNeil. 2015. "Deny Capabilities for Safe, Fast Actors." Proceedings of the 5th International Workshop on Programming Based on Actors, Agents, and Decentralized Control (AGERE! 2015), 1–12. https://doi.org/10.1145/2824815.2824816. ↩