Introduction

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.

See the Checker

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.

<!-- <!-- Linear-type checker demo --> -->
<p class="hint">Each token is a <b>linear resource</b> — it must be used exactly once. Add tokens, build a program with use/move/drop operations, then run the checker. It catches leaks (unused), double-use, and use-after-move.</p>
<div class="workspace">
  <div class="panel">
    <div class="panel-title">Resources</div>
    <div id="resource-list" class="resource-list"></div>
    <button id="btn-add" type="button">+ New token</button>
  </div>
  <div class="panel">
    <div class="panel-title">Program</div>
    <div id="stmt-list" class="stmt-list"></div>
    <div class="action-row">
      <select id="sel-action">
        <option value="use">use (read)</option>
        <option value="move">move (transfer)</option>
        <option value="drop">drop (free)</option>
      </select>
      <select id="sel-token"></select>
      <button id="btn-add-stmt" type="button">Add step</button>
    </div>
  </div>
</div>
<div class="check-row">
  <button id="btn-check" type="button">Check types</button>
  <button id="btn-reset" type="button" class="ghost">Reset</button>
</div>
<div id="result" class="result"></div>

/* Linear-type checker styles */
* { 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; } }

const i18nFmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
// Tiny linear-type checker: resources have three states.
// States: fresh (allocated, not yet used), consumed (use/drop applied), moved (ownership transferred).
// Ops: create = allocate; use = read (consumes); drop = free (consumes); move = transfer ownership (marks as moved).

let tokenCounter = 0;
// name -> state ('fresh' | 'consumed' | 'moved')
const tokens = {};
// ordered list of program steps
const stmts = [];

function freshName() {
  // Generate short single-letter names, then a+1, b+1 etc.
  const letters = 'abcdefghijklmnopqrstuvwxyz';
  return letters[tokenCounter++ % 26] + (tokenCounter > 26 ? String(Math.floor((tokenCounter - 1) / 26)) : '');
}

function renderResources() {
  // Render token chips and rebuild the token selector.
  const list = document.getElementById('resource-list');
  list.innerHTML = '';
  const sel = document.getElementById('sel-token');
  sel.innerHTML = '';
  for (const [name, state] of Object.entries(tokens)) {
    const chip = document.createElement('div');
    chip.className = 'token-chip' + (state === 'consumed' ? ' consumed' : state === 'moved' ? ' moved' : '');
    chip.textContent = name + ' : T';
    list.appendChild(chip);
    const opt = document.createElement('option');
    opt.value = name;
    opt.textContent = name;
    sel.appendChild(opt);
  }
  if (!Object.keys(tokens).length) {
    const placeholder = document.createElement('div');
    placeholder.style.color = '#9aabba';
    placeholder.style.fontSize = '.8rem';
    placeholder.textContent = 'No tokens yet.';
    list.appendChild(placeholder);
  }
}

function renderStmts() {
  // Render the statement list.
  const list = document.getElementById('stmt-list');
  list.innerHTML = '';
  if (!stmts.length) {
    const placeholder = document.createElement('div');
    placeholder.style.color = '#9aabba';
    placeholder.style.fontSize = '.8rem';
    placeholder.textContent = 'No steps yet.';
    list.appendChild(placeholder);
    return;
  }
  stmts.forEach((s) => {
    const chip = document.createElement('div');
    chip.className = 'stmt-chip';
    chip.textContent = s.label;
    list.appendChild(chip);
  });
}

document.getElementById('btn-add').addEventListener('click', () => {
  // Allocate a new fresh token and record a create step.
  const name = freshName();
  tokens[name] = 'fresh';
  stmts.push({ op: 'create', token: name, label: 'let ' + name + ' = alloc()' });
  renderResources();
  renderStmts();
  document.getElementById('result').textContent = '';
  document.getElementById('result').className = 'result';
});

document.getElementById('btn-add-stmt').addEventListener('click', () => {
  // Append a use/move/drop step for the selected token.
  const action = document.getElementById('sel-action').value;
  const name = document.getElementById('sel-token').value;
  if (!name) return;
  if (action === 'use') {
    stmts.push({ op: 'use', token: name, label: 'read(' + name + ')' });
  } else if (action === 'move') {
    stmts.push({ op: 'move', token: name, label: 'let b = move(' + name + ')' });
  } else if (action === 'drop') {
    stmts.push({ op: 'drop', token: name, label: 'drop(' + name + ')' });
  }
  renderStmts();
  document.getElementById('result').textContent = '';
  document.getElementById('result').className = 'result';
});

document.getElementById('btn-check').addEventListener('click', () => {
  // Re-simulate from the start and collect type errors.
  // Replay all statements to find type violations.
  const live = {};
  for (const [n] of Object.entries(tokens)) live[n] = 'fresh';

  const errors = [];
  for (const s of stmts) {
    if (s.op === 'create') {
      // Reset state on re-run (handles reset + re-check).
      live[s.token] = 'fresh';
    } else if (s.op === 'use' || s.op === 'move' || s.op === 'drop') {
      const state = live[s.token];
      if (state === 'consumed') {
        errors.push(i18nFmt('✗ Error: '%name%' already consumed — double-use via %op%.', { name: s.token, op: s.op }));
      } else if (state === 'moved') {
        errors.push(i18nFmt('✗ Error: '%name%' was moved — cannot %op% an invalidated value.', { name: s.token, op: s.op }));
      } else {
        // Mark as consumed or moved.
        live[s.token] = s.op === 'move' ? 'moved' : 'consumed';
      }
    }
  }

  // Any still-fresh token at the end is a leak.
  for (const [n, state] of Object.entries(live)) {
    if (state === 'fresh') {
      errors.push(i18nFmt('✗ Error: '%name%' was never consumed — resource leak.', { name: n }));
    }
  }

  const result = document.getElementById('result');
  if (!errors.length && Object.keys(live).length > 0) {
    result.textContent = '✓ All resources used exactly once — linear types satisfied!';
    result.className = 'result ok';
  } else if (!errors.length) {
    result.textContent = 'Add at least one token to check.';
    result.className = 'result warn';
  } else {
    result.textContent = errors[0];
    result.className = 'result bad';
  }
});

document.getElementById('btn-reset').addEventListener('click', () => {
  // Clear all tokens and statements.
  tokenCounter = 0;
  for (const k of Object.keys(tokens)) delete tokens[k];
  stmts.length = 0;
  renderResources();
  renderStmts();
  document.getElementById('result').textContent = '';
  document.getElementById('result').className = 'result';
});

renderResources();
renderStmts();
Result
Console

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.

The Formal Model

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

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

Linear logic (Girard, 1987) removes both. A formula AA 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 Γ⊢e:A\Gamma \vdash e : A means: use every variable in Γ\Gamma exactly once to evaluate ee of type AA. 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!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.

Where It Matters

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.

Conclusion

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.

Share this article

Pick a channel — or use your device's native share sheet.

Comments

Loading comments...

https://www.kipuhub.com/en/article/linear-types/Content licensed under CC BY-NC 4.0.