GaeBlogX Arista Networks, Software-Defined Networking

Recursive Types


Recap for Product/Sum Types

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

Product Types

Introductions

Eliminations

Sum Types

Introduction

Eliminations

Unit

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.

Introductions

Eliminations

Dynamics

Examples using Recursive Types

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

Eliminations

Dynamics

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:


Similar Posts

Comments

Search