PFPL Chapter 14 Generic Programming

Posted on In Disqus:

This part is not shown on PFPL preview version.

Introduction

Many programs are instances of a pattern in a particular situation. Sometimes types determine the pattern by a technique called (typed) generic programming.

Example: the natural number definition in Chapter 9 defines pattern of recursion on values of an inductive type, which is expressed as a generic program.

Consider a function $f:\rho\to\rho’$, we wish to extend $f$ to a transformation from type $\lbrack \rho/t\rbrack\tau$ to $\lbrack \rho/t\rbrack\tau$ by applying $f$ to various spots in the inputs, where $\rho$ occurs to obtain a value of type $\rho’$, leaving the rest of data structure alone.

$\tau$ can be $\text{nat}\times t$ and $f$ can be extended to $\text{nat}\times\rho\to\text{nat}\times\rho’$ that transform $\langle a,b\rangle$ to $\langle a,f(b)\rangle$.

Ambiguity and Type Operator

Ambiguity arises in many-one nature of substitution. A type can have the form $\lbrack\rho/t\rbrack\tau$ in different ways, according to how $t$ occur in $\tau$.

The ambiguity is resolved by giving a template that marks the occurrences of $t$ in $\tau$ at which $f$ is applied.

Such template is known as type operator $t.\tau$, which is a abstractor binding type variable $t$ and type $\tau$.

Polynomial Type Operators

A type operator is a type equipped with a designated variable whose occurrences mark the spots in the type where a transformation is applied. The abstractor has form $t.\tau$ such that $t\text{ type}\vdash\tau\text{ type}$.

An instance for a type operator $t.\tau$ i obtained by substituting $t$ with $\rho$ in $\tau$.

Polynomial type operator is constructed from

  • type variable $t$
  • types void and unit
  • product type constructors $\tau_1\times\tau_2$
  • sum type constructors $\tau_1+\tau_2$

Inductive Definition

$$
\displaylines{\dfrac{}{t.t\text{ poly}}\\
\dfrac{}{t.\text{unit poly}}\\
\dfrac{t.\tau_1\text{ poly}\phantom{“”}t.\tau_2\text{ poly}}{t.\tau_1\times\tau_2\text{ poly}}\\
\dfrac{}{t.\text{void poly}}\\
\dfrac{t.\tau_1\text{ poly}\phantom{“”}t.\tau_2\text{ poly}}{t.\tau_1+\tau_2\text{ poly}}}
$$

Closure under Substitution

If $t.\tau\text{ poly}$ and $t’.\tau’\text{ poly}$, then $t.\lbrack \tau/t’]\tau’\text{ poly}$.

By structural induction on $t’.\tau’\text{ poly}$, we can see that the conclusion is easily achieved.

Generic Extension

Polynomial type operators are templates for structure of data structure with slots for values of particular type.

Type operator $t.t\times(\text{nat}+t)$ specifies all types $\rho \times(\text{nat}+\rho)$ for any choices of $\rho$.

Thus a polynomial type operator designates points of interest in a data structure that have a common type.

Generic extension of a polynomial type operator is a form of expression with syntax
$$
\begin{align}
\text{Exp}&&e&&::=&&\text{map}\lbrace t.\tau\rbrace(x.e’)(e)&&\text{map}\lbrace t.\tau\rbrace(x.e’)(e)&&\text{generic extension}
\end{align}
$$
It specifies a program that applies a given function to all values lying at points of interest in a compound data structure to obtain a new one with applications at those points.

Statics

$$
\dfrac{t.\tau\text{ poly}\phantom{“”}\Gamma,x:\rho\vdash e’:\rho’\phantom{“”}\Gamma\vdash e:\lbrack\rho/t\rbrack\tau}{\Gamma\vdash\text{map}\lbrace t.\tau\rbrace(x.e’)(e):\lbrack\rho’/t\rbrack\tau}
$$

  • abstractor $x.e’$ serves as a mapping from $x:\rho$ to $e’:\rho’$.
  • generic extension of $t.\tau$ along with $x.e’$ specifies a mapping from $\lbrack\rho/t\rbrack\tau$ to $\lbrack\rho’/t\rbrack\tau$.

Dynamics

$$
\displaylines{\dfrac{}{\text{map}\lbrace t.t\rbrace(x.e’)(e)\longmapsto\lbrack e/x\rbrack e’}\\
\dfrac{}{\text{map}\lbrace t.\text{unit}\rbrace(x.e’)(e)\longmapsto e}\\
\dfrac{}{\text{map}\lbrace t.\tau_1\times\tau_2\rbrace(x.e’)(e)\longmapsto
\langle\text{map}\lbrace t.\tau_1\rbrace(x.e’)(e\cdot l),\text{map}\lbrace t.\tau_2\rbrace(x.e’)(e\cdot r)\rangle}\\
\dfrac{}{\text{map}\lbrace t.\text{void}\rbrace(x.e’)(e)\longmapsto\text{abort}(e)}\\
\dfrac{}{\text{map}\lbrace t.\tau_1+\tau_2\rbrace(x.e’)(e)\\\longmapsto\\\text{case }e\lbrace l\cdot x_1\hookrightarrow l\cdot\text{map}\lbrace t.\tau_1\rbrace(x.e’)(x_1) \shortmid r\cdot x_2\hookrightarrow r\cdot\text{map}\lbrace t.\tau_2\rbrace(x.e’)(x_2) \rbrace}}
$$

Preservation Theorem

If $\text{map}\lbrace t.\tau\rbrace(x.e’)(e):\tau’$ and $\text{map}\lbrace t.\tau\rbrace(x.e’)(e)\longmapsto e’’$, then $e’’:\tau’$.

Positive Type Operators

Positive type operators extend the polynomial type operators to admit restricted forms of function types.

$t.\tau_1\to\tau_2$ is a positive type operator if

  • $t$ does not occur in $\tau_1$
  • $t.\tau_2$ is a positive type operator

Any occurrences of type variable $t$ in domain of a function type are negative occurrences, whereas any occurrences of $t$ in range of a function type are positive occurrence.

A positive type operator is one for which only positive occurrences of $t$ are allowed.

The origin of positive occurrence is that function type $\tau_1\to\tau_2$ is analogous to implication $\phi_1\supset\phi_2$, which is classically equivalent to $\neg\phi_1\vee\phi_2$, so the occurrences in domain are negative occurrence.

Positive type operators are closed under substitution, just like polynomial type operators.

Inductive Definition

Judgment $t.\tau\text{ pos}$, which states that the abstractor $t.\tau$ is a positive type operator.
$$
\displaylines{\dfrac{}{t.t\text{ pos}}\\
\dfrac{}{t.\text{unit pos}}\\
\dfrac{t.\tau_1\text{ pos}\phantom{“”}t.\tau_2\text{ pos}}{t.\tau_1\times\tau_2\text{ pos}}\\
\dfrac{}{t.\text{void pos}}\\
\dfrac{t.\tau_1\text{ pos}\phantom{“”}t.\tau_2\text{ pos}}{t.\tau_1+\tau_2\text{ pos}}\\
\dfrac{\tau_1\text{ type}\phantom{“”}t.\tau_2\text{ pos}}{t.\tau_1\to\tau_2\text{ pos}}}
$$

Generic Extension

The generic extension follow similar definition as polynomial one with one more dynamics rule on function rule
$$
\dfrac{}{\text{map}^+\lbrace t.\tau_1\to\tau_2\rbrace)(x.e’)(e)\longmapsto\lambda(x_:\tau_1)\text{ map}^+\lbrace t.\tau_2\rbrace(x.e’)(e(x_1))}
$$
Since $t$ is not allowed in $\tau_1$, thus the type of result is $\tau_1\to\lbrack\rho’/t\rbrack\tau_2$, assuming $e$ is of type $\tau_1\to\lbrack\rho/t\rbrack\tau_2$.

If the result type is $\lbrack\rho’/t\rbrack\tau_1\to\lbrack\rho’/t\rbrack\tau_2$ given that $e$ with type $\lbrack\rho/t\rbrack\tau_1\to\lbrack\rho/t\rbrack\tau_2$. Then we might see that the extension yield a function $\lambda(x_1:\lbrack\rho’/t\rbrack\tau_1)\dots(e(\dots(x_1)))$.

The trouble is that we are given that $\text{map}\lbrace t.\tau_1\rbrace(x.e’)(-)$ transforms values of type $\lbrack\rho/t\rbrack\tau_1$ to $\lbrack\rho’/t\rbrack\tau_1$. We might have to change the $x_1$ type to fit it to $e$.

Exercise

Generic Extension of Const Type Op

It is easy to see that if the generic extension is applied on a constant type operator, where $t$ do not occur, then there will be no place for substitution, leaving $\text{map}\lbrace x.\tau\rbrace(x.e’)(e)$ evaluated to $e$ regardless of the choice of $e’$.

If we extend this to positive type operators, then it will yield $\lambda(x:\tau_1)e(x)$, which is not identical to $e$.

Database Schema

Since we know that database schema $\sigma$ be $\prod_{i\in I}\tau_i$, where first and last are in $I$ and $\tau_{first},\tau_{last}:\text{str}$.

Let $\sigma’$ be the database schema type operator, with $\prod_{i\in I}\tau_i’$ and $\tau_{first}’,\tau_{last}’:t$ as type variable.

$\sigma$ can be $\lbrack \text{str}/t\rbrack\sigma’$. Database type still follow the old convention $\text{nat}\times(\text{nat}\to\sigma)$.

Finally the generic extension has form $\text{map}\lbrace t.\text{nat}\times(\text{nat}\to\sigma)\rbrace(x.c(x))(d)$ where $d$ be database.

Non-Negative Occurrence

$$
\displaylines{\dfrac{}{t.t\text{ non-neg}}\\
\dfrac{t.\tau_1\text{ neg}\phantom{“”}t.\tau_2\text{ non-neg}}{t.\tau_1\to\tau_2\text{ non-neg}}\\
\dfrac{t.\tau_1\text{ non-neg}\phantom{“”}t.\tau_2\text{ neg}}{t.\tau_1\to\tau_2\text{ non-neg}}}
$$

(Non) Negative Generic Extension

$$
\displaylines{\dfrac{}{\text{map}^{\text{- -}}\lbrace t.t\rbrace(x.e’)(e)\longmapsto\lbrack e/x\rbrack e’}\\
\dfrac{}{\text{map}^{\text{- -}}\lbrace t.\tau_1\to\tau_2\rbrace(x.e’)(e)\longmapsto\lambda(x_1:\lbrack\rho’/t\rbrack\tau_1) \text{ map}^{\text{- -}}\lbrace t.\tau_2\rbrace(x.e’)(e(\text{map}^{-}\lbrace t.\tau_1 \rbrace(x.e’)(x_1)))}\\
\dfrac{}{\text{map}^{-}\lbrace t.\tau_1\to\tau_2\rbrace(x.e’)(e)\longmapsto\lambda(x_1:\lbrack\rho/t\rbrack\tau_1) \text{ map}^{-}\lbrace t.\tau_2\rbrace(x.e’)(e(\text{map}^{\text{- -}}\lbrace t.\tau_1 \rbrace(x.e’)(x_1)))}}
$$

Then the type operator $t.(t\to\text{bool})\to\text{bool}$ with function $f$ of type $(\rho\to\text{bool})\to\text{bool}$ and $x.e’$ can construct $\lambda(g:\rho’\to\text{bool})f(\lambda(x:\rho)g(e’))$ for generic extension.