Recursive Types
Recap for Product/Sum Types
Brief recap for product and sum to have a consensus on notations.
Product Types
\[\tau_1\times\tau_2\]Introductions
\[\frac{\Gamma\vdash e_1:\tau_2,\Gamma\vdash e_2:\tau_2}{\Gamma\vdash <e_1,e_2>:\tau_1\times\tau_2}\]Eliminations
\[\frac{\Gamma\vdash e:\tau_1\times\tau_2}{\Gamma\vdash fst(e):\tau_1}\] \[\frac{\Gamma\vdash e:\tau_1\times\tau_2}{\Gamma\vdash snd(e):\tau_2}\]Sum Types
\[\tau_1+\tau_2\]Introduction
\[\frac{\Gamma\vdash e_1:\tau_1}{\Gamma\vdash inl_{\tau_1,\tau_2}(e_1):\tau_1+\tau_2}\] \[\frac{\Gamma\vdash e_2:\tau_2}{\Gamma\vdash inr_{\tau_1,\tau_2}(e_2):\tau_1+\tau_2}\]Eliminations
\[\frac{\Gamma\vdash e:\tau_1+\tau_2;\Gamma,x_1:\tau_2\vdash e_1:\sigma;\Gamma,x_2:\tau_2\vdash e_2:\sigma}{\Gamma\vdash case(e)of\{inl(x_1)\hookrightarrow e_1,inr(x_2)\hookrightarrow e_2\}:\sigma}\]Unit
\[\frac{}{\Gamma\vdash <>:unit}\]Recursive Types in a Partial Language
Examples
Natural Numbers
We can write
\[\mathbb{N}\cong unit+\mathbb{N}\]where $\cong$ means “type isomorphism” which means to write functions back and forth that compose to the identity.
From left to right:
\[\lambda x:\mathbb{N}:=rec\{0\hookrightarrow inl(<>),s(y)\hookrightarrow inr(y)\}\]From right to left:
\[\lambda x:unit+\mathbb{N}:=case(z)of\{inl(\_)\hookrightarrow 0,inr(y)\hookrightarrow s(y)\}\]It works because anything is observationally equivalent to $<>$ at type $unit$:
\[\_\sim_{unit}<>\]Lists
Any list is either the empty list or a cons with the type and another list.
\[\tau list\cong unit+(\tau\times\tau list)\]From left to right:
\[\lambda l:\tau list:=case(l)of\{[]\hookrightarrow inl(<>),x::xs\hookrightarrow inr(x,xs)\}\]Construction
What we’ve got here is that: certain types can be characterize as solutions to equations of the form:
\[t\cong\sigma(t)\]$\mathbb{N}$ solves $t=unit+t$
$\tau list$ solves $t=unit+(\tau\times t)$
\[\frac{\Delta,t\ type\vdash\tau\ type}{\Delta\vdash rec(t.\tau)\ type}\]which is a/the solution to $t\cong \tau(t)$. i.e.
\[rec(t.\tau)\cong [rec(t.\tau)/t]\tau\]Introductions
\[\frac{\Gamma\vdash e:[rec(t.\tau)/t]\tau}{\Gamma\vdash fold(e):rec(t.\tau)}\]Eliminations
\[\frac{\Gamma\vdash e:rec(t.\tau)}{\Gamma\vdash unfold(e):[rec(t.\tau)/t]\tau}\]Dynamics
\[unfold(fold(e))\mapsto e\]Examples using Recursive Types
\[\mathbb{N}:=rec(t.unit+t)\] \[z:\mathbb{N}:=fold(inl(<>))\] \[s(e):\mathbb{N}:=fold(inr(e))\]Bridging Recursive Types and Programs
In this language, even though there is no loops, no recursive functions in the terms, we can still get general recursion just from self-referencial types. Meaning that self-referential types will give us self-referential codes. How to do?
- Define a type of self-referential programs, and get $fix(x.e)$ from it
- Define the type of self-referential programs from $rec(t.\tau)$
Self Types
The following thing is only used as a bridge between $fix$ and $rec$ such that we can define both $fix$ and $rec$ from it. It’s only to help the constructions.
In the following rules, $x$ could be interpreted as this in a normal programming language.
$\tau self$ represents a self-referential computation of a $\tau$
Introductions
\[\frac{\Gamma,x:\tau self\vdash e:\tau}{\Gamma\vdash self(x.e):\tau self}\]Eliminations
\[\frac{\Gamma\vdash e:\tau self}{\Gamma\vdash unroll(e):\tau}\]Dynamics
\[\frac{}{self(x.e)\ value}\] \[\frac{e\mapsto e'}{unroll(e)\mapsto unroll(e')}\] \[unroll(self(x.e))\mapsto[self(x.e)/x]e\]Construct Recursive Programs
Now we have $\tau self$, the above two steps can be rephrased as:
- We want to get a recursive computation of any type, i.e. $fix(x.e):\tau$, from self types $\tau self$
- We want to get self types $\tau self$ from recursive types $rec(x.e)$
From Recursive Computation to Self Types
We have $\tau self$, and we want:
\[\frac{x:\tau\vdash e:\tau}{fix(x.e):\tau}\] \[\frac{}{fix(x.e)\mapsto[fix(x.e)/x]e}\]Solution:
\[fix(x.e):\tau:=unroll(self(y:\tau self.[unroll(y)/x]e))\]From Self Types to Recursive Types
We want to solve:
\[\tau self\cong \tau self\rightarrow\tau\]Solution:
\[\tau self:=rec(t.(t\rightarrow\tau))\] \[self(x.e):=fold(\lambda (x:\tau self).(e:\tau))\] \[unroll(e):=(unfold(e):\tau self\rightarrow \tau)(e)\]