GaeBlogX Arista Networks, Software-Defined Networking

2019-01-20
Yanxi Chen

Recap for Product/Sum Types

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

Recursive Types in a Partial Language

Examples

Natural Numbers

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

Lists

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

From left to right:

Construction

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

which is a/the solution to $t\cong \tau(t)$. i.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$

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:

Solution:

From Self Types to Recursive Types

We want to solve:

Solution: