# Haskell: The Free Boolean Cube

An exploration of things beyond Free and Cofree

# The Free Boolean Cube

There's a concept that I've been working with lately that I've taken to calling 'the free boolean cube'. If you're familiar with the lambda cube, you'll find this to be similar, albeit about different things.

If you are into Haskell and recursion, you may be familiar with the data types `Fix`

, `Free`

, and `Cofree`

.

`data Fix f = Fix (f (Fix f))`

`data Free f a = Pure a | Free (f (Free f a))`

`data Cofree f a = Cofree a (f (Cofree f a))`

Ignoring `Fix`

for the moment (which is just plain recursion), `Free`

and `Cofree`

are infamously duals, analogous to sum types and product types with a dash of recursion mixed in. `Free`

is an exclusive disjunction, better known as `xor`

, whereas `Cofree`

is a conjunction, better known as `and`

, and they are both quite useful when you need to do something with a recursive data structure.

It may help to think of `Cofree`

an annotated structure, and `Free`

as a partial structure. You can use `Cofree`

to attach an annotation to data at every level, or you can use `Free`

to replace data with one instead. This makes `Free`

equivalent to `data Either a b = Left a | Right b`

and `Cofree`

equivalent to `data Pair a b = Pair a b`

, except that we recurse instead of `b`

.

If we squint at the constructors of `Free`

and `Cofree`

, we see that they contain a similar structure: `(f (Free f a))`

and `(f (Cofree f a))`

, and that it really is the same structure as `Fix`

a la `(f (Fix f))`

. In fact, looking at these three, it seems obvious that they are mixes of either annotation `a`

or recursion `f`

, or both.

This begs the question - what about other potential combinations? If `Free`

and `Cofree`

are `Either`

and `Pair`

, then what is the free equivalent of `data These a b = This a | That b | These a b`

? What about other boolean operations? I couldn't find anything about this, so I did a bit of research on my own, and and tried to answer these questions myself.

This has lead me to expand Free vs Cofree into a cube lattice where Free and Cofree are on opposite corners, and the points are all the possible combinations of the constructors `Pure`

, `Free`

, and `Cofree`

, renamed `Annotation`

, `Recursion`

, and `Conjunction`

respectively. We get:

Empty:

`Void`

Annotation:

`Identity a`

aka`a`

Recursion:

`Fix f`

aka`f`

Conjunction:

`Cofree f a`

aka`a * f`

Annotation | Recursion:

`Free f a`

aka`a + f`

Annotation | Conjunction:

`UntoFree f a`

aka`a + (a * f)`

or`a * maybe f`

Recursion | Conjunction:

`OntoFree f a`

aka`f + (a * f)`

or`maybe a * f`

Annotation | Recursion | Conjunction:

`TheseFree f a`

aka`a + f + (a * f)`

(Pardon my nomenclature, it is still experimental).

The dual nature of Free and Cofree is immediately obvious, as they are literally on opposite corners -but if `Free`

and `Cofree`

correspond to `Xor`

and `And`

on the boolean truth table, then some other interesting things leap out.

First off is the obvious correspondence of the `Void`

type having no constructors. Then we have 'just annotation' being equivalent to `Identity a`

. Following that is 'just recursion', which is `Fix f`

. It is interesting to see these pop up out of a truth table, but in retrospect it is very fitting. Then we have `Free`

and `Cofree`

which started this whole thing.

But after them, we have something new. What exactly are `UntoFree`

, `OntoFree`

, and `TheseFree`

? Well, `TheseFree`

corresponds to inclusive disjunction `or`

, whereas Unto `a * maybe f`

and Onto `maybe a * f`

correspond to `p`

and `q`

as columns 10 and 12 of that table.

Note that columns 10 and 12 of that table correspond to projection function in the sense of the second definition, namely that Unto and Onto are surjective (in some hybrid-value-type sense) to

`Identity a`

and`Fix f`

respectively - I hope that makes sense, as I'm still working on defining / outlining it more precisely.

But what do these structures actually mean?

It helps to remember that `Free`

and `Cofree`

are *recursive* sum and product types - that is they aren't just `xor`

and `and`

applied to one level of a data structure, they are applied to all levels. So every level of a `Cofree`

is an annotation plus recursion, and every level of a `Free`

is an annotation else recursion - and as a consequence, every level of `Cofree`

*must* have both, and every level of `Free`

*must not* have both.

But what if we wanted to?

This is where our boolean table has lead us - although we cannot make a `Cofree`

that has some annotations or recursions missing, and we cannot make a `Free`

that keeps both, we now understand the data structures that do allow us to do that sort of thing - `UntoFree`

, `OntoFree`

, and `TheseFree`

. Using our earlier notions of `Cofree`

being 'annotated data' and `Free`

being 'partial data', we can understand `UntoFree`

to be 'fully annotated partial data', `OntoFree`

to be 'partially annotated full data', and thus `TheseFree`

to be 'partially annotated partial data'.

Rather than just fulfilling a table, we've actually found something potentially useful, as this `free cube`

precisely describes the various levels of knowledge one might have about a particular object - something that should be quite useful for developing distributed APIs.

To say that `Free`

and `Cofree`

are duals does not do the concept justice.

It is worth mentioning that the 'free boolean cube' is effectively one half of the free boolean algebra, and that our cube is the triple hasse diagram of `{ann,rec,conj}`

. If we look at it further, it appears that the dimensions of our cube unfold in a way that relates sum types, product types, and recursion. The sum of annotation and recursion makes `Void`

, `Identity`

, `Fix`

, and `Free`

form a square, and the product of `Identity`

and `Fix`

create a third constructor `Cofree`

that pops it out into a cube. There's more to be said about this in the future.