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]
<>
Leave a Reply