Part 5 - Polynomial Type Operators, Inductive and Coinductive types

Polynomial Type Operators

TODO

Inductive and Coinductive types

The primary motivation for inductive and coinductive types is to provide us with a mechanism for generating types like the natural numbers in later languages we'll learn, like System F, PCF, and untyped lambda calculus. This is a core foundation of the other topics, so make sure you know it well (even if you can't pull the proofs off right away)

Inductive types

The natural numbers serve as a good gateway as an inductive type, since it's inductively defined and all.

The book redefines the introduction and elimination forms for the natural numbers as such:

$$ \frac{\Gamma \vdash e: \text{unit} + \text{nat}}{\Gamma \vdash \text{fold}_\text{nat}(e): nat} $$

$$ \frac{\Gamma, x: \text{unit} + \tau \vdash e_1: \tau \quad \Gamma \vdash e_2: \text{nat}}{\text{rec}_\text{nat}(x.e_1;e_2): \tau} $$

And the dyanmics as such:

$$ \overline{\text{fold}_\text{nat}(e) \text{ val}} $$

$$ \frac{e_2 \rightarrow e'2}{\text{rec}\text{nat}(x.e_1;e_2) \rightarrow \text{rec}_\text{nat}(x.e_1;e_2)} $$

$$ \overline{\text{rec}\text{nat}(x.e_1;\text{fold}\text{nat}(e_2)) \rightarrow [\text{map}{t.\text{unit+t}}(y.\text{rec}_\text{nat}(x.e_1;y))(e_2)/x]e_1} $$

To define a doubling function over this type, we have

$$ \texttt{rec}(x. \texttt{case } x { l.<> \hookrightarrow fold(l.<>) | r.x' \hookrightarrow r.fold(r.fold(r.x')) })(\texttt{fold}(e)) $$

Coinductive types

Instead of giving a robust definition of what a coinductive type is, we'll instead venture to show a coinductive type: this is the definition of a stream of natural numbers

$$ \frac{\Gamma \vdash e: \texttt{stream}}{\Gamma \vdash \texttt{hd}(e): nat} $$

$$ \frac{\Gamma \vdash e: \texttt{stream}}{\Gamma \vdash \texttt{tl}(e): stream} $$

$$ \frac{\Gamma \vdash e: \tau \quad \Gamma, x: \tau \vdash e_1: \texttt{nat} \quad \Gamma, x: \tau \vdash e_2: \tau}{\Gamma \vdash \texttt{strgen } x \texttt{ is } e \texttt{ in } <hd \hookrightarrow e_1, tl \hookrightarrow e_2> : stream} $$

So a "stream of natural numbers" is really just the expression $\texttt{strgen } x \texttt{ is } \texttt{z} \texttt{ in } <hd \hookrightarrow x, tl \hookrightarrow s(x)>$

and "stream of even naturals" would be $\texttt{strgen } x \texttt{ is } \texttt{z} \texttt{ in } <hd \hookrightarrow x, tl \hookrightarrow s(s(x))>$