# 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)\]