In mathematical logic and type theory, the λ-cube (also written lambda 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 kind of dependency between terms and types. Here, "dependency" refers to the capacity of a term or type to bind a term or type. The respective dimensions of the λ-cube correspond to:
x-axis ( → {\displaystyle \rightarrow } ): types that can depend on terms, corresponding to dependent types. y-axis ( ↑ {\displaystyle \uparrow } ): terms that can depend on types, corresponding to polymorphism. z-axis ( ↗ {\displaystyle \nearrow } ): types that can depend on other types, corresponding to (binding) 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. The λ-cube can be generalized into the concept of a pure type system.
Examples of systems
(λ→) Simply typed lambda calculus The simplest system found in the λ-cube is the simply typed lambda calculus, also called λ→. In this system, the only way to construct an abstraction is by making a term depend on a term, with the typing rule:
Γ , x : σ ⊢ t : τ Γ ⊢ λ x . t : σ → τ {\displaystyle {\frac {\Gamma ,x:\sigma \;\vdash \;t:\tau }{\Gamma \;\vdash \;\lambda x.t:\sigma \to \tau }}}
(λ2) System F In System F (also named λ2 for the "second-order typed lambda calculus") there is another type of abstraction, written with a Λ {\displaystyle \Lambda } , that allows terms to depend on types, with the following rule:
Γ ⊢ t : σ Γ ⊢ Λ α . t : Π α . σ if α does not occur free in Γ {\displaystyle {\frac {\Gamma \;\vdash \;t:\sigma }{\Gamma \;\vdash \;\Lambda \alpha .t:\Pi \alpha .\sigma }}\;{\text{ if }}\alpha {\text{ does not occur free in }}\Gamma }
The terms beginning with a Λ {\displaystyle \Lambda } are called polymorphic, as they can be applied to different types to get different functions, similarly to polymorphic functions in ML-like languages. For instance, the polymorphic identity of OCaml has type meaning it can take an argument of any type 'a and return an element of that type. This type corresponds in λ2 to the type Π α . α → α {\displaystyle \Pi \alpha .\alpha \to \alpha } .
(λω) System Fω In System F ω _ {\displaystyle {\underline {\omega }}} a construction is introduced to supply types that depend on other types. This is called a type constructor and provides a way to build "a function with a type as a value". An example of such a type constructor is the type of binary trees with leaves labeled by data of a given type A {\displaystyle A} : T R E E := λ A : ∗ . Π B . ( A → B ) → ( B → B → B ) → B {\displaystyle {\mathsf {TREE}}:=\lambda A:*.\Pi B.(A\to B)\to (B\to B\to B)\to B} , where " A : ∗ {\displaystyle A:*} " informally means " A {\displaystyle A} is a type". This is a function that takes a type parameter A {\displaystyle A} as an argument and returns the type of T R E E {\displaystyle {\mathsf {TREE}}} s of values of type A {\displaystyle A} . In concrete programming, this feature corresponds to the ability to define type constructors inside the language, rather than considering them as primitives. The previous type constructor roughly corresponds to the following definition of a tree with labeled leaves in OCaml: This type constructor can be applied to other types to obtain new types. E.g., to obtain type of trees of integers: System F ω _ {\displaystyle {\underline {\omega }}} is generally not used on its own, but is useful to isolate the independent feature of type constructors.
(λP) Lambda-P In the λP system, also named λΠ, which is closely related to the LF Logical Framework, one has so called dependent types. These are types that are allowed to depend on terms. The crucial introduction rule of the system is
… excerpt ends here. Continue reading the full article.
