More or less from Wikipedia:
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
Further Reading:
https://en.wikipedia.org/wiki/Lambda_cube
http://www.rbjones.com/rbjpub/logic/cl/tlc001.htm
https://en.wikipedia.org/wiki/Calculus_of_constructions
https://en.wikipedia.org/wiki/System_F
[* 11.86, *11.87]
<>
Equivalent eXchange 