Someone's Intermediate Representation

0%

# From Monomorphic to Polymorphic

So far we are dealing with monomorphic languages since every expression has a unique type. If we want a same behavior over different types, different programs will have to be created.

The expression patterns codify generic (type-independent) behaviors that are shared by all instances of the pattern. Such generic expressions are polymorphic.

# Polymorphic Abstraction

Language F is a variant of T in which we eliminate the type of natural numbers.

## Syntax Table

\begin{aligned} \text{Typ}&&\tau&&::=&&t&&t&&\text{variable}\\ &&&&&&\to(\tau_1;\tau_2)&&\tau_1\to\tau_2&&\text{function}\\ &&&&&&\forall(t.\tau)&&\forall(t.\tau)&&\text{polymorphic}\\ \text{Exp}&&e&&::=&&x&&x\\ &&&&&&\lambda\lbrace\tau\rbrace(x.e)&&\lambda(x:\tau)e&&\text{abstraction}\\ &&&&&&\text{ap}(e_1;e_2)&&e_1(e_2)&&\text{application}\\ &&&&&&\Lambda(t.e)&&\Lambda(t)e&&\text{type abstraction}\\ &&&&&&\text{App}\lbrace\tau\rbrace(e)&&e\lbrack\tau\rbrack&&\text{type application} \end{aligned}

Type abstraction $\Lambda(t.e)$ defines a generic/polymorphic function with type variable $t$ for unspecified type within $e$.

Universal type $\forall(t.\tau)$ classifies polymorphic functions.

Type application $\text{App}\lbrace\tau\rbrace(e)$ applies a polymorphic function to a specific type.

## Statics

Statics consists of two judgment forms:

• Type formation judgment $\Delta\vdash\tau\text{ type}$
• Typing judgment $\Delta\space\Gamma\vdash e:\tau$

Hypotheses $\Delta$ have the form $t\text{ type}$ and hypotheses $\Gamma$ have the form $x:\tau$.

### Type Formation Rules

$$\displaylines{\dfrac{}{\Delta,t\text{ type}\vdash t\text{ type}}\\ \dfrac{\Delta\vdash\tau_1\text{ type}\phantom{“”}\Delta\vdash\tau_2\text{ type}}{\Delta\vdash\to(\tau_1;\tau_2)\text{ type}}\\ \dfrac{\Delta,t\text{ type}\vdash\tau\text{ type}}{\Delta\vdash\forall(t.\tau)\text{ type}}}$$

### Typing Rules

$$\displaylines{\dfrac{}{\Delta\space\Gamma,x:\tau\vdash x:\tau}\\ \dfrac{\Delta\vdash\tau_1\text{ type}\phantom{“”}\Delta\space\Gamma,x:\tau_1\vdash e:\tau_2}{\Delta\space\Gamma\vdash\lambda\lbrace\tau_1\rbrace(x.e):\to(\tau_1;\tau_2)}\\ \dfrac{\Delta\space\Gamma\vdash e_1:\to(\tau_2;\tau)\phantom{“”}\Delta\space\Gamma\vdash e_2:\tau_2}{\Delta\space\Gamma\vdash\text{ap}(e_1;e_2):\tau}\\ \dfrac{\Delta,t\text{ type }\space\Gamma\vdash e:\tau}{\Delta\space\Gamma\vdash\Lambda(t.e):\forall(t.\tau)}\\ \dfrac{\Delta\space\Gamma\vdash e:\forall(t.\tau’)\phantom{“”}\Delta\vdash\tau\text{ type}}{\Delta\space\Gamma\vdash\text{App}\lbrace\tau\rbrace(e):\lbrack\tau/t\rbrack\tau’}}$$

### Regularity Lemma

If $\Delta\space\Gamma\vdash e:\tau$ and $\Delta\vdash\tau_i\text{ type}$ for each assumptions $x_i:\tau_i$ in $\Gamma$, then $\Delta\vdash\tau\text{ type}$.

### Substitution Lemma

1. If $\Delta,t\text{ type}\vdash\tau’\text{ type}$ and $\Delta\vdash\tau\text{ type}$, then $\Delta\vdash\lbrack\tau/t\rbrack\tau’\text{ type}$.
2. If $\Delta,t\text{ type }\space\Delta\vdash e’:\tau’$ and $\Gamma\vdash\tau\text{ type}$, then $\Delta\space\lbrack\tau/t\rbrack\Gamma\vdash\lbrack\tau/t\rbrack e’:\lbrack\tau/t\rbrack\tau’$.
3. If $\Delta\space\Gamma,x:\tau\vdash e’:\tau’$ and $\Delta\space\Gamma\vdash e:\tau$, then $\Delta\space\Gamma\vdash\lbrack e/x\rbrack e’:\tau’$.

### Examples on Polymorphic Types

Polymorphic identity function $I$ can be written as $\Lambda(t)\lambda(x:t)x$ with polymorphic type $\forall(t.t\to t)$.

Instances of the polymorphic identity function are written as $I\lbrack\tau\rbrack$ and have type $\tau\to\tau$.

## Dynamics

$$\displaylines{\dfrac{}{\lambda\lbrace\tau\rbrace(x.e)\text{ val}}\\ \dfrac{}{\Lambda(t.e)\text{ val}}\\ \dfrac{\lbrack e_2\text{ val}\rbrack}{\text{ap}(\lambda\lbrace\tau_1\rbrace(x.e);e_2)\longmapsto\lbrack e_2/x\rbrack e}\\ \dfrac{e_1\longmapsto e_1’}{\text{ap}(e_1;e_2)\longmapsto\text{ap}(e_1’;e_2)}\\ \Big\lbrack\dfrac{e_1\text{ val}\phantom{“”}e_2\longmapsto e_2’}{\text{ap}(e_1;e_2)\longmapsto\text{ap}(e_1;e_2’)}\Big\rbrack\\ \dfrac{}{\text{App}\lbrace\tau\rbrace(\Lambda(t.e))\longmapsto\lbrack\tau/t\rbrack e}\\ \dfrac{e\longmapsto e’}{\text{App}\lbrace\tau\rbrace(e)\longmapsto\text{App}\lbrace\tau\rbrace(e’)}}$$

### Canonical Forms Lemma

Suppose $e:\tau$ and $e\text{ val}$, then

1. If $\tau=\to(\tau_1;\tau_2)$, then $e=\lambda\lbrace\tau_1\rbrace(x.e_2)$ with $x:\tau_1\vdash e_2:\tau_2$.
2. If $\tau=\forall(t.\tau’)$, then $e=\Lambda(t.e’)$ with $t\text{ type}\vdash e’:\tau’$.

### Preservation Theorem

If $e:\tau$ and $e\longmapsto e’$, then $e’:\tau$.

### Progress Theorem

If $e:\tau$, then either $e\text{ val}$ or $\exists e’,e\longmapsto e’$.

# Polymorphic Definability

F is very expressive. The definability is most naturally expressed using definitional equality, which is the least congruence with the axioms:
$$\displaylines{\dfrac{\Delta\space\Gamma,x:\tau_1\vdash e_2:\tau_2\phantom{“”}\Delta\space\Gamma\vdash e_1:\tau_1}{\Delta\space\Gamma\vdash(\lambda(x:\tau_1)e_2)(e_1)\equiv\lbrack e_1/x\rbrack e_2:\tau_2}\\ \dfrac{\Delta,t\text{ type }\space\Gamma\vdash e:\tau\phantom{“”}\Delta\vdash\rho\text{ type}}{\Delta\space\Gamma\vdash\Lambda(t)e\lbrack\rho\rbrack\equiv\lbrack\rho/t\rbrack e:\lbrack\rho/t\rbrack\tau}}$$

## Product Type

The nullary product, or unit, type is definable in F as
\begin{aligned} \text{unit}&\triangleq\forall(t.t\to t)\\ \langle\rangle&\triangleq\Lambda(r)\lambda(x:r)x \end{aligned}
Binary products are definable in F by
\begin{aligned} \tau_1\times\tau_2&\triangleq\forall(r.(\tau_1\to\tau_2\to r)\to r)\\ \langle e_1,e_2\rangle&\triangleq\Lambda(r)\space \lambda(x:\tau_1\to\tau_2\to r)\space x(e_1)(e_2)\\ e\cdot\text{l}&\triangleq e\lbrack\tau_1\rbrack(\lambda(x:\tau_1)\space \lambda(y:\tau_2)\space x)\\ e\cdot\text{r}&\triangleq e\lbrack\tau_2\rbrack(\lambda(x:\tau_1)\space \lambda(y:\tau_2)\space y) \end{aligned}
The definitional equalities are derivable in F from definition
$$\langle e_1,e_2\rangle\cdot\text{l}\equiv e_1:\tau_1\\ \langle e_1,e_2\rangle\cdot\text{r}\equiv e_2:\tau_2$$

## Sum Type

The nullary sum, or void, type is definable in F as
\begin{aligned} \text{void}&\triangleq\forall(r.r)\\ \text{case }e\lbrace\space\rbrace&\triangleq e\lbrack\rho\rbrack \end{aligned}
Binary sums are defined in F by
\begin{aligned} \tau_1+\tau_2&\triangleq\forall(r.(\tau_1\to\tau)\to(\tau_2\to\tau)\to\tau)\\ \text{l}\cdot e&\triangleq\Lambda(r)\space \lambda(x:\tau_1\to r)\space \lambda(y:\tau_2\to r)\space x(e)\\ \text{r}\cdot e&\triangleq\Lambda(r)\space \lambda(x:\tau_1\to r)\space \lambda(y:\tau_2\to r)\space y(e)\\ \text{case }e\lbrace\text{l}\cdot x_1\hookrightarrow e_1\shortmid\text{r}\cdot x_2\hookrightarrow e_2\rbrace&\triangleq e\lbrack\rho\rbrack(\lambda(x_1:\tau_1)\space e_1)(\lambda(x_2:\tau_2)\space e_2) \end{aligned}
The definitional equalities are definable in F from definition
$$\text{case l}\cdot d_1\lbrace\text{l}\cdot x_1\hookrightarrow e_1\shortmid\text{r}\cdot x_2\hookrightarrow e_2\rbrace\equiv\lbrack d_1/x_1\rbrack e_1:\rho\\ \text{case r}\cdot d_2\lbrace\text{l}\cdot x_1\hookrightarrow e_1\shortmid\text{r}\cdot x_2\hookrightarrow e_2\rbrace\equiv\lbrack d_2/x_2\rbrack e_2:\rho$$

## Church Numeral Encoding

The natural numbers under lazy interpretation are definable in F.

If we have an iterator with a following definition as
$$\dfrac{e_0:\text{nat}\phantom{“”}e_1:\tau\phantom{“”}x:\tau\vdash e_2:\tau}{\text{iter}\lbrace e_1;x.e_2\rbrace(e_0):\tau}$$
then we can define a function of type $\text{nat}\to\forall(t.t\to(t\to t)\to t)$, yields a polymorphic function that have an initial z of type t and a transformation s of type t -> t.

In this way we may define the natural numbers in F by
\begin{aligned} \text{nat}&\triangleq\forall(t.t\to(t\to t)\to t)\\ \text{z}&\triangleq\Lambda(t)\space \lambda(z:t)\space \lambda(s:t\to t)\space z\\ \text{s}(e)&\triangleq\Lambda(t)\space \lambda(z:t)\space \lambda(s:t\to t)\space s(e\lbrack t\rbrack(z)(s))\\ \text{iter}\lbrace e_1;x.e_2\rbrace&\triangleq e_0\lbrack\tau\rbrack(e_1)(\lambda(x:\tau)\space e_2) \end{aligned}

## SKI Combinator

The K combinator have a relatively easier definition since its dynamics has form like
$$\dfrac{a_1\text{ comb}\phantom{“”}a_2\text{ comb}}{\text{k }a_1\space a_2\equiv a_1}$$
Then polymorphic definition of K can be
$$\text{k}\triangleq\Lambda(t_0)\Lambda(t_1)\lambda(e_0:t_0)\lambda(e_1:t_1)e_0:\forall (t_0.\forall(t_1.t_0\to t_1\to t_0))$$
For S combinator the dynamics goes like
$$\dfrac{a_1\text{ comb}\phantom{“”}a_2\text{ comb}\phantom{“”}a_3\text{ comb}}{\text{s}\space a_1\space a_2\space a_3\equiv(a_1\space a_3)(a_2\space a_3)}$$
Then polymorphic definition of S can be
$$\text{S}\triangleq\Lambda(t_0)\space \Lambda(t_1)\space \Lambda(t_2)\space\lambda(e_0:t_0\to t_1\to t_2)\space \lambda(e_1:t_0\to t_1)\space \lambda(e_2:t_0)\space(e_0(e_2))(e_1(e_2))\\:\forall(t_0.\forall(t_1.\forall(t_2.(t_0\to t_1\to t_2)\to(t_0\to t_1)\to t_0\to t_2)))$$

## Church Boolean

The church boolean in F can be defined as
\begin{aligned} \text{bool}&\triangleq\forall(t.t\to t\to t)\\ \text{true}&\triangleq\Lambda(t)\space \lambda(x:t)\space \lambda(y:t)\space x\\ \text{false}&\triangleq\Lambda(t)\space \lambda(x:t)\space \lambda(y:t)\space y\\ \text{if }e\text{ then }e_0\text{ else }e_1&\triangleq e\lbrack\rho\rbrack(e_0)(e_1) \end{aligned}

## Inductive Natural Number List

The natural number list by inductive type in F can be defined as
\begin{aligned} \text{natlist}&\triangleq\forall(t.t\to(\text{nat}\to t\to t)\to t)\\ \text{nil}&\triangleq\Lambda(t)\space \lambda(n:t)\space \lambda(c:\text{nat}\to t\to t)\space n\\ \text{cons}(e_0;e_1)&\triangleq\Lambda(t)\space \lambda(n:t)\space \lambda(c:\text{nat}\to t\to t)\space c(e_0)(e_1\lbrack t\rbrack(n)(c))\\ \text{rec }e\lbrace\text{nil}\hookrightarrow e_0\shortmid\text{cons}(x;y)\hookrightarrow e_1\rbrace&\triangleq e\lbrack\rho\rbrack(e_0)((\lambda(x:\rho)\space \lambda(y:\text{nat}\to t\to t)\space e_1)) \end{aligned}

## Arbitrary Inductive Type

For inductive type with a general form $\mu(t.\tau)$ in F, the polymorphic type can be defined as
\begin{aligned} \mu(t.\tau)&\triangleq\forall(t.(\tau\to t)\to t)\\ \text{fold}\lbrace\rbrace(e)&\triangleq\Lambda(t)\space\lambda(f:\tau\to t)\space f(\text{map}\lbrace t.\tau\rbrace(y.y\lbrack t\rbrack(f))(e))\\ \text{rec}\lbrace.\rbrace(x.e’;e)&\triangleq e\lbrack\rho\rbrack(\lambda(x:\tau)\space e’) \end{aligned}

# Parametricity Overview

Polymorphic types severely constrains the behaviors of the elements. We may prove useful theorems about expression knowing only its type, without looking at its code.

If $i :\forall(t.t\to t)$, then it is the identity function.

If $c:\forall(t.t\to t\to t)$, then it can be either

• $\Lambda(t)\lambda(x:t)\lambda(y:t)x$
• $\Lambda(t)\lambda(x:t)\lambda(y:t)y$

## Parametricity and Free Theorems

Parametricity properties are properties of F that a program of F can be proved by knowing only its type.

Sometimes such properties are called free theorems since they come from typing for free, without touching code.

## Parametricity Theorem

An example on $i:\forall(t.t\to t)$ in F may help understand how things work.

$i$ in F enjoys the property: $\forall \tau\text{ type}$ and any property $\mathcal P$ of $\tau$, then if $\mathcal P$ holds of $x:\tau$, then $\mathcal P$ holds of $i\lbrack\tau\rbrack(x)$.

It suffices to fix $x_0:\tau$ and consider property $\mathcal{P}_{x_0}$ that holds of $y:\tau$ iff $y$ is equivalent to $x_0$.

By proof by contradiction we can easily see that $x_0$ is equivalent to $y$ and $i\lbrack\tau\rbrack$ is the identity function $\lambda(x:\tau)x$.

For a list with elements with type $t$, the list has type $t\text{ list}$.

$f:\forall(t.t\text{ list}\to t\text{ list})$ is an arbitrary function and the elements of $f\lbrack\tau\rbrack(l)$ are a subset of those of $l$.

Fix $\tau$ and $l_0:\tau\text{ list}$. Define $\mathcal{P}_{l_0}$ to hold of $e:\tau$ iff $e$ is among the elements of $l_0$.

By parametricity $f$ must preserve $\mathcal{P}$, then the input elements and output elements must meet.

In this way the set of elements of $f\lbrack\tau\rbrack(l_0)$ is a subset of $l_0$. Thus $f$ cannot transform elements of input in any way.