Typing Rules and Derivations
The three rules of
λ→
define the typing relation, but a rule on its own only says "if these premises hold,
then this conclusion holds". To actually certify that a term is well-typed you must stack the
rules into a derivation — a finite tree whose root is the judgment you want and whose
every leaf is an axiom. This page is about that tree: how to read an inference rule, how to
build a full derivation, why type-checking is exactly the search for such a tree, and
the quietly powerful principle of inversion that makes the search deterministic.
How to read a rule
Every typing rule is a horizontal bar. Above the bar sit zero or more premises; below
it sits a single conclusion; the rule's name is written to the side.
\dfrac{\text{premise}_1 \qquad \cdots \qquad \text{premise}_n}{\text{conclusion}}\;\textsf{(Name)}
Read it as an implication: "to establish the conclusion, it suffices to establish all
premises." A rule with no premises above the bar is an axiom — it
holds unconditionally, and every branch of a derivation must terminate in one. Our three rules again,
so the shapes are fresh in mind:
\dfrac{x{:}T \in \Gamma}{\Gamma \vdash x : T}\;\textsf{(T-Var)} \qquad \dfrac{\Gamma,\,x{:}T_1 \vdash t : T_2}{\Gamma \vdash \lambda x{:}T_1.\,t : T_1 \to T_2}\;\textsf{(T-Abs)}
\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)}
T-Var is an axiom (its "premise" is a side-condition, a lookup, not a judgment to derive). T-Abs has
one premise; T-App has two. A derivation is any tree built by fitting conclusions into
premise slots — the conclusion of one rule becomes a premise of the rule below it — until every
upward branch ends in an axiom.
Building a full derivation
Take the context \Gamma = f{:}\text{Nat}\to\text{Nat},\; x{:}\text{Nat} and
the term f\,(f\,x) — apply f, then apply
f again. We claim \Gamma \vdash f\,(f\,x) : \text{Nat}.
Rather than guess the top-level type and work down, here we build the tree synthetically:
start from the leaves the context hands us and compose them upward until the goal falls out. Watch:
The two innermost leaves are pure context lookups (T-Var):
\Gamma \vdash f : \text{Nat}\to\text{Nat} and
\Gamma \vdash x : \text{Nat}. T-App fits them together — the function's
domain \text{Nat} matches the argument
x — yielding \Gamma \vdash f\,x : \text{Nat}.
Now that intermediate judgment becomes the argument premise of the outer application, whose
function premise is another lookup of f. A final T-App composes
them into the root \Gamma \vdash f\,(f\,x) : \text{Nat}. The nesting of the
term is mirrored exactly by the nesting of the tree.
Type-checking is derivation search
Here is the pivotal idea: a type-checker is a procedure that searches for a derivation.
Given \Gamma and t, it asks "which rule could
conclude a judgment about this term?", recursively checks that rule's premises, and if all
succeed, returns the type at the root. Because our rules are syntax-directed — the
outermost shape of t uniquely selects the rule (a variable ⟹ T-Var, a
\lambda ⟹ T-Abs, an application ⟹ T-App) — the "search" has no
branching and no backtracking. It is a single deterministic walk over the term.
The checker below makes the tree visible: alongside the type it returns a Deriv record
tagging the rule used and its sub-derivations, then pretty-prints the whole tree with indentation.
Reading its output top-to-bottom is reading the derivation root-to-leaves.
type Ty = { kind: "Base"; name: string } | { kind: "Fun"; from: Ty; to: Ty };
type Term =
| { kind: "Var"; name: string }
| { kind: "Abs"; param: string; paramTy: Ty; body: Term }
| { kind: "App"; fn: Term; arg: Term };
type Ctx = Record<string, Ty>;
// A derivation node: the rule used, the judgment it proves, and its children.
type Deriv = { rule: string; judgment: string; kids: Deriv[] };
const base = (name: string): Ty => ({ kind: "Base", name });
const show = (t: Ty): string =>
t.kind === "Fun" ? `(${show(t.from)}→${show(t.to)})` : t.name;
const tyEq = (a: Ty, b: Ty): boolean =>
a.kind === "Fun" && b.kind === "Fun"
? tyEq(a.from, b.from) && tyEq(a.to, b.to)
: a.kind === "Base" && b.kind === "Base" && a.name === b.name;
const ctxStr = (ctx: Ctx) => {
const es = Object.entries(ctx);
return es.length ? es.map(([k, t]) => `${k}:${show(t)}`).join(", ") : "∅";
};
const termStr = (t: Term): string => {
switch (t.kind) {
case "Var": return t.name;
case "Abs": return `λ${t.param}:${show(t.paramTy)}. ${termStr(t.body)}`;
case "App": return `(${termStr(t.fn)} ${termStr(t.arg)})`;
}
};
// Search for a derivation; the rule is chosen by the SHAPE of the term (syntax-directed).
function derive(ctx: Ctx, t: Term): { ty: Ty; d: Deriv } {
const j = (ty: Ty) => `${ctxStr(ctx)} ⊢ ${termStr(t)} : ${show(ty)}`;
switch (t.kind) {
case "Var": { // T-Var: no sub-goals (an axiom)
const ty = ctx[t.name];
if (!ty) throw new Error(`unbound ${t.name}`);
return { ty, d: { rule: "T-Var", judgment: j(ty), kids: [] } };
}
case "Abs": { // T-Abs: one sub-goal (the body)
const { ty: bTy, d: bD } = derive({ ...ctx, [t.param]: t.paramTy }, t.body);
const ty: Ty = { kind: "Fun", from: t.paramTy, to: bTy };
return { ty, d: { rule: "T-Abs", judgment: j(ty), kids: [bD] } };
}
case "App": { // T-App: two sub-goals (fn and arg)
const { ty: fTy, d: fD } = derive(ctx, t.fn);
const { ty: aTy, d: aD } = derive(ctx, t.arg);
if (fTy.kind !== "Fun") throw new Error(`${termStr(t.fn)} is not a function`);
if (!tyEq(fTy.from, aTy)) throw new Error(`arg is ${show(aTy)}, want ${show(fTy.from)}`);
return { ty: fTy.to, d: { rule: "T-App", judgment: j(fTy.to), kids: [fD, aD] } };
}
}
}
function printDeriv(d: Deriv, indent = "") {
console.log(`${indent}${d.judgment} [${d.rule}]`);
for (const k of d.kids) printDeriv(k, indent + " ");
}
// Γ = f:Nat→Nat, x:Nat ; term f (f x).
const Nat = base("Nat");
const ctx: Ctx = { f: { kind: "Fun", from: Nat, to: Nat }, x: Nat };
const term: Term = {
kind: "App",
fn: { kind: "Var", name: "f" },
arg: { kind: "App", fn: { kind: "Var", name: "f" }, arg: { kind: "Var", name: "x" } },
};
const { ty, d } = derive(ctx, term);
console.log(`Result type: ${show(ty)}\n`);
printDeriv(d);
Inversion: reading the rules backwards
The reason the search never has to guess is a structural fact called the inversion lemma
(or generation lemma). It runs the rules backwards: from a valid judgment about a
term of a given shape, it tells you which rule must have been used last and therefore
what its premises must have been. Because each term-former is concluded by exactly one rule,
the last step of any derivation is forced.
- If \Gamma \vdash x : T then x{:}T \in \Gamma.
(The only way to type a variable is T-Var.)
- If \Gamma \vdash \lambda x{:}T_1.\,t : R then
R = T_1 \to T_2 for some T_2 with
\Gamma,\,x{:}T_1 \vdash t : T_2. (Its type must be an arrow with domain
exactly the annotation.)
- If \Gamma \vdash t_1\,t_2 : R then there is a type
T_{11} with \Gamma \vdash t_1 : T_{11} \to R
and \Gamma \vdash t_2 : T_{11}. (An application forces the function's
codomain to be the result and its domain to be the argument's type.)
Inversion is the workhorse of every metatheory proof to come. When we later prove
preservation by induction, each case begins "by inversion on the typing derivation,
the last rule was …", instantly recovering the premises we need. It is also what licenses the
recursive derive above to descend without a choice point: the shape of the term
is the proof of which rule applies.
Uniqueness of types
Inversion has an immediate, satisfying corollary. Because each syntactic form is handled by exactly one
rule, and that rule reconstructs the type from the sub-terms' types with no freedom, a term has
at most one type in a given context.
- If \Gamma \vdash t : T and
\Gamma \vdash t : T', then T = T'.
- Moreover the derivation itself is unique: there is exactly one tree proving the judgment.
This is why typeOf can safely return a type rather than a set of possible types —
the answer is a function of (\Gamma, t), not a relation to be searched over.
(Add subtyping or polymorphism and uniqueness weakens to a "principal type"; in bare
\lambda_{\to} it is exact.)
The two-dimensional "premises over a bar, name to the side" notation was not invented for types — it is
Gerhard Gentzen's natural deduction (1934), the standard format for proofs in logic.
A typing derivation is literally a proof tree in that older sense, which is not a coincidence
but the seed of the Curry–Howard correspondence: read
the types as propositions and the very same tree becomes a proof of a logical formula. When you build
a typing derivation you are, without noticing, doing formal logic — a fact we will cash in fully on a
later page.
A derivation is a tree, not a linear chain — and every branch must reach an axiom. A
frequent mistake is to "type-check" a term by writing a single column of judgments, or to leave a
branch dangling on an assumption you never discharged. Both are non-derivations. T-App has
two premises, so the tree branches; each branch is an independent obligation that must
bottom out in T-Var (or a constant axiom). A judgment with an open leaf — a premise still
unproven — proves nothing. Equally, do not confuse the side-condition
x{:}T\in\Gamma of T-Var with a premise to derive: it is a lookup you either
can or cannot perform, and if you cannot, the term is simply ill-typed.