Foundations of Functional Programming/Second-order λ-calculus

The second-order λ-calculus is a typed λ-calculus which extends the simply typed λ-calculus with parametric polymorphism. One can write a single type which says, for example, that the identity function has type , for any type . This type is written . This type is pronounced, "for all alpha, alpha to alpha." It means the same as the type a -> a in Haskell or ML. The piece of syntax is called a "type quantifier."

Like the simply typed λ-calculus, the second-order λ-calculus comes in two flavors: an implicitly typed flavor, and an explicitly typed flavor. Neither flavor is Turing complete. Type checking is undecidable in the implicitly typed calculus, but decidable in the explicitly typed calculus.

The Hindley-Milner type system is another polymorphic type system which addresses the shortcomings of the implicitly typed second-order λ-calculus that we have just mentioned (namely, Turing incompleteness and undecidability of type checking). It is an implicitly typed, polymorphic type system which is Turing complete, and which enjoys decidable type checking.

Type syntax

edit

Both flavors of the second-order λ-calculus have the same syntax for types, which just augments the syntax of the simply typed λ-calculus with type quantifiers.

 

As usual, parentheses can be used to disambiguate scope. When there are nested quantifiers over the same variable, variables bind to the innermost quantifier. E.g., in  , the   in   binds to the innermost quantifier, not the outermost quantifier.

We distinguish between free occurrences and bound occurrences of type variables, much as we distinguished between free and bound occurrences of variables in the untyped λ-calculus. A free occurrence of a type variable   is one does not occur in the scope of a quantifier over  .

If   is a type expression which might have free occurrences of  , and   is a type expression, we define the substitution   as the result of replacing all free occurrences of   in   with  , possibly renaming bound variables in   if necessary to avoid variable capture.

Implicitly typed second-order λ-calculus

edit

The definitions of value expressions, statements, declarations, and contexts are the same for the implicitly typed second-order λ-calculus as for the implicitly simply typed λ-calculus.

Type theory

edit

The following rules define the valid type entailments in the implicitly typed calculus:

(axiom)   if   is a member of  .
(→-elimination)  
(→-introduction)  
( -elimination)  
( -introduction   if   does not occur free in  .

The new rules are the rules for the quantifier. The first new rule allows us to instantiate polymorphic types; it says that if an expression has a polymorphic type, then it has every instance of that type.

The second new rule allows us to prove that an expression has a polymorphic type. The idea is that if we can derive that an expression has a type involving   without making any special assumptions about  , then the expression's type can be made polymorphic in  .

Example type derivation

edit

Now we give an example type derivation using the new rules. We will show that the function   has the polymorphic type  . This is the same as the similar derivation we did for the simply typed λ-calculus, except for two added steps at the end.

  1.   (axiom)
  2.   (axiom)
  3.   (→-elimination, from 1 and 2)
  4.   (→-introduction, from 3)
  5.   (→-introduction, from 4)
  6.   ( -introduction, from 5)
  7.   ( -introduction, from 6)

Properties of the calculus

edit
  • β-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 undecidable (though they are semidecidable, i.e. computably enumerable). See Wells (1993).

Explicitly typed second-order λ-calculus

edit

In the case of the simply typed λ-calculi, the differences between the implicitly typed and explicitly typed versions were not very large. The differences between the implicitly and explicitly typed versions of second-order λ-calculus are more substantial.

In the explicitly typed calculus, we think of a value of type   as a function from types to values. For instance, the identity function   is a function which takes a type   and returns a function  . Such functions from types to values are denoted by "Λ-abstractions." For example, here is the definition of the polymorphic identity function in the explicitly typed calculus:

 

Values and β-reduction

edit

The syntax for types has already been described. The new syntax for values is as follows:

 

The rules for β-reduction are now expanded to include rules for β-reducing Λ-abstractions:

  •  
  •  

As before, one can β-reduce an expression by performing either of the above transformations on any of its subexpressions.

Type theory

edit

Here are the rules defining the valid type entailments in the explicitly typed calculus:

(axiom)   if   is a member of  .
(→-elimination)  
(→-introduction)  
( -elimination)  
( -introduction   if   does not occur free in  .

Example type derivation

edit

Now we repeat our usual example, giving a type derivation using the new rules. We will show that the function   has the polymorphic type  .

  1.   (axiom)
  2.   (axiom)
  3.   (→-elimination, from 1 and 2)
  4.   (→-introduction, from 3)
  5.   (→-introduction, from 4)
  6.   ( -introduction, from 5)
  7.   ( -introduction, from 6)

To show how application of  -elimination works, we show that  :

  1.   (from previous derivation)
  2.   ( -elimination, from 1)
  3.   ( -elimination, from 2)


Properties of the calculus

edit
  • β-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.