• Recap for Product/Sum Types
  • Product Types
    • Introductions
    • Eliminations
  • Sum Types
    • Introduction
    • Eliminations
  • Unit
• Recursive Types in a Partial Language
  • Examples
    • Natural Numbers
    • Lists
  • Construction
  • Introductions
  • Eliminations
  • Dynamics
  • Examples using Recursive Types
• Bridging Recursive Types and Programs
  • Self Types
    • Introductions
    • Eliminations
    • Dynamics
  • Construct Recursive Programs
    • From Recursive Computation to Self Types
    • From Self Types to Recursive Types

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

Product Types

$$tau_1timestau_2$$

Introductions

$$% <![CDATA[ frac{Gammavdash e_1:tau_2,Gammavdash e_2:tau_2}{Gammavdash <e_1,e_2>:tau_1timestau_2} %]]>$$

Eliminations

$$frac{Gammavdash e:tau_1timestau_2}{Gammavdash fst(e):tau_1}$$
$$frac{Gammavdash e:tau_1timestau_2}{Gammavdash snd(e):tau_2}$$

Sum Types

$$tau_1+tau_2$$

Introduction

$$frac{Gammavdash e_1:tau_1}{Gammavdash inl_{tau_1,tau_2}(e_1):tau_1+tau_2}$$
$$frac{Gammavdash e_2:tau_2}{Gammavdash inr_{tau_1,tau_2}(e_2):tau_1+tau_2}$$

Eliminations

$$frac{Gammavdash e:tau_1+tau_2;Gamma,x_1:tau_2vdash e_1:sigma;Gamma,x_2:tau_2vdash e_2:sigma}{Gammavdash case(e)of{inl(x_1)hookrightarrow e_1,inr(x_2)hookrightarrow e_2}:sigma}$$

Unit

$$% <![CDATA[ frac{}{Gammavdash <>: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:

$$% <![CDATA[ lambda x:mathbb{N}:=rec{0hookrightarrow 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$:

$$% &lt;![CDATA[ _sim_{unit}&lt;&gt; %]]&amp;gt;$$

Lists

Any list is either the empty list or a cons with the type and another list.

$$tau listcong unit+(tautimestau list)$$

From left to right:

$$% &lt;![CDATA[ lambda l:tau list:=case(l)of{[]hookrightarrow inl(&lt;&gt;),x::xshookrightarrow inr(x,xs)} %]]&amp;gt;$$

Construction

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

$$tcongsigma(t)$$

$mathbb{N}$ solves $t=unit+t$

$tau list$ solves $t=unit+(tautimes t)$

$$frac{Delta,t typevdashtau type}{Deltavdash rec(t.tau) type}$$

which is a/the solution to $tcong tau(t)$. i.e.

$$rec(t.tau)cong [rec(t.tau)/t]tau$$

Introductions

$$frac{Gammavdash e:[rec(t.tau)/t]tau}{Gammavdash fold(e):rec(t.tau)}$$

Eliminations

$$frac{Gammavdash e:rec(t.tau)}{Gammavdash unfold(e):[rec(t.tau)/t]tau}$$

Dynamics

$$unfold(fold(e))mapsto e$$

Examples using Recursive Types

$$mathbb{N}:=rec(t.unit+t)$$
$$% &lt;![CDATA[ z:mathbb{N}:=fold(inl(&lt;&gt;)) %]]&amp;gt;$$
$$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$

Introductions

$$frac{Gamma,x:tau selfvdash e:tau}{Gammavdash self(x.e):tau self}$$

Eliminations

$$frac{Gammavdash e:tau self}{Gammavdash unroll(e):tau}$$

Dynamics

$$frac{}{self(x.e) value}$$
$$frac{emapsto 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:tauvdash 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 selfcong tau selfrightarrowtau$$

Solution:

$$tau self:=rec(t.(trightarrowtau))$$
$$self(x.e):=fold(lambda (x:tau self).(e:tau))$$
$$unroll(e):=(unfold(e):tau selfrightarrow tau)(e)$$