Lesson 6.1 — Typing judgments, derivations and type safety¶
Techniques: typing judgments, inference rules and derivation trees (Church 1940; Martin-Löf; the notation of [Car96, TAPL]); type safety proved syntactically by progress and preservation (Wright & Felleisen 1994 [WF94]), after Milner's semantic "well-typed programs cannot go wrong" (1978 [Mil78]) · Pebble implements: pebble-spec §5–§9 are typing rules;
typeCheckbuilds one derivation per function (exercises E1–E6) · Drills:typing-derivation,progress-preservation· Prerequisites: Chapter 5 (every name already bound to its declaration); induction on trees · Time: 5 hours
A type checker answers one question about every expression: what kind of value can this produce? Before you can implement one (Lesson 6.3 onward), you need a precise way to say what the right answer is — independently of any algorithm — and a precise sense in which the answer is useful. This lesson gives both. The first half turns a language's typing rules into mathematics: judgments, inference rules and the derivation trees built from them. The second half proves the theorem that justifies the whole enterprise: a program the rules accept never reaches a state the language has no rule for. You will prove it completely for a small functional language, see which lemma breaks when a rule is changed carelessly, and see what "going wrong" looks like in a real system when the type system is bypassed.
1. Problem and motivation¶
Typing judgments, inference rules and derivations¶
The problem. A language specification says, in prose, things like "a + b requires both operands to be int and has type int" (pebble-spec §8.3). A compiler needs an unambiguous definition of which programs are well typed and what type each expression has, one that two implementations can agree on and that proofs can be written about. The standard tool is an inductive definition: a set of inference rules, each saying "if these judgments hold, then this one does". A program is well typed exactly when there is a finite tree of rule applications, a derivation, that concludes it.
The notation goes back to logic: Gentzen's natural deduction (1935), Church's simply typed λ-calculus (1940), and Martin-Löf's judgments. Cardelli's survey [Car96, §3] made it the lingua franca of language definitions, and every modern type-system paper and textbook [TAPL, Ch. 8–9; PFPL, Ch. 2–4] writes rules this way. In pebblec, each rule of pebble-spec §8 becomes one case of typeCheck; each call of the checker on a subexpression is one premise of a rule.
Type safety by progress and preservation¶
The problem. A type system is only worth its restrictions if it guarantees something. Milner stated the guarantee in 1978 as a slogan and a theorem: "well-typed programs cannot go wrong" [Mil78, §3]. He gave the language a denotational semantics with a special value wrong for meaningless operations (adding a boolean to a function) and proved that well-typed expressions never denote wrong. That proof method is hard to extend to references, exceptions and continuations. Wright and Felleisen [WF94] replaced it with a syntactic method on the operational semantics: a well-typed term either is a value or can take a step (progress), and a step keeps the type (preservation, also called subject reduction). Together, by induction on the number of steps, a well-typed program never reaches a stuck state. That is the method this lesson uses, and the one [TAPL, §8.3, §9.3] and [PFPL, Ch. 6] teach.
For Pebble, "going wrong" would mean the lowering (Chapter 11) meeting an operation it cannot translate — add on a string, a call with too few arguments. The type checker's job is to make that impossible; the traps of pebble-spec §11.3 (overflow, bounds, division by zero) are not type errors: they are defined behaviors of well-typed programs.
2. Definitions and algorithms¶
Typing judgments, inference rules and derivations¶
The running language of this lesson is the simply typed λ-calculus with integers, booleans and let [TAPL, Ch. 9, §11.5]. It is small enough for complete proofs and has every feature that makes Pebble's checker interesting: variables, functions, operators with fixed operand types, conditionals and local bindings.
Definition 6.1.1 (Types and terms)
Types \(\tau ::= \mathsf{int} \mid \mathsf{bool} \mid \tau_1 \to \tau_2\), with \(\to\) associating to the right. Terms
where \(x\) ranges over variables and \(n\) over integers. \(\lambda x{:}\tau.\,e\) and \(\mathsf{let}\ x = e_1\ \mathsf{in}\ e_2\) bind \(x\) in \(e\) and \(e_2\); a term is closed if it has no free variables. Terms are identified up to renaming of bound variables (Lesson 5.2).
Definition 6.1.2 (Context and typing judgment)
A typing context \(\Gamma\) is a finite partial function from variables to types, written \(x_1{:}\tau_1, \dots, x_k{:}\tau_k\); \(\emptyset\) is the empty context and \(\Gamma, x{:}\tau\) is \(\Gamma[x \mapsto \tau]\) (a later binding of \(x\) replaces an earlier one, which is shadowing). A typing judgment \(\Gamma \vdash e : \tau\) is a formula read "in context \(\Gamma\), term \(e\) has type \(\tau\)". It is a claim, not a fact: rules decide which judgments are derivable.
Definition 6.1.3 (Inference rules; Figure 6.1.1)
An inference rule is a scheme \(\dfrac{J_1 \quad \cdots \quad J_k}{J}\) with premises \(J_i\) and a conclusion \(J\) (an axiom when \(k = 0\)), in which metavariables (\(\Gamma, e, \tau, \dots\)) stand for arbitrary contexts, terms and types; a rule instance replaces the metavariables consistently. The typing rules of the running language are (Figure 6.1.1):
Definition 6.1.4 (Derivation)
A derivation of \(J\) is a finite tree whose nodes are judgments, whose root is \(J\), and in which every node together with its children is an instance of some rule (the children are the premises, the node the conclusion; a leaf is an axiom instance or a side condition such as \(\Gamma(x) = \tau\)). \(J\) is derivable, written \(\vdash J\) or just "\(J\) holds", if it has a derivation. A tree that fails the instance condition at some node is invalid at that node. The set of derivable judgments is the smallest set closed under the rules, so properties of derivable judgments are proved by induction on derivations (rule induction).
Reading a rule both ways
T-App read downwards is a proof step: if you have derivations of \(\Gamma \vdash f : \mathsf{int} \to \mathsf{bool}\) and \(\Gamma \vdash 3 : \mathsf{int}\), you may conclude \(\Gamma \vdash f\,3 : \mathsf{bool}\). Read upwards it is an algorithm step: to type \(f\,3\), type \(f\), check that its type is an arrow, type \(3\), compare it with the arrow's domain. Pebble's rule for calls (pebble-spec §8.6) is T-App with \(n\) arguments.
Definition 6.1.5 (Syntax-directed rule system)
A rule system is syntax-directed if, for every term form, exactly one rule has a conclusion whose term is of that form, and every premise of that rule is about an immediate subterm (with a context computed from the conclusion's). Figure 6.1.1 is syntax-directed; adding a rule without a matching term form — a subsumption rule \(\dfrac{\Gamma \vdash e : \sigma \quad \sigma <: \tau}{\Gamma \vdash e : \tau}\) (Lesson 6.5) — breaks it.
For a syntax-directed system the derivation of a term has exactly one node per subterm, and finding it is a recursive walk:
Algorithm 6.1.6 (TypeOf: derivation search for a syntax-directed system)
- Input: a context \(\Gamma\) and a term \(e\).
- Output: the type \(\tau\) with \(\Gamma \vdash e : \tau\), or fail.
- Precondition: Figure 6.1.1's rules; every λ carries its parameter type.
- Postcondition: returns \(\tau\) iff \(\Gamma \vdash e : \tau\) is derivable (Theorem 6.1.11); the recursion tree is the derivation.
- Invariant: each call on \((\Gamma', e')\) is made with the context that the unique applicable rule prescribes for the premise about \(e'\).
function TypeOf(Γ, e):
case e of
x: if x ∈ dom(Γ): return Γ(x) else fail
n: return int
true, false: return bool
λx:τ1. e1: τ2 ← TypeOf(Γ[x ↦ τ1], e1); return τ1 → τ2
e1 e2: τf ← TypeOf(Γ, e1); τa ← TypeOf(Γ, e2)
if τf = τ1 → τ2 and τa = τ1: return τ2 else fail
e1 + e2, e1 < e2: if TypeOf(Γ, e1) = int and TypeOf(Γ, e2) = int:
return int (for +) or bool (for <)
else fail
if e1 then e2 else e3: if TypeOf(Γ, e1) = bool:
τ ← TypeOf(Γ, e2)
if TypeOf(Γ, e3) = τ: return τ
fail
let x = e1 in e2: τ1 ← TypeOf(Γ, e1); return TypeOf(Γ[x ↦ τ1], e2)
fail propagates: a call that receives fail from a recursive call fails. Type equality is structural equality of type trees (constant time if types are hash-consed, §5).
Type safety by progress and preservation¶
Safety is a statement about how programs run, so it needs an operational semantics. The one below is call-by-value, left to right, small-step [TAPL, §5.3, §9.3].
Definition 6.1.7 (Values and evaluation; Figure 6.1.2)
Values \(v ::= n \mid \mathsf{true} \mid \mathsf{false} \mid \lambda x{:}\tau.\, e\). \([x \mapsto v]e\) is the substitution of \(v\) for the free occurrences of \(x\) in \(e\) (only closed values are substituted below, so no capture can occur). The one-step evaluation relation \(e \longrightarrow e'\) on closed terms is the smallest relation closed under:
where \(\oplus \in \{+, <\}\) and integers are mathematical (unbounded); \(\longrightarrow^{*}\) is the reflexive-transitive closure.
Definition 6.1.8 (Stuck term; type safety)
A closed term \(e\) is in normal form if there is no \(e'\) with \(e \longrightarrow e'\), and stuck if it is a normal form but not a value (for example \(\mathsf{true} + 1\) or \(3\ 4\)). A type system is safe (sound) for a semantics if no closed well-typed term reaches a stuck term: \(\emptyset \vdash e : \tau\) and \(e \longrightarrow^{*} e'\) imply that \(e'\) is not stuck. The syntactic method splits this into progress (\(\emptyset \vdash e : \tau\) implies \(e\) is a value or \(e \longrightarrow e'\) for some \(e'\)) and preservation (\(\emptyset \vdash e : \tau\) and \(e \longrightarrow e'\) imply \(\emptyset \vdash e' : \tau\)).
The drill progress-preservation uses an even smaller language, the typed arithmetic expressions of [TAPL, Ch. 3 and 8]: booleans, 0, succ, pred, iszero, if, with types \(\mathsf{Nat}\) and \(\mathsf{Bool}\) and the same two theorems (the drill prints its rules). It is small enough that a computer can check a rule set by enumerating every term up to a size bound, which is exactly how the drill's oracle decides which property a broken rule destroys.
3. Worked examples¶
Typing judgments, inference rules and derivations¶
The running term, closed, with the drill's pre-order numbering of its subterms:
Algorithm 6.1.6 visits the subterms in pre-order and returns types in post-order. One row per call (the context grows under the λ and in the let body):
| node | subterm | \(\Gamma\) at the node | rule | type returned |
|---|---|---|---|---|
| s1 | let f = λx:int. x + 1 in if f 2 < 5 then f 3 else 0 |
∅ | T-Let | int |
| s2 | λx:int. x + 1 |
∅ | T-Abs | int -> int |
| s3 | x + 1 |
x : int | T-Add | int |
| s4 | x |
x : int | T-Var | int |
| s5 | 1 |
x : int | T-Int | int |
| s6 | if f 2 < 5 then f 3 else 0 |
f : int -> int | T-If | int |
| s7 | f 2 < 5 |
f : int -> int | T-Lt | bool |
| s8 | f 2 |
f : int -> int | T-App | int |
| s9 | f |
f : int -> int | T-Var | int -> int |
| s10 | 2 |
f : int -> int | T-Int | int |
| s11 | 5 |
f : int -> int | T-Int | int |
| s12 | f 3 |
f : int -> int | T-App | int |
| s13 | f |
f : int -> int | T-Var | int -> int |
| s14 | 3 |
f : int -> int | T-Int | int |
| s15 | 0 |
f : int -> int | T-Int | int |
- s2 returns
int -> intonly after s3 returnedintin the extended context: T-Abs's premise is about the body. - s8 checks that s9's type is an arrow and that its domain equals s10's type
int; s12 repeats the check. s6 compares the branch types s12 and s15. - The derivation tree is this table read as a tree (s1's children are s2 and s6; s6's are s7, s12, s15; and so on). Written as nested fractions, its top reads
Try it
./course drill typing-derivation --seed 4 --difficulty hard --solution builds a derivation for a random term and then asks you to find the invalid nodes of a corrupted one: a node whose conclusion does not follow from its children's claimed conclusions by its rule (Definition 6.1.4).
Type safety by progress and preservation¶
Evaluate \(e_{\mathrm{run}}\) step by step (Figure 6.1.2) and re-type every intermediate term. Write \(g\) for \(\lambda x{:}\mathsf{int}.\,x+1\).
| step | term | rule used | type of the term |
|---|---|---|---|
| 0 | let f = g in if f 2 < 5 then f 3 else 0 |
— | int |
| 1 | if g 2 < 5 then g 3 else 0 |
E-LetV | int |
| 2 | if (2 + 1) < 5 then g 3 else 0 |
E-If ← E-Op1 ← E-Beta | int |
| 3 | if 3 < 5 then g 3 else 0 |
E-If ← E-Op1 ← E-Add | int |
| 4 | if true then g 3 else 0 |
E-If ← E-Lt | int |
| 5 | g 3 |
E-IfTrue | int |
| 6 | 3 + 1 |
E-Beta | int |
| 7 | 4 |
E-Add | int (a value: evaluation ends) |
- Every row has type
int: preservation, observed seven times. Every row but the last can step: progress. - Step 1 substitutes the value \(g\) for \(f\) (Lemma 6.1.15 is what keeps the type). Step 2 shows the congruence rules at work: the only redex is inside the condition inside the
if. - The subterm
f 2 < 5of step 0 had typebool, and so does each of its reducts3 < 5andtrue: preservation holds at every subterm, which is what the inductive proof exploits.
A broken rule set. Add to the arithmetic language of the drill the rule \(\dfrac{\Gamma \vdash t : \mathsf{Bool}}{\Gamma \vdash \mathsf{succ}\ t : \mathsf{Nat}}\) (T-SuccBool). Then \(\vdash \mathsf{succ}\ \mathsf{true} : \mathsf{Nat}\), but no evaluation rule applies to succ true and it is not a value: progress fails. Preservation survives: a term typed by the new rule is succ t with t : Bool, and it can only step inside t (E-Succ), to succ t' with t' : Bool by preservation for t, which the new rule types Nat again. Exhaustive enumeration agrees: the drill's oracle checks the 3 873 terms of at most 6 nodes and finds succ true as the smallest counterexample.
Try it
./course drill progress-preservation --seed 2 --difficulty hard --solution combines two mutations; the worked solution names the lemma of the proof below that each one breaks.
4. Invariants and correctness¶
Typing judgments, inference rules and derivations¶
Every proof below uses the same first step: because the system is syntax-directed, the shape of a term determines the last rule of any derivation of it.
Lemma 6.1.9 (Inversion of the typing relation)
- If \(\Gamma \vdash x : \tau\) then \(\Gamma(x) = \tau\).
- If \(\Gamma \vdash n : \tau\) then \(\tau = \mathsf{int}\); if \(\Gamma \vdash b : \tau\) for a boolean \(b\) then \(\tau = \mathsf{bool}\).
- If \(\Gamma \vdash \lambda x{:}\tau_1.\,e : \tau\) then \(\tau = \tau_1 \to \tau_2\) for some \(\tau_2\) with \(\Gamma, x{:}\tau_1 \vdash e : \tau_2\).
- If \(\Gamma \vdash e_1\, e_2 : \tau\) then there is \(\tau_1\) with \(\Gamma \vdash e_1 : \tau_1 \to \tau\) and \(\Gamma \vdash e_2 : \tau_1\).
- If \(\Gamma \vdash e_1 + e_2 : \tau\) then \(\tau = \mathsf{int}\) and both \(e_i\) have type \(\mathsf{int}\); likewise for \(<\) with \(\tau = \mathsf{bool}\).
- If \(\Gamma \vdash \mathsf{if}\ e_1\ \mathsf{then}\ e_2\ \mathsf{else}\ e_3 : \tau\) then \(\Gamma \vdash e_1 : \mathsf{bool}\), \(\Gamma \vdash e_2 : \tau\) and \(\Gamma \vdash e_3 : \tau\).
- If \(\Gamma \vdash \mathsf{let}\ x = e_1\ \mathsf{in}\ e_2 : \tau\) then there is \(\tau_1\) with \(\Gamma \vdash e_1 : \tau_1\) and \(\Gamma, x{:}\tau_1 \vdash e_2 : \tau\).
Proof
Each clause by inspecting the last rule of the derivation. By Definition 6.1.5 exactly one rule of Figure 6.1.1 has a conclusion whose term has the given form (T-Var for variables, T-Int, T-Bool, T-Abs, T-App, T-Add or T-Lt, T-If, T-Let), so that rule ended the derivation, and its premises are exactly the listed judgments with the conclusion's type substituted for its metavariable.
Theorem 6.1.10 (Uniqueness of types)
If \(\Gamma \vdash e : \tau\) and \(\Gamma \vdash e : \tau'\) then \(\tau = \tau'\), and the two derivations are identical.
Proof
By induction on \(e\) (structural). Variables and constants: Lemma 6.1.9(1–2) determines \(\tau\) from \(\Gamma\) or the constant. λ: both types are \(\tau_1 \to \tau_2\) and \(\tau_1 \to \tau_2'\) with the body typed in the same context \(\Gamma, x{:}\tau_1\) (Lemma 6.1.9(3)); by the induction hypothesis \(\tau_2 = \tau_2'\). Application: Lemma 6.1.9(4) gives \(\Gamma \vdash e_1 : \tau_1 \to \tau\) and \(\Gamma \vdash e_1 : \tau_1' \to \tau'\); the hypothesis on \(e_1\) makes the arrows equal, so \(\tau = \tau'\). Operators, if, let: the same pattern with Lemma 6.1.9(5–7); for let the hypothesis on \(e_1\) makes the two contexts for \(e_2\) equal before it is applied to \(e_2\). The derivations coincide because each node's rule and premises are forced.
Theorem 6.1.11 (Algorithm 6.1.6 is correct)
For every \(\Gamma\) and \(e\), TypeOf\((\Gamma, e)\) terminates; it returns \(\tau\) iff \(\Gamma \vdash e : \tau\) is derivable, and fails iff no type is derivable.
Proof
Termination: each recursive call is on an immediate subterm, so the recursion depth is at most the height of \(e\) and the number of calls is the number of subterms. Soundness (returns \(\tau\) ⇒ derivable), by induction on \(e\): each branch returns a type only after its recursive calls returned types for which, by the induction hypothesis, derivations exist; those derivations are exactly the premises of the rule for that branch, whose side conditions (an arrow with the right domain, int operands, equal branch types) are the tests the branch performs, so the rule builds a derivation of the result. Completeness (derivable ⇒ returns it), by induction on the derivation: its last rule is the one of the branch for \(e\)'s form (Lemma 6.1.9), its premises are derivable, so by the induction hypothesis the recursive calls return exactly their types (unique by Theorem 6.1.10), and the branch's tests succeed and return the conclusion's type. Failure is then exactly the absence of a derivable type.
Type safety by progress and preservation¶
Lemma 6.1.12 (Canonical forms)
Let \(v\) be a closed value. If \(\emptyset \vdash v : \mathsf{int}\) then \(v\) is an integer \(n\); if \(\emptyset \vdash v : \mathsf{bool}\) then \(v \in \{\mathsf{true}, \mathsf{false}\}\); if \(\emptyset \vdash v : \tau_1 \to \tau_2\) then \(v = \lambda x{:}\tau_1.\, e\) for some \(x\) and \(e\).
Proof
A value is an integer, a boolean or a λ (Definition 6.1.7). By Lemma 6.1.9(2–3) an integer has only type int, a boolean only bool, and a λ only an arrow type whose domain is its annotation. So each type is possible for exactly one of the three forms.
Theorem 6.1.13 (Progress)
If \(\emptyset \vdash e : \tau\) then \(e\) is a value or there is \(e'\) with \(e \longrightarrow e'\).
Proof
By induction on the derivation of \(\emptyset \vdash e : \tau\), with a case for its last rule.
- T-Var: impossible, since \(\emptyset(x)\) is undefined.
- T-Int, T-Bool, T-Abs: \(e\) is a value.
- T-App, \(e = e_1\, e_2\) with \(\emptyset \vdash e_1 : \tau_1 \to \tau\) and \(\emptyset \vdash e_2 : \tau_1\). By the induction hypothesis on \(e_1\): if \(e_1 \longrightarrow e_1'\) then \(e \longrightarrow e_1'\, e_2\) by E-App1. Otherwise \(e_1\) is a value; by the hypothesis on \(e_2\), either \(e_2 \longrightarrow e_2'\) and \(e \longrightarrow e_1\, e_2'\) by E-App2, or \(e_2\) is a value too. Then Lemma 6.1.12 gives \(e_1 = \lambda x{:}\tau_1.\, e_0\), and E-Beta applies.
- T-Add, T-Lt, \(e = e_1 \oplus e_2\) with both operands of type
int. As for application, E-Op1 or E-Op2 applies unless both are values; then Lemma 6.1.12 makes them integers and E-Add or E-Lt applies. - T-If, \(e_1 : \mathsf{bool}\). If \(e_1\) steps, E-If applies. Otherwise \(e_1\) is a value, hence
trueorfalse(Lemma 6.1.12), and E-IfTrue or E-IfFalse applies. - T-Let: if \(e_1\) steps, E-Let1; otherwise \(e_1\) is a value and E-LetV applies.
Every case ends in a value or a step. The cases use canonical forms exactly where an elimination form meets a value; that is where a broken rule set breaks progress (§6).
Lemma 6.1.14 (Weakening)
If \(\Gamma \vdash e : \tau\) and \(y \notin \mathrm{dom}(\Gamma)\), then \(\Gamma, y{:}\sigma \vdash e : \tau\) for every \(\sigma\). In particular, a closed term typable in \(\emptyset\) has the same type in every context.
Proof
By induction on the derivation of \(\Gamma \vdash e : \tau\). T-Var: \(\Gamma(x) = \tau\) and \(x \neq y\) (as \(y \notin \mathrm{dom}(\Gamma)\)), so \((\Gamma, y{:}\sigma)(x) = \tau\). T-Int, T-Bool: the rules ignore the context. T-App, T-Add, T-Lt, T-If: apply the induction hypothesis to each premise (same context) and reapply the rule. T-Abs, premise \(\Gamma, x{:}\tau_1 \vdash e_0 : \tau_2\): rename the bound \(x\) if necessary (terms are equal up to renaming, Definition 6.1.1) so that \(x \neq y\); then \(y \notin \mathrm{dom}(\Gamma, x{:}\tau_1)\), the hypothesis gives \(\Gamma, x{:}\tau_1, y{:}\sigma \vdash e_0 : \tau_2\), and since \(x \neq y\) this context equals \(\Gamma, y{:}\sigma, x{:}\tau_1\) (a finite map), so T-Abs concludes. T-Let: the first premise as for application, the second as for T-Abs. For the corollary, apply the lemma once per variable of the context.
Lemma 6.1.15 (Substitution)
If \(\Gamma, x{:}\sigma \vdash e : \tau\) and \(\emptyset \vdash v : \sigma\) for a closed value \(v\), then \(\Gamma \vdash [x \mapsto v]e : \tau\).
Proof
By induction on the derivation of \(\Gamma, x{:}\sigma \vdash e : \tau\).
- T-Var, \(e = y\). If \(y = x\) then \(\tau = \sigma\) and \([x \mapsto v]x = v\); \(\emptyset \vdash v : \sigma\) weakens to \(\Gamma \vdash v : \sigma\) (Lemma 6.1.14). If \(y \neq x\) then \([x \mapsto v]y = y\) and \(\Gamma(y) = \tau\), so T-Var applies.
- T-Int, T-Bool: the substitution changes nothing and the rules ignore the context.
- T-App, T-Add, T-Lt, T-If: substitution distributes over the subterms; apply the induction hypothesis to each premise and reapply the rule.
- T-Abs, \(e = \lambda y{:}\tau_1.\, e_0\), premise \(\Gamma, x{:}\sigma, y{:}\tau_1 \vdash e_0 : \tau_2\). If \(y = x\), the λ rebinds \(x\), so \([x \mapsto v]e = e\) and the inner context equals \(\Gamma, y{:}\tau_1\) (the later binding wins); the premise is already \(\Gamma, y{:}\tau_1 \vdash e_0 : \tau_2\) and T-Abs gives \(\Gamma \vdash e : \tau\). If \(y \neq x\), the context equals \(\Gamma, y{:}\tau_1, x{:}\sigma\); the hypothesis gives \(\Gamma, y{:}\tau_1 \vdash [x \mapsto v]e_0 : \tau_2\), and since \(v\) is closed, \([x \mapsto v]e = \lambda y{:}\tau_1.\, [x \mapsto v]e_0\) (no capture), so T-Abs concludes.
- T-Let: the first premise as for application; the body as in the T-Abs case, including the case \(y = x\).
Theorem 6.1.16 (Preservation)
If \(\emptyset \vdash e : \tau\) and \(e \longrightarrow e'\), then \(\emptyset \vdash e' : \tau\).
Proof
By induction on the derivation of \(e \longrightarrow e'\) (Figure 6.1.2). Evaluation relates closed terms, and every subterm of a closed term that is not under a binder is closed, so every typing below is in the empty context.
- Congruence rules (E-App1, E-App2, E-Op1, E-Op2, E-If, E-Let1): one immediate subterm steps. Inversion (Lemma 6.1.9) gives the premise typing that subterm; the induction hypothesis gives the same type to its reduct; the original typing rule then types \(e'\) with \(\tau\). (For E-Let1 the stepping subterm is \(e_1\), whose type \(\tau_1\) is kept, so the context for the body is unchanged.)
- E-Beta, \((\lambda x{:}\tau_1.\,e_0)\,v \longrightarrow [x \mapsto v]e_0\). Inversion (4) gives \(\emptyset \vdash \lambda x{:}\tau_1.\,e_0 : \sigma \to \tau\) and \(\emptyset \vdash v : \sigma\); inversion (3) gives \(\sigma = \tau_1\) and \(x{:}\tau_1 \vdash e_0 : \tau\). Lemma 6.1.15 with \(\Gamma = \emptyset\) gives \(\emptyset \vdash [x \mapsto v]e_0 : \tau\).
- E-LetV: the same argument with inversion (7) in place of (3–4).
- E-Add, E-Lt: inversion (5) gives \(\tau = \mathsf{int}\) (resp. \(\mathsf{bool}\)), and the result is an integer (resp. boolean), which has that type.
- E-IfTrue, E-IfFalse: inversion (6) gives the chosen branch type \(\tau\).
Corollary 6.1.17 (Type safety: well-typed programs cannot go wrong)
If \(\emptyset \vdash e : \tau\) and \(e \longrightarrow^{*} e'\), then \(e'\) is not stuck; moreover \(\emptyset \vdash e' : \tau\).
Proof
By induction on the number of steps \(k\). For \(k = 0\), \(e' = e\) is well typed, and by progress (Theorem 6.1.13) it is a value or steps, so it is not stuck. For \(k + 1\), \(e \longrightarrow^{*} e'' \longrightarrow e'\) with \(\emptyset \vdash e'' : \tau\) by the hypothesis; preservation (Theorem 6.1.16) gives \(\emptyset \vdash e' : \tau\), and progress again shows \(e'\) is not stuck.
Which lemma a broken rule set breaks. Progress uses canonical forms at every elimination form (application of a value, arithmetic on values, if on a value). Adding a typing rule that gives a type to a value of the "wrong" form — 0 : Bool, or succ t : Nat for t : Bool — falsifies canonical forms, and progress fails on the term that eliminates it (if 0 then … else …, succ true). Removing an evaluation rule (E-IfFalse) leaves a well-typed redex without a step: progress fails directly. Preservation uses inversion: a typing rule that forgets a premise (T-IfAny, which does not type the else branch) lets E-IfFalse produce a term of another type; an evaluation rule that produces a value of another type (pred 0 → true) fails the E-Pred case. The drill's thirteen mutations cover these four patterns; the unit tests check its enumeration against these verdicts at two size bounds.
5. Complexity¶
| Technique | Time (worst) | Time (typical) | Space | Variables |
|---|---|---|---|---|
| TypeOf (Algorithm 6.1.6) | \(\Theta(n \cdot m)\) with type trees; \(\Theta(n)\) with hash-consed types | linear | \(O(n + d)\) | \(n\) subterms, \(m\) largest type, \(d\) nesting depth |
| Checking a given derivation | \(\Theta(N \cdot m)\) | linear | \(O(N)\) | \(N\) nodes |
| Safety by enumeration (drill oracle) | \(\Theta(T_s \cdot s)\) per rule set | 0.1 s for \(s = 6\) | \(O(T_s)\) | \(T_s\) terms of size \(\le s\) |
Justification. Algorithm 6.1.6 makes one call per subterm (Theorem 6.1.11). Each call does constant work except type comparisons (application, if), which compare two type trees in \(O(m)\); building \(\tau_1 \to \tau_2\) is \(O(1)\) with shared pointers. With hash-consing (every type built once in a table, so equal types are the same pointer), comparisons are \(O(1)\) and the whole run is \(\Theta(n)\). Recursion depth is the term's height \(d\). Checking a claimed derivation compares, at each of its \(N\) nodes, the conclusion with the rule applied to the children's conclusions: one type comparison per node.
Pathological family. Let \(T_m\) be a right-nested arrow of \(m\) ints and \(f : T_m \to T_m\) in \(\Gamma\); the term \(P_k = f\,(f\,(\cdots (f\,y)))\) with \(k\) applications (\(y : T_m\)) makes \(k\) comparisons of \(T_m\) against \(T_m\), costing \(\Theta(k \cdot m)\) with tree equality but \(\Theta(k)\) with pointer equality. Production checkers intern types for exactly this reason: Clang's ASTContext uniques every type, and so does Pebble's (pebble/include/pebble/AST/ASTContext.h: "Types are uniqued ... so they compare by pointer").
Enumeration. The number of arithmetic terms of exactly \(s\) nodes grows exponentially (3, 9, 27, 108, 567, 3 159, 17 496 for \(s = 1, \dots, 7\): 3 873 terms up to size 6, 21 369 up to size 7); checking each one's steps and types is linear in its size, which is why the drill stops at size 6 and the unit tests confirm the verdicts at size 8.
Scale. Syntax-directed checking is cheap in practice: on a generated 132 002-line Pebble program (2 000 functions fn fK(a: int, b: float) -> int, each 20 rounds of s = s + a * k - (s / 3) % 7;, t = t * b + k - t / 2.0; and bump(&mut s, k);, then a for loop with an if and a call of the previous function), pebblec --emit=typed-ast, which runs name resolution, the type checker and the flow checks, takes 0.56–0.61 s against 0.42–0.44 s for --emit=ast, which only parses (reference solutions, RelWithDebInfo, this course's container, three runs each; both print a dump of about the same size). Checking adds about a third to the cost of parsing and printing: one linear pass. Proofs, by contrast, scale badly by hand: progress and preservation for a full language have hundreds of cases.
6. Variants and refinements¶
Typing judgments, inference rules and derivations¶
- Declarative vs algorithmic systems. A declarative system may contain rules that are not syntax-directed (subsumption, Lesson 6.5; generalization, Chapter 7). Its algorithm is then a different, syntax-directed system proved equivalent to it (Theorem 6.5.6 does this for subtyping). Trade-off: declarative rules are easier to understand and prove sound; algorithmic ones are easier to implement.
- Church vs Curry style. Figure 6.1.1 is Church-style: λ carries its parameter type, and types are part of the term. Curry-style λ\(x\).\(e\) has no annotation and many derivable types; finding one is inference (Chapter 7). Bidirectional typing (Lesson 6.4) lets annotations be omitted where an expected type exists.
- Elaboration. Real checkers do not only accept or reject; they produce a typed tree with implicit operations made explicit (Clang's
ImplicitCastExprin the box below, Pebble's literal typed asfloat). An elaborating judgment \(\Gamma \vdash e \rightsquigarrow e' : \tau\) carries the output term [PFPL, Ch. 23].
Type safety by progress and preservation¶
- Denotational ("cannot go wrong") soundness [Mil78]: interpret types as sets of values not containing wrong; soundness is the statement that the meaning of a well-typed term lies in its type's set. Scales poorly to mutable state; replaced in practice by the syntactic method.
- Safety with state, exceptions and control [WF94, §5–6]: preservation is stated for configurations \(\langle e, \mu \rangle\) with a store typing \(\Sigma\) that may grow; exceptions add "raise" as a legitimate normal form next to values. Pebble's traps play the role of exceptions:
trapis a defined outcome, not a stuck state. - Semantic type soundness via logical relations (RustBelt [JJKD18]): types are interpreted as predicates on values in a program logic, which admits code that the syntactic rules cannot type (library code using
unsafe) as long as it behaves well. The price is a much heavier proof. - Mechanized metatheory. The progress/preservation proof is standard fare for proof assistants; the lesson's proof is the one of [TAPL, §9.3] and is mechanized in many tutorials. The drill's enumeration is the cheap, bounded-model-checking cousin: it cannot prove safety, but it finds counterexamples fast.
7. In real compilers¶
Typing judgments, inference rules and derivations¶
Clang's semantic analysis is Algorithm 6.1.6 for C and C++: each Sema::ActOn… and Build… method checks the premises of one rule and builds the conclusion node with its type; Sema::CheckAssignmentConstraints [CLANG-SemaExpr] is the premise "the value's type can be assigned to the target's". The AST that comes out is the derivation, with every conversion made explicit. rustc's check_expr_with_expectation in compiler/rustc_hir_typeck/src/expr.rs [RUSTC-Typeck] is the same recursion for Rust (with the checking mode of Lesson 6.4).
A derivation you can print: Clang's typed AST
Reproduce (clang 23.1.2):
cat > deriv.c <<'EOF'
int twice(int (*f)(int), int x) { return f(f(x)); }
EOF
clang-23 -fsyntax-only -Xclang -ast-dump -fno-color-diagnostics deriv.c | sed -n '/FunctionDecl.*twice/,$p' | sed -E 's/ 0x[0-9a-f]+//g'
Output (complete):
`-FunctionDecl <deriv.c:1:1, col:51> col:5 twice 'int (int (*)(int), int)' external-linkage
|-ParmVarDecl <col:11, col:23> col:17 used f 'int (*)(int)'
|-ParmVarDecl <col:26, col:30> col:30 used x 'int'
`-CompoundStmt <col:33, col:51>
`-ReturnStmt <col:35, col:48>
`-CallExpr <col:42, col:48> 'int'
|-ImplicitCastExpr <col:42> 'int (*)(int)' <LValueToRValue>
| `-DeclRefExpr <col:42> 'int (*)(int)' lvalue ParmVar 'f' 'int (*)(int)'
`-CallExpr <col:44, col:47> 'int'
|-ImplicitCastExpr <col:44> 'int (*)(int)' <LValueToRValue>
| `-DeclRefExpr <col:44> 'int (*)(int)' lvalue ParmVar 'f' 'int (*)(int)'
`-ImplicitCastExpr <col:46> 'int' <LValueToRValue>
`-DeclRefExpr <col:46> 'int' lvalue ParmVar 'x' 'int'
What to notice: this is the derivation of twice's body, one node per subterm (Definition 6.1.4). Each CallExpr is a T-App node whose premises are the function ('int (*)(int)', an arrow) and the argument ('int', its domain); each DeclRefExpr is a T-Var leaf reading the parameter's type from the context. The ImplicitCastExpr <LValueToRValue> nodes are elaboration (§6): C's rules convert a variable (an l-value, Lesson 6.8) to its value before use, and Clang writes that step into the tree.
Type safety by progress and preservation¶
No production compiler proves its type system sound, but the guarantee is what makes their optimizers legal: Clang's TBAA (Chapter 19) and rustc's noalias rely on the source language's typing rules being respected. Languages differ in where they put the trapped errors (Lesson 6.2): Java's JVM re-checks bytecode with a verifier so that even hand-written class files cannot get stuck; GHC's Core is re-typechecked after every optimization pass with -dcore-lint. The one way out is an explicit escape hatch — unsafeCoerce in Haskell, unsafe in Rust, casts through void * in C — and the box shows what "going wrong" means once you take it.
Going wrong on purpose: GHC's unsafeCoerce
Reproduce (GHC 9.4.7):
mkdir -p hs && cat > hs/Wrong.hs <<'EOF'
import Unsafe.Coerce (unsafeCoerce)
main :: IO ()
main = do
print (length [1 :: Int, 2, 3])
-- A well-typed program cannot go wrong; unsafeCoerce steps outside the type system:
let f = unsafeCoerce (42 :: Int) :: Int -> Int
print (f 1)
EOF
ghc -O0 -v0 hs/Wrong.hs -o hs/wrong && ./hs/wrong; echo "exit status: $?"
cat > hs/Right.hs <<'EOF'
main :: IO ()
main = print ((42 :: Int) 1)
EOF
LC_ALL=C.UTF-8 ghc -O0 -v0 hs/Right.hs -o hs/right; echo "exit status: $?"
Output (complete; the garbage number depends on memory layout and may differ on your machine):
3
-1729382256910270464
exit status: 0
hs/Right.hs:2:15: error:
• Couldn't match expected type ‘t0 -> a0’ with actual type ‘Int’
• The function ‘42 :: Int’ is applied to one value argument,
but its type ‘Int’ has none
In the first argument of ‘print’, namely ‘((42 :: Int) 1)’
In the expression: print ((42 :: Int) 1)
|
2 | main = print ((42 :: Int) 1)
| ^^^^^^^^^^^^^
exit status: 1
What to notice: (42 :: Int) 1 is the stuck term 3 4 of Definition 6.1.8, and GHC rejects it statically — T-App's premise "the function has an arrow type" fails. unsafeCoerce claims an Int is an Int -> Int, which falsifies canonical forms (Lemma 6.1.12); the program then applies an integer as if it were a closure and prints garbage instead of getting stuck. Safety (Corollary 6.1.17) holds only for programs derived by the rules.
8. Comparison¶
| Technique | Power / precision | Speed (asymptotic · practical) | Output / error quality | Implementation effort | Typical use |
|---|---|---|---|---|---|
| Typing judgments and derivations | Defines exactly the well-typed programs; syntax-directed rules give unique types (Theorem 6.1.10) and a checking algorithm for free (Theorem 6.1.11) | \(\Theta(n)\) with interned types · negligible in compilers | A failed premise names the rule and the subterm: the natural error location | Low for syntax-directed rules; a separate algorithm for declarative ones | Every language specification and type-system paper; the structure of every checker |
| Syntactic type safety (progress + preservation) | Guarantees no stuck states for all well-typed programs (Corollary 6.1.17); scales to state and exceptions [WF94] | A proof, not an algorithm; bounded enumeration finds counterexamples in 0.1 s (drill) | Pinpoints the lemma a bad rule breaks | High by hand for real languages (hundreds of cases); routine in proof assistants | Language design (Wasm, Java/FJ, ML), validating rule changes |
Choose derivations as the definition of every type system you implement: write the rules first, check that they are syntax-directed, and let the checker follow them one rule per case. Choose the syntactic safety proof whenever you change a language's rules — even informally, walk through progress (does every elimination form have a step for every canonical value?) and preservation (does every step keep the type?) — and use bounded enumeration, as the drill does, to find counterexamples quickly.
9. Assessment¶
| Technique | Quiz ids | Drill | Flashcard tag | Exercises |
|---|---|---|---|---|
| Typing judgments and derivations | derivation-rules, derivation-invalid-node |
typing-derivation |
judgments |
E1–E6 (every rule of the checker) |
| Syntactic type safety | progress-preservation-mutations, canonical-forms-role |
progress-preservation |
safety |
— (theory; the drill checks rule sets) |
References¶
See the chapter references.