PFPL Chapter 16 System F of Polymorphic Types

Posted on In Disqus:

Please refer this link from page 141 to 149.

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.