Type Checking and Type Judgments

A typing judgment is a formal statement of the shape

read "in context $\Gamma$, the expression $e$ has type $T$." Here $\Gamma$ (capital gamma) is the typing context (also called a type environment): a finite sequence or set of bindings $x_1 : T_1, x_2 : T_2, \ldots, x_n : T_n$ recording the assumed type of every free variable currently in scope. The judgment is not code that runs — it is a claim, and the type checker's job is to decide whether that claim is provable. Judgments are proved using typing rules, written as inference rules in the standard logical style:

Each rule says: if you already have derivations of the premises (judgments above the line), you may conclude the judgment below the line. A rule with no premises is called an axiom. For example, in a simple typed language with booleans, integers, variables, and functions, typical rules include:

The notation $\Gamma, x : T_1$ means "$\Gamma$ extended with the new binding $x : T_1$"; this is how contexts grow when a rule descends into the body of a binder like a lambda. Crucially, each rule's premises mention strictly smaller subexpressions than its conclusion — this is what makes the rules syntax-directed: for any expression form, at most one rule's conclusion pattern matches, so checking proceeds by structural recursion on the abstract syntax tree with no guessing. A full proof that $\Gamma \vdash e : T$ holds is a tree — a derivation tree or type derivation — whose leaves are axioms and whose internal steps apply rules to already-derived judgments. Type checking is the algorithmic search for such a tree; type checking succeeds exactly when the tree exists, and the checker either constructs it (implicitly, via recursive calls) or reports precisely where no rule applies. This connects tightly to What Is a Type System? as the formal skeleton behind the informal notion of "a system of typing rules," and it explains why type checking behaves differently from the value computation studied under Static vs Dynamic Typing — it reasons about types alone, never running the program.

Concretely, a type checker is a recursive function `typeOf(Γ, e)` that either returns the unique type $T$ such that $\Gamma \vdash e : T$, or signals failure. Because the rules are syntax-directed, the function dispatches on the shape of `e`, mirrors each rule literally, and recurses on subexpressions — exactly like a recursive-descent evaluator, except it manipulates types instead of values. There are two closely related tasks that people sometimes conflate:

• Type checking (bidirectional "checking" mode): given `Γ`, `e`, and a candidate type `T`, decide whether `Γ ⊢ e : T`.
• Type synthesis / inference (the "synthesizing" mode used below): given `Γ` and `e`, compute the unique `T` with `Γ ⊢ e : T`, or fail.

For the simply-typed core shown above (with explicit lambda annotations), synthesis is fully determined — every construct has exactly one applicable rule, and it either produces a type or fails. This is the design goal: no backtracking, no search over rules — the syntax of `e` alone selects the rule. ```

# typeOf(Γ, e): compute the type of e under context Γ, or raise TypeError function typeOf(Γ, e): match e: case True: return Bool # (T-True) case False: return Bool # (T-True variant) case IntLit(n): return Int # (T-Int) case Var(x): if x in dom(Γ): # (T-Var) return Γ[x] else: raise TypeError("unbound variable " + x) case Lambda(x, T1, body): Γ' = Γ.extend(x, T1) # Γ, x:T1 T2 = typeOf(Γ', body) # (T-Abs) return Arrow(T1, T2) case App(e1, e2): Tf = typeOf(Γ, e1) # (T-App) Ta = typeOf(Γ, e2) if Tf is Arrow(T1, T2) and T1 == Ta: return T2 else: raise TypeError("bad application: expected " + Tf.domain + " got " + Ta) case If(e1, e2, e3): T1 = typeOf(Γ, e1) # (T-If) if T1 != Bool: raise TypeError("condition not Bool") T2 = typeOf(Γ, e2) T3 = typeOf(Γ, e3) if T2 != T3: raise TypeError("branches disagree: " + T2 + " vs " + T3) return T2 default: raise TypeError("unknown expression form") ``` Each `case` in `typeOf` is a direct transcription of one inference rule: the recursive calls are the premises, the returned type (or the equality checks that must hold first) is the conclusion. Function `dom(Γ)` returns the set of variables bound in `Γ`, and `Γ.extend(x, T1)` returns a new context with `x : T1` prepended — the standard implementation is a list (a "cons" structure), so lookup and extension are both $O(1)$ to perform, with lookup taking $O(|\Gamma|)$ time to scan. The rule (T-Var) deserves special note: it is the only rule that reads from $\Gamma$, and it is what makes the context necessary at all. Without a running record of bound variables' types, the checker would have no way to assign a type to `x` once it appears freely inside a lambda body.

Growing the context. The only place $\Gamma$ changes is inside `T-Abs`: entering the body of `λx:T1. e` requires assuming `x : T1`, so the recursive call uses `Γ' = Γ, x:T1`, not `Γ`. When that recursive call returns (or the checker "pops back out" of the lambda), the extension is discarded — bindings are scoped exactly like variable scope in the source language. This context discipline is why shadowing works correctly: if `x` is already bound in `Γ`, extending it with a fresh `x:T1` simply makes the new binding the one found by the nearest lookup, matching lexical scoping.

Error reporting. A production checker does not just say "TypeError" — it reports the expected type, the found type, and the source location, because the whole point of static typing is to give the programmer actionable feedback before running anything.

Time complexity. For a language without subtyping or polymorphism (like the fragment above), `typeOf` visits every AST node exactly once, doing $O(1)$ work per node aside from context lookup and type equality checks:

• Context lookup, `T-Var`, costs $O(d)$ where $d$ is the nesting depth (number of enclosing binders) — bounded by the size of the program, so $O(n)$ in the worst case per lookup with a naive list-based context.
• Type equality checks (`T1 == Ta`, `T2 == T3`) compare two type expressions structurally; for simple types this is $O(s)$ where $s$ is the size of the type (linear-size types make this effectively $O(1)$ in practice, but pathological type-level constructs, e.g. large records or recursive type synonyms, can make this more expensive).

Summing over all $n$ AST nodes gives overall time

in the naive implementation, where $d_{\max}$ is the maximum variable-lookup depth. In practice, this is reduced to amortized $O(n)$ by implementing contexts as hash maps (symbol tables) rather than lists, making `T-Var` lookup $O(1)$ expected time; this is exactly what real compilers do. So: type checking a simply-typed program is linear in program size, matching the intuition that it should cost about as much as one more traversal of the AST — comparable to a parsing or scope-resolution pass.

Space complexity. The context $\Gamma$ at any point has size proportional to the current nesting depth, so it needs $O(d_{\max})$ space on the call stack at the deepest point of recursion; total space (including the AST itself) is $O(n)$.

Why this terminates. The recursion in `typeOf` always calls itself on a strictly smaller subexpression (a child in the AST), and the AST is finite, so by well-founded induction on expression size the recursion always terminates — there is no risk of infinite loops, unlike general program execution. This is a key structural difference from evaluating the program (which may loop forever); type checking a terminating-or-not program is guaranteed to itself terminate, given a decidable base type-equality check.

Why this is correct (soundness of the checker relative to the rules). "Correctness" here means: `typeOf(Γ, e)` returns `T` if and only if the judgment $\Gamma \vdash e : T$ has a derivation using the inference rules. This is proved by structural induction on `e`:

• Base cases (`True`, `False`, `IntLit`, `Var`): the function's behavior is a direct transcription of the corresponding axiom or lookup rule; it returns `T` exactly when that rule's conclusion is derivable.
• Inductive cases (`Lambda`, `App`, `If`): by the induction hypothesis, the recursive calls correctly compute the types of the (strictly smaller) subexpressions if and only if those subjudgments are derivable. The function then checks exactly the side conditions the corresponding rule demands (matching argument types, matching branch types, `Bool` condition) before assembling the conclusion — so the top-level call succeeds if and only if all premises of the relevant rule are derivable, which by definition of a derivation tree is if and only if the whole judgment is derivable.

Because each syntax form maps to exactly one rule (the rules' conclusions have disjoint syntactic shapes), the algorithm never needs to guess or backtrack: this determinism is what makes type synthesis in this fragment a total, decidable function rather than an approximate search. This same argument — that a syntax-directed algorithm faithfully mirrors a set of inference rules — is exactly the technique later used to establish Type Safety and Soundness for richer calculi such as The Simply-Typed Lambda Calculus, where the added theorems (progress and preservation) build on precisely this notion of a derivable judgment.

Honest tradeoffs. This clean picture depends on annotated binders (`λx:T1. e` states `T1` explicitly). Once a language drops annotations and expects type inference (e.g., Hindley–Milner-style `let`-polymorphism), the checker must solve unification constraints rather than merely dispatch syntactically, and complexity results become subtler (Hindley–Milner inference is efficient in practice but has been shown exponential in adversarial cases due to let-polymorphism's interaction with sharing). Adding subtyping breaks the "exactly one applicable rule" property and typically requires an explicit subsumption rule plus a separate subtype-checking algorithm, trading simplicity for expressiveness.

Take the language above and check the expression

starting from the empty context $\Gamma_0 = \varnothing$. We trace `typeOf(∅, e)` call by call.

The final answer is

This matches the derivation tree drawn above, read bottom-to-top as "what must already be true" and top-to-bottom as "what the checker returns as it unwinds the recursion."

A second trace, showing a rejection. Now check $e' = \lambda x{:}\texttt{Bool}.\ \texttt{if}\ x\ \texttt{then}\ 3\ \texttt{else}\ \texttt{false}$. 1. `typeOf(∅, e')` invokes T-Abs, recursing into `typeOf({x:Bool}, if x then 3 else false)`. 2. T-If needs `x : Bool` (✓, via T-Var), then `typeOf({x:Bool}, 3) = Int` and `typeOf({x:Bool}, false) = Bool`. 3. T-If's side condition demands $T_2 = T_3$, but `Int ≠ Bool`. 4. `typeOf` raises `TypeError("branches disagree: Int vs Bool")`, and no derivation tree exists for the top-level judgment — the checker correctly reports the program as ill-typed, without ever attempting to execute the branches. This second trace is the important asymmetric case: it shows the checker actively refuting a judgment, not merely confirming an easy well-typed program, and it demonstrates exactly which rule and which side condition fails — the information a real diagnostic message would surface.

The specific $\Gamma \vdash e : T$ notation and the systematic "inference rule" presentation used throughout modern compiler courses and papers was popularized through the natural-deduction style of proof theory (Gentzen) applied to typing by later logicians and language designers, and it became the standard teaching and specification vehicle for programming-language type systems in the late twentieth century — the same style used to state the progress and preservation theorems central to Type Safety and Soundness.

Every statically typed production compiler runs some descendant of the `typeOf` algorithm above. javac and rustc perform syntax-directed type checking (extended with generics, subtyping, and trait/overload resolution) as a dedicated compiler phase before code generation, catching mismatched arguments and incompatible branches exactly as in the worked example. The TypeScript compiler (tsc) layers a structural type checker over JavaScript's untyped runtime, using contexts to track variable types across nested closures and reporting the precise rule and location that fails, mirroring the diagnostic style shown above. GHC (Haskell) implements a far richer version of this framework — Hindley–Milner inference with type classes — where the context $\Gamma$ also carries class constraints, but the core judgment-and-derivation skeleton is unchanged. Proof assistants such as Coq and Agda take the idea to its logical endpoint: via the Curry–Howard correspondence, a typing derivation is a mathematical proof, so their type checkers double as proof checkers. Finally, IDE tooling (autocomplete, "type at cursor," inline error squiggles) is typically the type checker's `typeOf` function invoked interactively on partial or edited ASTs, which is why understanding the recursive, context-threading structure described here explains both compiler errors and everyday editor feedback.

Ask the tutor: Can you show how this typing-rule framework needs to change once we add a `let`-binding with polymorphism, as in Hindley–Milner type inference?