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.