Intermediate Representations

Bytecode

Instructions

Instructions for times:

comm : a * b <=> b * a
assocl : a * (b * c) => (a * b) * c
assocr : (a * b) * c => a * (b * c)
mapl (f : a => b) : a * c => b * c
mapr (f : b => c) : a * b => a * c
unitil : a => a * 1
unitir : a => 1 * a
unitel : a * 1 => a
uniter : 1 * a => a

Instructions for plus:

comm : a + b <=> b + a
assocl : a + (b + c) => (a + b) + c
assocr : (a + b) + c => a + (b + c)
mapl (f : a => b) : a + c => b + c
mapr (f : b => c) : a + b => a + c
inl (b : type) : a => a + b
inr (b : type) : b => a + b
out : a + a => a

Distributivity:

distl : a * (b + c) => (a * b) + (a * c)
distr : (a + b) * c => (a * c) + (b * c)
factl : (a * b) + (a * c) => a * (b + c)
factr : (a * c) + (b * c) => (a + b) * c

Recursion:

project: rec r. f(r) -> f(rec r. f(r))
embed: f(rec r. f(r)) -> rec r. f(r)

project and embed are no-ops which exist to make type-checking easier (i.e. isorecursive over equirecursive types).

Most instructions are redundant

Most of these instructions are redundant:

All of the l/r variants can be implemented in terms of each other using commutativity.
All of the plus instructions can be implemented in terms of map, in, and out.
Alternatively, we could have replaced map and out with a single instruction, if (f : a => c) (g : b => c) : a + b => c.

So "morally", there are only about 10 instructions: comm, assoc, map, uniti, unite, inl, inr, if, dist, and fact.

Most instructions are reversible

Inverses of instructions:

comm / comm
assocl / assocr
map f / map f*
uniti / unite
dist / fact

The only irreversible instructions are in and out.

Instructions are algebraic laws

We have a symmetric monoidal category with coproducts where * distributes over +. This isn't quite a distributive symmetric monoidal category, because * isn't a product.

Likewise, we almost have a distributive lattice (characterized as a meet-semilattice with binary joins), but * isn't guaranteed to be idempotent.

The reversible fragment is a wide dagger symmetric monoidal subcategory.

That's really all we need

We simply don't need functions, polymorphism, or 0.

0 isn't very interesting when characterized as an initial object or as the unit for +; I find it's only interesting in the context of second-order polymorphism, as forall a. a.

Finite-state 1-bit cons machine

Instructions:

comm
assoc
factor
dist
map
unite
uniti
inl
inr

Redundant instructions:

l/r variants
out

There is a finite number of states, and a state transition table which determines the next state based on the current state and a single bit extracted using dist.

Finite-state random-access 1-bit register machine