The Simply-Typed Lambda Calculus (λ→)
The untyped lambda calculus is gloriously unrestrained: any term may be applied to any other. That
freedom is exactly what makes it Turing-complete — and exactly what lets it write down
nonsense. Nothing stops you from forming \text{true}\ \text{true},
applying a boolean as if it were a function, or building the non-terminating
\Omega = (\lambda x.\,x\,x)(\lambda x.\,x\,x). The
simply-typed lambda calculus, written \lambda_{\to} and
introduced by Alonzo Church in 1940, is the smallest disciplined language you get by layering a
type system on top: a set of rules that decides, purely from the syntax, which terms
are meaningful — and quietly discards the rest.
\lambda_{\to} is the fruit fly of programming-language theory.
It is tiny enough to fit on a napkin, yet rich enough that everything important — typing contexts,
derivation trees, type soundness, even the Curry–Howard
bridge to logic — appears here in its purest form. Master this page and the machinery of far larger
languages (System F, Haskell's core, Rust's borrow checker) reads as elaboration, not revolution.
Two grammars: types and terms
We build \lambda_{\to} from two mutually-referring grammars. First the
types. Starting from one or more base types — write a generic base as
\iota (say \text{Bool} or
\text{Nat}) — the only way to build a new type is the
function arrow:
T \;::=\; \iota \;\mid\; T \to T
The arrow is right-associative, so
\text{Nat} \to \text{Nat} \to \text{Nat} means
\text{Nat} \to (\text{Nat} \to \text{Nat}) — a function that takes a
\text{Nat} and returns another function. That is the whole type
language: base types and arrows, nothing else. (No products, sums, or polymorphism yet — those are
deliberate extensions.)
Second the terms. Church's key move over the untyped calculus is that every
\lambda-binder carries an explicit type annotation on its
parameter:
t \;::=\; x \;\mid\; \lambda x{:}T.\;t \;\mid\; t\;t
Read left to right: a variable x; an
abstraction \lambda x{:}T.\,t (an anonymous function whose
argument x is declared to have type T); and an
application t\;t (feed the right term to the left one). To
do anything interesting we usually add a base type with constants — booleans
\text{true}, \text{false} and a conditional
\text{if}\;t\;\text{then}\;t\;\text{else}\;t, or naturals with
0 and \text{succ} — but the three forms above are
the irreducible core.
The typing context \Gamma
A term like x or f\;x has no type in the
abstract — it depends on what x and f are
assumed to be. That assumption set is the typing context (or environment),
written \Gamma: a finite list of variable-to-type bindings.
\Gamma \;::=\; \varnothing \;\mid\; \Gamma,\; x{:}T
We write x{:}T \in \Gamma to mean "the context binds
x to T", and
\Gamma, x{:}T to mean "extend \Gamma with a new
binding" (shadowing any earlier x). The central object of the whole theory
is the typing judgment
\Gamma \vdash t : T
pronounced "under assumptions \Gamma, term
t has type T". The turnstile
\vdash is the barrier between what we assume (left) and what we
conclude (right). When the context is empty we write simply
\vdash t : T — a closed, self-contained term.
The three rules
The typing relation \Gamma \vdash t : T is defined inductively by
three rules, one per term form. Each is written as an inference rule: whatever sits
above the line (the premises) justifies what sits below (the conclusion).
Variable (T-Var). A variable's type is whatever the context says it is — an
axiom, with only a lookup as its premise:
\dfrac{x{:}T \in \Gamma}{\Gamma \vdash x : T}\;\textsf{(T-Var)}
Abstraction (T-Abs). To type a function, type its body with the parameter added to
the context. If the body has type T_2 given
x{:}T_1, the whole function has the arrow type
T_1 \to T_2:
\dfrac{\Gamma,\; x{:}T_1 \;\vdash\; t : T_2}{\Gamma \vdash \lambda x{:}T_1.\;t \;:\; T_1 \to T_2}\;\textsf{(T-Abs)}
Application (T-App). To type an application, the function must have an arrow type
whose domain matches the argument's type exactly; the result is the arrow's
codomain:
\dfrac{\Gamma \vdash t_1 : T_{11} \to T_{12} \qquad \Gamma \vdash t_2 : T_{11}}{\Gamma \vdash t_1\;t_2 \;:\; T_{12}}\;\textsf{(T-App)}
That is the entire type system — three rules (plus one axiom per constant, e.g.
\Gamma \vdash \text{true} : \text{Bool}). Every well-typed program is a
tree of these rules stacked on one another. A term is well-typed exactly
when such a tree exists; if no tree can be built, the term is rejected.
A worked derivation
Let us type the closed term (\lambda x{:}\text{Bool}.\;x)\;\text{true} —
the identity on booleans, applied to \text{true}. We expect the answer
\text{Bool}, and the derivation tree shows precisely why. Watch it
assemble from the goal down to the leaves — this goal-directed growth is exactly what a type-checker
does.
The root is the goal \vdash (\lambda x{:}\text{Bool}.\,x)\;\text{true} : \text{Bool}.
Because the term is an application, only T-App can conclude it, spawning two
sub-goals: the function \lambda x{:}\text{Bool}.\,x must have type
\text{Bool} \to \text{Bool}, and the argument
\text{true} must have type \text{Bool} — its
domain. The function sub-goal is discharged by T-Abs, which in turn needs
x{:}\text{Bool} \vdash x : \text{Bool} — closed by T-Var,
a context lookup. The argument sub-goal is closed by the T-True axiom. Every leaf is
an axiom, so the tree is complete and the term is well-typed at \text{Bool}.
What typing rules out
The power of the system is best felt through what it rejects. Try to build a derivation for
\text{true}\;\text{false} — applying a boolean to a boolean. The only rule
that concludes an application is T-App, which demands the function have an
arrow type; but \text{true} has type
\text{Bool}, which is not an arrow. No rule applies, no tree exists, the
term is ill-typed — rejected before it ever runs. The same fate meets the untyped
\Omega: the self-application x\;x would need
x to have both type T \to U and type
T simultaneously — impossible for a finite simple type.
Below is the whole three-rule system as an executable type-checker. The recursion mirrors the
rules one-for-one: Var is a lookup, Abs extends the context and recurses,
App checks the arrow's domain against the argument. Run it and watch the well-typed terms
report a type while the ill-typed ones are caught.
// ── Types of λ→ : base types Bool, Nat, and function types T1 → T2. ──
type Ty =
| { kind: "Bool" }
| { kind: "Nat" }
| { kind: "Fun"; from: Ty; to: Ty };
// ── Terms: variables, TYPED abstractions, applications, plus constants. ──
type Term =
| { kind: "Var"; name: string }
| { kind: "Abs"; param: string; paramTy: Ty; body: Term }
| { kind: "App"; fn: Term; arg: Term }
| { kind: "True" }
| { kind: "False" }
| { kind: "Zero" }
| { kind: "Succ"; n: Term };
type Ctx = Record<string, Ty>;
function tyEq(a: Ty, b: Ty): boolean {
if (a.kind === "Fun" && b.kind === "Fun")
return tyEq(a.from, b.from) && tyEq(a.to, b.to);
return a.kind === b.kind;
}
function show(t: Ty): string {
return t.kind === "Fun" ? `(${show(t.from)}→${show(t.to)})` : t.kind;
}
// ── The typing relation Γ ⊢ term : Ty , as a recursive function. ──
function typeOf(ctx: Ctx, t: Term): Ty {
switch (t.kind) {
case "True": case "False": return { kind: "Bool" };
case "Zero": return { kind: "Nat" };
case "Succ": {
if (!tyEq(typeOf(ctx, t.n), { kind: "Nat" })) throw new Error("succ expects a Nat");
return { kind: "Nat" };
}
case "Var": { // (T-Var): context lookup
const ty = ctx[t.name];
if (!ty) throw new Error(`unbound variable ${t.name}`);
return ty;
}
case "Abs": { // (T-Abs): extend Γ, type the body
const bodyTy = typeOf({ ...ctx, [t.param]: t.paramTy }, t.body);
return { kind: "Fun", from: t.paramTy, to: bodyTy };
}
case "App": { // (T-App): domain must match argument
const fnTy = typeOf(ctx, t.fn);
const argTy = typeOf(ctx, t.arg);
if (fnTy.kind !== "Fun") throw new Error("applying a non-function");
if (!tyEq(fnTy.from, argTy))
throw new Error(`argument is ${show(argTy)}, expected ${show(fnTy.from)}`);
return fnTy.to;
}
}
}
// Convenience constructors.
const Bool: Ty = { kind: "Bool" };
const v = (name: string): Term => ({ kind: "Var", name });
const lam = (p: string, ty: Ty, body: Term): Term => ({ kind: "Abs", param: p, paramTy: ty, body });
const app = (fn: Term, arg: Term): Term => ({ kind: "App", fn, arg });
const T: Term = { kind: "True" }, F: Term = { kind: "False" };
function check(label: string, t: Term) {
try { console.log(`${label} : ${show(typeOf({}, t))}`); }
catch (e) { console.log(`${label} ✗ ${(e as Error).message}`); }
}
check("(λx:Bool. x) true ", app(lam("x", Bool, v("x")), T)); // → Bool
check("λx:Bool. λy:Bool. x ", lam("x", Bool, lam("y", Bool, v("x")))); // → Bool→(Bool→Bool)
check("true false ", app(T, F)); // ✗ non-function
check("(λx:Bool. x) (λy:Bool. y)", app(lam("x", Bool, v("x")), lam("y", Bool, v("y")))); // ✗ mismatch
There are two philosophies about where types live, and they name two whole styles of type
theory. In the intrinsic (or Church) style — the one on this page — the type
annotation \lambda x{:}T is part of the term itself. An
untyped term is not even a legal object; there is no
\lambda x.\,x without its T, and every
well-formed term has a unique type baked in. In the extrinsic (or Curry)
style, terms are the bare untyped ones and typing is an external verdict
assigned afterwards: the same term \lambda x.\,x can be given
\text{Bool} \to \text{Bool}, \text{Nat} \to \text{Nat},
or infinitely many types. Church types things; Curry types meanings. Type
inference — Haskell and ML figuring out your types for you — lives naturally in the
Curry world, while dependently-typed proof assistants tend toward Church. Reynolds' insight is that,
for \lambda_{\to}, the two give the same well-typed programs — they are two
readings of one system.
An annotation is not a check — it is a claim the rules still verify. A common
beginner error is to think \lambda x{:}T.\,t declares the whole
function's type or that the annotation somehow makes the term well-typed by fiat. It does neither.
T is only the parameter's type; the return type is
computed by typing the body, and the term is well-typed only if a full derivation exists. You
can write a perfectly well-formed term that is still ill-typed: for instance
\lambda x{:}\text{Bool}.\;x\;x parses fine but fails T-App (a
\text{Bool} is not a function). Well-formed (parses) and well-typed (has a
derivation) are different bars — the type-checker enforces the second, and the annotation is merely an
input to that check, never a substitute for it.
Why the annotations? Uniqueness and decidability
Church's explicit annotations buy two beautiful properties. First, unique typing: in
the intrinsic system every term has at most one type, given the context. The rules are
syntax-directed — the outermost term-former determines which rule must conclude the
judgment, so there is never a choice to backtrack over. Second, and consequently,
type-checking is decidable: the recursive typeOf above always
terminates (it recurses on strictly smaller subterms) and answers yes-with-a-type or no. There is no
search, no undecidability, no halting-problem obstruction — a striking contrast to running
the term, and a foretaste of why simply-typed terms behave so tamely.