Chris Grounds

Wander mode

A constellation of ideas

The interactive lambda cube

Explore the cube to find out what happens when we let terms and types depend on one another.

Barendregt’s λ-cube
Choose a type system. Use the arrow keys to move between systems.

Each arrow adds one kind of dependency.

The starting point

λ→ Simply typed
lambda calculus

Terms can depend on terms: a function takes a value and returns a value. Its argument and result types are fixed.

Logic
Propositional logicThe implicational fragment: A → B reads as “A implies B”. The formula below says implications chain.(A → B) → (B → C) → A → C
Languages

All six support simply typed functions.

Example in Haskell
compose :: (Int -> Bool) -> (Bool -> String) -> Int -> String
compose f g x = g (f x)
  • Polymorphism No
  • Type operators No
  • Dependent types No

Add polymorphism

λ2 System F

Terms can also depend on types. Abstract over a type to write one function that works for every choice of that type.

Logic
Second-order propositional logicQuantify over propositions.∀A. ∀B. A → B → A
Languages

Ticks indicate parametric polymorphism; generic functions are not necessarily full, impredicative System F.

Example in Haskell
const :: forall a b. a -> b -> a
const x _ = x
  • Polymorphism Yes
  • Type operators No
  • Dependent types No

Add type operators

λω Types from types

Types can depend on types. A type-level function takes a type and constructs another type.

Logic
Weak higher-order propositional logicBuild operators on propositions, without quantifying over propositions in proofs.Self := λA. A → A, so Self(P) is P → P
Languages

Here type operators require general higher-kinded abstraction. TypeScript type aliases and Rust generic associated types provide only part of that capability.

Example in Haskell
type Dup a = (a, a)

first :: Dup Int -> Int
first (x, _) = x
  • Polymorphism No
  • Type operators Yes
  • Dependent types No

Add dependent types

λP Types from terms

A type can depend on a value. A dependent function’s result type may mention the argument it receives.

Logic
First-order predicate logicImplication and universal quantification over individuals; propositions may depend on those individuals.∀x. (P(x) → Q(x)) → P(x) → Q(x)
Languages

Ticks require general dependent functions. Rust const generics, TypeScript literal types, and Haskell type-level encodings do not meet that criterion.

Example in Lean
def last : (n : Nat) → Fin (n + 1) :=
  fun n => ⟨n, Nat.lt_succ_self n⟩
  • Polymorphism No
  • Type operators No
  • Dependent types Yes

Combine two extensions

λω System Fω

Combine polymorphism with type operators. Functions can abstract over type constructors as well as ordinary types.

Logic
Higher-order propositional logicConstruct proposition operators and quantify over them.∀F. ∀A. F(A) → F(A)
Languages

Haskell supports higher-kinded polymorphism. TypeScript and Rust need encodings for general abstraction over type constructors.

Example in Haskell
newtype Compose f g a = Compose (f (g a))

decompose :: forall f g a. Compose f g a -> f (g a)
decompose (Compose x) = x
  • Polymorphism Yes
  • Type operators Yes
  • Dependent types No

Combine two extensions

λP2 Polymorphism
meets dependency

Abstract over types and let types depend on values. Neither feature requires type-level functions from types to types.

Logic
Second-order predicate logicQuantify over individuals and predicates on them.x = y := ∀P. P(x) → P(y)
Languages

Rocq, Idris, and Lean combine polymorphism with general dependent functions.

Example in Lean
theorem leibniz_refl {α : Type} (x : α) :
    ∀ P : α → Prop, P x → P x :=
  fun _ h => h
  • Polymorphism Yes
  • Type operators No
  • Dependent types Yes

Combine two extensions

λPω Two ways to
construct types

Types can depend on both types and values. This corner combines dependent types with type operators, without polymorphism.

Logic
Weak higher-order predicate logicBuild higher-order predicate operators and quantify over individuals, without polymorphic quantification.Sym := λR. ∀x. ∀y. R(x, y) → R(y, x)
Languages

Rocq, Idris, and Lean combine type operators with general dependent functions.

Example in Lean
def Sym (R : Nat → Nat → Prop) : Prop :=
  ∀ x y, R x y → R y x

theorem eq_sym' : Sym (· = ·) :=
  fun _ _ h => h.symm
  • Polymorphism No
  • Type operators Yes
  • Dependent types Yes

All three extensions

λC Calculus of
Constructions

The far corner brings together polymorphism, type operators, and dependent types. Every path from λ→ adds the same three capabilities.

Logic
Higher-order predicate logicCombine quantification over individuals, predicates, and higher-order predicate operators.∀R. Sym(R) → ∀x. ∀y. R(x, y) → R(y, x)
Languages

Rocq, Idris, and Lean support all three capabilities. Their universe and quantification rules differ from the original calculus.

Example in Lean
def Sym {α : Type} (R : α → α → Prop) : Prop :=
  ∀ x y, R x y → R y x

theorem sym_apply {α : Type} (R : α → α → Prop)
    (h : Sym R) (x y : α) : R x y → R y x :=
  h x y
  • Polymorphism Yes
  • Type operators Yes
  • Dependent types Yes

Reading the logic and language labels

Under Curry–Howard, types act as propositions and terms as proofs. The logic names here refer to intuitionistic systems, with implication and the quantifiers available at each corner. “Weak higher-order” means operators are available without the polymorphic quantification added by the upward edge.

✓ means practical support for the corner’s capabilities, possibly within a richer language; ✗ means those capabilities are not fully available natively. This is a feature comparison, not a claim that a language implements the exact calculus or its logic. Polymorphism includes ordinary generics; type operators require general higher-kinded abstraction; dependent types require general dependent functions. Recursion, effects, and universe rules are outside this checklist.

How to navigate the cube

Start at λ→, where functions take values. Travel upwards for polymorphism, diagonally for type operators, or to the right for dependent types.

Haskell’s polymorphism and higher-kinded types make System Fω a useful point of reference, though a full programming language has many features beyond this cube. The dependent-types direction asks a further question: what if a type could mention a value?

References