2 minute read

Recap for Product/Sum Types

Brief recap for product and sum to have a consensus on notations.

Product Types



\[\frac{\Gamma\vdash e_1:\tau_2,\Gamma\vdash e_2:\tau_2}{\Gamma\vdash <e_1,e_2>:\tau_1\times\tau_2}\]


\[\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



\[\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}\]


\[\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}\]


\[\frac{}{\Gamma\vdash <>:unit}\]

Recursive Types in a Partial Language


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$:



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


What we’ve got here is that: certain types can be characterize as solutions to equations of the form:


$\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\]


\[\frac{\Gamma\vdash e:[rec(t.\tau)/t]\tau}{\Gamma\vdash fold(e):rec(t.\tau)}\]


\[\frac{\Gamma\vdash e:rec(t.\tau)}{\Gamma\vdash unfold(e):[rec(t.\tau)/t]\tau}\]


\[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?

  1. Define a type of self-referential programs, and get $fix(x.e)$ from it
  2. 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$


\[\frac{\Gamma,x:\tau self\vdash e:\tau}{\Gamma\vdash self(x.e):\tau self}\]


\[\frac{\Gamma\vdash e:\tau self}{\Gamma\vdash unroll(e):\tau}\]


\[\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:

  1. We want to get a recursive computation of any type, i.e. $fix(x.e):\tau$, from self types $\tau self$
  2. 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}\]


\[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\]


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