PFPL Chapter 20 System FPC of Recursive Types

Posted on In Disqus:

Please refer this link from page 177 to 184.

Intros on System FPC and Recursive Types

FPC is a language with products, sums, partial functions, and recursive types.

Recursive types are solutions to type equations $t\cong\tau$ where there is no restriction on $t$ occurrence in $\tau$. Equivalently, it is a fixed point up to isomorphism of associated unrestricted type operator $t.\tau$. When removing the restriction on type operator, we may see the solution satisfies $t\cong t\rightharpoonup t$, which describes a type is isomorphic to the type of partial function defined on itself.

Types are not sets: they classify computable functions not arbitrary functions. With types we may solve such type equations. The penalty is that we must admit non-termination. For one thing, type equations involving functions have solutions only if the functions involved are partial.

A benefit of working in the setting of partial functions is that type operations have unique solutions (up to isomorphism). But what about the inductive/coinductive type as solution to same type equation? This turns out that based on fixed dynamics, be it lazy or eager:

  • Under a lazy dynamics, recursive types have a coinductive flavor, and inductive analogs are inaccessible.
  • Under an eager dynamics, recursive types have an inductive flavor, but coinductive analogs are accessible as well.

Solving Type Equations

The syntax table of recursive type is defined as follows
$$
\begin{aligned}
\text{Typ}&&\tau&&::=&&t&&t&&\text{self-reference}\newline
&&&&&&\text{rec}(t.\tau)&&\text{rec }t\text{ is }\tau&&\text{recursive type}\newline
\text{Exp}&&e&&::=&&\text{fold}\lbrace t.\tau\rbrace(e)&&\text{fold}(e)&&\text{fold}\newline
&&&&&&\text{unfold}(e)&&\text{unfold}(e)&&\text{unfold}
\end{aligned}
$$

Recursive types have the same general form as inductive/coinductive types.

Statics

$$
\displaylines{\dfrac{\Delta,t\text{ type}\vdash\tau\text{ type}}{\Delta\vdash\text{rec}(t.\tau)\text{ type}}\\
\dfrac{\Gamma\vdash e:\lbrack\text{rec}(t.\tau)/t\rbrack\tau}{\Gamma\vdash\text{fold}\lbrace t.\tau\rbrace(e):\text{rec}(t.\tau)}\\
\dfrac{\Gamma\vdash e:\text{rec}(t.\tau)}{\Gamma\vdash\text{unfold}(e):\lbrack\text{rec}(t.\tau)/t\rbrack\tau}}
$$

Dynamics

$$
\displaylines{\dfrac{\lbrack e\text{ val}\rbrack}{\text{fold}\lbrace t.\tau\rbrace(e)\text{ val}}\\
\Big\lbrack\dfrac{e\longmapsto e’}{\text{fold}\lbrace t.\tau\rbrace(e)\longmapsto\text{fold}\lbrace t.\tau\rbrace(e’)}\Big\rbrack\\
\dfrac{e\longmapsto e’}{\text{unfold}(e)\longmapsto\text{unfold}(e’)}\\
\dfrac{\text{fold}\lbrace t.\tau\rbrace(e)\text{ val}}{\text{unfold}(\text{fold}\lbrace t.\tau\rbrace(e))\longmapsto e}}
$$

Safety Theorem

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

Inductive and Coinductive Types

Recursive types may be used to represent inductive types such as natural numbers and natural number list.

Example First on Natural Number

Use an eager dynamics for FPC, the recursive type $\rho=\text{rec }t\text{ is }\lbrack z\hookrightarrow\text{unit},s\hookrightarrow t\rbrack$ satisfies the type equation $\rho\cong\lbrack z\hookrightarrow\text{unit},s\hookrightarrow\rho\rbrack$, and is isomorphic to the type of eager natural numbers.

Introduction and elimination forms defined on $\rho$ is defined with following equations
$$
\begin{aligned}
z&\triangleq\text{fold}(z\cdot\langle\rangle)\\
s(e)&\triangleq\text{fold}(s\cdot e)\\
\text{ifz }e\lbrace z\hookrightarrow e_0\shortmid s(x)\hookrightarrow e_1\rbrace&\triangleq\text{case unfold}(e)\space\lbrace z\cdot\underline{}\hookrightarrow e_0\shortmid s\cdot x\hookrightarrow e_1\rbrace
\end{aligned}
$$
On the other hand, with an lazy dynamics of natural numbers in PCF, the same recursive type $\rho’=\text{rec }t\text{ is }\lbrack z\hookrightarrow\text{unit},s\hookrightarrow t\rbrack$ satisfying $\rho\cong\lbrack z\hookrightarrow\text{unit},s\hookrightarrow\rho\rbrack$ is not the type of natural numbers.

Consider what chapter 15 mentioned, $\rho’$ contains infinity number $\omega$ which is not natural number.

Another Example on Natlist

Using an eager dynamics for FPC, the natlist is defined by recursive type $\text{rec }t\text{ is }\lbrack z\hookrightarrow\text{unit},c\hookrightarrow\text{nat}\times t\rbrack$, satisfying the type equation $\text{natlist}\cong\lbrack n\hookrightarrow\text{unit},c\hookrightarrow\text{nat}\times\text{natlist}\rbrack$.

Introduction and elimination forms are given by equations
$$
\begin{aligned}
\text{nil}&\triangleq\text{fold}(n\cdot\langle\rangle)\\
\text{cons}(e_1;e_2)&\triangleq\text{fold}(c\cdot\langle e_1,e_2\rangle)\\
\text{case }e\lbrace\text{nil}\hookrightarrow e_0\shortmid\text{cons}(x;y)\hookrightarrow e_1\rbrace&\triangleq\text{case unfold}(e)\space\lbrace n\cdot\underline{}\hookrightarrow e_0\shortmid c\cdot\langle x,y\rangle\hookrightarrow e_1\rbrace
\end{aligned}
$$
Consider the same recursive type under a context of lazy dynamics for FPC. Then we can see a value of such recursive type has the form $\text{fold}(e)$, where $e$ is an unevaluated computation of the sum type.

Redefine (Co)Inductive Type

Consider the recursive type $\tau\triangleq\text{rec }t\text{ is }\tau’$ and the associated inductive type and coinductive type $\mu(t.\tau’)$ and $\nu(t.\tau’)$. We redefine these types consistently with statics of inductive and coinductive types here
$$
\begin{aligned}
\text{fold}\lbrace t.\tau’\rbrace(e)&\triangleq\text{fold}(e)\\
\text{rec}\lbrace t.\tau’\rbrace(x.e’;e)&\triangleq(\text{fix }r\text{ is }\lambda(u:
\tau)\space e_{rec})(e),\text{ where}\\
e_{rec}&\triangleq\lbrack\text{map}\lbrace t.\tau’\rbrace(x.r(x))(\text{unfold}(u))/x\rbrack e’\\
\text{unfold}\lbrace t.\tau’\rbrace(e)&\triangleq\text{unfold}(e)\\
\text{gen}\lbrace t.\tau’\rbrace(x.e’;e)&\triangleq(\text{fix }g\text{ is }\lambda(u:\rho)\space e_{gen})(e),\text{ where}\\
e_{gen}&\triangleq\text{fold}(\text{map}\lbrace t.\tau’\rbrace(x.g(x))(\lbrack u/x\rbrack e’))
\end{aligned}
$$

Dynamics is ill-behaved. Under eager interpretation, the generator may not converge, depending on choice of $e’$; under lazy interpretation, the recursor may not converge, depending on choice of $e’$.

The outcome shows that in the eager case the recursive type is inductive, not coinductive; whereas in the lazy case the recursive type is coinductive, not inductive.

Coinductive Signal Transducer

We can define type Sig for signal to be the coinductive type of infinite streams of booleans, then we can also define the type of a signal transducer as $\text{Sig}\rightharpoonup\text{Sig}$.

Sig as a coinductive type can have form $\nu(t.e’)$ follows previous redefined coinductive type. In each of its unfold and generate, it gets a new boolean value out. Thus it can have definition $\nu(t.\text{bool}\times t)$.

The definition applies in lazy dynamics, whereas under an eager definition one may use $\nu(t.\text{unit}\rightharpoonup\text{bool}\times t)$. Maybe we just need to feed it with something we do not care in case it won’t stop.

The NOR here can have the type of $\text{Sig}\times\text{Sig}\rightharpoonup\text{Sig}$, with definition as
$$
\lambda(a,b)\text{gen}\lbrace t.\text{bool}\times t\rbrace(\langle a,b\rangle.\langle e_{nor}\langle\text{hd}(a),\text{hd}(b)\rangle,\langle\text{tl}(a),\text{tl}(b)\rangle\rangle;a,b)
$$

Self-Reference

In general recursive expression $\text{fix}\lbrace\tau\rbrace(x.e)$, the variable $x$ stands for the expression itself. Self-reference is effected by the unrolling transition and it substitutes itself for $x$ in its body during execution.
$$
\text{fix}\lbrace\tau\rbrace(x.e)\longmapsto\lbrack\text{fix}\lbrace\tau\rbrace(x.e)/x\rbrack e
$$

It is useful to think $x$ as an implicit argument to $e$ that it is instantiated to itself when expression is used.

Type of self-referential expressions given by the syntax table
$$
\begin{aligned}
\text{Typ}&&\tau&&::=&&\text{self}(\tau)&&\tau\text{ self}&&\text{self-referential type}\\
\text{Exp}&&e&&::=&&\text{self}\lbrace\tau\rbrace(x.e)&&\text{self }x\text{ is }e&&\text{self-referential expression}\\
&&&&&&\text{unroll}(e)&&\text{unroll}(e)&&\text{unroll self-reference}
\end{aligned}
$$

Statics and Dynamics

The statics of these constructs is defined as
$$
\displaylines{\dfrac{\Gamma,x:\text{self}(\tau)\vdash e:\tau}{\Gamma\vdash\text{self}\lbrace\tau\rbrace(x.e):\text{self}(\tau)}\\
\dfrac{\Gamma\vdash e:\text{self}(\tau)}{\Gamma\vdash\text{unroll}(e):\tau}}
$$
The dynamics is given by
$$
\displaylines{\dfrac{}{\text{self}\lbrace\tau\rbrace(x.e)\text{ val}}\\
\dfrac{e\longmapsto e’}{\text{unroll}(e)\longmapsto\text{unroll}(e’)}\\
\dfrac{}{\text{unroll}(\text{self}\lbrace\tau\rbrace(x.e))\longmapsto\lbrack\text{self}\lbrace\tau\rbrace(x.e)/x\rbrack e}}
$$

The main difference, compared to general recursion, is that we distinguish a type of self-referential expressions, instead of having self-reference at every type. It’s all a matter of taste.

Recursive Type Defined Self-Reference

We can define the $\text{self}(\tau)$ with recursive type since a self-referential expression of type $\tau$ depends on the expression itself. It satisfies the isomorphism $\text{self}(\tau)\cong\text{self}(\tau)\rightharpoonup \tau$.

The type equation can be solved by type operator $t.t\rightharpoonup\tau$, where $t\notin\tau$ is a type variable. Required fixed point is just the recursive type $\text{self}(\tau)\triangleq\text{rec}(t.t\rightharpoonup\tau)$. Redefinition on type is shown as follows
$$
\begin{aligned}
\text{self}(\tau)&\triangleq\text{rec}(t.t\rightharpoonup\tau)\\
\lambda(x)\space e&:\space\space\text{self}(\tau)\rightharpoonup\tau\equiv\lbrack\text{rec}(t.t\rightharpoonup\tau)/t\rbrack(t\rightharpoonup\tau)\\
\text{self}\lbrace\tau\rbrace(x.e)&:\space\space\text{rec}(t.t\rightharpoonup\tau)\equiv\text{self}(\tau)\\
\text{self}\lbrace\tau\rbrace(x.e)&\triangleq\text{fold}(\lambda(x:\text{self}(\tau))\space e)\\
\text{unroll}(e:\text{self}(\tau))&:\space\space\tau\\
\text{unroll}(e:\text{rec}(t.t\rightharpoonup\tau))&\triangleq(\text{unfold}(e:\text{rec}(t.t\rightharpoonup\tau)):\lbrack\text{rec}(t.t\rightharpoonup\tau)/t\rbrack(t\rightharpoonup\tau))(e)\\
&\equiv\text{unfold}(e)(e)
\end{aligned}
$$
It is easy to check that final line of redefinition is correct by $\text{unroll}(\text{self}\lbrace\tau\rbrace(y.e))\longmapsto^\ast\lbrack\text{self}\lbrace\tau\rbrace(y.e)/y\rbrack e$.

Self-Reference Defined Fixed Point

We may define $\text{fix}\lbrace\tau\rbrace(x.e)$ to stand for the expression $\text{unroll}(\text{self}\lbrace\tau\rbrace(y.\lbrack\text{unroll}(y)/x\rbrack e))$.

$$
\begin{aligned}
\text{unroll}(\text{self}\lbrace\tau\rbrace(y.\lbrack\text{unroll}(y)/x\rbrack e))&\equiv\lbrack\text{self}\lbrace\tau\rbrace(y.\lbrack\text{unroll}(y)/x\rbrack e)/y\rbrack(\lbrack\text{unroll}(y)/x\rbrack e)\\
&\equiv\lbrack\text{unroll}(\text{self}\lbrace\tau\rbrace(y.\lbrack\text{unroll}(y)/x\rbrack e))/x\rbrack e
\end{aligned}
$$

Also in $\text{fix}\lbrace\tau\rbrace(x.e)$ form, we can see that
$$
\begin{aligned}
\text{fix}\lbrace\tau\rbrace(x.e)&=\text{unroll}(\text{self}\lbrace\tau\rbrace(y.\lbrack\text{unroll}(y)/x\rbrack e))\\
&\longmapsto^\ast\lbrack\text{unroll}(\text{self}\lbrace\tau\rbrace(y.\lbrack\text{unroll}(y)/x\rbrack e))/x\rbrack e\\
&=\lbrack\text{fix}\lbrace\tau\rbrace(x.e)/x\rbrack e
\end{aligned}
$$

In this way we define factorial as $\text{fact}\triangleq\text{self }f:\text{nat}\to\text{nat}\text{ is }\lambda(n:\text{nat})\text{ ifz }n\space\lbrace z\hookrightarrow s(z)\shortmid s(n’)\hookrightarrow n\times \text{unroll}(f)(n’)\rbrace$.

The Origin of State

The concept of state in computation has its origins in the concept of recursion, or self-reference.

RS latch as an example maintains its output at logic level of zero or one in response to a signal on the R or S inputs. We can implement an RS latch using recursive types.

The idea is to use self-reference to model the passage of time, with the current output being computed from its input and its previous output. It is a value of type $\tau_{rsl}$ given by
$$
\text{res }t\text{ is }\langle\text{X}\hookrightarrow\text{bool},\text{Q}\hookrightarrow\text{bool},\text{N}\hookrightarrow t\rangle
$$

The X and Q components of the latch represents its current outputs. (Q represents the current of latch), and N represents the next state of the latch.

If $e:\tau_{rsl}$, then we define e @ X to mean $\text{unfold}(e)\cdot \text{X}$, and e @ Q and e @ N are defined similarly.

  • e @ X and e @ Q evaluate to boolean output of latch $e$
  • e @ N evaluates to another latch representing its evolution over time based on its inputs

For given value $r$ and $s$, a new latch is computed from an old latch by the recursive function $rsl$ with definition
$$
\text{fix }rsl\text{ is }\lambda(l:\tau_{rsl})\space e_{rsl}
$$
where $e_{rsl}$ is the expression
$$
\text{fix }this\text{ is fold}(\langle\text{X}\hookrightarrow e_{NOR}(\langle s, l@\text{Q}),\text{Q}\hookrightarrow e_{NOR}(\langle r,l@\text{X}\rangle)),\text{N}\hookrightarrow rsl(this) \rangle)
$$

Coinductive RS Latch

According to the previous settings of lazy dynamics with PCF, we can try to interpret RS latch expression with coinductive type, which still follows the previous $\tau_{rsl}$ type.

Consider an initial state type $\rho\triangleq\langle\text{X}\hookrightarrow\text{bool},\text{Q}\hookrightarrow\text{bool}\rangle$ and we initialize them with $\langle\text{false},\text{false}\rangle$. Then we can get the RS latch expression
$$
\begin{aligned}
e_{rsl}&\triangleq\text{gen}\lbrace t.\tau_{rsl}’\rbrace(\langle\text{X}\hookrightarrow x,\text{Q}\hookrightarrow q\rangle.e_{rsl}’;\langle\text{X}\hookrightarrow\text{false},\text{Q}\hookrightarrow\text{false}\rangle),\text{ where}\\
e_{rsl}’&\triangleq\langle\text{X}\hookrightarrow x,\text{Q}\hookrightarrow q,\text{N}\hookrightarrow\langle e_{nor}\langle s,q\rangle,e_{nor}\langle x,r\rangle\rangle\rangle
\end{aligned}
$$
Then we can simplify previously stated self-reference expression of RS latch like
$$
\displaylines{\text{fix }g\text{ is }\lambda(\langle\text{X}\hookrightarrow x,\text{Q}\hookrightarrow q)\text{ fold}(e_{rsl}’’), \text{ where}\\
e_{rsl}’’\triangleq\langle\text{X}\hookrightarrow x,\text{Q}\hookrightarrow q,\text{N}\hookrightarrow g(e_{nor}\langle s,q\rangle,e_{nor}\langle x,r\rangle)}
$$

SKI Combinator as Recursive Type

Consider the type $\text{D}\triangleq\text{rec }t\text{ is }t\rightharpoonup t$, then we can try to define element $\text{k}:\text{D}$ and $\text{s}:\text{D}$ and application that satisfying:

  • $x:\text{D},y:\text{D}\vdash x\cdot y:\text{D}$
  • $\text{k}\cdot x\cdot y\longmapsto^\ast x$
  • $\text{s}\cdot x\cdot y\cdot z\longmapsto^\ast (x\cdot z)\cdot(y\cdot z)$

We can easily find definition of $\text{k}\triangleq\text{fold}(\lambda(x:\text{D})\space\text{fold}(\lambda(y:\text{D})\space x))$ follows the application convention $x\cdot y\triangleq(\text{unfold}(x))(y)$.

Then $s\triangleq\text{fold}(\lambda(x:\text{D})\space\text{fold}(\lambda(y:\text{D})\space\text{fold}(\lambda(z:\text{D})\space(x\cdot z)\cdot(y\cdot z))))$.