Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of GraphSearch.
Concept
Lambda cube
Summary
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".
Official source
About this result
This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.