Recap for Product/Sum TypesPermalink

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

Product TypesPermalink

IntroductionsPermalink

EliminationsPermalink

Sum TypesPermalink

IntroductionPermalink

EliminationsPermalink

UnitPermalink

Recursive Types in a Partial LanguagePermalink

ExamplesPermalink

Natural NumbersPermalink

We can write

where $\cong$ means “type isomorphism” which means to write functions back and forth that compose to the identity.

From left to right:

From right to left:

It works because anything is observationally equivalent to $<>$ at type $unit$:

ListsPermalink

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

From left to right:

ConstructionPermalink

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

$N$ solves $t=unit+t$

$\tau list$ solves $t=unit+(\tau \times t)$

which is a/the solution to $t\cong \tau \left(t\right)$. i.e.

IntroductionsPermalink

EliminationsPermalink

DynamicsPermalink

Examples using Recursive TypesPermalink

Bridging Recursive Types and ProgramsPermalink

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 TypesPermalink

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$

IntroductionsPermalink

EliminationsPermalink

DynamicsPermalink

Construct Recursive ProgramsPermalink

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 TypesPermalink

We have $\tau self$, and we want:

Solution:

From Self Types to Recursive TypesPermalink

We want to solve:

Solution: