Dependent Types and the Lambda Cube
So far our type systems have kept types and terms in separate worlds: terms compute, types classify, and
the two never truly mingle. Dependent types tear down that wall. They let a
type depend on a term — on an ordinary value. The classic example is the type of
vectors of length n, written
\mathsf{Vec}\,A\,n: here n is a runtime-ish number,
yet it appears inside a type. Now append can have the type
\mathsf{append} : \Pi(n:\mathbb{N}).\ \Pi(m:\mathbb{N}).\ \mathsf{Vec}\,A\,n \to \mathsf{Vec}\,A\,m \to \mathsf{Vec}\,A\,(n+m),
a type that states and enforces "the output length is the sum of the input lengths". Off-by-one
errors become type errors. Dependent types are the most expressive corner of the design space — powerful
enough that types can encode arbitrary specifications, and the type checker becomes a proof
checker. To see where they sit among everything we have built, we turn to Barendregt's
lambda cube.
Π-types: the dependent function
The one binder that makes dependent types work is the dependent function type, or
\Pi-type. Whereas the ordinary arrow A \to B
describes a function whose result type B is fixed,
\Pi(x:A).\,B(x) describes one whose result type
B(x) may mention the argument value x:
\dfrac{\Gamma,\, x:A \vdash t : B(x)}{\Gamma \vdash \lambda x{:}A.\,t \;:\; \Pi(x{:}A).\,B(x)}
\qquad
\dfrac{\Gamma \vdash f : \Pi(x{:}A).\,B(x) \quad \Gamma \vdash a : A}{\Gamma \vdash f\,a : B(a)}
Two familiar things are special cases. When B does not depend on
x, \Pi(x{:}A).\,B collapses to the plain arrow
A \to B. And when A is itself the type of
types, \Pi(X{:}\mathord{*}).\,B is exactly the polymorphic
\forall X.\,B of System F. Universal quantification is just a dependent
function that happens to take a type. Dually, the dependent pair
\Sigma(x{:}A).\,B(x) — a value x together with
evidence of type B(x) — generalises both the product and the existential
\exists X.\,B.
The lambda cube: three axes of dependency
Start from the simply typed lambda calculus (\lambda_\to), where the only
abstraction is "terms depending on terms" (ordinary functions). There are three independent
ways to add more, and each is one axis of a cube. Switch on any subset of the three and you get
one of 2^3 = 8 systems.
-
Terms depending on types (→ \lambda 2, System F):
polymorphism. A term abstracts over a type: \Lambda X.\,\lambda x{:}X.\,x.
-
Types depending on types (→ \lambda\underline{\omega}):
type operators / higher kinds. A type abstracts over a type:
\lambda X.\,X\to X, e.g. \mathsf{List} as a
function on types.
-
Types depending on terms (→ \lambda P, LF): dependent
types proper. A type abstracts over a value: \mathsf{Vec}\,A\,n.
The far corner, with all three switched on, is \lambda P\omega = \lambda C,
the Calculus of Constructions — the most expressive system of the cube and the
theoretical core of the proof assistant Coq (and, extended, of Lean and Agda). System
F_\omega (\lambda\omega) — polymorphism plus type
operators, but no term-dependency — is the well-behaved system underneath Haskell's and Scala's
type-level programming.
Curry–Howard: proofs are programs
Dependent types matter because of one of the deepest facts in logic and computing — the
Curry–Howard correspondence: propositions are types, and proofs are
programs. To prove a proposition is to construct a term of the corresponding type; the type checker,
checking that term, is checking the proof.
| Logic | Types |
|---|
| implication A \Rightarrow B | function A \to B |
| conjunction A \land B | product A \times B |
| disjunction A \lor B | sum / variant A + B |
| universal \forall x.\,P(x) | dependent function \Pi(x{:}A).\,P(x) |
| existential \exists x.\,P(x) | dependent pair \Sigma(x{:}A).\,P(x) |
| true / false | unit \mathbf{1} / empty \mathbf{0} |
The \forall/\Pi and
\exists/\Sigma rows are why we needed dependent
types: only when a type can quantify over values can it express "for all numbers
n…" — a real mathematical theorem. In a dependently typed language the code
below is, quite literally, a handful of tiny proofs.
// Curry-Howard in miniature: propositions are types, proofs are terms.
// A proof of A ⇒ A is the identity function (the simplest tautology).
const identity = <A>(a: A): A => a;
// Modus ponens: from a proof of A ⇒ B and a proof of A, derive B — just application.
const modusPonens = <A, B>(imp: (a: A) => B, proofA: A): B => imp(proofA);
// ∧-introduction is pairing; ∧-elimination is projection.
const andIntro = <A, B>(a: A, b: B): [A, B] => [a, b];
const andElimL = <A, B>(p: [A, B]): A => p[0];
// ∨-introduction: injecting into a sum (a tagged union).
type Or<A, B> = { tag: "left"; val: A } | { tag: "right"; val: B };
const orIntroR = <A, B>(b: B): Or<A, B> => ({ tag: "right", val: b });
console.log("proof of A⇒A on 7 :", identity(7));
console.log("modus ponens (·2) on 5 :", modusPonens((n: number) => n * 2, 5));
console.log("∧-elim-left of (3,'ok') :", andElimL(andIntro(3, "ok")));
console.log("∨-intro-right of true :", JSON.stringify(orIntroR<number, boolean>(true)));
Every line type-checks precisely because it is a valid proof. Add the ability to quantify over values —
dependent types — and this same game scales up to proving the correctness of sorting algorithms,
compilers (CompCert), and even the Four Colour Theorem. The type checker is the referee.
Yes — and it changed the field. CompCert, a C compiler by Xavier Leroy, is written and
proved correct in Coq, whose kernel is the Calculus of Constructions sitting at the far corner
of the lambda cube. The proof is a dependently typed term establishing that the compiled assembly
behaves exactly like the source C program — so CompCert simply cannot introduce a
miscompilation bug, a guarantee no amount of testing can give. When the famous "Csmith" fuzzing study
threw millions of random C programs at production compilers, it found hundreds of bugs in GCC and LLVM —
and none in CompCert's verified core. The Four Colour Theorem and the Feit–Thompson theorem have
likewise been fully machine-checked in Coq. Curry–Howard is not a curiosity; it is how we now build
software and mathematics we can actually trust.
Once a type can contain a term, deciding whether two types are equal may require
running those terms. Is \mathsf{Vec}\,A\,(2+2) the same type as
\mathsf{Vec}\,A\,4? Only if 2+2 reduces to
4 — so type equality is definitional (computational) equality,
and the type checker must evaluate. This has a sharp consequence: if the term language allows
non-termination, type checking can loop forever and become undecidable. That is why serious
dependently typed languages (Coq, Agda, Idris, Lean) insist every function be total —
provably terminating — enforced by a termination/positivity checker. It is the same totality we lost when
recursive types
made the calculus Turing-complete, now bought back deliberately: you cannot have unrestricted general
recursion and sound, decidable dependent type checking at once. Dependent-type power is paid for
in the discipline of totality.