PFPL Chapter 16 System F of Polymorphic Types
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
- 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}$.
- 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’$.
- 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
- 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$.
- 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.