View source for Foundations of Functional Programming/Second-order λ-calculus

The second-order λ-calculus is a typed λ-calculus which extends the [[../Simply typed λ-calculus|simply typed λ-calculus]] with parametric polymorphism. One can write a single type which says, for example, that the identity function has type <math>\alpha \to \alpha</math>, for ''any'' type <math>\alpha</math>. This type is written <math>\forall \alpha (\alpha \to \alpha)</math>. This type is pronounced, "for all alpha, alpha to alpha." It means the same as the type <code>a -> a</code> in Haskell or ML. The piece of syntax <math>\forall \alpha</math> 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|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 ==

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.

<math>
\begin{array}{rcl}
\text{TypeVar}  &::=& \alpha\ |\ \beta\ |\ \cdots \\
\text{TypeExpr} &::=& \text{TypeVar} \\
                &|&   \text{TypeExpr} \to \text{TypeExpr} \\
                &|&   \forall\ \text{TypeVar}\ .\ \text{TypeExpr}
\end{array}
</math>

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 <math>\forall \alpha \forall \beta \forall \alpha (\beta \to \alpha)</math>, the <math>\alpha</math> in <math>\beta \to \alpha</math> 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 <math>\alpha</math> is one does not occur in the scope of a quantifier over <math>\alpha</math>.

If <math>\mathbf{A}</math> is a type expression which might have free occurrences of <math>\alpha</math>, and <math>\mathbf{B}</math> is a type expression, we define the substitution <math>\mathbf{A}[\alpha/\mathbf{B}]</math> as the result of replacing all free occurrences of <math>\alpha</math> in <math>\mathbf{A}</math> with <math>\mathbf{B}</math>, possibly renaming bound variables in <math>\mathbf{A}</math> if necessary to avoid variable capture.

== Implicitly typed second-order λ-calculus ==

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 ===

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

{| class="wikitable"
|-
| (axiom) || <math>\Gamma \vdash x : \mathbf{T}</math> || if <math>x : \mathbf{T}</math> is a member of <math>\Gamma</math>.
|-
| (→-elimination) || <math>\frac{\Gamma \vdash A : \mathbf{T} \to \mathbf{U} \ \ \ \Gamma \vdash B : \mathbf{T}}{\Gamma \vdash AB : \mathbf{U}}</math> || 
|-
| (→-introduction) || <math>\frac{\Gamma,x : \mathbf{T} \vdash A : \mathbf{U}}{\Gamma \vdash \lambda x. A : \mathbf{T} \to \mathbf{U}}</math> || 
|-
| (<math>\forall</math>-elimination) || <math>\frac{\Gamma \vdash A : \forall \alpha. \mathbf{T}}{\Gamma \vdash A : \mathbf{T}[\alpha/\mathbf{U}]}</math> ||
|-
| (<math>\forall</math>-introduction || <math>\frac{\Gamma \vdash A : \mathbf{T}}{\Gamma \vdash A : \forall \alpha. \mathbf{T}}</math> || if <math>\alpha</math> does not occur free in <math>\Gamma</math>.
|}

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 <math>\alpha</math> without making any special assumptions about <math>\alpha</math>, then the expression's type can be made polymorphic in <math>\alpha</math>.

=== Example type derivation ===

Now we give an example type derivation using the new rules. We will show that the function <math>A = \lambda x \lambda y. xy</math> has the polymorphic type <math>\forall \alpha \forall \beta ((\alpha \to \beta) \to \alpha \to \beta)</math>. This is the same as the similar derivation we did for the [[../Simply typed λ-calculus|simply typed λ-calculus]], except for two added steps at the end.

# <math>x : \alpha \to \beta, y : \alpha \vdash x : \alpha \to \beta</math> (axiom)
# <math>x : \alpha \to \beta, y : \alpha \vdash y : \alpha</math> (axiom)
# <math>x : \alpha \to \beta, y : \alpha \vdash xy : \beta</math> (→-elimination, from 1 and 2)
# <math>x : \alpha \to \beta \vdash \lambda y. xy : \alpha \to \beta</math> (→-introduction, from 3)
# <math>\vdash \lambda x \lambda y. xy : (\alpha \to \beta) \to \alpha \to \beta</math> (→-introduction, from 4)
# <math>\vdash \lambda x \lambda y. xy : \forall \beta ((\alpha \to \beta) \to \alpha \to \beta</math> (<math>\forall</math>-introduction, from 5)
# <math>\vdash \lambda x \lambda y. xy : \forall \alpha \forall \beta ((\alpha \to \beta) \to \alpha \to \beta</math> (<math>\forall</math>-introduction, from 6)

=== Properties of the calculus ===

* β-reduction preserves type: if <math>\Gamma \vdash A : \mathbf{T}</math> and and <math>A</math> β-reduces to <math>A'</math>, then <math>\Gamma \vdash A' : \mathbf{T}</math>.
* The [[../Strongly and weakly normalizing λ-calculi|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 [http://dl.acm.org/citation.cfm?id=859871 Wells (1993)].

== Explicitly typed second-order λ-calculus ==

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 <math>\forall \alpha. \mathbf{A}</math> as a ''function'' from types to values. For instance, the identity function <math>\text{id} : \forall \alpha.\ \alpha \to \alpha</math> is a function which takes a type <math>\mathbf{T}</math> and returns a function <math>\text{id}\ \mathbf{T} : \mathbf{T} \to \mathbf{T}</math>. 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:

<math>\text{id} = \Lambda \alpha\lambda x : \alpha.\ x</math>

=== Values and β-reduction ===

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

<math>
\begin{array}{rcl}
\text{Var} &::=& a\ |\ b\ |\ c\ |\ \cdots \\
\text{Expr} &::=& \text{Var} \\
            &|&   \text{Expr}\ \text{Expr} \\
            &|&   \text{Expr}\ \text{TypeExpr} \\
            &|&   \lambda\ \text{Var}\ :\ \text{TypeExpr}.\ \text{Expr} \\
            &|&   \Lambda\ \text{TypeVar}.\ \text{Expr} \\
\end{array}
</math>

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

* <math>(\lambda x. A)B \to_\beta A[x/B]</math>
* <math>(\Lambda \alpha. A)\mathbf{T} \to_\beta A[\alpha/\mathbf{T}]</math>

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

=== Type theory ===

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

{| class="wikitable"
|-
| (axiom) || <math>\Gamma \vdash x : \mathbf{T}</math> || if <math>x : \mathbf{T}</math> is a member of <math>\Gamma</math>.
|-
| (→-elimination) || <math>\frac{\Gamma \vdash A : \mathbf{T} \to \mathbf{U} \ \ \ \Gamma \vdash B : \mathbf{T}}{\Gamma \vdash AB : \mathbf{U}}</math> || 
|-
| (→-introduction) || <math>\frac{\Gamma,x : \mathbf{T} \vdash A : \mathbf{U}}{\Gamma \vdash (\lambda x : \mathbf{T}. A) : \mathbf{T} \to \mathbf{U}}</math> || 
|-
| (<math>\forall</math>-elimination) || <math>\frac{\Gamma \vdash A : \forall \alpha. \mathbf{T}}{\Gamma \vdash A\mathbf{U} : \mathbf{T}[\alpha/\mathbf{U}]}</math> ||
|-
| (<math>\forall</math>-introduction || <math>\frac{\Gamma \vdash A : \mathbf{T}}{\Gamma \vdash (\Lambda \alpha. A) : \forall \alpha. \mathbf{T}}</math> || if <math>\alpha</math> does not occur free in <math>\Gamma</math>.
|}

=== Example type derivation ===

Now we repeat our usual example, giving a type derivation using the new rules. We will show that the function <math>A = \Lambda \alpha \Lambda \beta \lambda x : \alpha \lambda y : \beta. xy</math> has the polymorphic type <math>\forall \alpha \forall \beta ((\alpha \to \beta) \to \alpha \to \beta)</math>.

# <math>x : \alpha \to \beta, y : \alpha \vdash x : \alpha \to \beta</math> (axiom)
# <math>x : \alpha \to \beta, y : \alpha \vdash y : \alpha</math> (axiom)
# <math>x : \alpha \to \beta, y : \alpha \vdash xy : \beta</math> (→-elimination, from 1 and 2)
# <math>x : \alpha \to \beta \vdash \lambda y : \alpha. xy : \alpha \to \beta</math> (→-introduction, from 3)
# <math>\vdash \lambda x : \alpha \to \beta \lambda y : \alpha. xy : (\alpha \to \beta) \to \alpha \to \beta</math> (→-introduction, from 4)
# <math>\vdash \Lambda \beta \lambda x \lambda y. xy : \forall \beta ((\alpha \to \beta) \to \alpha \to \beta</math> (<math>\forall</math>-introduction, from 5)
# <math>\vdash \Lambda \alpha \Lambda \beta \lambda x \lambda y. xy : \forall \alpha \forall \beta ((\alpha \to \beta) \to \alpha \to \beta</math> (<math>\forall</math>-introduction, from 6)

To show how application of <math>\forall</math>-elimination works, we show that <math>A\gamma\delta : (\gamma \to \delta) \to \gamma \to \delta</math>:

# <math>\vdash \Lambda \alpha \Lambda \beta \lambda x \lambda y. xy : \forall \alpha \forall \beta ((\alpha \to \beta) \to \alpha \to \beta</math> (from previous derivation)
# <math>\vdash (\Lambda \alpha \Lambda \beta \lambda x \lambda y. xy)\gamma : \forall \beta ((\gamma \to \beta) \to \gamma \to \beta</math> (<math>\forall</math>-elimination, from 1)
# <math>\vdash (\Lambda \alpha \Lambda \beta \lambda x \lambda y. xy)\gamma\delta : (\gamma \to \delta) \to \gamma \to \delta</math> (<math>\forall</math>-elimination, from 2)


=== Properties of the calculus ===

* β-reduction preserves type: if <math>\Gamma \vdash A : \mathbf{T}</math> and and <math>A</math> β-reduces to <math>A'</math>, then <math>\Gamma \vdash A' : \mathbf{T}</math>.
* The [[../Strongly and weakly normalizing λ-calculi|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.
{{CourseCat}}