Linear Types

Every program manages resources — memory, file handles, network connections. Most languages either hand the job to a garbage collector (slow, unpredictable) or to the programmer directly (fast, but catastrophically easy to get wrong: leak the resource, free it twice, or use it after it's gone).

Linear types offer a third way. A linear value must be consumed exactly once: you can't ignore it (no leak) and you can't use it again after it's consumed (no double-free, no use-after-free). The compiler enforces this at compile time — no runtime cost at all.

The idea traces back to Jean-Yves Girard's linear logic (1987), a logic where hypotheses are resources rather than eternal truths: using a hypothesis once consumes it. Translating that into type theory gives you a type checker that tracks ownership the way an accountant tracks money.

Modern languages like Rust build their entire ownership and borrowing model on this foundation. Every value has a single owner; moving it transfers ownership; the compiler rejects any program that would leave a resource orphaned or double-consumed.

Below is a miniature linear-type checker. Each token is a linear resource that must be consumed exactly once. Click the actions to build a small program, then run the checker to see whether every resource is used exactly once.

<!-- {{c_intro}} -->
<p class="hint">{{hint_para}}</p>
<div class="workspace">
  <div class="panel">
    <div class="panel-title">{{panel_resources}}</div>
    <div id="resource-list" class="resource-list"></div>
    <button id="btn-add" type="button">{{btn_add_token}}</button>
  </div>
  <div class="panel">
    <div class="panel-title">{{panel_program}}</div>
    <div id="stmt-list" class="stmt-list"></div>
    <div class="action-row">
      <select id="sel-action">
        <option value="use">{{opt_use}}</option>
        <option value="move">{{opt_move}}</option>
        <option value="drop">{{opt_drop}}</option>
      </select>
      <select id="sel-token"></select>
      <button id="btn-add-stmt" type="button">{{btn_add_stmt}}</button>
    </div>
  </div>
</div>
<div class="check-row">
  <button id="btn-check" type="button">{{btn_check}}</button>
  <button id="btn-reset" type="button" class="ghost">{{btn_reset}}</button>
</div>
<div id="result" class="result"></div>

/* {{c_css_intro}} */
* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; color: #222; margin: 0; }
.hint { font-size: .88rem; color: #444; margin: 0 0 .8rem; line-height: 1.5; }
.workspace { display: grid; grid-template-columns: 1fr 1fr; gap: .7rem; margin-bottom: .7rem; }
.panel { border: 1px solid #cdd9e3; border-radius: 8px; padding: .6rem .7rem; background: #f7f9fb; }
.panel-title { font-size: .78rem; font-weight: 700; text-transform: uppercase; letter-spacing: .06em;
               color: #5a7088; margin-bottom: .45rem; }
.resource-list, .stmt-list { min-height: 48px; margin-bottom: .45rem; display: flex;
                              flex-direction: column; gap: .25rem; }
.token-chip { display: inline-flex; align-items: center; gap: .3rem; padding: .2rem .5rem;
              border-radius: 5px; font: 600 .82rem ui-monospace, monospace; background: #dce8f5;
              color: #1d3557; border: 1px solid #b0c9e3; }
.token-chip.consumed { background: #fde8e8; color: #b91c1c; border-color: #f5b4b4; text-decoration: line-through; }
.token-chip.moved { background: #e8f3e8; color: #166534; border-color: #a7d3a9; }
.stmt-chip { font: .82rem ui-monospace, monospace; padding: .18rem .45rem; border-radius: 5px;
             background: #eef1f5; border: 1px solid #d0d8e3; color: #374151; }
.action-row { display: flex; gap: .35rem; flex-wrap: wrap; }
select { font: .82rem system-ui, sans-serif; padding: .3rem .4rem; border: 1px solid #b0c9e3;
         border-radius: 6px; background: #fff; }
.check-row { display: flex; gap: .5rem; margin-bottom: .5rem; }
button { font: 600 .82rem system-ui, sans-serif; padding: .38rem .8rem; border: 1px solid #1d3557;
         background: #1d3557; color: #fff; border-radius: 7px; cursor: pointer; }
button.ghost { background: #fff; color: #1d3557; }
button.small { font-size: .75rem; padding: .22rem .5rem; }
.result { font-size: .9rem; font-weight: 600; min-height: 1.5em; }
.result.ok { color: #0a7d33; }
.result.bad { color: #c92f3c; }
.result.warn { color: #b45309; }
@media (max-width: 420px) { .workspace { grid-template-columns: 1fr; } }

// Code not found

Notice how the checker distinguishes three error modes: unused (a leaked resource), double-use (a freed-then-reused resource), and use-after-consume (borrowing a value that was already moved). Every real-world memory safety bug falls into one of these three categories — and a linear type checker rules out all of them statically.

Classical logic has two structural rules that type systems usually inherit silently:

• Weakening: you may ignore a hypothesis — $A, B \vdash C$ implies $A \vdash C$.
• Contraction: you may duplicate a hypothesis — $A \vdash C$ implies $A, A \vdash C$.

Linear logic (Girard, 1987) removes both. A formula $A$ on the left side of a sequent is a resource you must consume exactly once. Keeping weakening but dropping contraction gives affine types (at most once — Rust's actual model). Dropping both gives strict linear types (exactly once).

In a linear type system the typing judgment $\Gamma \vdash e : A$ means: use every variable in $\Gamma$ exactly once to evaluate $e$ of type $A$. Two key consequences:

• No leaks: the compiler verifies $\Gamma$ is fully consumed — nothing left over.
• No double-free: the type of a variable disappears from the environment after it is used.

The exponential modality $!A$ re-introduces copying for values that are genuinely shareable (read-only data, integers, booleans). This is how Rust's immutable borrows work: a &T reference is a copyable, read-only alias; the owned T is linear.

Linear types are a special case of substructural type systems — type systems that control how many times a variable may appear. They sit alongside type inference and program equivalence as pillars of the theoretical foundations of programming languages.

The exactly-once discipline shows up wherever resources are precious or dangerous:

• Systems programming (Rust): Rust's ownership system is affine types in disguise. Every allocation has one owner; moves transfer it; borrows are time-limited. The result: memory safety without a garbage collector — the whole idea behind Rust's zero-cost abstractions.
• Quantum computing: a quantum state cannot be copied (the no-cloning theorem). Quantum programming languages like Quipper and Q# use linear types to enforce this at the language level.
• Session types: communication protocols can be typed linearly so that each message in a protocol is sent and received exactly once, ruling out deadlocks and protocol violations statically.
• Operating system capabilities: in capability-safe systems, a capability token grants access to a resource. Making tokens linear means they cannot be forged, leaked, or used twice — the foundation of systems like seL4 and Wasm component model.
• Compilers and IRs: LLVM's SSA form and continuation-passing style (CPS) treat each definition as used exactly once by construction, which is why they are so amenable to optimization.

In every case the invariant is the same: the compiler, not the programmer, counts the uses.

Linear types are one of the cleanest ideas in type theory: strip two structural rules from logic, and you get a type checker that counts resources like a ledger. Every use must balance — no leftovers, no double spends.

The gap between "the programmer intends to manage this resource correctly" and "the compiler proves it" is exactly where memory safety bugs live. Linear types close that gap without a garbage collector, without runtime overhead, and without waiting for the bug to appear in production.

From Girard's blackboard in 1987 to every Rust program compiled today, the insight is the same: ownership is a type, and the compiler is the auditor.

Curious how type systems reason about other program properties? See type inference for how types can be deduced automatically, or program equivalence for the harder question of when two programs compute the same thing.