In mathematical logic and type theory, the λ-cube is a framework introduced by Henk Barendregt to investigate the different dimensions in which the calculus of constructions is a generalization of the simply typed λ-calculus. Each dimension of the cube corresponds to a new way of making objects depend on other objects, namely
- terms allowed to depend on types, corresponding to polymorphism.
- types depending on terms, corresponding to dependent types.
- types depending on types, corresponding to type operators.
The different ways to combine these three dimensions yield the 8 vertices of the cube, each corresponding to a different kind of typed system.
So in the diagram above, we have emblazoned the names of these type systems ordered from lower left to upper right:
- λ→: the simply typed lambda calculus, our base system
- λ2: add 1. above to λ→, giving what is also known as System F or the Girard–Reynolds polymorphic lambda calculus
- λP: add 2. above to λ→
- λ_ω_: add 3. above to λ→
- λP2: combine 1. and 2., λ2 and λP
- λω: combine 1. and 3., λ2 and λ_ω_
- λP_ω_: combine 2. and 3., λP and λ_ω_
- λC: combine 1., 2., and 3., giving the calculus of constructions
[* 11.86, *11.87]