## 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’$, 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$.