Progress and Preservation (Type Safety)
A type-checker earns its keep only if its "yes" means something. We want a precise guarantee:
if the checker accepts a program, then running it will never reach a nonsensical state — never try to
apply an integer, branch on a function, or take the predecessor of a boolean. Milner distilled the
promise into a slogan — "well-typed programs cannot go wrong" — but a slogan is not a
proof. This page states the guarantee formally as type safety (or type
soundness) and proves it the way Wright and Felleisen taught the field in 1994: as the
conjunction of two theorems, Progress and Preservation.
Type safety is a bridge between the two halves of a language's definition — its
static semantics (the typing relation
\Gamma \vdash t : T) and its
operational
semantics (the step relation t \to t'). Neither theorem alone suffices;
together they lock the two semantics into agreement.
What does "go wrong" mean? Getting stuck
In a small-step semantics, evaluation is a sequence of rewrites
t \to t' \to t'' \to \cdots. Two good outcomes exist: the sequence reaches
a value (a finished result — \text{true}, a numeral, a
\lambda), or it runs forever. The bad outcome is a
stuck term: a non-value that cannot step, because no evaluation rule matches
its shape. \text{if}\;(\lambda x{:}T.x)\;\text{then}\;\ldots is stuck — the
guard is a function, and no \text{if}-rule fires. "Going wrong" is exactly
getting stuck. Type safety is the claim that a well-typed term never gets stuck.
\textbf{stuck}(t)\;\;\overset{\text{def}}{\equiv}\;\; t \text{ is a normal form (no } t' \text{ with } t \to t') \;\wedge\; t \text{ is not a value.}
The two theorems
Fix a closed, well-typed term \vdash t : T. Progress says it is not stuck
right now; Preservation says stepping keeps it well-typed, so it is not stuck at the
next moment either. Chaining them gives safety for the whole run.
- If \vdash t : T (a closed, well-typed term), then either
t is a value, or there exists a term t' with
t \to t'.
- Equivalently: a well-typed closed term is never stuck — it can always make
progress, unless it is already finished.
- If \Gamma \vdash t : T and t \to t', then
\Gamma \vdash t' : T.
- Evaluation does not change a term's type: the type T is an
invariant of the whole reduction sequence.
Their corollary is the theorem we actually wanted:
- If \vdash t : T and t \to^{*} t' (any
number of steps), then t' is not stuck.
- Proof: \vdash t' : T by repeated Preservation, and then
t' is a value-or-can-step by Progress. So a well-typed term reaches a
value or diverges — it cannot go wrong.
Safety as an invariant, pictured
Type safety is best seen as an invariant chasing a moving target. Preservation is the
horizontal guarantee — the type T is carried unchanged along every arrow.
Progress is the vertical guarantee — at every node the term is a value or has an outgoing arrow, so the
crossed-out "stuck" state is unreachable. Watch a concrete well-typed term evaluate:
Every term in the chain carries the same type \text{Nat} — that is
Preservation holding step after step. And at no point is the term a stuck non-value: it either steps
(Progress via a matching rule) or, at the end, is the value 0. The
forbidden state at the bottom — a non-value with no move — is exactly what Progress rules out for
well-typed terms; an ill-typed term like \text{if}\;0\;\text{then}\;\ldots
could land there, but the type-checker never let it in.
The two supporting lemmas
Each theorem leans on one workhorse lemma. Progress needs to know that a value of a given type has the
shape that type promises — the Canonical Forms lemma. Preservation needs to
know that substituting an argument into a function body respects types — the
Substitution lemma.
- If v is a value and \vdash v : \text{Bool},
then v is \text{true} or
\text{false}.
- If v is a value and
\vdash v : T_1 \to T_2, then
v = \lambda x{:}T_1.\,t for some body t.
- If \Gamma,\,x{:}S \vdash t : T and
\Gamma \vdash s : S, then
\Gamma \vdash [x \mapsto s]\,t : T.
- Substituting a well-typed term of type S for a variable assumed to
have type S leaves the overall type T
unchanged.
Proof sketch, by induction
Both theorems are proved by induction on the typing derivation (equivalently, on the
structure of t), using inversion to expose the last rule.
Progress — case on the last typing rule for the closed term
t. If it is T-Var, that is vacuous: a closed term has no free variables.
If T-Abs, then t is a \lambda — a value, done. If
T-App with t = t_1\,t_2, apply the induction hypothesis to
t_1: either it steps (so t steps by the
congruence rule E-App1), or it is a value; then likewise for t_2; and if
both are values, Canonical Forms tells us t_1 = \lambda x{:}T.\,t_{12}, so
the redex fires by \beta-reduction (E-AppAbs). Every case yields a value or
a step — no stuck state.
Preservation — case on the evaluation step t \to t'. The
interesting case is \beta-reduction
(\lambda x{:}T_{11}.\,t_{12})\,v \to [x \mapsto v]\,t_{12}: by inversion the
function has type T_{11}\to T_{12} with
x{:}T_{11} \vdash t_{12} : T_{12}, and the argument has type
T_{11}; the Substitution lemma then delivers
\vdash [x\mapsto v]\,t_{12} : T_{12} — the same type. The congruence cases
follow directly from the induction hypothesis. Type is preserved at every step.
Watching safety hold, in code
Nothing beats seeing the invariant survive. Below is a tiny language of booleans and numbers with a
small-step evaluator step1 and a type-checker typeOf. We evaluate a
well-typed term one step at a time and print its type after each — and it never changes (Preservation),
while the term is always a value or steppable (Progress), until it lands on a value.
type Term =
| { kind: "True" } | { kind: "False" } | { kind: "Zero" }
| { kind: "Succ"; n: Term } | { kind: "Pred"; n: Term } | { kind: "IsZero"; n: Term }
| { kind: "If"; c: Term; t: Term; e: Term };
const isNum = (t: Term): boolean =>
t.kind === "Zero" || (t.kind === "Succ" && isNum(t.n));
const isValue = (t: Term): boolean =>
t.kind === "True" || t.kind === "False" || isNum(t);
// ── Small-step evaluation: one rewrite, or null if none applies. ──
function step1(t: Term): Term | null {
switch (t.kind) {
case "If":
if (t.c.kind === "True") return t.t; // E-IfTrue
if (t.c.kind === "False") return t.e; // E-IfFalse
{ const c = step1(t.c); return c ? { kind: "If", c, t: t.t, e: t.e } : null; }
case "Succ": { const n = step1(t.n); return n ? { kind: "Succ", n } : null; }
case "Pred":
if (t.n.kind === "Zero") return { kind: "Zero" }; // pred 0 → 0
if (t.n.kind === "Succ" && isNum(t.n.n)) return t.n.n; // pred (succ nv) → nv
{ const n = step1(t.n); return n ? { kind: "Pred", n } : null; }
case "IsZero":
if (t.n.kind === "Zero") return { kind: "True" };
if (t.n.kind === "Succ" && isNum(t.n.n)) return { kind: "False" };
{ const n = step1(t.n); return n ? { kind: "IsZero", n } : null; }
default: return null; // values don't step
}
}
// ── Typing: Bool and Nat. Throws on ill-typed terms. ──
function typeOf(t: Term): "Bool" | "Nat" {
switch (t.kind) {
case "True": case "False": return "Bool";
case "Zero": return "Nat";
case "Succ": case "Pred":
if (typeOf(t.n) !== "Nat") throw new Error("expects Nat");
return "Nat";
case "IsZero":
if (typeOf(t.n) !== "Nat") throw new Error("iszero expects Nat");
return "Bool";
case "If": {
if (typeOf(t.c) !== "Bool") throw new Error("guard must be Bool");
const a = typeOf(t.t), b = typeOf(t.e);
if (a !== b) throw new Error("branches disagree");
return a;
}
}
}
const show = (t: Term): string => {
switch (t.kind) {
case "True": return "true"; case "False": return "false"; case "Zero": return "0";
case "Succ": return `succ(${show(t.n)})`;
case "Pred": return `pred(${show(t.n)})`;
case "IsZero": return `iszero(${show(t.n)})`;
case "If": return `if ${show(t.c)} then ${show(t.t)} else ${show(t.e)}`;
}
};
const num = (k: number): Term => (k === 0 ? { kind: "Zero" } : { kind: "Succ", n: num(k - 1) });
// term: if iszero(pred(succ 0)) then 0 else succ(succ 0)
let term: Term = {
kind: "If",
c: { kind: "IsZero", n: { kind: "Pred", n: num(1) } },
t: num(0),
e: num(2),
};
console.log(`start type = ${typeOf(term)} (this must stay fixed)\n`);
let steps = 0;
while (!isValue(term)) {
console.log(`${show(term)} : ${typeOf(term)}`); // type re-checked every step
const next = step1(term);
if (next === null) { console.log("STUCK — impossible for a well-typed term!"); break; }
term = next;
steps++;
}
console.log(`${show(term)} : ${typeOf(term)} ← value reached in ${steps} steps (Progress + Preservation held)`);
Preservation's older name is Subject Reduction, and the phrase is a genuine pun from
logic. In a judgment t : T, logicians called the term
t the "subject" and the type T the
"predicate", by analogy with subject–predicate grammar. The theorem says that when you
reduce (evaluate) the subject, the predicate still holds of it — the subject may
change but its type survives reduction. The dual, "subject expansion"
(does un-stepping preserve types?), is false in general — a well-typed result can come from
an ill-typed redex — which is a favourite exam trap. So the arrow of safety points forward only:
stepping keeps types, but stepping backward need not.
Preservation alone is not safety — and neither is Progress alone. Students often prove
Preservation and declare victory, but a language could preserve types perfectly and still get
stuck: imagine a semantics with no rule for
\text{if}\;0\;\text{then}\ldots — a term that never changes type simply
because it never steps. Preservation is vacuously true there, yet the term is stuck. You need Progress
to forbid the stuck state and Preservation to keep the term well-typed so that Progress
keeps applying. Conversely, a semantics that "steps" a bad term to some arbitrary junk could
satisfy Progress while violating Preservation. Safety is the conjunction; drop either half and
the guarantee collapses.
Where safety can be lost
The proof is delicate precisely because small changes break it. Add a general
fixed-point operator and safety survives (you only
lose termination). But add an unchecked cast, Java-style array covariance, or a
null that inhabits every type, and Preservation or Canonical Forms fails — which is why
those features come bolted to a runtime check (a ClassCastException, a
NullPointerException) that re-imposes the guarantee dynamically. Every unsound feature in
a real language is, in the end, a place where one of these two theorems could not be made to hold
statically.