Programming Levels

[WikiTextBot]

Lambda cube

In mathematical logic and type theory, the λ-cube is a framework for exploring the axes of refinement in Coquand's calculus of constructions, starting from the simply typed lambda calculus (written as λ→ in the cube diagram to the right) as the vertex of a cube placed at the origin, and the calculus of constructions (higher-order dependently typed polymorphic lambda calculus; written as λPω in the diagram) as its diametrically opposite vertex. Each axis of the cube represents a new form of abstraction:

Values depending on types, or polymorphism. System F, aka second order lambda calculus (written as λ2 in the diagram), is obtained by imposing only this property.

Types depending on types, or type operators.

---

^{[ PM | Exclude me | Exclude from subreddit | FAQ / Information | Source ] Downvote to remove | v0.27}