Type Checking
The parser guarantees a program is well-formed; the type checker guarantees it is
well-behaved. Multiplying a string by a function, indexing an integer as if it were an array,
calling a two-argument function with one argument — all are perfectly grammatical and utterly meaningless.
Type checking is the phase that walks the
AST, assigns
a type to every expression, and rejects the ones that do not fit together. It is the compiler's last and
best chance to catch a whole class of bugs before the program ever runs — the difference between a
red squiggle in your editor and a 3 a.m. production crash.
A type system is a tractable, syntactic method for proving the absence of certain program
behaviours by classifying values into types. The checker consults the
symbol table
for the types of names, then propagates types up the tree — a textbook synthesized attribute in
attribute-grammar
terms: each node's type is computed from its children's.
Type expressions
Types themselves have structure — they are little trees, called type expressions. A base
type (int, bool, char) is a leaf; constructors build compound types
from smaller ones:
- arrays: \texttt{array}(n, \tau) — n elements of type \tau;
- products: \tau_1 \times \tau_2 — a record or tuple;
- functions: \tau_1 \to \tau_2 — argument type to result type;
- pointers: \texttt{pointer}(\tau).
Type checking then reduces to two operations: computing the type expression of each construct, and asking
whether two type expressions are equivalent. That second question is subtler than it looks.
Two notions of "the same type"
When are two types equal? There are two answers, and languages genuinely disagree.
-
Structural equivalence: two type expressions are equal iff they have the same
shape — the same constructor applied to equivalent parts, recursively. Under structural equivalence a
Point = { x: int, y: int } and a Pair = { x: int, y: int } are the
same type. TypeScript, Go's structural interfaces, and OCaml objects work this way.
-
Name equivalence: two types are equal iff they came from the same declared name.
Under name equivalence
Point and Pair are different types even though
their fields match — a value of one cannot be passed where the other is expected. C's struct
tags, Ada, Haskell's newtype, and Java classes are name-equivalent.
Neither is "right"; they trade convenience against safety. Structural equivalence is flexible — anything
with the right shape fits. Name equivalence is protective — it lets you declare Metres and
Seconds that are both double underneath yet refuse to be added, catching unit
errors the structural checker would wave straight through.
The rules as inference judgments
Type systems are specified with typing judgments of the form
\Gamma \vdash e : \tau, read "under the type environment
\Gamma (the symbol table), expression e has type
\tau." Each language construct gets an inference rule: premises
above the line, conclusion below. To type-check is to build this derivation bottom-up, matching each AST
node to its rule. A variable takes its type from the environment:
\frac{x : \tau \;\in\; \Gamma}{\Gamma \vdash x : \tau}\quad(\textsc{Var})
Addition demands two integer operands and yields an integer; the comparison operators demand matching
operands and yield a boolean:
\frac{\Gamma \vdash e_1 : \texttt{int} \quad \Gamma \vdash e_2 : \texttt{int}}{\Gamma \vdash e_1 + e_2 : \texttt{int}}\;(\textsc{Add}) \qquad \frac{\Gamma \vdash e_1 : \tau \quad \Gamma \vdash e_2 : \tau}{\Gamma \vdash e_1 \lt e_2 : \texttt{bool}}\;(\textsc{Lt})
Statements have judgments too. An assignment requires the value's type to match the variable's; a
conditional requires a boolean guard; a function call requires each argument to match the corresponding
parameter type, and gives back the declared return type:
\frac{\Gamma \vdash f : \tau_1 \to \tau_2 \quad \Gamma \vdash e : \tau_1}{\Gamma \vdash f(e) : \tau_2}\;(\textsc{App}) \qquad \frac{\Gamma \vdash a : \texttt{array}(n,\tau) \quad \Gamma \vdash i : \texttt{int}}{\Gamma \vdash a[i] : \tau}\;(\textsc{Index})
Read (App) aloud: "if f is a function from
\tau_1 to \tau_2, and the argument
e has type \tau_1, then the call has type
\tau_2." Every checker in the world is these rules, walked over an AST.
Types flowing up a typed AST
Because the type of a node is synthesized from its children, checking (a + b) \lt c
— with a, b, c : \texttt{int} — is a post-order walk that decorates each node
with its type and applies the matching rule. Watch the leaves resolve from the environment, the
+ demand two ints and yield int, and the
\lt yield the final bool.
If any premise failed — say c were a string — the
\lt rule would find its two operands of different types and the checker would
report a type error at that node, pinpointing exactly where the mismatch lives.
Coercions: when the checker inserts a conversion
Strict rules would reject 3 + 4.0 — an int added to a
float. Most languages instead permit an implicit coercion (a widening
conversion): the checker notices the mismatch, confirms it is a safe promotion
(\texttt{int} \to \texttt{float} loses no information), and inserts a conversion
node so both operands share a type. Formally this is a subtyping/coercion rule that says "an
int may be used where a float is wanted." The key discipline: the compiler makes
the conversion explicit in the tree, so later phases see a homogeneous, well-typed expression, and
coercions only ever widen — a narrowing \texttt{float} \to \texttt{int}
must be requested by the programmer, because it can silently lose data.
// A recursive type-checker for a tiny expression language. Types: "int" | "bool".
type Type = "int" | "bool";
type Expr =
| { kind: "num"; value: number }
| { kind: "bool"; value: boolean }
| { kind: "var"; name: string }
| { kind: "add"; left: Expr; right: Expr } // int × int → int
| { kind: "lt"; left: Expr; right: Expr } // τ × τ → bool
| { kind: "if"; cond: Expr; then: Expr; else_: Expr };
// Γ, the type environment (the symbol table).
type Env = Record<string, Type>;
function typeOf(e: Expr, gamma: Env): Type {
switch (e.kind) {
case "num": return "int";
case "bool": return "bool";
case "var": {
const t = gamma[e.name];
if (!t) throw new Error(`unbound variable '${e.name}'`);
return t; // (Var): look it up in Γ
}
case "add": { // (Add): both must be int
const l = typeOf(e.left, gamma), r = typeOf(e.right, gamma);
if (l !== "int" || r !== "int")
throw new Error(`'+' needs int + int, got ${l} + ${r}`);
return "int";
}
case "lt": { // (Lt): operands must match, result bool
const l = typeOf(e.left, gamma), r = typeOf(e.right, gamma);
if (l !== r) throw new Error(`'<' needs matching operands, got ${l} < ${r}`);
return "bool";
}
case "if": { // guard must be bool; branches must agree
if (typeOf(e.cond, gamma) !== "bool") throw new Error("if-guard must be bool");
const t = typeOf(e.then, gamma), f = typeOf(e.else_, gamma);
if (t !== f) throw new Error(`if-branches disagree: ${t} vs ${f}`);
return t;
}
}
}
const gamma: Env = { a: "int", b: "int", c: "int", flag: "bool" };
// Well typed: (a + b) < c -> bool
const ok: Expr = { kind: "lt",
left: { kind: "add", left: { kind: "var", name: "a" }, right: { kind: "var", name: "b" } },
right: { kind: "var", name: "c" } };
console.log("(a + b) < c :", typeOf(ok, gamma));
// Ill typed: a + flag -> reported error
const bad: Expr = { kind: "add",
left: { kind: "var", name: "a" }, right: { kind: "var", name: "flag" } };
try { typeOf(bad, gamma); } catch (err) { console.log("caught:", (err as Error).message); }
The first expression checks to bool; the second is caught with a precise message. That is the
entire shape of a type checker: one recursive function, one case per rule, the environment
threaded through — exactly the inference rules above, turned into code.
Not for free. A type system can only approximate the set of programs that will not go wrong — the
exact set is undecidable. So every checker makes a choice about which side to err on. Reject too little and
bugs slip through to run time (weak typing); reject too much and you turn away perfectly safe programs,
forcing casts and boilerplate (an over-strict system). The art is picking rules that are sound
(they never accept a program that will commit the forbidden error) while staying expressive enough that
real code type-checks without a fight. Sound, decidable, and expressive — you get to pick where on that
triangle to sit, and every language's "feel" is largely that choice.
The first trap is assuming everyone means the same thing by "same type." Two records with identical fields
are the same type under structural equivalence and different types under name equivalence —
so a program that type-checks in TypeScript may be rejected in C or Ada, and vice versa. When you read or
write a type checker, pin down which equivalence it uses before you reason about it; the two give
opposite answers on the same code.
The second trap is implicit coercion. Silent conversions are convenient until they are
catastrophic: an \texttt{int} \to \texttt{float} widening is harmless, but a
\texttt{float} \to \texttt{int} narrowing quietly truncates, and chains of
automatic promotions can turn a comparison into something you never wrote. The rule to hold onto: automatic
coercions should only ever widen (lose no information), and any conversion that can lose data must
be spelled out by the programmer. When a language breaks that rule "for convenience," it manufactures a
rich supply of bugs the type checker was supposed to prevent.