Lambda cube

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 (): types that can bind terms, corresponding to dependent types. y-axis (): terms that can bind types, corresponding to polymorphism. z-axis (): types that can bind 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. 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 In System F (also named λ2 for the "second-order typed lambda calculus") there is another type of abstraction, written with a , that allows terms to depend on types, with the following rule: The terms beginning with a 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 fun x -> x of OCaml has type 'a -> 'a 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 . In System F 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 : , where "" informally means " is a type".