The Simply-Typed Lambda Calculus

The untyped lambda calculus has three term forms: variables $x$, abstractions $\lambda x. t$, and applications $t_1\, t_2$. Nothing stops you from writing $x\,x$ or applying a variable to itself, so evaluation can either succeed, or get stuck (e.g. trying to apply a non-function), or loop forever. The Simply-Typed Lambda Calculus restricts the syntax with a type system: every abstraction is annotated with the type of its argument, $\lambda x{:}\tau_1.\ t$, and every term is assigned a type by a set of inference rules. A term "type-checks" only if every subterm's type matches how it is used — in particular, only functions of type $\tau_1\to\tau_2$ may be applied to arguments of type $\tau_1$. Types in STLC are built from a set of base types (e.g. $\mathrm{Bool}$, or an uninterpreted atom $\iota$) and the function type constructor $\to$, which is right-associative: $\tau_1 \to \tau_2 \to \tau_3$ means $\tau_1 \to (\tau_2 \to \tau_3)$. A typing context (or environment) $\Gamma$ is a finite partial function from variables to types, written as a list $x_1{:}\tau_1, \dots, x_n{:}\tau_n$. A typing judgment $\Gamma \vdash t : \tau$ asserts that, assuming the free variables of $t$ have the types recorded in $\Gamma$, the term $t$ has type $\tau$. This is exactly the Type Checking and Type Judgments machinery, specialized to a language with only functions. The system is syntax-directed: each term constructor (variable, abstraction, application) has exactly one typing rule whose conclusion has that shape, so a derivation tree mirrors the term's parse tree. This is what makes type checking mechanical rather than a search problem — a crucial difference from full Type Inference and Hindley-Milner systems, where types are not fully annotated and the checker must guess them.

Syntax. Terms and types are given by the grammars

A value is an abstraction $\lambda x{:}\tau.\ t$ — evaluation stops there; it is already "finished data" in this pure calculus. Reduction is the usual beta reduction (see Beta Reduction), with the standard call-by-value or call-by-name strategy:

together with congruence rules that let reduction happen inside subterms (e.g. reduce the function before the argument, then reduce the argument). Substitution $[x \mapsto s]t$ is capture-avoiding, exactly as in the untyped calculus.

Typing rules. Three rules, one per constructor, given as natural-deduction-style inference rules:

Read bottom-up, T-App says: to apply $t_1$ to $t_2$, the function's domain type must exactly match the argument's type; the result has the function's codomain type. There is no rule that lets you apply an $\iota$ to anything — this is precisely the syntactic restriction that rules out `x x`.

Type checking as an algorithm. Because the rules are syntax-directed and every abstraction carries its argument type, type checking reduces to one recursive function with no guessing or backtracking: ``` function typeOf(Γ, t): match t: case Variable(x): if x in Γ: return Γ[x] else: error "unbound variable x" case Abs(x, τ1, body): Γ' = Γ extended with x : τ1 τ2 = typeOf(Γ', body) return Arrow(τ1, τ2) case App(t1, t2): τ1 = typeOf(Γ, t1) τ2 = typeOf(Γ, t2) match τ1: case Arrow(σ1, σ2): if τ2 == σ1: return σ2 else: error "argument type mismatch: expected σ1, got τ2" case _: error "applying a non-function of type τ1" ``` `typeOf` walks the term once, threading the context $\Gamma$ downward (extended only at abstractions) and returning a type upward at every node; equality of types (`τ2 == σ1`) is plain structural equality on the type grammar, itself computable by a trivial recursive comparison. The figure below shows the derivation tree for the identity-composition term $\lambda f{:}\iota\to\iota.\ \lambda x{:}\iota.\ f\ (f\ x)$, matched against the recursive calls of `typeOf`.

Reading the tree bottom-up mirrors exactly the recursive descent of `typeOf`: leaves are `T-Var` lookups, each `App` node combines two recursively-computed types via `T-App`, and each `Abs` node extends $\Gamma$, recurses, then wraps the result in an arrow via `T-Abs`. The final judgment at the root, $\emptyset \vdash \lambda f{:}\iota\to\iota.\ \lambda x{:}\iota.\ f\,(f\,x) : (\iota\to\iota)\to(\iota\to\iota)$, is the type of "apply $f$ twice" — a two-argument-free closed term whose type alone tells you its shape.

Time and space complexity of type checking. `typeOf` visits each node of the term's abstract syntax tree exactly once, doing constant work at variables and applications (a context lookup, or two recursive results plus one structural type-equality test) and constant work at abstractions (extending $\Gamma$). If the term has $n$ nodes and types have depth at most $d$ (bounded by $n$ in the worst case, since a term of size $n$ cannot mention a type larger than what its annotations spell out), then:

• Type equality checking costs $O(d)$ in the worst case (comparing two type trees).
• Context lookup costs $O(n)$ in a naive list-based environment, or $O(\log n)$ / $O(1)$ amortized with a hash map or array-backed environment.
• Total time: $O(n \cdot d)$ worst case, which collapses to $O(n)$ for the common case where annotated types have bounded size relative to program size (true in virtually all realistic annotated programs). Space is $O(n)$ for the recursion stack and the context, since $\Gamma$ grows only along the path from root to the current node (contexts are restored on backtracking out of an `Abs`, standard in a tree-recursive implementation).

This is exponentially cheaper than inference without annotations, which in richer systems (unification-based Hindley–Milner, see Type Inference and Hindley-Milner) must solve for unknown types rather than just check given ones.

Progress. If $\emptyset \vdash t : \tau$, then either $t$ is a value, or there exists $t'$ with $t \to t'$. *Proof sketch, by induction on the typing derivation. The T-Var case is vacuous (no closed term is a bare variable, since $\Gamma = \emptyset$). The T-Abs case is immediate: abstractions are values. The interesting case is T-App: $t = t_1\,t_2$ with $\Gamma \vdash t_1 : \tau_1\to\tau_2$ and $\Gamma \vdash t_2 : \tau_1$. By the induction hypothesis, $t_1$ is either a value or steps. If $t_1$ steps, the congruence rule lets $t$ step. If $t_1$ is a value, it must — by inspecting the typing rules — be an abstraction $\lambda x{:}\tau_1.\ t_1'$, because T-Abs is the only rule that can produce a function type for a value (this is the <strong>canonical forms lemma</strong>: a value of type $\tau_1\to\tau_2$ is necessarily a lambda abstraction). Then either $t_2$ steps (congruence again), or $t_2$ is itself a value, in which case E-AppAbs fires and $t$ steps. In every branch $t$ is a value or steps — it is never stuck* (an application whose head is not a function).

Preservation (subject reduction). If $\Gamma \vdash t : \tau$ and $t \to t'$, then $\Gamma \vdash t' : \tau$. *Proof sketch, by induction on the derivation of $t \to t'$, using a <strong>substitution lemma</strong>: if $\Gamma, x{:}\tau_1 \vdash t_2 : \tau_2$ and $\Gamma \vdash v_1 : \tau_1$, then $\Gamma \vdash [x \mapsto v_1] t_2 : \tau_2$ (itself proved by induction on the typing derivation of $t_2$, pushing the substitution through each rule). For the base case E-AppAbs, $t = (\lambda x{:}\tau_1.\ t_1)\ v_2$ typed via T-App from $\Gamma \vdash \lambda x{:}\tau_1.\ t_1 : \tau_1\to\tau_2$ and $\Gamma \vdash v_2 : \tau_1$; inverting T-Abs gives $\Gamma, x{:}\tau_1 \vdash t_1 : \tau_2$, and the substitution lemma yields $\Gamma \vdash [x\mapsto v_2]t_1 : \tau_2$ exactly as required. Congruence cases follow directly from the induction hypothesis applied to the reduced subterm, rebuilt with the same typing rule. Together, progress and preservation constitute <strong>type safety</strong>: starting from a well-typed closed term, every reduction sequence either terminates in a value or continues stepping, but never* reaches a stuck non-value term. This "well-typed programs don't get stuck" slogan is the exact statement proved; it foreshadows the general treatment in Type Safety and Soundness for languages with many more term forms.

Strong normalization. STLC has a stronger property that progress/preservation alone do not give: every well-typed term, under any reduction strategy, reaches a value in finitely many steps — there are no infinite reduction sequences. This cannot be proved by a naive induction on term structure, because reduction can grow a term (substitution duplicates subterms, e.g. $(\lambda x. x\,x)\,y \to y\,y$ can expand under further substitution). The standard proof method is Tait's method of logical relations: define, by induction on the type $\tau$ (not the term!), a predicate $\mathrm{SN}_\tau(t)$ — "reducible at type $\tau$" — such that $\mathrm{SN}_\iota(t)$ means $t$'s reduction sequences are all finite, and $\mathrm{SN}_{\tau_1\to\tau_2}(t)$ means $t$ terminates and $t\,s$ is reducible at $\tau_2$ whenever $s$ is reducible at $\tau_1$. One shows every reducible term terminates, every well-typed term is reducible (by induction on typing derivations), and hence every well-typed term terminates. This is why STLC, despite embedding the shape of general computation, cannot express an infinite loop — the price of the arrow type's discipline is the loss of Turing completeness, which is exactly what makes STLC decidable for type checking and guarantees termination, unlike the untyped calculus or languages with general recursion.

Honesty about tradeoffs. Strong normalization is a blessing and a curse. It rules out non-terminating bugs, but it also rules out legitimate non-terminating programs — an operating system kernel, a web server's event loop, or `while(true)` cannot be written in pure STLC. Real languages add explicit recursion (a `fix` or `letrec` construct, or general recursive functions), which immediately destroys strong normalization while keeping type safety intact; this is precisely the trade made by every practical typed language built on this core.

Take $\Gamma_0 = \emptyset$ and the term

— apply "apply twice" to the identity function on $\iota$. We trace both the type checker and the evaluator.

Step 8 is not a coincidence — it is preservation in action: the type computed once at the start ($\iota\to\iota$) is exactly the type of the final value after three beta reductions, even though the term's shape changed completely. This is the guarantee that lets a compiler type-check a program once, before running it, and trust that the type remains valid at every intermediate stage of execution — no runtime type tag or check is ever needed. Now contrast with a term that fails to type-check, to see progress's contrapositive at work: $t' = (\lambda x{:}\iota.\ x)\ (\lambda y{:}\iota.\ y)$. Here `typeOf` computes $\iota\to\iota$ for the argument, but the function $\lambda x{:}\iota.x$ expects type $\iota$ — the T-App rule's premise $\Gamma \vdash t_2 : \tau_1$ fails to unify $\iota$ with $\iota\to\iota$, so `typeOf` raises "argument type mismatch" and the term is rejected before it is ever run. Untyped, this term would reduce fine to $\lambda y{:}\iota.y$; typed, STLC refuses it purely on structural grounds, illustrating that the type system is a conservative, sound-but-incomplete filter — it rejects some terms that would actually behave fine, in exchange for rejecting all terms that would get stuck.

The typed lambda calculus arose from efforts to avoid the logical paradoxes (like Russell's paradox and Curry's paradox) that plague untyped systems of self-application, tying type theory's origins directly to foundational mathematics rather than to programming.

The connection between types and logic was made exact by the Curry–Howard correspondence: types correspond to propositions, and well-typed terms correspond to proofs — a function type $\tau_1 \to \tau_2$ is the proposition "$\tau_1$ implies $\tau_2$", and constructing a term of that type is constructing a proof. This correspondence is why type systems in proof assistants and type systems in programming languages are, at a deep level, the same mathematical object studied from two directions.

Every statically typed functional language — ML, Haskell, OCaml, F#, Scala's core, Rust's trait-resolved core — is built by layering features onto STLC's arrow-type discipline: parametric polymorphism turns it into System F, mutable state and effects are added on top, and algebraic data types (see Algebraic Data Types and Pattern Matching) extend the type grammar with sums and products alongside the function arrow. Proof assistants such as Coq, Agda, and Lean are built on dependently typed descendants of STLC, using the Curry–Howard correspondence to represent mathematical proofs as well-typed programs, so that a type checker literally verifies a proof. Compilers use STLC-style progress-and-preservation arguments as the template for proving that an intermediate representation (an IR like GHC's Core, or a bytecode verifier's internal type system, such as the JVM's) is safe to optimize and execute. Type checkers embedded in editors and IDEs (for real-time error squiggles) run essentially the `typeOf` algorithm above, scaled up with richer types, on every keystroke. Even outside functional languages, the discipline of "check the types once, trust it forever" underlies static analyses in Java, C#, and TypeScript, all descendants — in typing-rule spirit if not history — of the arrow-typed calculus first written down to save mathematics from paradox.

Ask the tutor: How does adding a `fix` operator change the progress and preservation proofs, and why do they still go through even though normalization fails?