Lambda Cube

The Lambda Cube are a series of successive refinements applied to simply-typed lambda calculus. In ASCII art, we have something like the following:

   λω-------λΠω
   /|      /|
  / |     / |
λ2--|---λΠ2 |
 | λω----|--λΠω
 | /     | /
 |/      |/
λ→-------λΠ

The “floor model” is λ→, the simply-typed lambda calculus. We have the following different “dimensions” to the lambda cube:

• λ2, a.k.a. “System F”, allows for polymorphism (c.f., Pierce TAPL ch.23)
• λω allows for types depending on types (or “type operators” and “kinding”, c.f. Pierce’s TAPL ch.29), and
• λΠ allows for types depending on terms (a.k.a., dependent types, c.f., David Aspinall and Martin Hofmann’s “Dependent Types” — ch.2 in Advanced Topics in Types and Programming Languages, ed. Benjamin C. Pierce).

The other vertices are obtained mixing these “basis calculi” together in a “compatible” manner. For example, λω combines type operators and System F (c.f., Pierce’s TAPL, ch.30). Or λΠω, otherwise known as the “Calculus of Constructions” (also discussed briefly in Aspinall and Hofmann’s article) combines λω with dependent types.

References

• Benjamin C. Pierce, Types and Programming Languages. MIT Press, 2002. Implements type checkers for 6 of the vertices of the lambda cube, in Standard ML. Very pedagogical, beautifully done.
• Benjamin C. Pierce, ed., Advanced Topics in Types and Programming Languages. MIT Press, 2005.