Foundations of Functional Programming/The λ-cube

The λ-cube is a set of eight type theories which combine three different type system features in all the possible ways. These three features are:

  • Values depending on types, also known as polymorphic types.
  • Types depending on types, also known as type constructors.
  • Types depending on values, also known as dependent types.
The λ-cube. Direction of each arrow is direction of inclusion.

The fourth natural item in this list, namely values depending on values, is a feature of all λ-calculi; any language with functions has this feature. Indeed, we can see each of these three type system features as a way of extending the notion of a function:

  • Polymorphically typed expressions are functions from types to values.
  • Type constructors are functions from types to types.
  • Dependent types are functions from values to types.
  • And, of course, functions from values to values are a feature of all λ-calculi and have no special name.

The description of polymorphically typed expressions as functions from types to values may sound unfamiliar to the ear. However, it is exactly how they are described in the second-order λ-calculus. An expression of type has the form , and to instantiate it to an expression of type you write .

This syntax makes it clear how polymorphically typed values can be understood as functions from types to values. A polymorphically typed value takes a type as an argument, and returns an instance of itself instantiated to that type.

Basic structure of the λ-cubeEdit

The basic structure of the λ-cube is explained by the following table:

Polymorphic types? Type constructors? Dependent types?
λ→ (explicitly simply typed λ-calculus) No No No
λ2 (explicitly typed second-order λ-calculus) Yes No No
λω No Yes No
λP No No Yes
λω Yes Yes No
λP2 Yes No Yes
λPω No Yes Yes
λPω (calculus of constructions) Yes Yes Yes

Two of these systems are familiar. λ→ is (modulo minor syntactic variations) the explicitly simply typed λ-calculus. λ2 is (modulo minor syntactic variations) the explicitly typed second-order λ-calculus. λPω, the fullest system in the λ-cube, is also called the "calculus of constructions."

SyntaxEdit

Unlike the systems we have considered so far, the systems of the λ-cube make no syntactic distinction between types and values. There is one kind of expression, encompassing both type and value expressions. This corresponds to the fact that in the systems of the λ-cube, types are in essence a special kind of value. Henceforth we will use the term "value" in a way which is inclusive of types.

The systems of the λ-cube also introduce a distinction between variables and constants which was not present in the systems we have considered so far. This distinction corresponds roughly to the same distinction in programming languages. We will denote variables by   as before, and we will denote constants by ad hoc labels; but when we need to refer to an arbitrary constant, we will use bold lower case letters  . We continue to use   to denote arbitrary expressions.

The syntax is as follows:

 

This syntax should be somewhat familiar. In relation to the explicitly typed second-order λ-calculus, the λ-abstractions in this syntax serve both the role of the λ-abstractions and the Λ-abstractions of the explicitly typed second-order λ-calculus. That is, a λ-abstraction can denote a function which takes either a non-type value, or a type, as an argument.

Dependent function type syntaxEdit

The syntax   is a generalization of the syntax   for a function type. This generalized syntax is needed to express dependent types. The syntax's special meaning arises when   occurs free in  . In this case,   expresses the type of a function which takes a value   of type   and produces a value of type  , where   is an expression denoting a type which depends on the value of  .

Let us give a simple example of this syntax being used. Suppose   is a type constructor for fixed length vectors: so  , where   is a type and   is a natural number, denotes the type of vectors of length   with elements of type  .

Now consider a function   which takes an integer   and a natural number  , and produces a vector consisting of   copies of  . Such a function has type

 

In this example we have used the syntax   as a shorthand for  , where   does not occur free in  . We will continue to do this. That is, in general,

 

is shorthand for

 ,

where   is a variable which does not occur free in  .

We will close this topic by noting that in most presentations of the λ-cube, the syntax   is used instead of  . The former syntax is motivated by the analogy between dependent function types and dependent Cartesian products in higher mathematics. We prefer our syntax for its greater familiarity from a programming perspective.

SortsEdit

The λ-cube is the first place we encounter the notion of "sorts." A sort is best understood, in simple terms, as a "type of types." In the λ-cube, where types are a kind of value, types generally have types, in the sense that they can appear on the left hand side of typing judgments.

We shall denote the "type of types" by  .   is the simplest example of a sort. (A more common notation for this sort is  , but we choose our notation for greater familiarity, and for its use in programming languages such as Idris.)

So far, I have given no reason to think that there are any sorts under than  . If sorts are types of types, and   is the type of types, why would there be any sorts other than  ?

The reason that the systems of the λ-cube (and many other λ-calculi) have more than one sort is to resolve the following problem. What is the type of  ? It is natural to say that  , the type of types, is a type, and that therefore  . The problem is that the assumption that   gives rise to paradoxes such as Girard's paradox which render λ-calculi logically inconsistent.

For this reason, many λ-calculi, including the systems of the λ-cube, come up with an additional sort, which we will call  , and stipulate that  , rather than  . This choice preserves logical consistency. (A more common notation for   is  .)

Another word on notation. We will also denote   by  , and systems such as Martin-Löf type theory have an infinite hierarchy of sorts  . That is the reason for writing the sort of   as  .

In the systems of the λ-cube, there are only two sorts:   (a.k.a.  ) and  . In the systems of the λ-cube,   does not belong to any sort; it does not appear on the left hand side of any typing judgments.

Syntactically speaking, sorts are constants. The two sorts are the only constants we will specifically need to deal with; if we didn't need sorts, we could formulate the systems of the λ-cube without constants, as we did for previous calculi.

Declarations and contextsEdit

Declarations have the same syntax as before. However, contexts are defined differently in the systems of the λ-cube than in the systems we have seen so far.

In the systems we have seen so far, contexts are sets of declarations. Sets are unordered collections. In the systems of the λ-cube, contexts are sequences -- ordered finite collections -- of declarations. We denote a context by a comma-separated list of its constituent declarations. An empty context is denoted by whitespace; so for example,   means that the empty context entails that  .

The reason for this is that in the systems of the λ-cube, often a declaration is required for another declaration to make sense. The simplest example is that for the typing judgment   to make sense, where   is a variable standing for a type and   a variable standing for an ordinary value, one must have  . A context consisting of the single declaration   is not valid; however, the context   is valid. On the other hand, if we swap the order of the declarations, the resulting context   is invalid, because at the occurrence of the declaration   we don't know that   is a type.

In the systems we considered before, this particular necessity did not exist because there was a syntactic distinction between types and values, and so you could tell just by looking at it that a variable represented a type.

In greater generality, for a variable to occur on the right hand side of a statement, it must have a type declared in the context governing the statement. For a declaration   which occurs within a context  , the context governing it is the part of   which comes before  .

Type theoryEdit

The rules of β-reduction in all systems of the λ-cube are as they have been before.

The different systems of the λ-cube differ in their rules defining valid type entailments. We will begin by giving the rules which are common to all of the systems. In the following rules,   denotes any sort (one of   or  ).

(axiom)  
(start)  
(weakening)  
(application)  
(abstraction)  
(conversion)  

β-conversionEdit

The final rule in the above table, the conversion rule, uses a symbol we have not seen before:  , which stands for β-convertibility. We say that two expressions are β-convertible when they can be connected by a series of (forwards or backwards) β-reduction steps. More precisely,   is the smallest equivalence relation which holds between two expressions if one is β-reducible to another. This mathematical definition needs more unpacking.

In mathematics, a "binary relation" (or just a "relation") on a set   is a set   of ordered pairs   of elements of  . Given elements  , we typically write   to mean that  .   means that   is related to   by the relation  .

A simple example of a relation is the relation   on the set of natural numbers,  .  , as a relation in the mathematical sense, is the set of pairs   of natural numbers such that   is less than or equal to  .

An "equivalence relation" on a set   is a relation   on   satisfying the following axioms:

  • Reflexivity: For all  ,  .
  • Symmetry: For all  , if   then  .
  • Transitivity: For all  , if   and  , then  .

A simple example of an equivalence relation is the identity relation on any set  : that is, the relation which an object bears only to itself. A more complex example of an equivalence relation is the relation on natural numbers of being congruent modulo seven: i.e., of having the same remainder when divided by seven.

The relation  , called β-convertibility, is the least equivalence relation on the set of expressions of the λ-cube such that if an expression   is β-reducible to an expression  , then  . More precisely,   is the intersection (in the set-theoretic sense) of all equivalence relations   on λ-cube expressions such that if   β-reduces to   then  . It can be proven that this intersection is itself an equivalence relation.

System-specific rulesEdit

The systems of the λ-cube differ in what kinds of functions they allow. The kinds of functions under consideration are: functions from values to values; functions from types to values; functions from types to types; and functions from values to types. For each of these four types of functions, there is a rule to the effect that functions of that type exist.

For example, the rule stating that functions from values to values exist reads as follows:

 

The rule stating that functions from types to values exist reads as follows:

 

The difference between these rules is the sort of  ; in the former rule,   is a   (a type of regular values), and in the latter rule,   is a   (a type of types).

The general pattern is that   is a   for functions taking regular values, and a   for functions taking types. Similarly,   is a   for functions producing regular values, and a   for functions producing types. The sort of the resulting function type is the same as the sort of  .

Now we describe the general pattern formally. Let   and   be sorts. The "  rule" is the rule:

 

The systems of the λ-cube are differentiated by which of the   rules they have. The following table describes the   rules of each system, and the feature each rule provides:

Feature: Ordinary functions Polymorphic types Type constructors Dependent types
Rule:        
λ→ (explicitly simply typed λ-calculus) Yes No No No
λ2 (explicitly typed second-order λ-calculus) Yes Yes No No
λω Yes No Yes No
λP Yes No No Yes
λω Yes Yes Yes No
λP2 Yes Yes No Yes
λPω Yes No Yes Yes
λPω (calculus of constructions) Yes Yes Yes Yes

Properties of the calculiEdit

All systems of the λ-cube have the following properties:

  • β-reduction preserves type: if   and and   β-reduces to  , then  .
  • The strong normalization property holds, so that all functions typeable in the calculus halt, and the calculus is not Turing complete.
  • The problems of type checking and typability are decidable.
  • Every value expression has at most one type, up to β-conversion. More precisely, for any expression   and any context  , if two expressions   and   are such that   and  , then  .