Type Checking in Compilers

A type system is a collection of rules that assigns types — labels like `int`, `bool`, `string`, or `int → int` — to program expressions, and that rejects programs where these labels would be combined inconsistently. Formally, a typing rule is usually written as a judgment ``` Γ ⊢ e : τ ``` read "under type environment Γ, expression `e` has type `τ`." The environment Γ is exactly the information a symbol table provides: a mapping from identifiers to their declared types (and, for functions, their parameter and return types). Typing rules are given in inference rule form, with premises above a line and a conclusion below: ``` Γ ⊢ e1 : int Γ ⊢ e2 : int ───────────────────────────── (T-Add) Γ ⊢ e1 + e2 : int ``` This rule says: if `e1` and `e2` can both be shown to have type `int` under Γ, then `e1 + e2` has type `int` under Γ. A type checker is an algorithm that mechanically applies rules like this to derive (or fail to derive) a judgment for the root of the AST. There are two closely related but distinct tasks that go by the name "type checking":

• Type checking proper: every expression is annotated with an expected type (as in explicitly-typed languages like Java or C), and the algorithm merely verifies consistency — a pure checking judgment `Γ ⊢ e ⇐ τ`.
• Type inference: types are not all given, and the algorithm must reconstruct them — a synthesis judgment `Γ ⊢ e ⇒ τ`, as in ML or Haskell, where `let x = 3 in x + 1` has no explicit annotation on `x` at all.

Most real compilers use a bidirectional mix: literals, operators, and calls to explicitly-declared functions synthesize their type upward from their subexpressions, while contexts with an expected type (e.g., a function body against its declared return type, or an `if`-branch against its sibling) check an expression against that expectation. This hybrid keeps the algorithm simple, syntax-directed (one rule per AST node shape), and — critically — decidable and efficient, unlike unrestricted inference for very expressive type systems. The other essential concept is type equivalence: the rule for when two type expressions denote "the same" type. Two common disciplines are structural equivalence (two record types are equal if their field names and types match, regardless of name) and nominal equivalence (two types are equal only if they were declared with the same name, as in Java classes). This choice is a design decision baked into the type checker's equality-testing subroutine, and it changes which programs are accepted.

The type checker is driven by the abstract syntax tree and the symbol table, both already built by earlier phases. Concretely: 1. Scope resolution has already run. Every identifier reference in the AST is linked (or linkable, via scoped lookup) to the declaration that introduces it, and each declaration node carries a declared or inferred type slot. 2. The checker walks the AST, most commonly in a single post-order (bottom-up) traversal for synthesis, augmented with an "expected type" parameter passed downward for checking contexts. 3. At each node, the checker looks up exactly one typing rule matching that node's syntactic shape (this is what makes the algorithm syntax-directed — no search over which rule to apply). 4. Every rule either succeeds, producing a type for the node (and possibly writing it into a decoration slot on the node), or fails, in which case a type error is reported, typically along with a recovery type (often a distinguished `error` type) so checking can continue and report multiple errors in one pass rather than stopping at the first. 5. Declarations update the symbol table as they are traversed (for languages with sequential, C-like scoping) or are pre-registered in a first pass (for languages with mutually recursive top-level declarations, like most functional languages, which need a pre-pass to collect all top-level signatures before checking any body). The heart of the algorithm is a big `case` dispatch, one arm per AST node kind. Here is a checker for a small imperative expression/statement language with integers, booleans, variables, functions, and arrays — enough to expose all the interesting cases (arithmetic, comparisons, function calls, assignment, arrays, and control flow). ```pseudocode // Types are one of: INT, BOOL, ARRAY(T), FUNC(paramTypes, returnType), ERROR function typeOf(node, env): // env: symbol table / type environment (Γ) switch node.kind: case IntLiteral: return INT case BoolLiteral: return BOOL case Identifier(name): entry = env.lookup(name) // uses scope-resolution linkage if entry == NOT_FOUND: report("undeclared identifier: " + name, node) return ERROR return entry.type case BinOp(op, left, right): tL = typeOf(left, env) tR = typeOf(right, env) if tL == ERROR or tR == ERROR: return ERROR // fault already reported downstream expected = signatureOf(op) // e.g. (+): INT×INT→INT, (<): INT×INT→BOOL if tL == expected.leftType and tR == expected.rightType: return expected.resultType report("operator " + op + " expects " + expected.leftType + ", " + expected.rightType + " but got " + tL + ", " + tR, node) return ERROR case ArrayIndex(base, index): tBase = typeOf(base, env) tIndex = typeOf(index, env) if tIndex != INT: report("array index must be INT, got " + tIndex, node) if tBase is ARRAY(elemType): return elemType if tBase != ERROR: report("indexing into non-array type " + tBase, node) return ERROR case Call(fname, args): entry = env.lookup(fname) if entry == NOT_FOUND or not (entry.type is FUNC(params, ret)): report(fname + " is not a callable function", node) return ERROR (params, ret) = entry.type if length(args) != length(params): report("arity mismatch calling " + fname, node) return ERROR for i in 0 .. length(args)-1: tArg = typeOf(args[i], env) if tArg != params[i] and tArg != ERROR: report("argument " + i + " of " + fname + " expects " + params[i] + " got " + tArg, node) return ret case Assign(target, value): tTarget = typeOf(target, env) // must be an lvalue: Identifier or ArrayIndex tValue = typeOf(value, env) if tTarget != ERROR and tValue != ERROR and tTarget != tValue: report("cannot assign " + tValue + " to " + tTarget, node) return VOID case If(cond, thenBranch, elseBranch): tCond = typeOf(cond, env) if tCond != BOOL and tCond != ERROR: report("if-condition must be BOOL, got " + tCond, node) checkStmt(thenBranch, env) checkStmt(elseBranch, env) return VOID case FuncDecl(name, params, retType, body): innerEnv = env.newChildScope() for p in params: innerEnv.declare(p.name, p.type) innerEnv.declare("__return__", retType) // used to check return stmts checkStmt(body, innerEnv) return FUNC(typesOf(params), retType) case Return(expr): tExpr = typeOf(expr, env) tExpected = env.lookup("__return__").type if tExpr != tExpected and tExpr != ERROR: report("return type mismatch: expected " + tExpected + " got " + tExpr, node) return VOID default: error("unhandled AST node kind: " + node.kind) ``` Two structural points deserve emphasis. First, the traversal for a value-producing node like `BinOp` synthesizes upward: it computes children's types first, then derives the parent's type — this is the post-order, "type-of" style. Second, a statement node like `If` uses a sibling helper `checkStmt` that has no return type of interest (statements aren't expressions) but still must recursively verify its substructure — this is why real checkers usually split `typeOf` (synthesis for expressions) from `checkStmt` (verification for statements), even though both share the same environment-threading discipline. The error-recovery discipline — propagating a special `ERROR` type instead of aborting — is what lets a single compilation pass report many independent type errors instead of stopping at the first one, and it is essential for usable error messages: without it, one bad variable reference could cascade into dozens of spurious secondary errors.

Time complexity. For a syntax-directed checker with no unification (i.e., every node's type is either explicitly annotated or derivable purely from its children — the setting of the pseudocode above), the algorithm visits each AST node exactly once and does O(1) work per node beyond symbol table access. If the symbol table supports O(1) expected-amortized lookup (hash map) or O(log n) worst-case (balanced tree keyed per scope), the whole checker runs in ``` O(n) expected/amortized, n = number of AST nodes O(n log n) worst case with balanced-tree symbol tables ``` This is a direct consequence of the traversal structure: `typeOf` and `checkStmt` recurse exactly once per child, so the recursion tree has the same size as the AST, and each call does a bounded amount of local work (a signature lookup, an arity check, an equality test between two already-computed type representations). Type equality itself must be examined carefully: for simple base types it is O(1), but for structural equivalence of recursive types (records containing records, or recursive algebraic data types) it requires care to avoid infinite loops on cyclic type definitions — standard fixes are memoized equality checks or comparing against a "seen pairs" set, keeping it linear in the size of the types being compared rather than the whole program.

Type inference is a different story. Full Hindley–Milner-style inference (as in ML, Haskell, OCaml) does not require every subexpression to be annotated; it generates type constraints and solves them via unification with a substitution. Algorithm W runs in low-degree polynomial time on almost all real programs, but the classic result (Kanellakis, Mairson, Mitchell, 1991) is that let-polymorphic type inference is EXPTIME-complete in the worst case — nested `let`-bindings can force exponential blow-up in the size of the most general (principal) type. This worst case essentially never arises in hand-written code, which is why ML-family compilers feel fast in practice; but it is the honest theoretical complexity, and it is the reason some compilers cap generalization depth or add annotations to bound blow-up in generated code.

Correctness. The relevant correctness property for a type system is usually stated as type soundness, decomposed (following the standard Wright–Felleisen approach) into two lemmas about the language's small-step operational semantics `e → e'`:

• Progress: if `∅ ⊢ e : τ` (e is well-typed in the empty environment) then either `e` is a value, or there exists `e'` such that `e → e'`. Informally: a well-typed program is never stuck — it never reaches a state where no rule applies to a non-value (this rules out exactly the "add a string to a number at runtime" failure).
• Preservation (a.k.a. subject reduction): if `Γ ⊢ e : τ` and `e → e'`, then `Γ ⊢ e' : τ`. Informally: evaluation never changes an expression's type.

Together, progress and preservation give, by induction on the length of an evaluation sequence, the informal slogan "well-typed programs don't go wrong": starting from a well-typed term, every step either produces a value or another well-typed term, so the program can never get stuck in an ill-defined state (like trying to call a non-function or index a non-array). This is a genuine mathematical theorem for a given formal type system and operational semantics — it is proved once, by the language designer, by structural induction over the typing derivation and case analysis on the last rule used; the type checker's job is simply to mechanically decide the premise `Γ ⊢ e : τ` for a candidate program, so that the soundness theorem's guarantee actually applies to it. It is worth being honest about the limits: soundness says nothing about whether the program is correct with respect to its intended behavior — only that it will not crash with a type error at runtime. A well-typed program can still divide by zero, index out of bounds (if the type system doesn't track array lengths), or loop forever. Type checking is a discipline that eliminates one specific, large class of runtime failures, not a full correctness proof of program behavior.

Consider this small program in the language handled by the pseudocode checker above: ``` func f(n: INT) -> INT { return n + 1 } func main() -> INT { x: INT = 3 y: ARRAY(INT) = [10, 20, 30] return x + f(y[0]) } ``` Assume scope resolution has already produced a global symbol table with `f : FUNC([INT], INT)`, and that entering `main`'s body creates a child scope with `x : INT`, `y : ARRAY(INT)`, and `__return__ : INT`.

Every node resolves cleanly: the checker accepts the program, and the decorated AST now carries a type at every node, ready for a code generator that, e.g., selects an integer-add instruction directly at step 10 without emitting any runtime type dispatch. Now perturb the program to introduce two independent errors, to see the error-recovery discipline in action: ``` func main() -> INT { x: INT = 3 y: BOOL = true return x + f(y) // (1) f expects INT, got BOOL } // (2) '+' between INT and whatever f(y) is ``` Tracing: at the `Call` node, `f`'s param type is INT but the argument `y` has type BOOL — this arity is fine (1 vs 1) but the type mismatch is reported, and per the pseudocode, the call still returns its declared return type `INT` (not `ERROR`) because the call itself is well-formed even though one argument was wrong — a design choice that avoids also flagging the outer `+` as broken due to a propagated `ERROR`. The `BinOp(+)` node then sees `x : INT` and `f(y) : INT` and passes cleanly. The compiler reports exactly one diagnostic — "argument 0 of f expects INT got BOOL" — rather than cascading into a second, redundant complaint about `+`. This single design decision (return the declared type from a call even when an argument was ill-typed, rather than `ERROR`) is precisely what keeps error messages focused instead of an avalanche of noise.

Robin Milner's work on the ML language in the 1970s produced the type discipline — let-polymorphism plus principal-type inference — that made it possible to write untyped-looking code that is nonetheless fully and automatically type-checked, without sacrificing soundness. His 1978 paper "A Theory of Type Polymorphism in Programming" gave the algorithm now called Algorithm W, and the associated soundness result is often summarized by his own aphorism: "well-typed programs cannot 'go wrong.'" This framing — type safety as a theorem about a formal semantics, not a folk claim — set the standard for how every subsequent type system, from Java generics to Rust's borrow-and-type checker, is expected to be justified.

Every mainstream compiler for a statically typed language — GCC and Clang for C/C++, javac for Java, rustc for Rust, the OCaml and Haskell (GHC) compilers, TypeScript's `tsc` — implements a type-checking pass structured almost exactly as described here: an AST (or a lightly desugared version of it) walked with a symbol-table-backed environment, producing either a decorated tree or diagnostics. TypeScript is a particularly visible industrial case: it type-checks a superset of JavaScript without changing runtime semantics at all, purely to catch bugs before deployment, and its checker is a bidirectional synthesize/check algorithm operating over a structural type system with the specific complications of unions, intersections, and generics. Type checking is also the load-bearing wall behind performance: a JIT compiler or an ahead-of-time optimizer can eliminate runtime tag checks, dynamic dispatch, and boxing exactly to the extent that static types guarantee the relevant invariants — this is why moving from a dynamically typed language (Python, JavaScript) to a statically typed one (or adding gradual typing, as in TypeScript, mypy, or Julia's type inference) is a standard lever for both correctness and speed in large systems. Beyond conventional compilers, type checking underlies proof assistants (Coq, Agda, Lean), where "type checking the proof term" is verifying the mathematical proof, via the Curry–Howard correspondence between types and propositions — the same core algorithm from this article, applied to a language expressive enough to encode logic itself. It is also the reason a decorated AST is a prerequisite for generating a reliable Intermediate Representation: IR generation can assume every operation is well-typed and skip inserting runtime type guards that a dynamically typed target would require.

Ask the tutor: How would this type-checking algorithm change to support parametric polymorphism (generics), and why does that push the complexity story toward unification-based inference?