Introduction

Every time you run a program, something could go wrong: you might add a number to a string, call a method on null, or read a field that does not exist. Type checking is a static analysis that flags exactly those mistakes — before the program ever runs.

But a type checker is only useful if it means something. The question is: if the type checker is happy, does that really guarantee the program won't crash? The answer is captured in a theorem called type soundness, first stated cleanly by Wright and Felleisen in 1994.

It rests on two lemmas that together say: "a well-typed program never gets stuck." Progress says every well-typed program can always take a step (or is already finished). Preservation says that step doesn't break the typing. Together, they turn type annotations from documentation into a runtime guarantee.

Catch the Error Before It Runs

Below is a tiny expression evaluator with a built-in type checker. Each expression is either a number, a boolean, an addition of two numbers, or an if-then-else. The type checker assigns types before evaluation and rejects ill-typed programs.

<!-- Type Soundness demo — expression evaluator with type checker -->
<p class="hint">Type a small expression and press <b>Type-check</b>. If it passes, press <b>Evaluate</b>. A type error blocks evaluation — that is progress and preservation at work.</p>
<div class="editor-row">
  <div class="expr-group">
    <label for="expr-input">Expression</label>
    <input id="expr-input" type="text" placeholder="e.g.  1 + 2   or   if true then 10 else 20" spellcheck="false" autocomplete="off" />
  </div>
  <div class="btn-row">
    <button id="btn-check" type="button">Type-check</button>
    <button id="btn-run" type="button">Evaluate</button>
    <button id="btn-reset" type="button" class="ghost">Reset</button>
  </div>
</div>
<div class="result-area">
  <div class="result-box" id="type-box">
    <span class="box-label">Inferred type</span>
    <span class="box-value" id="type-out">—</span>
  </div>
  <div class="result-box" id="eval-box">
    <span class="box-label">Value</span>
    <span class="box-value" id="eval-out">—</span>
  </div>
</div>
<div class="status" id="status"></div>
<div class="examples-section">
  <p class="examples-label">Quick examples (click to load)</p>
  <div class="examples-row" id="examples-row"></div>
</div>

/* Styles for the type soundness demo */
* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; color: #222; margin: 0; background: #fff; }
.hint { font-size: .88rem; color: #444; margin: 0 0 .9rem; line-height: 1.5; }
.editor-row { display: flex; flex-direction: column; gap: .5rem; margin-bottom: .7rem; }
.expr-group { display: flex; flex-direction: column; gap: .3rem; }
label { font-size: .82rem; font-weight: 600; color: #555; }
input { font: 15px ui-monospace, monospace; padding: .45rem .7rem; border: 1.5px solid #b0bec5; border-radius: 8px; width: 100%; outline: none; transition: border-color .15s; }
input:focus { border-color: #1d3557; }
.btn-row { display: flex; gap: .5rem; flex-wrap: wrap; }
button { font: 600 13px system-ui, sans-serif; padding: .4rem .85rem; border: 1.5px solid #1d3557; background: #1d3557; color: #fff; border-radius: 8px; cursor: pointer; transition: opacity .15s; }
button:hover { opacity: .85; }
button.ghost { background: #fff; color: #1d3557; }
.result-area { display: flex; gap: .6rem; margin-bottom: .5rem; }
.result-box { flex: 1; border: 1.5px solid #cdd9e3; border-radius: 10px; padding: .5rem .7rem; background: #f4f8fb; min-height: 52px; }
.result-box.ok { border-color: #0a7d33; background: #e8f7ee; }
.result-box.bad { border-color: #c92f3c; background: #fdecea; }
.box-label { display: block; font-size: .74rem; font-weight: 700; color: #6b7a8d; text-transform: uppercase; letter-spacing: .04em; margin-bottom: .2rem; }
.box-value { font: 14px ui-monospace, monospace; word-break: break-all; }
.status { font-size: .9rem; font-weight: 600; min-height: 1.4em; margin-bottom: .4rem; }
.status.ok { color: #0a7d33; }
.status.bad { color: #c92f3c; }
.examples-label { font-size: .8rem; font-weight: 600; color: #555; margin: .3rem 0 .4rem; }
.examples-row { display: flex; flex-wrap: wrap; gap: .4rem; }
.ex-btn { font: 13px ui-monospace, monospace; padding: .25rem .6rem; border: 1px solid #adb1b8; background: #e8eef3; color: #1d3557; border-radius: 6px; cursor: pointer; }
.ex-btn:hover { background: #cdd9e3; }

const i18nFmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
// Type soundness demo: tiny expression language with type checker + evaluator.

// Grammar
// Expr = Num | Bool | Add(Expr,Expr) | If(Expr,Expr,Expr)
// Types: "Int" | "Bool" | "TypeError"

// Tokenizer and recursive-descent parser
function tokenize(src) {
  const tokens = [];
  let i = 0;
  while (i < src.length) {
    if (/\s/.test(src[i])) { i++; continue; }
    if (/\d/.test(src[i])) {
      let n = '';
      while (i < src.length && /\d/.test(src[i])) n += src[i++];
      tokens.push({ t: 'num', v: parseInt(n, 10) });
      continue;
    }
    if (src.slice(i, i + 4) === 'true') { tokens.push({ t: 'bool', v: true }); i += 4; continue; }
    if (src.slice(i, i + 5) === 'false') { tokens.push({ t: 'bool', v: false }); i += 5; continue; }
    if (src.slice(i, i + 2) === 'if') { tokens.push({ t: 'if' }); i += 2; continue; }
    if (src.slice(i, i + 4) === 'then') { tokens.push({ t: 'then' }); i += 4; continue; }
    if (src.slice(i, i + 4) === 'else') { tokens.push({ t: 'else' }); i += 4; continue; }
    if (src[i] === '+') { tokens.push({ t: '+' }); i++; continue; }
    if (src[i] === '(') { tokens.push({ t: '(' }); i++; continue; }
    if (src[i] === ')') { tokens.push({ t: ')' }); i++; continue; }
    throw new Error(i18nFmt('Unexpected character: '%ch%'', { ch: src[i] }));
  }
  return tokens;
}

// Parse a full expression
function parse(tokens) {
  let pos = 0;
  function peek() { return tokens[pos]; }
  function consume(type) {
    const tok = tokens[pos];
    if (!tok || (type && tok.t !== type)) throw new Error(i18nFmt('Expected '%expected%' but got '%got%'', { expected: type || '?', got: tok ? tok.t : 'EOF' }));
    pos++;
    return tok;
  }
  function parseExpr() {
    const left = parsePrimary();
    if (peek() && peek().t === '+') { consume('+'); const right = parsePrimary(); return { kind: 'add', left, right }; }
    return left;
  }
  function parsePrimary() {
    const tok = peek();
    if (!tok) throw new Error('Unexpected end of input');
    if (tok.t === 'num') { consume('num'); return { kind: 'num', v: tok.v }; }
    if (tok.t === 'bool') { consume('bool'); return { kind: 'bool', v: tok.v }; }
    if (tok.t === 'if') {
      consume('if'); const cond = parseExpr();
      consume('then'); const thenE = parseExpr();
      consume('else'); const elseE = parseExpr();
      return { kind: 'if', cond, thenE, elseE };
    }
    if (tok.t === '(') { consume('('); const e = parseExpr(); consume(')'); return e; }
    throw new Error(i18nFmt('Unexpected token: '%tok%'', { tok: tok.t }));
  }
  const result = parseExpr();
  if (pos !== tokens.length) throw new Error('Unexpected extra input after expression');
  return result;
}

// Type checker — enforces progress and preservation
// Progress: if typeOf(e) != TypeError, then e can step or is a value.
// Preservation: if typeOf(e) = T and e -> e', then typeOf(e') = T.
function typeOf(e) {
  if (e.kind === 'num') return 'Int';
  if (e.kind === 'bool') return 'Bool';
  if (e.kind === 'add') {
    // T-Add: both operands must be Int
    if (typeOf(e.left) === 'Int' && typeOf(e.right) === 'Int') return 'Int';
    return 'TypeError';
  }
  if (e.kind === 'if') {
    const tc = typeOf(e.cond), tt = typeOf(e.thenE), te = typeOf(e.elseE);
    // T-If: condition must be Bool, branches must share the same type
    if (tc === 'Bool' && tt !== 'TypeError' && te !== 'TypeError' && tt === te) return tt;
    return 'TypeError';
  }
  return 'TypeError';
}

// Evaluator — only called after type check passes
function evaluate(e) {
  if (e.kind === 'num') return e.v;
  if (e.kind === 'bool') return e.v;
  if (e.kind === 'add') return evaluate(e.left) + evaluate(e.right);
  if (e.kind === 'if') return evaluate(e.cond) ? evaluate(e.thenE) : evaluate(e.elseE);
  throw new Error('Evaluator stuck — should not happen for a well-typed expression');
}

// UI wiring
const examples = [
  { expr: '1 + 2', label: '1 + 2' },
  { expr: 'true', label: 'true' },
  { expr: 'if true then 10 else 20', label: 'if true then 10 else 20' },
  { expr: 'if false then 1 else 2', label: 'if false then 1 else 2' },
  { expr: '(1 + 2) + 3', label: '(1+2)+3' },
  { expr: 'true + 1', label: 'true + 1' },
  { expr: 'if 1 then 2 else 3', label: 'if 1 then 2 else 3' },
  { expr: 'if true then 1 else false', label: 'if true then 1 else false' },
];

const exRow = document.getElementById('examples-row');
examples.forEach(({ expr, label }) => {
  const b = document.createElement('button');
  b.className = 'ex-btn'; b.textContent = label;
  b.addEventListener('click', () => { document.getElementById('expr-input').value = expr; runCheck(); });
  exRow.appendChild(b);
});

function setResult(typeStr, evalStr, typeOk, evalOk) {
  const tb = document.getElementById('type-box'), to = document.getElementById('type-out');
  const eb = document.getElementById('eval-box'), eo = document.getElementById('eval-out');
  to.textContent = typeStr; tb.className = 'result-box ' + (typeOk ? 'ok' : 'bad');
  eo.textContent = evalStr; eb.className = 'result-box ' + (evalOk ? 'ok' : 'bad');
}

function setStatus(msg, cls) {
  const s = document.getElementById('status'); s.textContent = msg; s.className = 'status ' + cls;
}

function runCheck() {
  const src = document.getElementById('expr-input').value.trim();
  if (!src) { setResult('—', '—', false, false); setStatus('', ''); return; }
  let ast;
  try { ast = parse(tokenize(src)); }
  catch (err) { setResult('?', '?', false, false); setStatus(i18nFmt('Parse error: %msg%', { msg: err.message }), 'bad'); return; }
  const ty = typeOf(ast);
  if (ty === 'TypeError') {
    setResult('TypeError', 'blocked by type checker', false, false);
    setStatus('Type error — evaluation blocked. The type system caught this before running.', 'bad');
    return;
  }
  setResult(ty, '—', true, false);
  setStatus(i18nFmt('Well-typed: %ty%. Press Evaluate to run safely.', { ty: ty }), 'ok');
}

function runEval() {
  const src = document.getElementById('expr-input').value.trim();
  if (!src) { setResult('—', '—', false, false); setStatus('', ''); return; }
  let ast;
  try { ast = parse(tokenize(src)); }
  catch (err) { setResult('?', '?', false, false); setStatus(i18nFmt('Parse error: %msg%', { msg: err.message }), 'bad'); return; }
  const ty = typeOf(ast);
  if (ty === 'TypeError') {
    setResult('TypeError', 'blocked by type checker', false, false);
    setStatus('Type error — the type checker blocks evaluation. No runtime crash possible.', 'bad');
    return;
  }
  // Progress theorem: typeOf(ast) != TypeError => evaluate never gets stuck
  const val = evaluate(ast);
  setResult(ty, String(val), true, true);
  setStatus(i18nFmt('Evaluated to %val% (type: %ty%). Progress + preservation held every step.', { ty: ty, val: String(val) }), 'ok');
}

document.getElementById('btn-check').addEventListener('click', runCheck);
document.getElementById('btn-run').addEventListener('click', runEval);
document.getElementById('btn-reset').addEventListener('click', () => {
  document.getElementById('expr-input').value = '';
  setResult('—', '—', false, false); setStatus('', '');
});
Result
Console

Notice what happens when you mix types: true + 1 fails the type check instantly, even though the evaluator would happily try to compute something nonsensical. That rejection is progress and preservation in action — the type checker guarantees that evaluation can always proceed safely, or it refuses to start.

The Real Theorems

Type soundness is proved by two lemmas about the operational semantics of a language — the rules that say how expressions reduce to values.

Progress. If ee is a well-typed expression (written ⊢e:T\vdash e : T) and ee is not yet a value, then there exists an expression e′e' such that e→e′e \to e'. In plain English: a well-typed program is never stuck mid-computation.

Preservation (Subject Reduction). If ⊢e:T\vdash e : T and e→e′e \to e', then ⊢e′:T\vdash e' : T. A reduction step cannot change the type of the result. The guarantee survives every step of evaluation.

Together they imply: if a program type-checks, evaluation either terminates normally or diverges — it never crashes with an undefined operation. Wright and Felleisen proved this for Mini-ML in 1994 using structural induction on the typing derivation, not by testing programs. The proof is finite, yet it covers infinitely many possible inputs and execution paths.

The connection to the halting problem is subtle: type checking itself is decidable (in most common languages), but it only rules out a specific class of errors. Checking full correctness — does this program compute what I intended? — is still undecidable in general.

Where It Matters

The progress-and-preservation argument is not an academic curiosity — it is the engine behind the safety guarantees of every major typed language:

  • Rust: the borrow checker is an extended type system. Type soundness is what makes "if it compiles, it won't use-after-free" true, not just a slogan.
  • Java and Kotlin: the type system rules out most ClassCastException and null-pointer crashes; Kotlin's nullable types push the guarantee further.
  • Haskell: purity and the IO monad are enforced by the type system — a function typed Int -> Int cannot perform side effects, and soundness ensures that holds throughout execution.
  • TypeScript: adds soundness approximately. TypeScript intentionally trades full soundness for expressiveness (any, type assertions) — a useful reminder that soundness is a spectrum.
  • Proof assistants (Coq, Lean, Agda): type soundness is the foundation of the propositions-as-types correspondence — a proof of a theorem literally is a well-typed program.

Wherever you see a "type-safe" language promise, you are seeing the Wright–Felleisen theorem deployed at scale. Related ideas appear in circuit complexity (where gate types must match) and in formal verification of hardware.

Conclusion

Type soundness is deceptively simple: two lemmas about one step of evaluation, proved by induction, covering all programs forever. Yet the consequence is enormous — the type checker becomes a verifiable promise, not a style suggestion.

Progress says your program is never stranded without a next move. Preservation says each move respects the type contract. Together they mean: write code that passes the type checker, and an entire class of runtime disasters is mathematically impossible.

The next time a compiler tells you "type error," it is not being pedantic. It is invoking a proof — and saving you from a crash that might only appear at 3 a.m. in production. That is the quiet power of the halting problem's decidable cousin.

Share this article

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

Comments

Loading comments...

https://www.kipuhub.com/en/article/type-soundness-progress/Content licensed under CC BY-NC 4.0.