6 min read
On this page

Linear and Substructural Types

Structural Rules

In standard logic/type theory, contexts (assumptions) satisfy three structural rules:

  1. Weakening: If Gamma |- A, then Gamma, x:B |- A (unused assumptions can be added)
  2. Contraction: If Gamma, x:A, y:A |- B, then Gamma, z:A |- B[x,y := z] (assumptions can be duplicated)
  3. Exchange: If Gamma, x:A, y:B, Delta |- C, then Gamma, y:B, x:A, Delta |- C (order doesn't matter)

Substructural type systems restrict one or more of these rules, yielding different resource disciplines.

Taxonomy of Substructural Logics

| System | Weakening | Contraction | Exchange | Use Count | |---|---|---|---|---| | Structural (standard) | Yes | Yes | Yes | Any | | Affine | Yes | No | Yes | At most once | | Relevant (relevance) | No | Yes | Yes | At least once | | Linear | No | No | Yes | Exactly once | | Ordered | No | No | No | Exactly once, in order |

Linear Logic and Linear Types

Girard's Linear Logic (1987)

Linear logic treats propositions as resources that are consumed by use. Key connectives:

Multiplicatives:

  • A ⊗ B (tensor): Both A and B, independently
  • A ⅋ B (par): Dual of tensor
  • 1 (unit of tensor), ⊥ (unit of par)

Additives:

  • A & B (with): Choice offered to consumer (both available, pick one)
  • A ⊕ B (plus): Choice made by producer (one provided)
  • ⊤ (unit of with), 0 (unit of plus)

Exponentials:

  • !A (of course): A can be used any number of times (weakening + contraction)
  • ?A (why not): Dual of !A

The exponential ! is the bridge between linear and classical logic: !A permits unlimited use of A. The decomposition of intuitionistic implication: A -> B = !A ⊸ B (an unlimited A linearly implies B).

Linear Lambda Calculus

The linear lambda calculus enforces that every variable is used exactly once:

x:A |- x : A                                    (Var)

Gamma, x:A |- M : B
-----------------------                           (⊸-Intro)
Gamma |- lambda x. M : A ⊸ B

Gamma |- M : A ⊸ B    Delta |- N : A
-----------------------                           (⊸-Elim)
Gamma, Delta |- M N : B

Note: contexts in the application rule are split (Gamma, Delta are disjoint). This enforces linearity -- no variable appears in both M and N.

Tensor:

Gamma |- M : A    Delta |- N : B
-----------------------
Gamma, Delta |- (M, N) : A ⊗ B

Gamma |- M : A ⊗ B    Delta, x:A, y:B |- N : C
-----------------------
Gamma, Delta |- let (x,y) = M in N : C

Bang (!): Introduces unlimited use.

!Gamma |- M : A
-----------------------    (all variables in context must be banged)
!Gamma |- !M : !A

Gamma |- M : !A    Delta, x:A |- N : B
-----------------------
Gamma, Delta |- let !x = M in N : B

Session Types

Session types (Honda, 1993; Honda-Vasconcelos-Kubo, 1998) apply linear types to communication protocols. A session type describes the sequence of messages on a channel:

S ::= !A.S      (send A, then continue as S)
    | ?A.S      (receive A, then continue as S)
    | S1 + S2   (offer choice: either S1 or S2)
    | S1 & S2   (select: choose S1 or S2)
    | end       (session completed)
    | mu X. S   (recursive session)

Duality: Each session has two endpoints with dual types. If one end sends, the other receives:

  • dual(!A.S) = ?A.dual(S)
  • dual(?A.S) = !A.dual(S)
  • dual(S1 + S2) = dual(S1) & dual(S2)

Linearity ensures protocol compliance: A channel used non-linearly could lead to two threads both trying to receive on the same channel, or a message sent to a dead channel.

Example

type FileServer = ?Filename. !FileContents. end

-- Server has type FileServer
-- Client has type dual(FileServer) = !Filename. ?FileContents. end

Multiparty session types (Honda-Yoshida-Carbone, 2008) generalize to n-party protocols, specified by a global type that projects to local types for each participant.

Rust Ownership as Affine Typing

Rust's ownership system is an affine type system in disguise:

Ownership Rules

  1. Each value has exactly one owner
  2. When the owner goes out of scope, the value is dropped
  3. Values can be moved (transferred to a new owner -- consumes the original binding)
  4. Values can be borrowed (temporary references)

Affine, Not Linear

Rust is affine (at most once), not linear (exactly once), because values can be dropped without use. The Drop trait handles deallocation of moved-from bindings.

Move semantics: Assignment transfers ownership, invalidating the source:

s1 ← CREATE_STRING("hello")
s2 ← MOVE(s1)    // s1 is moved; using s1 here is a compile error

Borrowing as Controlled Aliasing

Shared references (&T): Multiple simultaneous borrows allowed, but no mutation. Mutable references (&mut T): Exactly one mutable borrow, no concurrent shared borrows.

This is a restricted form of fractional permissions (Boyland, 2003): a mutable reference holds the "full" permission, shared references hold "fractional" permissions, and you cannot have both simultaneously.

Lifetimes as Regions

Rust's lifetime annotations ('a) track how long borrows are valid. The borrow checker ensures references do not outlive their referents. This is connected to region-based memory management (Tofte-Talpin, 1997).

PROCEDURE LONGEST(x: ref[a] string, y: ref[a] string) → ref[a] string
    IF LENGTH(x) > LENGTH(y) THEN RETURN x ELSE RETURN y

The lifetime 'a constrains the output to live no longer than both inputs.

Quantitative Type Theory (QTT)

Quantitative Type Theory (Atkey, 2018; McBride, 2016) annotates each variable binding with a usage quantity:

Gamma, x :_q A |- M : B

where q is drawn from a resource semiring (R, +, *, 0, 1):

  • 0: variable not used at runtime (erased, type-level only)
  • 1: variable used exactly once (linear)
  • omega: variable used without restriction

Key rules:

Gamma, x :_1 A |- x : A                          (Var, uses 1 resource)

Gamma, x :_q A |- M : B
---------------------------                        (Pi-Intro)
Gamma |- lambda x. M : (x :_q A) -> B

Gamma |- M : (x :_q A) -> B    Delta |- N : A
---------------------------                        (Pi-Elim)
q * Delta + Gamma |- M N : B[x := N]

The context in the application rule scales Delta by q: if the function uses its argument q times, the resources for the argument are multiplied by q.

Advantages:

  • Subsumes linear, affine, and unrestricted types in a single framework
  • Distinguishes compile-time and runtime usage (0 vs nonzero)
  • Compatible with dependent types (unlike naive linear dependent types)

Idris 2 is built on QTT, making it the first practical dependently typed language with integrated linearity.

Graded Types and Coeffect Calculi

Graded type systems generalize QTT by allowing more sophisticated resource algebras:

Graded modal types: Box_r A means "a value of type A available at grade r." The grade r can track:

  • Usage counts: r in {0, 1, omega} (QTT)
  • Security levels: r in {Public, Secret} (information flow)
  • Sensitivity: r in R+ (differential privacy)
  • Timing: r in N (staged computation / multi-stage programming)

Coeffect calculus (Petricek-Orchard-Mycroft, 2014): Dual to effect systems. Effects describe what a computation does (outputs); coeffects describe what a computation needs (inputs/context requirements).

The grading forms a semiring or semiring module, ensuring that composition of contexts is well-defined.

Bunched Implications (BI)

BI logic (O'Hearn-Pym, 1999) combines additive and multiplicative connectives with two implications:

  • A -> B (additive/intuitionistic implication): contraction and weakening allowed
  • A -* B (multiplicative/linear implication): no contraction or weakening

Separation logic (Reynolds, 2002) is based on BI, with the "separating conjunction" * corresponding to tensor:

  • P * Q: P and Q hold on disjoint portions of the heap
  • P -* Q: if P holds on a disjoint extension of the heap, then Q holds on the combined heap

This connects linear types to verification of imperative programs with mutable state.

Practical Applications

Memory Management

  • Rust: Affine types ensure memory safety without garbage collection
  • Linear Haskell (Bernardy et al., 2018): Adds linear arrows (a %1 -> b) to Haskell for safe resource management
  • ATS: Dependent types with linear types for systems programming

Protocol Verification

  • Session types verify communication protocols at compile time
  • Applied to web services (Scribble), concurrent programming, and distributed systems

Resource Control

  • File handles, database connections, locks used exactly once
  • Prevents resource leaks and double-free errors

Quantum Computing

  • Quantum states cannot be cloned (no-cloning theorem) -- naturally modeled by linear types
  • Quipper, QWIRE use linear types for quantum circuit description

Language Support

| Language | Substructural Feature | Mechanism | |---|---|---| | Rust | Affine types | Ownership + borrow checker | | Linear Haskell | Linear arrows | Multiplicity annotations | | Idris 2 | QTT (0, 1, omega) | Quantity annotations | | ATS | Linear types | Viewtypes | | Clean | Uniqueness types | Unique type annotations | | Granule | Graded types | Coeffect system |

Theoretical Connections

  • Game semantics: Linear logic has clean game-semantic models (each move is played exactly once)
  • Coherence spaces: Girard's original model for linear logic
  • Day convolution: Graded comonads model context requirements categorically
  • Differential lambda calculus (Ehrhard-Regnier): Extends linear logic with differentiation, connecting to resource sensitivity and Taylor expansion of proofs