PFPL Chapter 15 Inductive and Coinductive Types

Posted on In Disqus:

This part is not shown on PFPL preview version.

Some Forms of Recursive Type

Inductive and coinductive types are two important forms of recursive type.

On inductive type, elements are intuitively those given by finite composition of its introduction forms.

If we specify behavior of a function on each of introduction forms of an inductive type, then the behavior is defined for all values of the type.

Such a function is a recursor or catamorphism.

It is actually generalized fold.

Elements of a coinductive type are those behave properly in response to a finite composition of its elimination forms.

If we specify the behavior of an element on each elimination forms, then we have fully specified the value of that type.

Such an element is a generator or anamorphism.

It is actually generalized unfold.

Example First on Inductive Types

On chapter 9 we defined the natural numbers, and we can see inductive types as this example.

Type nat is the least type containing z and closed under S(-).

The minimal condition is expressed by existence of iterator $\text{iter }e\lbrace z\hookrightarrow e_0\shortmid s(x)\hookrightarrow e_1 \rbrace$, which

  • transforms a natural number into a value of type $\tau$ when the number is z
  • transforms from its value on a number to the value on the successor of the number.
1
2
3
4
5
6
7
8
9
-- the example is defined on Natural Number set
data Nat = Z
         | Succ Nat
-- define a type with nil as start and step as a -> a for state transfer
type StepTrans a = (a, a -> a)
-- define function on each introduction forms of Nat for StepTrans
cataExample :: StepTrans a -> Nat -> a
cataExample s@(nil, step) Zero        = nil
cataExample s@(nil, step) (Succ n)    = step $ cataExample s n

Statics

$$
\displaylines{\dfrac{\Gamma\vdash e:\text{unit}+\text{nat}}{\Gamma\vdash\text{fold}_{\text{nat}}(e):\text{nat}}\\
\dfrac{\Gamma,x:\text{unit}+\tau\vdash e_1:\tau\phantom{“”}\Gamma\vdash e_2:\text{nat}}{\Gamma\vdash\text{rec}_{\text{nat}}(x.e_1;e_2):\tau}}
$$

  • $\text{fold}_{\text{nat}}(e)$ is the unique introduction form of nat.
    • z is $\text{fold}_{\text{nat}}(l\cdot\langle\rangle)$.
    • s(e) is $\text{fold}_{\text{nat}}(r \cdot e)$.
  • Recursor $\text{rec}_{\text{nat}}(x.e_1;e_2)$ takes abstractor $x.e_1$ that combines basis and inductive step into a single computation.
    • If $x$ is replaced by $l\cdot\langle\rangle$, then $e_1$ computes the base case of the recursion.
    • If $x$ is replaced by $r\cdot e$, then $e_1$ computes the inductive step from the recursive result on $e$.

Dynamics

$$
\displaylines{\dfrac{e\text{ val}}{\text{fold}_{\text{nat}}(e)\text{ val}}\\
\dfrac{e_2\longmapsto e_2’}{\text{rec}_{\text{nat}}(x.e_1;e_2)\longmapsto\text{rec}_{\text{nat}}(x.e_1;e_2’)}\\
\dfrac{}{\text{rec}_{\text{nat}}(x.e_1;\text{fold}_{\text{nat}}(e_2))\longmapsto\lbrack \text{map}\lbrace t.\text{unit}+t \rbrace(y.\text{rec}_{\text{nat}}(x.e_1;y))(e_2)/x \rbrack e_1}\\
\dfrac{\lbrack e_2\text{ val}\rbrack}{\text{rec}_{\text{nat}}(x.e_1;\text{fold}_{\text{nat}}(e_2))\longmapsto\lbrack\text{case }e_2 \lbrace l\cdot x\hookrightarrow l\cdot \langle\rangle\shortmid r\cdot y\hookrightarrow r\cdot\text{rec}_{\text{nat}}(x.e_1;y)\rbrace/x \rbrack e_1}}
$$

The last 2 rules express the similar meaning. The latter one expand the definition of generic extension in place.

Iterator by Recursor

Iterator $\text{iter }e\lbrace z\hookrightarrow e_0\shortmid s(x)\hookrightarrow e_1\rbrace$ can be formed by $\text{rec}_\text{nat}$ here. Iterator does not need the predecessor, only previous result is required.

Here we can construct $\text{rec}_{\text{nat}}(y.\text{case }y\lbrace \text{l}\cdot\underline{}\hookrightarrow e_0\shortmid\text{r}\cdot \underline{}\hookrightarrow e_1\rbrace;e)$, to avoid the calculation for predecessor.

Example First on Coinductive Types

An illustrative example of a coinductive type is the type of streams of natural numbers.

A stream is an infinite sequence of natural numbers such that element of the stream can be computed only after computing all preceding elements in that stream.

Computations of successive elements of the stream are consequentially dependent in that computation of one element influences computation of the next.

In this sense, the introduction form for streams is dual to the elimination form for the natural numbers.

1
2
3
4
5
6
7
8
9
10
11
12
-- still follow the definition of Nat previously
anaExample :: Integer -> Nat
anaExample i    = case i <= 0 of
                      true     -> Z
                      false    -> S $ anaExample (i - 1)
-- anamorphism with Maybe and show as unfold function
data Maybe a = Just a
             | Nothing
anamorphism :: (a -> Maybe (val, a)) -> a -> [val]
anamorphism f oS    = case f oS of
                          Nothing        -> []
                          Just (val, nS) -> val : anamorphism f nS

Statics

A stream is given by its behavior under the elimination form of stream type:

  • hd(e) returns the head element of steream
  • tl(e) returns the tail of the stream, with head removed

A stream is introduced by a generator, the dual of recursor, that defines head and tail of stream in terms of current stage of the stream, which is represented by a value of some type.

The statics of streams is given by the following rules
$$
\displaylines{\dfrac{\Gamma\vdash e:\text{stream}}{\Gamma\vdash\text{hd}(e):\text{nat}}\\
\dfrac{\Gamma\vdash e:\text{stream}}{\Gamma\vdash\text{tl}(e):\text{stream}}\\
\dfrac{\Gamma\vdash e:\tau\phantom{“”}\Gamma,x:\tau\vdash e_1:\text{nat}\phantom{“”}\Gamma,x:\tau\vdash e_2:\tau}{\Gamma\vdash\text{strgen }x\text{ is }e\text{ in }\langle\text{hd}\hookrightarrow e_1,\text{tl}\hookrightarrow e_2\rangle\space:\text{stream}}}
$$

Current stage of the stream is given by the expression $e$ and $e:\tau$, with head and tail defined as $e_1$, $e_2$.

Dynamics

$$
\displaylines{\dfrac{\lbrack e\text{ val}\rbrack}{\text{strgen }x\text{ is }e\text{ in }\langle\text{hd}\hookrightarrow e_1,\text{tl}\hookrightarrow e_2\rangle\text{ val}}\\
\dfrac{e\longmapsto e’}{\text{hd}(e)\longmapsto\text{hd}(e’)}\\
\dfrac{}{\text{hd}(\text{strgen }x\text{ is }e\text{ in }\langle\text{hd}\hookrightarrow e_1,\text{tl}\hookrightarrow e_2\rangle)\longmapsto\lbrack e/x\rbrack e_1}\\
\dfrac{e\longmapsto e’}{\text{tl}(e)\longmapsto\text{tl}(e’)}\\
\dfrac{}{\text{tl}(\text{strgen }x\text{ is }e\text{ in }\langle\text{hd}\hookrightarrow e_1,\text{tl}\hookrightarrow e_2\rangle)\longmapsto\text{strgen }x\text{ is }\lbrack e/x\rbrack e_2\text{ in }\langle\text{hd}\hookrightarrow e_1,\text{tl}\hookrightarrow e_2\rangle}}
$$

Reorganized Statics

We combine head and tail into a single elimination form, reorganize generator correspondingly.

$$
\displaylines{\dfrac{\Gamma\vdash e:\text{stream}}{\Gamma\vdash\text{unfold}_{\text{stream}}(e):\text{nat}\times\text{stream}}\\
\dfrac{\Gamma,x:\tau\vdash e_1:\text{nat}\times\tau\phantom{“”}\Gamma\vdash e_2:\tau}{\Gamma\vdash\text{gen}_{\text{stream}}(x.e_1;e_2):\text{stream}}}
$$

Reorganized Dynamics

$$
\displaylines{\dfrac{\lbrack e_2\text{ val}\rbrack}{\text{gen}_{\text{stream}}(x.e_1;e_2)\text{ val}}\\
\dfrac{e_0\longmapsto e_0’}{\text{unfold}_\text{stream}(e_0) \longmapsto \text{unfold}_\text{stream}(e_0’)}\\
\dfrac{}{\text{unfold}_{\text{stream}}(\text{gen}_{\text{stream}}(x.e_1;e_2))\longmapsto\text{map}\lbrace t.\text{nat}\times t\rbrace(y.\text{gen}_{\text{stream}}(x.e_1;y))(\lbrack e_2/x\rbrack e_1)}\\
\dfrac{}{\text{unfold}_{\text{stream}}(\text{gen}_{\text{stream}}(x.e_1;e_2))\longmapsto\langle(\lbrack e_2/x\rbrack e_1)\cdot \text{l},\text{gen}_\text{stream}(x.e_1;(\lbrack e_2/x\rbrack e_1)\cdot \text{r}) \rangle}}
$$

If we want to use $\text{gen}_{\text{stream}}$ to define the $\text{strgen}$, we can have $\text{gen}_{\text{stream}}(x.e;\langle e_1,e_2\rangle)$.

Statics

Consider a variant of T called M with natural numbers replaced by functions, products, sums and a rich class of inductive/coinductive types.

Types

$$
\begin{align}
\text{Typ}&&\tau&&::=&&t&&t&&\text{self-reference}\\
&&&&&&\text{ind}(t.\tau)&&\mu(t.\tau)&&\text{inductive}\\
&&&&&&\text{coi}(t.\tau)&&\nu(t.\tau)&&\text{coinductive}
\end{align}
$$

Type formation judgments have the form $t_1\text{ type},\dots,t_n\text{ type}\vdash\tau\text{ type}$.

We let $\Delta$ range over finite sets of hypotheses of the form $t\text{ type}$. Type formation is inductively defined by
$$
\displaylines{\dfrac{}{\Delta,t\text{ type}\vdash t\text{ type}}\\
\dfrac{}{\Delta\vdash\text{unit type}}\\
\dfrac{\Delta\vdash\tau_1\text{ type}\phantom{“”}\Delta\vdash\tau_2\text{ type}}{\Delta\vdash\text{prod}(\tau_1;\tau_2)\text{ type}}\\
\dfrac{}{\Delta\vdash\text{void type}}\\
\dfrac{\Delta\vdash\tau_1\text{ type}\phantom{“”}\Delta\vdash\tau_2\text{ type}}{\Delta\vdash\text{sum}(\tau_1;\tau_2)\text{ type}}\\
\dfrac{\Delta\vdash\tau_1\text{ type}\phantom{“”}\Delta\vdash\tau_2\text{ type}}{\Delta\vdash\text{arr}(\tau_1;\tau_2)\text{ type}}\\
\dfrac{\Delta,t\text{ type}\vdash\tau\text{ type}\phantom{“”}\Delta\vdash t.\tau\text{ pos}}{\Delta\vdash\text{ind}(t.\tau)\text{ type}}\\
\dfrac{\Delta,t\text{ type}\vdash\tau\text{ type}\phantom{“”}\Delta\vdash t.\tau\text{ pos}}{\Delta\vdash\text{coi}(t.\tau)\text{ type}}}
$$

Expressions

$$
\begin{align}
\text{Exp}&&e&&::=&&\text{fold}\lbrace t.\tau\rbrace(e)&&\text{fold}_{t.\tau}(e)&&\text{constructor}\\
&&&&&&\text{rec}\lbrace t.\tau\rbrace(x.e_1;e_2)&&\text{rec}(x.e_1;e_2)&&\text{recursor}\\
&&&&&&\text{unfold}\lbrace t.\tau\rbrace(e)&&\text{unfold}_{t.\tau}(e)&&\text{destructor}\\
&&&&&&\text{gen}\lbrace t.\tau\rbrace(x.e_1;e_2)&&\text{gen}(x.e_1;e_2)&&\text{generator}
\end{align}
$$

The statics for M is given by the following rules
$$
\displaylines{
\dfrac{\Gamma\vdash e:\lbrack\text{ind}(t.\tau)/t\rbrack \tau}{\Gamma\vdash\text{fold}\lbrace t.\tau\rbrace(e):\text{ind}(t.\tau)}\\
\dfrac{\Gamma,x:\lbrack\tau’/t\rbrack \tau\vdash e_1:\tau’\phantom{“”}\Gamma\vdash e_2:\text{ind}(t.\tau)}{\Gamma\vdash\text{rec}\lbrace t.\tau\rbrace(x.e_1;e_2):\tau’}\\
\dfrac{\Gamma\vdash e:\text{coi}(t.\tau)}{\Gamma\vdash\text{unfold}\lbrace t.\tau\rbrace(e):\lbrack\text{coi}(t.\tau)/t\rbrack\tau}\\
\dfrac{\Gamma\vdash e_2:\tau_2\phantom{“”}\Gamma,x:\tau_2\vdash e_1:\lbrack\tau_2/t\rbrack\tau}{\Gamma\vdash\text{gen}\lbrace t.\tau\rbrace(x.e_1;e_2):\text{coi}(t.\tau)}}
$$

Dynamics

We use the positive generic extension in this lazy dynamics for M here
$$
\displaylines{\dfrac{}{\text{fold}\lbrace t.\tau\rbrace(e)\text{ val}}\\
\dfrac{e_2\longmapsto e_2’}{\text{rec}\lbrace t.\tau\rbrace(x.e_1;e_2)\longmapsto\text{rec}\lbrace t.\tau\rbrace(x.e_1;e_2’)}\\
\dfrac{}{\text{rec}\lbrace t.\tau\rbrace(x.e_1;\text{fold}\lbrace t.\tau\rbrace(e_2))\longmapsto\lbrack \text{map}^+\lbrace t.\tau\rbrace(y.\text{rec}\lbrace t.\tau\rbrace(x.e_1;y))(e_2)/x\rbrack e_1}\\
\dfrac{e_2\text{ val}}{\text{gen}\lbrace t.\tau\rbrace(x.e_1;e_2)\text{ val}}\\
\dfrac{e\longmapsto e’}{\text{unfold}\lbrace t.\tau\rbrace(e)\longmapsto\text{unfold}\lbrace t.\tau\rbrace(e’)}\\
\dfrac{}{\text{unfold}\lbrace t.\tau\rbrace(\text{gen}\lbrace t.\tau\rbrace(x.e_1;e_2))\longmapsto\text{map}^+\lbrace t.\tau\rbrace(y.\text{gen}\lbrace t.\tau \rbrace(x.e_1;y))(\lbrack e_2/x\rbrack e_1)}}
$$

Preservation Lemma

If $e:\tau$ and $e\longmapsto e’$, then $e’:\tau$.

Progress Lemma

If $e:\tau$, then either $e\text{ val}$ or $\exists e’$ that $e\longmapsto e’$.

Termination for M Lemma

If $e:\tau$, then $\exists e’\text{ val}$ such that $e\longmapsto^\ast e’$.

Infinite data structures like streams, are represented as in a continuing state of creation, not as a completed whole.

Solving Type Equations

For a positive type operator $t.\tau$, we may say that the inductive type $\mu(t.\tau)$ and coinductive type $\nu(t.\tau)$ are both solutions (up to isomorphism) of type equation $t \cong \tau$
$$
\mu(t.\tau)\cong\lbrack\mu(t.\tau)/t\rbrack\tau\\
\nu(t.\tau)\cong\lbrack\nu(t.\tau)/t\rbrack\tau
$$

  • every value of an inductive type is the folding of a value of the unfolding of the inductive type
  • every value of unfolding of a coinductive type is the unfolding of a value of the coinductive type

Nat and Conat

Although $\mu(t.\tau)$ and $\nu(t.\tau)$ are both solutions to $t\cong\tau$, they are not isomorphic to each other.

For inductive type $\text{nat}\triangleq \mu(\text{unit}+t)$, nat is the smallest (most restrictive) type containing

  • Z given by $\text{fold}(l\cdot\langle\rangle)$
  • closed under formation of successor of any other $e$ of type nat given by $\text{fold}(r\cdot e)$

Dually, for coinductive type $\text{conat}\triangleq\nu(\text{unit}+t)$, conat is the largest (most permissive) type of expressions $e$ for which the unfolding $\text{unfold}(e)$ can be

  • Z by $l\cdot\langle\rangle$
  • successor to some other $e’$ of conat by $r\cdot e’$

nat is defined by composition of its introduction forms and sum injections.

conat is defined by its elimination forms (unfolding plus case analyses).

Infinite co-natural number $\omega$ can be defined as $\omega\triangleq\text{gen}(x.r\cdot x;\langle\rangle)$, then we can see $\text{unfold}(\omega)\longmapsto^\ast r\cdot\omega$.

We can also define a function $\text{nat}\to\text{conat}$ that satisfy
$$
\begin{cases}
\text{unfold}(i(z))\longmapsto^\ast l\cdot\langle\rangle\\[1ex]
\text{unfold}(i(s(\overline n)))\longmapsto^\ast r\cdot i(\overline n)
\end{cases}
$$
The structure of $i:\text{nat}\to\text{conat}$ with supporting functions $\tilde z:\text{conat}$ and $\tilde{s}:\text{conat}\to\text{conat}$
$$
\lambda(x:\text{nat})\text{ rec }x\lbrace z\hookrightarrow \tilde{z}\shortmid s(x)\text{ with }y\hookrightarrow\tilde{s}(y)\rbrace
$$
$\tilde{z}$ can be defined as $\text{gen}(x.l\cdot x;\langle\rangle)$ and $\tilde{s}$ can be defined as $\lambda(y:\text{conat})(x.(r\cdot x);y)$.

Exercise

15.4

Transform $\text{seq}\triangleq\text{nat}\to\text{nat}$ to $\text{stream}$, we can have $\lambda(q:\text{seq})\text{ strgen }x\text{ is }z\text{ in }\langle\text{hd}\hookrightarrow q(x),\text{tl}\hookrightarrow s(x)\rangle$.

15.5

$$
\begin{align}
\text{natlist}&\triangleq\mu(t.\text{unit}+(\text{nat}\times t))\\
\text{nil}&\triangleq\text{fold}(\text{l}\cdot\langle\rangle)\\
\text{cons}(e_1;e_2)&\triangleq\text{fold}(\text{r}\cdot\langle e_1;e_2\rangle)\\
\text{rec }e\lbrace\text{nil}\hookrightarrow e_0\shortmid\text{cons}(x;y)\hookrightarrow e_1\rbrace&\triangleq\text{rec}(z.\text{case }e\lbrace\text{l}\cdot\underline{}\hookrightarrow e_0\shortmid\text{r}\cdot u\hookrightarrow\lbrack u\cdot\text{l},u\cdot\text{r}/x,y \rbrack e_1\rbrace;e)
\end{align}
$$

15.6

  • The dynamics for itree can be described as
    $$
    \dfrac{}{\text{view}(\text{itgen }x\text{ is }e\text{ in }e’)\longmapsto\text{map}^+\lbrace t.t\times t\rbrace(y.\text{itgen }x\text{ is }e\text{ in }y)(\lbrack e/x\rbrack e’)}
    $$

  • The itree reformulated into coinductive type as $\text{itree}\triangleq\nu(t.(t\times t)\text{ opt})$.

    • The statics of itree can be reformuated with unfold and gen by
      $$
      \displaylines{\dfrac{\Gamma\vdash e:\text{itree}}{\Gamma\vdash\text{unfold}\lbrace t.(t\times t)\text{ opt}\rbrace(e):\lbrack \text{itree}/t\rbrack(t\times t)\text{ opt}}\\
      \dfrac{\Gamma\vdash e:\tau\phantom{“”}\Gamma,x:\tau\vdash e’:\lbrack\tau/t\rbrack(t\times t)\text{ opt}}{\Gamma\vdash\text{gen}\lbrace t.\text{itree}\rbrace(x.e’;e):\text{itree}}}
      $$

    • The dynamics of itree can be stated as before.

15.7

Define the signal as coinductive type $\nu(t.(\text{bool}\times\text{bool})\times t)$.
$$
\displaylines{e_{RS}\triangleq\lambda(\langle r,s\rangle:2\text{signal})\text{ gen}(\langle r’,s’\rangle.e_{RS}’;\langle \text{true},\text{false}\rangle)\\
e_{RS}’\triangleq\langle e_{NOR}\langle r,s’\rangle,e_{NOR}\langle r’,s\rangle\rangle}
$$