# Polymorphism in Typed Lambda Calculus

ABSTRACT GOES HERE

# Introduction

System F is a simple framework for describing universal computation. It is based on simply typed lambda calculus (stlc), but extends it with polymorphism in a structured way. Modern functional languages such as Haskell, MORE EXAMPLES are often based on a variant of System F.

To start simple, the identity function in System F is defined as

$\begin{array}{lcll} \mathbf{id} &:& \Delta \tau.\quad \tau \rightarrow \tau \\ &\triangleq& \Lambda \tau.\quad \lambda x : \tau.\quad x \end{array}$

If one is familiar with regular typed lambda calculus, one can guess already what is going on here. We can focus first on the last $$\lambda x : \tau.\quad x$$ part, which says that we care declaring a function of one argument (named $$x$$), which in turn evaluates to its argument. But then – in contrast to simply typed lambda calculus, $$\tau$$ is not a concrete type, but a type argument we must specify at application time. Type arguments are specified in the definition with an upper-case lambda, to distinguish it from arguments at the value level signified by the lower-case lambda.

Such a type-level argument is indicated at the type level by $$\Delta$$. In other words, if $$t : T$$ then

$\Lambda \tau.\quad t \quad:\quad \Delta \tau.\quad T$

As an example of a function taking two type-level arguments, the well-known constant function can be defined as

$\begin{array}{lcll} \mathbf{const} &:& \Delta \tau.\quad \Delta \sigma.\quad \tau \rightarrow \sigma \rightarrow \tau \\ &\triangleq& \Lambda \tau.\quad \Lambda \sigma.\quad \lambda a : \tau.\quad \lambda b : \sigma.\quad a \end{array}$

Similarly, a function to apply another function, which we’ll name $$\mathbf{funcall}$$ after its Lisp usage, may look like

$\begin{array}{lcll} \mathbf{funcall} &:& \Delta \tau.\quad \Delta \sigma.\quad (\tau \rightarrow \sigma) \rightarrow \tau \rightarrow \sigma \\ &\triangleq& \Lambda \tau.\quad \Lambda \sigma.\quad \lambda f : \tau \rightarrow \sigma.\quad \lambda x : \tau.\quad f x \end{array}$

The type signatures on the lambda parameters are mandatory, in line with what simply typed lambda calculus expects. The type at the top is redundant, given the types on the arguments. It is included merely for the benefit of the reader.

When applying functions with type arguments, the type-level arguments are specified in brackets, to differentiate them from value-level arguments. Specifying the type-level arguments is mandatory at the application site. We can look at the simplest application of the three functions we know to see it in practise.

$\begin{array}{lcll} \mathbf{appdemo} &:& \Delta \tau.\quad \Delta \sigma.\quad \tau \rightarrow \tau \\ &\triangleq& \Lambda \tau.\quad \Lambda \sigma.\quad \\ & & \mathbf{const}[\tau\rightarrow\tau][\sigma \rightarrow \sigma]\; \\ & & \quad (\mathbf{funcall}[\tau][\tau]\; (\mathbf{id} [\tau]))\;\\ & & \quad (\mathbf{id} [\sigma]) \end{array}$

# Simply Typed Lambda Calculus

Simply typed lambda calculus is a small framework for describing universal computation. Its most basic building block is the lambda abstraction. These abstractions can be used to encode a wide variety of concepts, but it is not without its problems. For example, we may have two combinators $$\mathbf{funcall}$$ and $$\mathbf{const}$$ defined as

$\begin{array}{lcll} \mathbf{funcall} &:& (\mathbb{Z} \rightarrow \mathbb{Z}) \rightarrow \mathbb{Z} \rightarrow \mathbb{Z} \\ &\triangleq& \lambda f : \mathbb{Z} \rightarrow \mathbb{Z}.\quad \lambda n : \mathbb{Z}.\quad f\; n \\ \mathbf{const} &:& \mathbb{B} \rightarrow \mathbb{Z} \rightarrow \mathbb{B} \\ &\triangleq& \lambda a : \mathbb{B}.\quad \lambda b : \mathbb{Z}.\quad a \end{array} \\$

and if we apply these as

For example, the next value in the Collatz sequence could be computed as

$\begin{array}{lclrl} \mathbf{collatz} &:& \mathbb{Z} \rightarrow \mathbb{Z} \\ &\triangleq& \lambda n : \mathbb{Z}. & \mathbf{ifZ} & (\mathbf{equal}\; n\; (\mathbf{div}\; n\; 2)) \\ & & & & (\mathbf{div}\; n\; 2) \\ & & & & (\mathbf{add}\; 1\; (\mathbf{mult}\; n\; 3)) \\ \end{array} \\$

where the types of most functions are the obvious candidates

$\begin{array}{lcl} \mathbf{add}, \mathbf{mult}, \mathbf{div} &:& \mathbb{Z} \rightarrow \mathbb{Z} \rightarrow \mathbb{Z} \\ \mathbf{equal} &:& \mathbb{Z} \rightarrow \mathbb{Z} \rightarrow \mathbb{B} \\ \end{array} \\$

but, crucially – and perhaps surprisingly – the type of $$\mathbf{ifZ}$$ is specialised as

$\begin{array}{lcl} \mathbf{ifZ} &:& \mathbb{B} \rightarrow \mathbb{Z} \rightarrow \mathbb{Z} \rightarrow \mathbb{Z} \\ \end{array} \\$

This is because in simply typed lambda calculus, every term must have a concrete type. In order to allow for coexistence of $$\mathbf{if}$$ constructs of different types, we must define them with different names. Besides the $$\mathbf{ifZ}$$ specialisation we’ve seen for integers, one may also want $$\mathbf{ifB}$$ for booleans, $$\mathbf{if}\Sigma$$ for characters, and so on.

One can imagine a construct that allows us to write generic functions that abstract over types, that would let us pass the type as the parameter to the function. Then we may be able to define $$\mathbf{collatz}$$ as

$\begin{array}{lclrl} \mathbf{collatz} &:& \mathbb{Z} \rightarrow \mathbb{Z} \\ &\triangleq& \lambda n : \mathbb{Z}. & \mathbf{if}\;[\mathbb{Z}] & (\mathbf{equal}\; n\; (\mathbf{div}\; n\; 2)) \\ & & & & (\mathbf{div}\; n\; 2) \\ & & & & (\mathbf{add}\; 1\; (\mathbf{mult}\; n\; 3)) \\ \end{array} \\$

passing the type $$\mathbb{Z}$$ as a type argument to $$\mathbf{if}$$, which now has type

$\begin{array}{lcl} \mathbf{if} &:& \Delta \tau.\quad \mathbb{B} \rightarrow \tau \rightarrow \tau \rightarrow \tau \\ \end{array} \\$

Thus, where we previously had to define a specific

$\begin{array}{lclrl} \mathbf{idZ} &:& \mathbb{Z} \rightarrow \mathbb{Z} \\ &\triangleq& \lambda n : \mathbb{Z}. & n \\ \end{array} \\$

we can now define

$\begin{array}{lclrl} \mathbf{id} &:& \Delta \tau.\quad \tau \rightarrow \tau \\ &\triangleq& \Lambda \tau.\quad \lambda n : \tau. & n \\ \end{array} \\$

#+END_COMMENT