PFPL Chapter 14 Generic Programming

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 }^{\prime }$, we wish to extend $f$ to a transformation from type $[\rho /t]\tau$ to $[\rho /t]\tau$ by applying $f$ to various spots in the inputs, where $\rho$ occurs to obtain a value of type ${\rho }^{\prime }$, 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 }^{\prime }$ that transform $⟨a,b⟩$ to $⟨a,f(b)⟩$.

Ambiguity and Type Operator

Ambiguity arises in many-one nature of substitution. A type can have the form $[\rho /t]\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}⊢\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

$$\begin{array}{c}{\displaystyle \frac{}{t.t\text{ poly}}}\\ {\displaystyle \frac{}{t.\text{unit poly}}}\\ {\displaystyle \frac{t.{\tau }_1\text{ poly}\phantom{“”}t.{\tau }_2\text{ poly}}{t.{\tau }_1\times {\tau }_2\text{ poly}}}\\ {\displaystyle \frac{}{t.\text{void poly}}}\\ {\displaystyle \frac{t.{\tau }_1\text{ poly}\phantom{“”}t.{\tau }_2\text{ poly}}{t.{\tau }_1+{\tau }_2\text{ poly}}}\end{array}$$

Closure under Substitution

If $t.\tau \text{ poly}$ and $t^{\prime }.{\tau }^{\prime }\text{ poly}$, then $t.[\tau /t^{\prime }]{\tau }^{\prime }\text{ poly}$.

By structural induction on $t^{\prime }.{\tau }^{\prime }\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{array}{rlrlrlrlrlr}\text{Exp}& & e& & ::=& & \text{map}\{t.\tau \}(x.e^{\prime })(e)& & \text{map}\{t.\tau \}(x.e^{\prime })(e)& & \text{generic extension}\end{array}$$
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

$${\displaystyle \frac{t.\tau \text{ poly}\phantom{“”}\mathrm{\Gamma },x:\rho ⊢e^{\prime }:{\rho }^{\prime }\phantom{“”}\mathrm{\Gamma }⊢e:[\rho /t]\tau }{\mathrm{\Gamma }⊢\text{map}\{t.\tau \}(x.e^{\prime })(e):[{\rho }^{\prime }/t]\tau }}$$

• abstractor $x.e^{\prime }$ serves as a mapping from $x:\rho$ to $e^{\prime }:{\rho }^{\prime }$.
• generic extension of $t.\tau$ along with $x.e^{\prime }$ specifies a mapping from $[\rho /t]\tau$ to $[{\rho }^{\prime }/t]\tau$.

Dynamics

$$\begin{gathered} \begin{array}{c}{\displaystyle \frac{}{\text{map}\{t.t\}(x.e^{\prime })(e)⟼[e/x]e^{\prime }}}\\ {\displaystyle \frac{}{\text{map}\{t.\text{unit}\}(x.e^{\prime })(e)⟼e}}\\ {\displaystyle \frac{}{\text{map}\{t.{\tau }_1\times {\tau }_2\}(x.e^{\prime })(e)⟼⟨\text{map}\{t.{\tau }_1\}(x.e^{\prime })(e\cdot l),\text{map}\{t.{\tau }_2\}(x.e^{\prime })(e\cdot r)⟩}}\\ {\displaystyle \frac{}{\text{map}\{t.\text{void}\}(x.e^{\prime })(e)⟼\text{abort}(e)}}\\ {\displaystyle \frac{}{\text{map}\{t.{\tau }_1+{\tau }_2\}(x.e^{\prime })(e) \\ ⟼ \\ \text{case }e\{l\cdot x_1\hookrightarrow l\cdot \text{map}\{t.{\tau }_1\}(x.e^{\prime })(x_1)\mid r\cdot x_2\hookrightarrow r\cdot \text{map}\{t.{\tau }_2\}(x.e^{\prime })(x_2)\}}}\end{array} \end{gathered}$$

Preservation Theorem

If $\text{map}\{t.\tau \}(x.e^{\prime })(e):{\tau }^{\prime }$ and $\text{map}\{t.\tau \}(x.e^{\prime })(e)⟼e^{″}$, then $e^{″}:{\tau }^{\prime }$.

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 ${\varphi }_1\supset {\varphi }_2$, which is classically equivalent to $\mathrm{\neg }{\varphi }_1\vee {\varphi }_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.
$$\begin{array}{c}{\displaystyle \frac{}{t.t\text{ pos}}}\\ {\displaystyle \frac{}{t.\text{unit pos}}}\\ {\displaystyle \frac{t.{\tau }_1\text{ pos}\phantom{“”}t.{\tau }_2\text{ pos}}{t.{\tau }_1\times {\tau }_2\text{ pos}}}\\ {\displaystyle \frac{}{t.\text{void pos}}}\\ {\displaystyle \frac{t.{\tau }_1\text{ pos}\phantom{“”}t.{\tau }_2\text{ pos}}{t.{\tau }_1+{\tau }_2\text{ pos}}}\\ {\displaystyle \frac{{\tau }_1\text{ type}\phantom{“”}t.{\tau }_2\text{ pos}}{t.{\tau }_1\to {\tau }_2\text{ pos}}}\end{array}$$

Generic Extension

The generic extension follow similar definition as polynomial one with one more dynamics rule on function rule
$${\displaystyle \frac{}{{\text{map}}^{+}\{t.{\tau }_1\to {\tau }_2\})(x.e^{\prime })(e)⟼\lambda (x_{:}{\tau }_1){\text{ map}}^{+}\{t.{\tau }_2\}(x.e^{\prime })(e(x_1))}}$$
Since $t$ is not allowed in ${\tau }_1$, thus the type of result is ${\tau }_1\to [{\rho }^{\prime }/t]{\tau }_2$, assuming $e$ is of type ${\tau }_1\to [\rho /t]{\tau }_2$.

If the result type is $[{\rho }^{\prime }/t]{\tau }_1\to [{\rho }^{\prime }/t]{\tau }_2$ given that $e$ with type $[\rho /t]{\tau }_1\to [\rho /t]{\tau }_2$. Then we might see that the extension yield a function $\lambda (x_1:[{\rho }^{\prime }/t]{\tau }_1)\dots (e(\dots (x_1)))$.

The trouble is that we are given that $\text{map}\{t.{\tau }_1\}(x.e^{\prime })(-)$ transforms values of type $[\rho /t]{\tau }_1$ to $[{\rho }^{\prime }/t]{\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}\{x.\tau \}(x.e^{\prime })(e)$ evaluated to $e$ regardless of the choice of $e^{\prime }$.

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 }^{\prime }$ be the database schema type operator, with $\prod _{i\in I}{\tau }_i^{\prime }$ and ${\tau }_{first}^{\prime },{\tau }_{last}^{\prime }:t$ as type variable.

$\sigma$ can be $[\text{str}/t]{\sigma }^{\prime }$. Database type still follow the old convention $\text{nat}\times (\text{nat}\to \sigma )$.

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

Non-Negative Occurrence

$$\begin{array}{c}{\displaystyle \frac{}{t.t\text{ non-neg}}}\\ {\displaystyle \frac{t.{\tau }_1\text{ neg}\phantom{“”}t.{\tau }_2\text{ non-neg}}{t.{\tau }_1\to {\tau }_2\text{ non-neg}}}\\ {\displaystyle \frac{t.{\tau }_1\text{ non-neg}\phantom{“”}t.{\tau }_2\text{ neg}}{t.{\tau }_1\to {\tau }_2\text{ non-neg}}}\end{array}$$

(Non) Negative Generic Extension

$$\begin{array}{c}{\displaystyle \frac{}{{\text{map}}^{\text{- -}}\{t.t\}(x.e^{\prime })(e)⟼[e/x]e^{\prime }}}\\ {\displaystyle \frac{}{{\text{map}}^{\text{- -}}\{t.{\tau }_1\to {\tau }_2\}(x.e^{\prime })(e)⟼\lambda (x_1:[{\rho }^{\prime }/t]{\tau }_1){\text{ map}}^{\text{- -}}\{t.{\tau }_2\}(x.e^{\prime })(e({\text{map}}^{-}\{t.{\tau }_1\}(x.e^{\prime })(x_1)))}}\\ {\displaystyle \frac{}{{\text{map}}^{-}\{t.{\tau }_1\to {\tau }_2\}(x.e^{\prime })(e)⟼\lambda (x_1:[\rho /t]{\tau }_1){\text{ map}}^{-}\{t.{\tau }_2\}(x.e^{\prime })(e({\text{map}}^{\text{- -}}\{t.{\tau }_1\}(x.e^{\prime })(x_1)))}}\end{array}$$

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^{\prime }$ can construct $\lambda (g:{\rho }^{\prime }\to \text{bool})f(\lambda (x:\rho )g(e^{\prime }))$ for generic extension.