THE LAMBDA CUBE three axes of abstraction — eight typed lambda calculi, one corner is the summit
Barendregt's lambda cube organizes typed lambda calculi along three independent axes of dependency: terms depending on types (polymorphism, System F), types depending on types (type operators, Fω), and types depending on terms (dependent types). Turn each axis on or off and you get 2³ = 8 corners: the plain simply-typed calculus at the origin, and the Calculus of Constructions (all three on) at the far corner — the basis of Coq. It is the map of the whole territory this batch has been walking: every type feature is a direction you can travel from the simplest calculus.
THE TECHNIQUE 3 independent axes, each on/off → 2³ = 8 systems
Three axes, each a kind of dependency you can add. The demo toggles them and counts the corner of the cube you land on — and the total, 2³ = 8: live demo
HISTORY & CREDIT Barendregt, 1991
“There are dozens of unrelated type systems.” — there are three axes and eight corners. Polymorphism, type operators, dependency: switch them on in combination and every typed lambda calculus in this batch appears at a corner of one cube. cited
1991 · Henk Barendregt — “Introduction to Generalized Type Systems”: the lambda cube, eight systems on three axes. 1988 · Coquand & Huet — the Calculus of Constructions, the cube's top corner (all three dependencies). now · the organizing map behind Coq/Rocq, Lean, Agda; Pure Type Systems generalize it.
Eight corners from three yes/no axes: λ→ at the origin, the Calculus of Constructions at the summit. The batch's darts are directions of travel on one small cube. Barendregt 1991
RECOMMEND FOR I-13 cube corner + total, computed
On the canonical compiler, the three axes give 2³ = 8 systems — the whole cube:
$ i13 run t_cube.i13 # 2^3 corners
axes = 3
systems = 8 -- lambda-> (origin) ... Calculus of Constructions (far corner)
Recommend: i13 sits at the origin of the cube — and one step below it. The simply-typed lambda calculus (all three axes off) is the origin; i13 is simpler still: untyped, one ground type (f64). Every axis of the cube — polymorphism, type operators, dependency — is a direction i13 chose not to travel, and the batch's 16 darts are those directions laid out. The cube is the map; types: NOT COVERED is i13 planting its flag before the map even begins — deliberately, to keep one value model and a validator that finishes in a single pass.