One of the tropes of detective movies is the almost miraculous ability to reconstruct an image from a blurry photograph. You just scan the picture, say “enhance!”, and voila, the face of the suspect or the registration number of their car appear on your computer screen.

With constant improvements in deep learning, we might eventually get there. In category theory, though, we do this all the time. We recover lost information. The procedure is based on the basic tenet of category theory: an object is defined by its interactions with the rest of the world. This is the basis of all universal constructions, the Yoneda lemma, Grothendieck fibration, Kan extensions, and practically everything else.

An iconic example is the construction of the left adjoint to a given functor, and that’s what we are going to study here. But first let me explain why I decided to pick this subject, and how it’s related to programming. I wanted to write a blog post about CPS (continuation passing style) and defunctionalization, and I stumbled upon an article in nLab that related defunctionalization to Freyd’s Adjoint Functor Theorem; in particular to the Solution Set Condition. Such an unexpected connection peaked my interest and I decided to dig deeper into it.

Adjunctions

Consider a functor from some category to another category .

A functor, in general, loses some data, so it’s normally impossible to invert it. It produces a “blurry” image of inside . Its left adjoint is a functor from to

that attempts to reconstruct lost information, to the best of its ability. Often the functor is forgetful, which means that it purposefully forgets some information. Its left adjoint is then called free, because it freely ad-libs the forgotten information.

Of course it’s not always possible, but under certain conditions such left adjoint exists. These conditions are spelled out in the Freyd’s General Adjoint Functor Theorem.

To understand them, we have to talk a little about size issues.

Size issues

A lot of interesting categories are large. It means that there are so many objects in the category that they don’t even form a set. The category of all sets, for instance, is large (there is no set of all sets). It’s also possible that morphisms between two objects don’t form a set.

A category in which objects form a set is called small, and a category in which hom-sets are sets is called locally small.

A lot of complexities in Freyd’s theorem are related to size issues, so it’s important to precisely spell out all the assumptions.

We assume that the source of the functor , the category , is locally small. It must also be small-complete, that is, every small diagram in must have a limit. (A small diagram is a functor from a small category.) We also want the functor to be continuous, that is, to preserve all small limits.

If it weren’t for size issues, this would be enough to guarantee the existence of the left adjoint, and we’ll first sketch the proof for this simplified case. In the general case, there is one more condition, the Solution Set Condition, which we’ll discuss later.

Left adjoint and the comma category

Here’s the problem we are trying to solve. We have a functor that maps objects and morphisms from to . We want to define another functor that goes in the opposite direction. We’re not looking for the inverse, so we’re not expecting the composition of this functor with to be identity, but we want it to be related to identity by two natural transformations called unit and counit. Their components are, respectively:

and, as long as they satisfy some additional triangle identities, they will establish the adjunction .

We are going to define point-wise, so let’s pick an object in and try to propagate it back to . To do that, we have to gather as much information about as possible. We will propagate all this information back to and find an object in that “looks the same.” Think of this as creating a hologram of and shipping it back to .

All information about is encoded in morphisms so, in order to generate our hologram, we’ll gather all morphisms that originate in . These morphisms form a category called the coslice category .

The objects in are pairs . In other words, these are all the arrows that emanate from , indexed by their target objects . But what really defines the structure of this category are morphisms between these arrows. A morphism in from to is a morphism that makes the following triangle commute:

We now have complete information about encoded in the slice category, but we have no way to propagate it back to . This is because, in general, the image of doesn’t cover the whole of . Even more importantly, not all morphisms in have corresponding morphisms in . We have to scale down our expectations, and define a partial hologram that does not capture all the information about ; only this part which can be back-propagated to using the functor . Such partial hologram is called a comma category .

The objects of are pairs , where is an object in . In other words, these are all the arrows emanating from whose target is in the image of . Again, the important structure is encoded in the morphisms of . These are the arrows in , that make the following diagram commute in

Notice an interesting fact: we can interpret these triangles as commutation conditions in a cone whose apex is and whose base is formed by objects and morphisms in the image of . But not all objects or morphism in the image of are included. Only those morphisms that make the appropriate triangle commute–and these are exactly the morphisms that satisfy the cone condition. So the comma category builds a cone in .

Constructing the limit

We can now take all this information about that’s been encoded in and move it back to . We define a projection functor that maps to , thus forgetting the morphism . What’s important, though, is that this functor keeps the information encoded in the morphisms of , because these are morphisms in .

The image of doesn’t necessarily cover the whole of , because not every has arrows coming from . Similarly, only some morphisms, the ones that make the appropriate triangle in commute, are picked by . But those objects and morphisms that are in the image of form a diagram in . This diagram is our partial hologram, and we can use it to pick an object in that looks almost exactly like . That object is the limit of this diagram. We pick the limit of this diagram as the definition of : the left adjoint of acting on .

Here’s the tricky part: we assumed that was small-complete, so every small diagram has a limit; but the diagram defined by is not necessarily small. Let’s ignore this problem for a moment, and continue sketching the proof. We want to show that the mapping that assigns the limit of to every is left adjoint to .

Let’s see if we can define the unit of the adjunction:

Since we have defined as the limit of the diagram and preserves limits (small limits, really; but we are ignoring size problems for the moment) then must be the limit of the diagram in . But, as we noted before, the diagram is exactly the base of the cone with the apex that we used to define the comma category . Since is the limit of this diagram, there must be a unique morphism from any other cone to it. In particular there must be a morphism from to it, because is an apex of the cone defined by the comma category. And that’s the morphism we’ll chose as our .

Incidentally, we can interpret itself as an object of the comma category , namely the one defined by the pair . In fact, this is the initial object in that category. If you pick any other object, say, , you can always find a morphism , which is just a leg, a projection, in the limiting cone that defines . It is automatically a morphism in because the following triangle commutes:

This is the triangle that defines as a morphism of cones, from the top cone with the apex , to the bottom (limiting) cone with the apex . We’ll use this interpretation later, when discussing the full version of the Freyd’s theorem.

We can also define the counit of the adjunction. Its component at is a morphism

First, we repeat our construction starting with . We define the comma category and use to create the diagram whose limit is . We pick to be a projection in the limiting cone. We are guaranteed that is in the base of the cone, because it’s the image of under .

To complete this proof, one should show that the unit and counit are natural transformations and that they satisfy triangle identities.

End of a comma category

An interesting insight into this construction can be gained using the end calculus. In my previous post, I talked about (weighted) colimits as coends, but the same argument can be dualized to limits and ends. For instance, this is our comma category as a category of elements in the coend notation:

The limit of of the projection functor over the comma category can be written in the end notation as

This, in turn, can be rewritten as a weighted limit, with every weighted by the set :

The pitchfork here is the power (cotensor) defined by the equation

You may think of as the product of copies of the object , where is a set. The name power conveys the idea of iterated multiplication. Or, since power is a special case of exponentiation, you may think of as a function object imitating mappings from to .

To continue, if the left adjoint exists, the weighted limit in question can be replaced by

which, using standard calculus of ends (see Appendix), can be shown to be isomorphic to . We end up with:

Solution set condition

So what about those pesky size issues? It’s one thing to demand the existence of all small limits, and a completely different thing to demand the existence of large limits (such requirement may narrow down the available categories to preorders). Since the comma category may be too large, maybe we can cut it down to size by carefully picking up a (small) set of objects out of all objects of . We may take some indexing set and construct a family of objects of indexed by elements of . It doesn’t have to be one family for all—we may pick a different family for every object for which we are performing our construction.

Instead of using the whole comma category , we’ll limit ourselves to a set of arrows . But in a comma category we also have morphisms between arrows. In fact they are the essential carriers of the structure of the comma category. Let’s have another look at these morphisms.

This commuting condition can be re-interpreted as a factorization of through . It so happens that every morphism can be trivially factorized through some by picking and . But if we restrict the factors to be members of the family then not every (for arbitrary ) can be automatically factorized. We have to demand it. That gives us the following:

Solution Set Condition: For every object there exists a small set with an -indexed family of objects in and a family of morphisms , such that every morphism can be factored through one of . That is, there exists a morphism such that

There is a shorthand for this statement: All comma categories admit weakly initial families of objects. We’ll come back to it later.

Freyd’s theorem

We can now formulate:

Freyd’s Adjoint Functor Theorem: If is a locally small and small-complete category, and the functor is continuous (small-limit preserving), and it satisfies the solution set condition, then has a left adjoint.

We’ve seen before that the key to defining the point-wise left adjoint was to find the initial object in the comma category . The problem is that this comma category may be large. So the trick is to split the proof into two parts: first defining a weakly initial object, and then constructing the actual initial object using equalizers. A weakly initial object has morphisms to every object in the category but, unlike its strong version, these morphisms don’t have to be unique.

An even weaker notion is that of a weakly initial set of objects. These are objects that among themselves have arrows to every object in the category, but it’s possible that no individual object has all the arrows. The solution set in Freyd’s theorem is such a weakly initial set in the comma category . Since we assumed that is small-complete, we can take a product of these objects and show that it’s weakly initial. The proof then proceeds with the construction of the initial object.

The details of the proof can be found in any category theory text or in nLab.

Next we’ll see the application of these results to the problem of defunctionalization of computer programs.

Appendix

To show that

it’s enough to show that the hom-functors from an arbitrary object are isomorphic

I used the continuity of the hom-functor, the definition of the power (cotensor) and the ninja Yoneda lemma.

It’s funny how similar ideas pop up in different branches of mathematics. Calculus, for instance, is built around metric spaces (or, more generally, Banach spaces) and measures. A limit of a sequence is defined by points getting closer and closer together. An integral is an area under a curve. In category theory, though, we don’t talk about distances or areas (except for Lawvere’s take on metric spaces), and yet we have the abstract notion of a limit, and we use integral notation for ends. The similarities are uncanny.

This blog post was inspired by my trying to understand the idea behind the Freyd’s adjoint functor theorem. It can be expressed as a colimit over a comma category, which is a special case of a Grothendieck fibration. To understand it, though, I had to get a better handle on weighted colimits which, as I learned, were even more general than Kan extensions.

Category of elements as coend

Grothendieck fibration is like splitting a category in two orthogonal directions, the base and the fiber. Fiber may vary from object to object (as in dependent types, which are indeed modeled as fibrations).

The simplest example of a Grothendieck fibration is the category of elements, in which fibers are simply sets. Of course, a set is also a category—a discrete category with no morphisms between elements, except for compulsory identity morphisms. A category of elements is built on top of a category using a functor

  

Such a functor is traditionally called a copresheaf (this construction works also on presheaves, ). Objects in the category of elements are pairs where is an object in , and is an element of a set.

A morphism from to is a morphism in , such that .

There is an obvious projection functor that forgets the second component of the pair

  

(In fact, a general Grothendieck fibration starts with a projection functor.)

You will often see the category of elements written using integral notation. An integral, after all, is a gigantic sum of tiny slices. Similarly, objects of the category of elements form a gigantic sum (disjoint union) of sets . This is why you’ll see it written as an integral

  

However, this notation conflicts with the one for conical colimits so, following Fosco Loregian, I’ll write the category of elements as

  

An interesting specialization of a category of elements is a comma category. It’s the category of arrows originating in the image of the functor and terminating at a fixed object in . The objects of are pairs where is an object in and is a morphism in . These morphisms are elements of the hom-set , so the comma category is just a category of elements for the functor

  

You’ll mostly see integral notation in the context of ends and coends. A coend of a profunctor is like a trace of a matrix: it’s a sum (a coproduct) of diagonal elements. But (co-)end notation may also be used for (co-)limits. Using the trace analogy, if you fill rows of a matrix with copies of the same vector, the trace will be the sum of the components of the vector. Similarly, you can construct a profunctor from a functor by repeating the same functor for every value of the first argument :

  

The coend over this profunctor is the colimit of the functor, a colimit being a generalization of the sum. By slight abuse of notation we write it as

  

This kind of colimit is called conical, as opposed to what we are going to discuss next.

Weighted colimit as coend

A colimit is a universal cocone under a diagram. A diagram is a bunch of objects and morphisms in selected by a functor from some indexing category . The legs of a cocone are morphisms that connect the vertices of the diagram to the apex of the cocone.

For any given indexing object , we select an element of the hom-set , as a wire of the cocone. This is a selection of an element of a set (the hom-set) and, as such, can be described by a function from the singleton set . In other words, a wire is a member of . In fact, we can describe the whole cocone as a natural transformation between two functors, one of them being the constant functor . The set of cocones is then the set of natural transformations:

  

Here, is the category of presheaves, that is functors from to , with natural transformations as morphisms. As a bonus, we get the cocone triangle commuting conditions from naturality.

Using singleton sets to pick morphisms doesn’t generalize very well to enriched categories. For conical limits, we are building cocones from zero-thickness wires. What we need instead is what Max Kelly calls cylinders obtained by replacing the constant functor with a more general functor . The result is a weighted colimit (or an indexed colimit, as Kelly calls it), . The set of weighted cocones is defined by natural transformations

  

and the weighted colimit is the universal one of these. This definition generalizes nicely to the enriched setting (which I won’t be discussing here).

Universality can be expressed as a natural isomorphism

  

We interpret this formula as a one-to-one correspondence: for every weighted cocone with the apex there is a unique morphism from the colimit to . Naturality conditions guarantee that the appropriate triangles commute.

A weighted colimit can be expressed as a coend (see Appendix 1)

  

The dot here stands for the tensor product of a set by an object. It’s defined by the formula

  

If you think of as the sum of copies of the object , then the above asserts that the set of functions from a sum (coproduct) is equivalent to a product of functions, one per element of the set ,

  

Right adjoint as a colimit

A fibration is like a two-dimensional category. Or, if you’re familiar with bundles, it’s like a fiber bundle, which is locally isomorphic to a cartesian product of two spaces, the base and the fiber. In particular, the category of elements is, roughly speaking, like a bundle whose base is the category , and the fiber is a (-dependent) set .

We also have a projection functor on the category of elements that ignores the component

  

The coend of this functor is the (conical) colimit

  

But this functor is constant along the fiber, so we can “integrate over it.” Since fibers depends on , different objects end up weighted differently. The result is a coend over the base category, with objects weighted by sets

  

Using a more traditional notation, this is the formula that relates a (conical) colimit over the category of elements and a weighted colimit of the identity functor

  

There is a category of elements that will be of special interest to us when discussing adjunctions: the comma category for the functor , in which the weight functor is the hom-functor

  

If we plug it into the last formula, we get

  

If the functor has a right adjoint

  

we can rewrite this as

  

and useing the ninja Yoneda lemma (see Appendix 2) we get a formula for the right adjoint in terms of a colimit of a comma category

  

Incidentally, this is the left Kan extension of the identity functor along . (In fact, it can be used to define the right adjoint as long as it preserves the functor .)

We’ll come back to this formula when discussing the Freyd’s adjoint functor theorem.

Appendix 1

I’m going to prove the following identity using some of the standard tricks of coend calculus

  

To show that two objects are isomorphic, it’s enough to show that their hom-sets to any object are isomorphic (this follows from the Yoneda lemma)

  

I first used the universal property of the colimit, then rewrote the set of natural transformations as an end, used the definition of the tensor product of a set and an object, and replaced an end of a hom-set by a hom-set of a coend (continuity of the hom-set functor).

Appendix 2

The proof of

  

follows the same pattern

  

I used the fact that a hom-set from a coend is isomorphic to an end of a hom-set (continuity of hom-sets). Then I applied the definition of a tensor. Finally, I used the Yoneda lemma for contravariant functors, in which the set of natural transformations is written as an end.

  

Previously we discussed ninth chords, which are the first in a series of extension chords. Extensions are the notes that go beyond the first octave. Since we build chords by stacking thirds on top of each other, the next logical step, after the ninth chord, is the eleventh and the thirteenth chords. And that’s it: there is no fifteenth chord, because the fifteenth would be the same as the root (albeit two octaves higher).

This strange musical arithmetic is best understood if we translate all intervals into their semitone equivalents in equal temperament. Since we started by constructing the E major chord, let’s work with the E major scale, which consists of the following notes:

|E |  |F#|  |G#|A  |  |B |  |C#|  |D#|E |

Let’s chart the chord tones taking E as the root.

We see the clash of several naming conventions. Letter names have their origin is the major diatonic scale, as implemented by the white keys on the piano starting from C.

|C |  |D |  |E |F |  |G |  |A |  |B |C |

They go in alphabetical order, wrapping around after G. On the guitar we don’t have white and black keys, so this convention seems rather arbitrary.

The names of intervals (here, marked by digits, with occasional accidental symbols) are also based on the diatonic scale. They essentially count the number of letters from the root (including the root). So the distance from E to B is 5, because you count E, F, G, A, B — five letters. For a mathematician this convention makes little sense, but it is what it is.

After 12 semitones, we wrap around, as far as note names are concerned. With intervals the situation is a bit more nuanced. The ninth can be, conceptually, identified with the second; the eleventh with the fourth; and the thirteenth with the sixth. But how we name the intervals depends on their harmonic function. For instance, the same note, C#, is called the sixth in the E6 chord, and the thirteenth in E13. The difference is that E13 also contains the (dominant) seventh and the ninth.

A full thirteenth chord contains seven notes (root, third, fifth, seventh, ninth, eleventh, and thirteenth), so it cannot possibly be voiced on a six-string guitar. We usually drop the eleventh (as you can see above). The ninth and the fifth can be omitted as well. The root is very important, since it defines the chord, but when you’re playing in a band, it can be taken over by the bass instrument. The third is important because it distinguishes between major and minor modes (but then again, you have power chords that skip the third). The seventh is somewhat important in defining the dominant role of the chord.

Notice that a thirteenth chord can be seen as two separate chords on top of each other. E13 can be decomposed into E7 with F#m on top (try to spot these two shapes in this grip). Seen this way, the major/minor clash is another argument to either drop the eleventh (which serves as the minor third of F#m) or sharp it.

Alternatively, one could decompose E13 into E with DΔ7 on top. The latter shape is also easily recognized in this grip.

I decided against listing eleventh chords because they are awkward to voice on the guitar and because they are rarely used. Thirteenth chords are more frequent, especially in jazz. You’ve seen E13, here’s G13:

It skips the 11th and the 5th; and the 9th at the top is optional.

The Role of Harmonics

It might be worth explaining why omitting the fifth in G13 doesn’t change the character of the chord. The reason is that, when you play the root note, you are also producing harmonics. One of the strongest harmonics is the fifth, more precisely, the fifth over the octave. So, even if you don’t voice it, you can hear it. In fact, a lot of the quality of a given chord voicing depends on the way the harmonics interact with each other, especially in the bass. When you strum the E chord on the guitar, you get a strong root sound E, and the B on the next thickest string amplifies its harmonic fifth. Compare this with the G shape, which also starts with the root, but the next string voices the third, B, which sounds okay, but not great, so some people mute it.

Inverted chords, even though they contain the same notes (up to octave equivalence) may sound dissonant, depending on the context (in particular, voice leading in the bass). This is why we don’t usually play the lowest string in C and A shapes, or the two lowest strings in the D shape.

In the C shape, the third in the bass clashes with the root and is usually muted. That’s because the strongest harmonic of E is B, which makes C/E sound like CΔ7.

On the other hand, when you play the CΔ7 chord, the E in the bass sounds great, for exactly the same reason.

You can also play C with the fifth in the bass, as C/G, and it sounds good, probably because the harmonic D of G gives it the ninth flavor. This harmonic is an octave and a fifth above G, so it corresponds to the D that would be voiced on the third fret of the B string.

The same reasoning doesn’t quite work for the A shape. Firstly, because all four lower strings in A/E voice the very strong power chord (two of them open strings) drowning out the following third. Also the fifth above E is the B that’s just two semitones below the third C# voiced on the B string. (Theoretically, C/G has a third doubled on the thinest string but that doesn’t seem to clash as badly with the D harmonic of G. Again, the ear beats theory!)

Next: Altered chords.

We have already discussed several kinds of seventh chords. But if you can extend the chord by adding a third above it, why not top it with yet another third? This way we arrive at the ninth chord. But a ninth is one whole step above the octave. So far we’ve been identifying notes that cross the octave with their counterparts that are 12 semitones lower. A mathematician would say that we are doing arithmetic modulo 12. But this is just a useful fiction. A lot of things in music theory can be motivated using modular arithmetic, but ultimately, we have to admit that if something doesn’t sound right, it’s not right.

A ninth is 14 semitones above the root (if you don’t flat or sharp it), so it should be identified with the second, which is 2 semitones up from the root. That puts it smack in the middle between the root and the third: a pretty jarring dissonance. We’ve seen a second used in a chord before, but it was playing the role of a suspended third. In a ninth chord, you keep the third, and move the second to the next octave, where it becomes a ninth and cannot do as much damage. Instead it provides color and tension, making things more interesting.

To construct E9, we start with E7. It has the root duplicated on the thinnest string, so it’s easy to raise it by two semitones to produce the ninth.

There are many variations of the ninth chord. There is a minor version, with the third lowered; the seventh can be raised to a major seventh; and the ninth itself can be flatted or sharped. We won’t cover all these.

Following the same pattern, C9 can be constructed from C7 by raising the root by two semitones.

We get a highly movable shape, especially if we put the fifth on the thinnest string. In particular, it can be moved one fret towards the nut to produce B9–a slight modification of the B7 grip we’ve seen before.

If you look carefully at this shape, you might recognize parts of Gm in it (the three thinnest strings). This is no coincidence. The fifth, the seventh, and the ninth of any ninth chord form a minor triad.

Here is the E9 grip obtained by transposing C9 down the fretboard. It’s used a lot in funk:

The same chord with a sharped ninth is called the Hendrix chord, after Jimi Hendrix who popularized it:

The E9 shape is not only movable, but it’s also easy to mutate. This is the minor version:

and this is the major seventh version:

Such chords are quite common in Bossa Nova.

A9 is obtained by raising the root of A7 by two semitones:

Can you spot the Dm shape raised by two frets?

Similarly, G9 is constructed from G7, and it conceals a Dm as part of it.

Next: Extension chords.

The tremendous success, in recent centuries, of science and technology explaining the world around us and improving the human condition helped create the impression that we are on the brink of understanding the Universe. The world is complex, but we seem to have been able to reduce its complexity down to a relatively small number of fundamental laws. These laws are formulated in the language of mathematics, and the idea is that, even if we can’t solve all the equations describing complex systems, at least we can approximate the solutions, usually with the help of computers. These successes led to a feeling bordering on euphoria at the power of our reasoning. Eugene Wigner summed up this feeling in his famous essay, The Unreasonable Effectiveness of Mathematics in the Natural Sciences.

Granted, there are still a few missing pieces, like the unification of gravity with the Standard Model, and the 95% of the mass of the Universe unaccounted for, but we’re working on it… So there’s nothing to worry about, right?

Actually, if you think about it, the idea that the Universe can be reduced to a few basic principles is pretty preposterous. If this turned out to be the case, I would be the first to believe that we live in a simulation. It would mean that this enormous Universe, with all the galaxies, stars, and planets was designed with one purpose in mind: that a bunch of sentient monkeys on the third planet from a godforsaken star in a godforsaken galaxy were able to understand it. That they would be able to build, in their puny brains–maybe extended with some silicon chips and fiber optics–a perfect model of it.

How do we understand things? By building models in our (possibly computer-enhanced) minds. Obviously, it only makes sense if the model is smaller than the actual thing; which is only possible if reality is compressible. Now compare the size and the complexity of the Universe with the size and the complexity of our collective brains. Even with lossy compression, the discrepancy is staggering. But, you might say, we don’t need to model the totality of the Universe, just the small part around us. This is where compositionality becomes paramount. We assume that the world can be decomposed, and that the relevant part of it can be modeled, to a good approximation, independent from the rest.

Reductionism, which has been fueling science and technology, was made possible by the decompositionality of the world around us. And by “around us” I mean not only physical vicinity in space and time, but also proximity of scale. Consider that there are 35 orders of magnitude between us and the Planck length (which is where our most precious model of spacetime breaks down). It’s perfectly possible that the “sphere of decompositionality” we live in is but a thin membrane; more of an anomaly than a rule. The question is, why do we live in this sphere? Because that’s where life is! Call it anthropic or biotic principle.

The first rule of life is that there is a distinction between the living thing and the environment. That’s the primal decomposition.

It’s no wonder that one of the first “inventions” of life was the cell membrane. It decomposed space into the inside and the outside. But even more importantly, every living thing contains a model of its environment. Higher animals have brains to reason about the environment (where’s food? where’s predator?). But even a lowly virus encodes, in its DNA or RNA, the tricks it uses to break into a cell. Show me your RNA, and I’ll tell you how you spread. I’d argue that the definition of life is the ability to model the environment. And what makes the modeling possible is that the environment is decomposable and compressible.

We don’t think much of the possibility of life on the surface of a proton, mostly because we think that the proton is too small. But a proton is closer to our scale than it is to the Planck scale. A better argument is that the environment at the proton scale is not easily decomposable. A quarkling would not be able to produce a model of its world that would let it compete with other quarklings and start the evolution. A quarkling wouldn’t even be able to separate itself from its surroundings.

Once you accept the possibility that the Universe might not be decomposable, the next question is, why does it appear to be so overwhelmingly decomposable? Why do we believe so strongly that the models and theories that we construct in our brains reflect reality? In fact, for the longest time people would study the structure of the Universe using pure reason rather than experiment (some still do). Ancient Greek philosophers were masters of such introspection. This makes perfect sense if you consider that our brains reflect millions of years of evolution. Euclid didn’t have to build a Large Hadron Collider to study geometry. It was obvious to him that two parallel lines never intersect (it took us two thousand years to start questioning this assertion–still using pure reason).

You cannot talk about decomposition without mentioning atoms. Ancient Greeks came up with this idea by pure reasoning: if you keep cutting stuff, eventually you’ll get something that cannot be cut any more, the “uncuttable” or, in Greek, ἄτομον [atomon]. Of course, nowadays we not only know how to cut atoms but also protons and neutrons. You might say that we’ve been pretty successful in our decomposition program. But these successes came at the cost of constantly redefining the very concept of decomposition.

Intuitively, we have no problem imagining the Solar System as composed of the Sun and the planets. So when we figured out that atoms were not elementary, our first impulse was to see them as little planetary systems. That didn’t quite work, and we know now that, in order to describe the composition of the atom, we need quantum mechanics. Things are even stranger when decomposing protons into quarks. You can split an atom into free electrons and a nucleus, but you can’t split a proton into individual quarks. Quarks manifest themselves only under confinement, at high energies.

Also, the masses of the three constituent quarks add up only to one percent of the mass of the proton. So where does the rest of the mass come from? From virtual gluons and quark/antiquark pairs. So are those also the constituents of the proton? Well, sort of. This decomposition thing is getting really tricky once you get into quantum field theory.

Human babies don’t need to experiment with falling into a precipice in order to learn to avoid visual cliffs. We are born with some knowledge of spacial geometry, gravity, and (painful) properties of solid objects. We also learn to break things apart very early in life. So decomposition by breaking apart is very intuitive and the idea of a particle–the ultimate result of breaking apart–makes intuitive sense. There is another decomposition strategy: breaking things into waves. Again, it was Ancient Greeks, Pythagoras who studied music by decomposing it into harmonics, and Aristotle who suggested that sound propagates through movement of air. Eventually we uncovered wave phenomena in light, and then the rest of the electromagnetic spectrum. But our intuitions about particles and weaves are very different. In essence, particles are supposed to be localized and waves are distributed. The two decomposition strategies seem to be incompatible.

Enter quantum mechanics, which tells us that every elementary chunk of matter is both a wave and a particle. Even more shockingly, the distinction depends on the observer. When you don’t look at it, the electron behaves like a wave, the moment you glance at it, it becomes a particle. There is something deeply unsatisfying about this description and, if it weren’t for the amazing agreement with experiment, it would be considered absurd.

Let’s summarize what we’ve discussed so far. We assume that there is some reality (otherwise, there’s nothing to talk about), which can be, at least partially, approximated by decomposable models. We don’t want to identify reality with models, and we have no reason to assume that reality itself is decomposable. In our everyday experience, the models we work with fit reality almost perfectly. Outside everyday experience, especially at short distances, high energies, high velocities, and strong gravitational fields, our naive models break down. A physicist’s dream is to create the ultimate model that would explain everything. But any model is, by definition, decomposable. We don’t have a language to talk about non-decomposable things other than describing what they aren’t.

Let’s discuss a phenomenon that is borderline non-decomposable: two entangled particles. We have a quantum model that describes a single particle. A two-particle system should be some kind of composition of two single-particle systems. Things may be complicated when particles are close together, because of possible interaction between them, but if they move in opposite directions for long enough, the interaction should become negligible. This is what happens in classical mechanics, and also with isolated wave packets. When one experimenter measures the state of one of the particles, this should have no impact on the measurement done by another far-away scientist on the second particle. And yet it does! There is a correlation that Einstein called “the spooky action at a distance.” This is not a paradox, and it doesn’t contradict special relativity (you can’t pass information from one experimenter to the other). But if you try to stuff it into either particle or wave model, you can only explain it by assuming some kind of instant exchange of data between the two particles. That makes no sense!

We have an almost perfect model of quantum mechanical systems using wave functions until we introduce the observer. The observer is the Godzilla-like mythical beast that behaves according to classical physics. It performs experiments that result in the collapse of the wave function. The world undergoes an instantaneous transition: wave before, particle after. Of course an instantaneous change violates the principles of special relativity. To restore it, physicists came up with quantum field theory, in which the observers are essentially relegated to infinity (which, for all intents and purposes, starts a few centimeters away from the point of the violent collision in an collider). In any case, quantum theory is incomplete because it requires an external classical observer.

The idea that measurements may interfere with the system being measured makes perfect sense. In the macro world, when we shine the light on something, we don’t expect to disturb it too much; but we understand that the micro world is much more delicate. What’s happening in quantum mechanics is more fundamental, though. The experiment forces us to switch models. We have one perfectly decomposable model in terms of the Schroedinger equation. It lets us understand the propagation of the wave function from one point to another, from one moment to another. We stick to this model as long as possible, but a time comes when it no longer fits reality. We are forced to switch to a different, also decomposable, particle model. Reality doesn’t suddenly collapse. It’s our model that collapses because we insists–we have no choice!–on decomposability. But if nature is not decomposable, one model cannot possibly fit all of it.

What happens when we switch from one model to another? We have to initialize the new model with data extracted from the old model. But these models are incompatible. Something has to give. In quantum mechanics, we lose determinism. The transition doesn’t tell us how exactly to initialize the new model, it only gives us probabilities.

Notice that this approach doesn’t rely on the idea of a classical observer. What’s important is that somebody or something is trying to fit a decomposable model to reality, usually locally, although the case of entangled particles requires the reconciliation of two separate local models.

Model switching and model reconciliation also show up in the interpretation of the twin paradox in special relativity. In this case we have three models: the twin on Earth, the twin on the way to Proxima Centauri, and the twin on the way back. They start by reconciling their models–synchronizing the clocks. When the astronaut twin returns from the trip, they reconcile their models again. The interesting thing happens at Proxima Centauri, where the second twin turns around. We can actually describe the switch between the two models, one for the trip to, and another for the trip back, using more advanced general relativity, which can deal with accelerating frames. General relativity allows us to keep switching between local models, or inertial frames, in a continuous way. One could speculate that similar continuous switching between wave and particle models is what happens in quantum field theory.

In math, the closest match to this kind of model-switching is in the definition of topological manifolds and fiber bundles. A manifold is covered with maps–local models of the manifold in terms of simple n-dimensional spaces. Transitions between maps are well defined, but there is no guarantee that there exists one global map covering the whole manifold. To my knowledge, there is no theory in which such transitions would be probabilistic.

Seen from the distance, physics looks like a very patchy system, full of holes. Traditional wisdom has it that we should be able to eventually fill the holes and connect the patches. This optimism has its roots in the astounding series of successes in the first half of the twentieth century. Unfortunately, since then we have entered a stagnation era, despite record number of people and resources dedicated to basic research. It’s possible that it’s a temporary setback, but there is a definite possibility that we have simply reached the limits of decomposability. There is still a lot to explore within the decomposability sphere, and the amount of complexity that can be built on top of it is boundless. But there may be some areas that will forever be out of bounds to our reason.

Fig 1. Current decomposability sphere.

• GR: General Relativity (gravity)
• SR: Special Relativity
• PQFT: Perturbative Quantum Field Theory (compatible with SR)
• QM: Quantum Mechanics (non-relativistic)
• BB: Big Bang
• H: Higgs Field
• SB: Symmetry Breaking (inflation)

Previously, we talked about the construction of initial algebras. The dual construction is that of terminal coalgebras. Just like an algebra can be used to fold a recursive data structure into a single value, a coalgebra can do the reverse: it lets us build a recursive data structure from a single seed.

Here’s a simple example. We define a tree that stores values in its nodes

data Tree a = Leaf | Node a (Tree a) (Tree a)

We can build such a tree from a single list as our seed. We can choose the algorithm in such a way that the tree is ordered in a particular way

split :: Ord a => [a] -> Tree a
split [] = Leaf
split (a : as) = Node a (split l) (split r)
  where (l, r) = partition (<a) as

A traversal of this tree will produce a sorted list. We’ll get back to this example after working out some theory behind it.

The functor

The tree in our example can be derived from the functor

data TreeF a x = LeafF | NodeF a x x

instance Functor (TreeF a) where
  fmap _ LeafF = LeafF
  fmap f (NodeF a x y) = NodeF a (f x) (f y)

Let’s simplify the problem and forget about the payload of the tree. We’re interested in the functor

data F x = LeafF | NodeF x x

Remember that, in the construction of the initial algebra, we were applying consecutive powers of the functor to the initial object. The dual construction of the terminal coalgebra involves applying powers of the functor to the terminal object: the unit type () in Haskell, or the singleton set in .

Let’s build a few such trees. Here are a some terms generated by the single power of F

w1, u1 :: F ()
w1 = LeafF
u1 = NodeF () ()

And here are some generated by the square of F acting on ()

w2, u2, t2, s2 :: F (F ())

w2 = LeafF
u2 = NodeF w1 w1
t2 = NodeF w1 u1
s2 = NodeF u1 u1

Or, graphically

Notice that we are getting two kinds of trees, ones that have units () in their leaves and ones that don’t. Units may appear only at the -st layer (root being the first layer) of .

We are also getting some duplication between different powers of . For instance, we get a single LeafF at the level and another one at the level (in fact, at every consecutive level after that as well). The node with two LeafF leaves appears at every level starting with , and so on. The trees without unit leaves are the ones we are familiar with—they are the finite trees. The ones with unit leaves are new and, as we will see, they will contribute infinite trees to the terminal coalgebra . We’ll construct the terminal coalgebra as a limit of an -chain.

Terminal coalgebra as a limit

As was the case with initial algebras, we’ll construct a chain of powers of , except that we’ll start with the terminal rather than the initial object, and we’ll use a different morphism to link them together. By definition, there is only one morphism from any object to the terminal object. In category theory, we’ll call this morphism (upside-down exclamation mark) and implement it in Haskell as a polymorphic function

unit :: a -> ()
unit _ = ()

First, we’ll use to connect to , then lift to connect to , and so on, using to transform to .

Let’s see how it works in Haskell. Applying unit directly to F () turns it into ().

Values of the type F (F ()) are mapped to values of the type F ()

w2' = fmap unit w2
> LeafF
u2' = fmap unit u2
> NodeF () ()
t2' = fmap unit t2
> NodeF () ()
s2' = fmap unit s2
> NodeF () ()

and so on.

The following pattern emerges. contains trees that end with either leaves (at any level) or values of the unit type (only at the lowest, -st level). The lifted morphism (the st power of fmap acting on unit) operates strictly on the th level of a tree. It turns leaves and two-unit-nodes into single units ().

Alternatively, we can look at the preimages of these mappings—conceptually reversing the arrows. Observe that all trees at the level can be seen as generated from the trees at the level by replacing every unit () with either a leaf LeafF or a node NodeF ()().

It’s as if a unit were a universal seed that can either sprout a leaf or a two-unit-node. We’ll see later that this process of growing recursive data structures from seeds corresponds to anamorphisms. Here, the terminal object plays the role of a universal seed that may give rise to two parallel universes. These correspond to the inverse image (a so-called fiber) of the lifted unit.

Now that we have an -chain, we can define its limit. It’s easier to understand a limit in the category of sets. A limit in is a set of cones whose apex is the singleton set.

The simplest example of a limit is a product of sets. In that case, a cone with a singleton at the apex corresponds to a selection of elements, one per set. This agrees with our understanding of a product as a set of tuples.

A limit of a directed finite chain is just the starting set of the chain (the rightmost object in our pictures). This is because all projections, except for the rightmost one, are determined by commuting triangles. In the example below, is determined by :

and so on. Here, every cone from is fully determined by a function , and the set of such functions is isomorphic to .

Things are more interesting when the chain is infinite, and there is no rightmost object—as is the case of our -chain. It turns out that the limit of such a chain is the terminal coalgebra for the functor .

In this case, the interpretation where we look at preimages of the morphisms in the chain is very helpful. We can view a particular power of acting on as a set of trees generated by expanding the universal seeds embedded in the trees from the lower power of . Those trees that had no seeds, only LeafF leaves, are just propagated without change. So the limit will definitely contain all these trees. But it will also contain infinite trees. These correspond to cones that select ever growing trees in which there are always some seeds that are replaced with double-seed-nodes rather than LeafF leaves.

Compare this with the initial algebra construction which only generated finite trees. The terminal coalgebra for the functor TreeF is larger than the initial algebra for the same functor.

We have also seen a functor whose initial algebra was an empty set

data StreamF a x = ConsF a x

This functor has a well-defined non-empty terminal coalgebra. The -th power of (StreamF a) acting on () consists of lists of as

ConsF a1 (ConsF a2 (... (ConsF an ())...))

The lifting of unit acting on such a list replaces the final (ConsF a ()) with () thus shortening the list by one item. Its “inverse” replaces the seed () with any value of type a (so it’s a multi-valued inverse, since there are, in general, many values of a). The limit is isomorphic to an infinite stream of a. In Haskell it can be written as a recursive data structure

data Stream a = ConsF a (Stream a)

Anamorphism

The limit of a diagram is defined as a universal cone. In our case this would be the cone consisting of the object we’ll call , with a set of projections

such that any other cone factors through . We want to show that (if it exists) is a terminal coalgebra.

First, we have to show that is indeed a coalgebra, that is, there exists a morphism

We can apply to the whole diagram. If preserves -limits, then we get a universal cone with the apex and the -chain with on the left. But our original object forms a cone over the same chain (ignoring the projection ). Therefore there must be a unique mapping from it to .

The coalgebra is terminal if there is a unique morphism from any other coalgebra to it. Consider, for instance, a coalgebra . With this coalgebra, we can construct an -chain

We can connect the two omega chains using the terminal morphism from to and all its liftings

Notice that all squares in this diagram commute. The leftmost one commutes because is the terminal object, therefore the mapping from to it is unique, so the composite must be the same as . is therefore an apex of a cone over our original -chain. By universality, there must be a unique morphism from to the limit of this -chain, . This morphism is in fact a coalgebra morphism and is called the anamorphism.

Adjunction

The constructions of initial algebras and terminal coalgebras can be compactly described using adjunctions.

There is an obvious forgetful functor from the category of -algebras to . This functor just picks the carrier and forgets the structure map. Under certain conditions, the left adjoint free functor exists

This adjunction can be evaluated at the initial object (the empty set in ).

This shows that there is a unique algebra morphism—the catamorphism— from to any algebra . This is because the hom-set is a singleton for every . Therefore is the initial algebra .

Conversely, there is a cofree functor

It can be evaluated at a terminal object

showing that there is a unique coalgebra morphism—the anamorphism—from any coalgebra to . This shows that is the terminal coalgebra .

Fixed point

Lambek’s lemma works for both, initial algebras and terminal coalgebras. It states that their structure maps are isomorphisms, therefore their carriers are fixed points of the functor

The difference is that is the least fixed point, and is the greatest fixed point of . They are, in principle, different. And yet, in a programming language like Haskell, we only have one recursively defined data structure defining the fixed point

newtype Fix f = Fix { unFix :: f (Fix f) }

So which one is it?

We can define both the catamorphisms from-, and anamorphisms to-, the fixed point:

type Algebra f a = f a -> a

cata :: Functor f => Algebra f a -> Fix f -> a
cata alg = alg . fmap (cata alg) . unfix

type Coalgebra f a = a -> f a

ana :: Functor f => Coalgebra f a -> a -> Fix f
ana coa = Fix . fmap (ana coa) . coa

so it seems like Fix f is both initial as the carrier of an algebra and terminal as the carrier of a coalgebra. But we know that there are elements of that are not in —namely infinite trees and infinite streams—so the two fixed points are not isomorphic and cannot be both described by the same Fix f.

However, they are not unrelated. Because of the Lambek’s lemma, the initial algebra gives rise to a coalgebra , and the terminal coalgebra generates an algebra .

Because of universality, there must be a (unique) algebra morphism from the initial algebra to , and a unique coalgebra morphism from to the terminal coalgebra . It turns out that these two are given by the same morphism between the carriers. This morphism satisfies the equation

which makes it both an algebra and a coalgebra morphism

Furthermore, it can be shown that, in , is injective: it embeds in . This corresponds to our observation that contains plus some infinite data structures.

The question is, can Fix f describe infinite data? The answer depends on the nature of the programming language: infinite data structures can only exist in a lazy language. Since Haskell is lazy, Fix f corresponds to the greatest fixed point. The least fixed point forms a subset of Fix f (in fact, one can define a metric in which it’s a dense subset).

This is particularly obvious in the case of a functor that has no terminating leaves, like the stream functor.

data StreamF a x = StreamF a x
  deriving Functor

We’ve seen before that the initial algebra for StreamF a is empty, essentially because its action on Void is uninhabited. It does, however have a terminal coalgebra. And, in Haskell, the fixed point of the stream functor indeed generates infinite streams

type Stream a = Fix (StreamF a)

How do we know that? Because we can construct an infinite stream using an anamorphism. Notice that, unlike in the case of a catamorphism, the recursion in an anamorphism doesn’t have to be well founded and, indeed, in the case of a stream, it never terminates. This is why this won’t work in an eager language. But it works in Haskell. Here’s a coalgebra whose carrier is Int

coaInt :: Coalgebra (StreamF Int) Int
coaInt n = StreamF n (n + 1)

It generates an infinite stream of natural numbers

ints = ana coaInt 0

Of course, in Haskell, the work is not done until we demand some values. Here’s the function that extracts the head of the stream:

hd :: Stream a -> a
hd (Fix (StreamF x _)) = x

And here’s one that advances the stream

tl :: Stream a -> Stream a
tl (Fix (StreamF _ s)) = s

This is all true in , but Haskell is not . I had a discussion with Edward Kmett and he pointed out that Haskell’s fixed point data type can be considered the initial algebra as well. Suppose that you have an infinite data structure, like the stream we were just discussing. If you apply a catamorphism for an arbitrary algebra to it, it will most likely never terminate (try summing up an infinite stream of integers). In Haskell, however, this is interpreted as the catamorphism returning the bottom , which is a perfectly legitimate value. And once you start including bottoms in your reasoning, all bets are off. In particular Void is no longer uninhabited—it contains —and the colimit construction of the initial algebra is no longer valid. It’s possible that some of these results can be generalized using domain theory and enriched categories, but I’m not aware of any such work.

Bibliography

1. Adamek, Introduction to coalgebra
2. Michael Barr, Terminal coalgebras for endofunctors on sets

There is a bit of folklore about algebras in Haskell, which says that both the initial algebra and the terminal coalgebra for a given functor are defined by the same fixed point formula. This works for most common cases, but is not true in general. What is definitely true is that they are both fixed points–this result is called the Lambek’s lemma–but there may be many fixed points. The initial algebra is the least fixed point, and the terminal coalgebra is the greatest fixed point.

In this series of blog posts I will explore the ways one can construct these (co-)algebras using category theory and illustrate it with Haskell examples.

In this first installment, I’ll go over the construction of the initial algebra.

A functor

Let’s start with a simple functor that generates binary trees. Normally, we would store some additional data in a tree (meaning, the functor would take another argument), either in nodes or in leaves, but here we’re just interested in pure shapes.

data F a = Leaf 
         | Node a a
  deriving Show

Categorically, this functor can be written as a coproduct (sum) of the terminal object (singleton) and the product of with itself, here written simply as

The lifting of functions is given by this implementation of fmap

instance Functor F where
  fmap _ Leaf       = Leaf
  fmap f (Node x y) = Node (f x) (f y)

We can use this functor to build arbitrary level trees. Let’s consider, for instance, terms of type F Int. We can either build a Leaf, or a Node with two numbers in it

x1, y1 :: F Int
x1 = Leaf
y1 = Node 1 2 

With those, we can build next-level values of the type or, in our case, F (F Int)

x2, y2 :: F (F Int)
x2 = Leaf
y2 = Node x1 y1

We can display y2 directly using show

> Node Leaf (Node 1 2)

or draw the corresponding tree

Since is an endofunctor, so is . Lifting a function to can be implemented by applying fmap twice. Here’s the action of the function (+1) on our test values

fmap (fmap (+1)) x2
> Leaf
fmap (fmap (+1)) y2
> Node Leaf (Node 2 3)

or, graphically,

You can see that Leafs at any level remain untouched; only the contents of bottom Nodes in the tree are transformed.

The colimit construction

The carrier of the initial algebra can be constructed as a colimit of an infinite sequence. This sequence is constructed by applying powers of to the initial object which we’ll denote as . We’ll first see how this works in our example.

The initial object in Haskell is defined as a type with no data constructor (we are ignoring the question of non-termination in Haskell).

data Void
  deriving Show

In Set, this is just an empty set.

The Show instance for Void requires the pragma

{-# language EmptyDataDeriving #-}

Even though there are no values of the type Void, we can still construct a value of the type F Void

z1 :: F Void
z1 = Leaf

This degenerate version of a tree can be drawn as

This illustrates a very important property of our : Its action on an empty set does not produce an empty set. This is what allows us to generate a non-trivial sequence of powers of starting with the empty set.

Not every functor has this property. For instance, the construction of the initial algebra for the functor

data StreamF a x = ConsF a x

will produce an uninhabited type (empty set). Notice that this is different from its terminal coalgebra, which is the infinite stream

data Stream a = Cons a (Stream a)

This is an example of a functor whose initial algebra is not the same as the terminal coalgebra.

Double application of our F to Void produces, again, a Leaf, as well as a Node that contains two Leafs.

z2, v2 :: F (F Void)
z2 = Leaf

v2 = Node z1 z1
> Node Leaf Leaf

Graphically,

In general, powers of acting on Void generate trees which terminate with Leafs, but there is no possibility of having terminal Nodes). Higher and higher powers of acting on Void will eventually produce any tree we can think of. But for any given power, there will exist even larger trees that are not generated by it.

In order to get all the trees, we could try to take a sum (a coproduct) of infinitely many powers. Something like this

The problem is that we’d also get a lot of duplication. For instance, we saw that z1 was the same tree as z2. In general, a single Leaf is produced at all non-zero powers of acting on Void. Similarly, all powers of greater than one produce a single node with two leaves, and so on. Once a particular tree is produced at some power of , all higher powers of will also produce it.

We have to have a way of identifying multiply generated trees. This is why we need a colimit rather than a simple coproduct.

As a reminder, a coproduct is defined as a universal cocone. Here, the base of the cocone is the set of all powers of acting on (Haskell Void).

In a more general colimit, the objects in the base of the cocone may be connected by morphisms.

Coming from the initial object, there can be only one morphism. We’ll call this morphism or, in Haskell, absurd

absurd :: Void -> a
absurd a = case a of {}

This definition requires another pragma

{-# language EmptyCase #-}

We can construct a morphism from to as a lifting of , . In Haskell, the lifting of absurd doesn’t change the shape of trees. Here it is acting on a leaf

z1' :: F (F Void)
z1' = fmap absurd z1
> Leaf

We can continue this process of lifting absurd to higher and higher powers of

z2', v2' :: F (F (F Void))

z2' = fmap (fmap absurd) z2
> Leaf

v2' = fmap (fmap absurd) v2
> Node Leaf Leaf

We can construct an infinite chain (this kind of directed chain indexed by natural numbers is called an -chain)

We can use this chain as the base of our cocone. The colimit of this chain is defined as the universal cocone. We will call the apex of this cocone

In these constructions have simple interpretations. A coproduct is a discriminated union. A colimit is a discriminated union in which we identify all those injections that are connected by morphisms in the base of the cocone. For instance

and so on.

Here we use the lifted absurd (or in the picture above) as the morphisms that connect the powers of acting of Void (or in the picture).

These are exactly the identifications that we were looking for. For instance, maps the leaf generated by to the leaf which is the element of . Or, translating it to Haskell, (fmap absurd) maps the leaf generated by F Void to the leaf generated by F (F Void), and so on.

All trees generated by the ‘th power of are injected into the ‘st power of by absurd lifted by the th power of .

The colimit is formed by equivalence classes with respect to these identifications. In particular, there is a class for a degenerate tree consisting of a single leaf whose representative can be taken from F Void, or from F (F Void), or from F (F (F Void)) and so on.

Initiality

The colimit is exactly the initial algebra for the functor . This follows from the universal property of the colimit. First we will show that for any algebra there is a unique morphism from to . Indeed, we can build a cocone with at its apex and the injections given by

and so on…

Since the colimit is defined by the universal cocone, there is a unique morphism from it to . It can be shown that this morphism is in fact an algebra morphism. This morphism is called a catamorphism.

Fixed Point

Lambek’s lemma states that the initial algebra is a fixed point of the functor that defines it

This can also be seen directly, by applying the functor to every object and morphism in the -chain that defines the colimit. We get a new chain that starts at

But the colimit of this chain is the same as the colimit of the original chain. This is becuase we can always add back the initial object to the chain, and define its injection as the composite

On the other hand, if we apply to the whole universal cocone, we’ll get a new cocone with the apex . In principle, this cocone doesn’t have to be universal, so we cannot be sure that is a colimit. If it is, we say that preserves the particular type of colimit—here, the -colimit.

Remember: the image of a cocone under a functor is always a cocone (this follows from functoriality). Preservation of colimits is an additional requirement that the image of a universal cocone be universal.

The result is that, if preserves -colimits, then the initial algebra is a fixed point of

because both sides can be obtained as a colimit of the same -chain.

Bibliography

1. Adamek, Milius, Moss, Initial Algebras, Terminal Coalgebras, and
   the Theory of Fixed Points of Functors

We live in interesting times. For instance, we are witnessing several extinction events all at once. One of them is the massive extinction of species. The other is the extinction of jobs. Both are caused by advances in technology. As programmers, we might consider ourselves immune to the latter–after all, somebody will have to program these self-driving trucks that eliminate the need for drivers, or the diagnostic tools that eliminate the need for doctors. Eventually, though, even programming jobs will be automated. I can imagine the last programmer putting finishing touches on the program that will make his or her job redundant.

But before we get there, let’s consider which programming tasks are the first to go, and which have the biggest chance to persist for the longest time. Experience tells us that it’s the boring menial jobs that get automated first. So any time you get bored with your work, take note: you are probably doing something that a computer could do better.

One such task is the implementation of user interfaces. All this code that’s behind various buttons, input fields, sliders, etc., is pretty much standard. Granted, you have to put a lot of effort to make the code portable to a myriad of platforms: various desktops, web browsers, phones, watches, fridges, etc. But that’s exactly the kind of expertise that is easily codified. If you find yourself doing copy and paste programming, watch out: your buddy computer can do it too. The work on generating UI has already started, see for instance, pix2code.

The design of user interfaces, as opposed to their implementation, will be more resistant to automation. Not only because it involves creativity, but also because it deals with human issues. Good design must serve the human in front of it. I’m not saying that modeling a human user is impossible, but it’s definitely harder. Of course, in many standard tasks, a drastically simplified human model will work just fine.

So I’m sorry to say that, but those programmers who specialize in HTML and JavaScript will have to retrain themselves.

The next job on the chopping block, in my opinion, is that of a human optimizer. In fact the only reason it hasn’t been eliminated yet is economical. It’s still cheaper to hire people to optimize code than it is to invest in the necessary infrastructure. You might think that programmers are expensive–the salaries of programmers are quite respectable in comparison to other industries. But if this were true, a lot more effort would go into improving programmers’ productivity, in particular in creating better tools. This is not happening. But as demand for software is growing, and the AI is getting cheaper, at some point the economic balance will change. It will be advantageous to use AI to optimize code.

I’m sorry to say that, but C and C++ programmers will have to go. These are the languages whose only raison d’être is to squeeze maximum performance from hardware. We’ll probably always be interested in performance, but there are other ways of improving it. We are familiar with optimizing compilers that virtually eliminated the job of an assembly language programmer. They use optimizers that are based on algorithmic principles–that is methods which are understandable to humans. But there is a whole new generation of AI waiting in the aisles, which can be trained to optimize code written in higher level languages. Imagine a system, which would take this definition of quicksort written in Haskell:

qsort [] = []
qsort (p:xs) = qsort lesser ++ [p] ++ qsort greater
    where (lesser, greater) = partition (< p) xs

and produce code that would run as fast as its hand-coded C counterpart. Even if you don’t know Haskell, I can explain this code to you in just a few sentences. The first line says that sorting an empty list produces an empty list. The second line defines the action of quicksort on a list that consists of a head p–that will be our pivot–and the tail xs. The result is the concatenation (the symbol ++) of three lists. The first one is the result of (recursively) sorting the list lesser, the second is the singleton list containing the pivot, and the third is the result of sorting the list greater. Finally, the pair of lists (lesser, greater) is produced by partitioning xs using the predicate (< p), which reads “less than p.” You can’t get any simpler than that.

Of course the transformation required for optimizing this algorithm is highly nontrivial. Depending on the rest of the program, the AI might decide to change the representation of data from a list to a vector, replace copying by destructive swapping, put some effort in selecting a better pivot, use a different algorithm for sorting very short lists, and so on. This is what a human optimizer would do. But how much harder is this task than, say, playing a game of go against a grandmaster?

I am immensely impressed with the progress companies like Google or IBM made in playing go, chess, and Jeopardy, but I keep asking myself, why don’t they invest all this effort in programming technology? I can’t help but see parallels with Ancient Greece. The Ancient Greeks made tremendous breakthroughs in philosophy and mathematics–just think about Plato, Socrates, Euclid, or Pythagoras–but they had no technology to speak of. Hero of Alexandria invented a steam engine, but it was never put to work. It was only used as a parlor trick. There are many explanations of this phenomenon, but one that strikes close to home is that the Greeks didn’t need technology because they had access to cheap labor through slavery. I’m not implying that programmers are treated like slaves–far from it–but they seem to be considered cheap labor. In fact it’s so cheap to produce software that most of it is given away for free, or for the price of users’ attention in ad-supported software. A lot of software is just bait that’s supposed to entice the user to buy something more valuable, like beer.

It’s gradually becoming clear that programming jobs are diverging. This is not yet reflected in salaries, but as the job market matures, some programming jobs will be eliminated, others will increase in demand. The one area where humans are still indispensable is in specifying what has to be done. The AI will eventually be able to implement any reasonable program, as long as it gets a precise enough specification. So the programmers of the future will stop telling the computer how to perform a given task; rather they will specify what to do. In other words, declarative programming will overtake imperative programming. But I don’t think that explaining to the AI what it’s supposed to do will be easy. The AI will continue to be rather dumb, at least in the foreseeable future. It’s been noted that software that can beat the best go players in the world would be at a complete loss trying to prepare a dinner or clean the dishes. It’s able to play go because it’s reasonably easy to codify the task of playing go– the legal moves and the goal of the game. Humans are extremely bad at expressing their wishes, as illustrated by the following story:

A poor starving peasant couple are granted three wishes and the woman, just taking the first thing that comes to her mind, wishes for one sausage, which she receives immediately. Her husband, pointing out that she could have wished for immense wealth or food to last them a lifetime, becomes angry with her for making such a stupid wish and, not thinking, wishes the sausage were stuck on her nose. Sure enough, the sausage is stuck in the middle of her face, and then they have to use the third wish to make it go away, upon which it disappears completely.

As long as the dumb AI is unable to guess our wishes, there will be a need to specify them using a precise language. We already have such language, it’s called math. The advantage of math is that it was invented for humans, not for machines. It solves the basic problem of formalizing our thought process, so it can be reliably transmitted and verified. The definition of quicksort in Haskell is very mathematical. It can be easily verified using induction, because it’s recursive, and it operates on a recursive data structure: a list. The first line of code establishes the base case: an empty list is trivially sorted. Then we perform the induction step. We assume that we know how to sort all proper sublists of our list. We create two such sublists by partitioning the tail around the pivot. We sort the sublists, and then construct the final sorted list by inserting the pivot between them. As mathematical proofs go, this one is not particularly hard. In fact, in a typical mathematical text, it would be considered so trivial as to be left as an exercise for the reader.

Still, this kind of mathematical thinking seems to be alien to most people, including a lot of programmers. So why am I proposing it as the “programming language” of the future? Math is hard, but let’s consider the alternatives. Every programming language is a compromise between the human and the computer. There are languages that are “close to the metal,” like assembly or C, and there are languages that try to imitate natural language, like Cobol or SQL. But even in low level languages we try to use meaningful names for variables and functions in an attempt to make code more readable. In fact, there are programs that purposefully obfuscate source code by removing the formatting and replacing names with gibberish. The result is unreadable to most humans, but makes no difference to computers. Mathematical language doesn’t have to be machine readable. It’s a language that was created by the people, for the people. The reason why we find mathematical texts harder to read than, say, C++ code is because mathematicians work at a much higher abstraction level. If we tried to express the same ideas in C++, we would very quickly get completely lost.

Let me give you a small example. In mathematics, a monad is defined as a monoid in the category of endofunctors. That’s a very succinct definition. In order to understand it, you have to internalize a whole tower of abstractions, one built on top of another. When we implement monads in Haskell, we don’t use that definition. We pick a particular very simple category and implement only one aspect of the definition (we don’t implement monadic laws). In C++, we don’t even do that. If there are any monads in C++, they are implemented ad hoc, and not as a general concept (an example is the future monad which, to this day, is incomplete).

There is also some deeper math in the quicksort example. It’s a recursive function and recursion is related to algebras and fixed points. A more elaborate version of quicksort decomposes it into its more fundamental components. The recursion is captured in a combination of unfolding and folding that is called a hylomorphism. The unfolding is described by a coalgebra, while folding is driven by an algebra.

data TreeF a r = Leaf | Node a r r
  deriving Functor

split :: Ord a => Coalgebra (TreeF a) [a]
split [] = Leaf
split (a: as) = Node a l r 
  where (l, r) = partition (< a) as
    
join :: Algebra (TreeF a) [a]
join Leaf = []
join (Node a l r) = l ++ [a] ++ r

qsort :: Ord a => [a] -> [a]
qsort = hylo join split

You might think that this representation is an overkill. You may even use it in a conversation to impress your friends: “Quicksort is just a hylomorphism, what is the problem?” So how is it better than the original three-liner?

qsort [] = []
qsort (p:xs) = qsort lesser ++ [p] ++ qsort greater
    where (lesser, greater) = partition (< p) xs

The main difference is that the flow of control in this new implementation is driven by a data structure generated by the functor TreeF. This functor describes a binary tree whose every node has a value of type a and two children. We use those children in the unfolding process to store lists of elements, lesser ones on the left, greater (or equal) on the right. Then, in the folding process, these children are replenished again–this time with sorted lists. This may seem like an insignificant change, but it uses a different processing ability of our brains. The recursive function tells us a linear, one-dimensional, story. It appeals to our story-telling ability. The functor-driven approach appeals to our visual cortex. There is an up and down, and left and right in the tree. Not only that, we can think of the algorithm in terms of movement, or animation. We are first “growing” the tree from the seed and then “traversing” it to gather the fruit from the branches. These are some powerful metaphors.

If this kind of visualization works for us, it might as well work for the AI that will try to optimize our programs. It may also be able to access a knowledge base of similar algorithms based on recursion schemes and category theory.

I’m often asked by programmers: How is learning category theory going to help me in my everyday programming? The implication being that it’s not worth learning math if it can’t be immediately applied to your current job. This makes sense if you are trying to locally optimize your life. You are close to the local minimum of your utility function and you want to get even closer to it. But the utility function is not constant–it evolves in time. Local minima disappear. Category theory is the insurance policy against the drying out of your current watering hole.

What does Gödel’s incompletness theorem, Russell’s paradox, Turing’s halting problem, and Cantor’s diagonal argument have to do with the fact that negation has no fixed point? The surprising answer is that they are all related through
Lawvere’s fixed point theorem.

Before we dive deep into category theory, let’s unwrap this statement from the point of view of a (Haskell) programmer. Let’s start with some basics. Negation is a function that flips between True and False:

  not :: Bool -> Bool
  not True  = False
  not False = True

A fixed point is a value that doesn’t change under the action of a function. Obviously, negation has no fixed point. There are other functions with the same signature that have fixed points. For instance, the constant function:

  true True  = True
  true False = True

has True as a fixed point.

All the theorems I listed in the preamble (and a few more) are based on a simple but extremely powerful proof technique invented by Georg Cantor called the diagonal argument. I’ll illustrate this technique first by showing that the set of binary sequences is not countable.

Cantor’s job interview question

A binary sequence is an infinite stream of zeros and ones, which we can represent as Booleans. Here’s the definition of a sequence (it’s just like a list, but without the nil constructor), together with two helper functions:

  data Seq a = Cons a (Seq a)
    deriving Functor
  
  head :: Seq a -> a
  head (Cons a as) = a

  tail :: Seq a -> Seq a
  tail (Cons a as) = as

And here’s the definition of a binary sequence:

  type BinSeq = Seq Bool

If such sequences were countable, it would mean that you could organize them all into one big (infinite) list. In other words we could implement a sequence generator that generates every possible binary sequence:

  allBinSeq :: Seq BinSeq

Suppose that you gave this problem as a job interview question, and the job candidate came up with an implementation. How would you test it? I’m assuming that you have at your disposal a procedure that can (presumably in infinite time) search and compare infinite sequences. You could throw at it some obvious sequences, like all True, all False, alternating True and False, and a few others that came to your mind.

What Cantor did is to use the candidate’s own contraption to produce a counter-example. First, he extracted the diagonal from the sequence of sequences. This is the code he wrote:

  diag :: Seq (Seq a) -> Seq a
  diag seqs = Cons (head (head seqs)) (diag (trim seqs))

  trim :: Seq (Seq a) -> Seq (Seq a)
  trim seqs = fmap tail (tail seqs)

You can visualize the sequence of sequences as a two-dimensional table that extends to infinity towards the right and towards the bottom.

  T F F T ...
  T F F T ...
  F F T T ...
  F F F T ...
  ...

Its diagonal is the sequence that starts with the fist element of the first sequence, followed by the second element of the second sequence, third element of the third sequence, and so on. In our case, it would be a sequence T F T T ....

It’s possible that the sequence, diag allBinSeq has already been listed in allBinSeq. But Cantor came up with a devilish trick: he negated the whole diagonal sequence:

  tricky = fmap not (diag allBinSeq)

and ran his test on the candidate’s solution. In our case, we would get F T F F ... The tricky sequence was obviously not equal to the first sequence because it differed from it in the first position. It was not the second, because it differed (at least) in the second position. Not the third either, because it was different in the third position. You get the gist…

Power sets are big

In reality, Cantor did not screen job applicants and he didn’t even program in Haskell. He used his argument to prove that real numbers cannot be enumerated.

But first let’s see how one could use Cantor’s diagonal argument to show that the set of subsets of natural numbers is not enumerable. Any subset of natural numbers can be represented by a sequence of Booleans, where True means a given number is in the subset, and False that it isn’t. Alternatively, you can think of such a sequence as a function:

  type Chi = Nat -> Bool

called a characteristic function. In fact characteristic functions can be used to define subsets of any set:

  type Chi a = a -> Bool

In particular, we could have defined binary sequences as characteristic functions on naturals:

  type BinSeq = Chi Nat

As programmers we often use this kind of equivalence between functions and data, especially in lazy languages.

The set of all subsets of a given set is called a power set. We have already shown that the power set of natural numbers is not enumerable, that is, there is no function:

  enumerate :: Nat -> Chi Nat

that would cover all characteristic functions. A function that covers its codomain is called surjective. So there is no surjection from natural numbers to all sequences of natural numbers.

In fact Cantor was able to prove a more general theorem: for any set, the power set is always larger than the original set. Let’s reformulate this. There is no surjection from the set to the set of characteristic functions (where stands for the two-element set of Booleans).

To prove this, let’s be contrarian and assume that there is a surjection:

  enumP :: A -> Chi A

Since we are going to use the diagonal argument, it makes sense to uncurry this function, so it looks more like a table:

  g :: (A, A) -> Bool
  g = uncurry enumP

Diagonal entries in the table are indexed using the following function:

  delta :: a -> (a, a)
  delta x = (x, x)

We can now define our custom characteristic function by picking diagonal elements and negating them, as we did in the case of natural numbers:

  tricky :: Chi A
  tricky = not . g . delta

If enumP is indeed a surjection, then it must produce our function tricky for some value of x :: A. In other words, there exists an x such that tricky is equal to enumP x.
This is an equality of functions, so let’s evaluate both functions at x (which will evaluate g at the diagonal).

  tricky x == (enumP x) x

The left hand side is equal to:

  tricky x = {- definition of tricky -}
  not (g (delta x)) = {- definition of g -}
  not (uncurry enumP (delta x)) = {- uncurry and delta -}
  not ((enumP x) x)

So our assumption that there exists a surjection A -> Chi A led to a contradition!

  not ((enumP x) x) == (enumP x) x

Real numbers are uncountable

You can kind of see how the diagonal argument could be used to show that real numbers are uncountable. Let’s just concentrate on reals that are greater than zero but less than one. Those numbers can be represented as sequences of decimal digits (the digits following the decimal point). If these reals were countable, we could list them one after another, just like we attempted to list all streams of Booleans. We would get some kind of a table infinitely extending to the right and towards the bottom. There is one small complication though. Some numbers have two equivalent decimal representations. For instance is the same as , with infinitely many nines. So lets remove all rows from our table that end in an infinity of nines. We get something like this:

  3 5 0 5 ...
  9 9 0 8 ...
  4 0 2 3 ...
  0 0 9 9 ...
  ...

We can now apply our diagonal argument by picking one digit from every row. These digits form our diagonal number. In our example, it would be 3 9 2 9.

In the previous proof, we negated each element of the sequence to get a new sequence. Here we have to come up with some mapping that changes each digit to something else. For instance, we could add one to it, modulo nine. Except that, again, we don’t want to produce nines, because we could end up with a number that ends in an infinity of nines. But something like this will work just fine:

  h n = if n == 8 
        then 3
        else (n + 1) `mod` 9

The important part is that our function h replaces every digit with a different digit. In other words, h doesn’t have a fixed point.

Lawvere’s fixed point theorem

And this is what Lawvere realized: The diagonal argument establishes the relationship between the existence of a surjection on the one hand, and the existence of a no-fix-point mapping on the other hand. So far it’s been easy to find a no-fix-point functions. But let’s reverse the argument: If there is a surjection then every function must have a fixed point. That’s because, if we could find a no-fixed-point function, we could use the diagonal argument to show that there is no surjection.

But wait a moment. Except for the trivial case of a function on a one-element set, it’s always possible to find a function that has no fixed point. Just return something else than the argument you’re called with. This is definitely true in , but when you go to other categories, you can’t just construct morphisms willy-nilly. Even in categories where morphisms are functions, you might have constraints, such as continuity or smoothness. For instance, every continuous function from a real segment to itself has a fixed point (Brouwer’s theorem).

As usual, translating from the language of sets and functions to the language of category theory takes some work. The tricky part is to generalize the definition of a fixed point and surjection.

Points and string diagrams

First, to define a fixed point, we need to be able to define a point. This is normally done by defining a morphism from the terminal object , such a morphism is called a global element. In , the terminal object is a singleton set, and a morphism from a singleton set just picks an element of a set.

Since things will soon get complicated, I’d like to introduce string diagrams to better visualise things in a cartesian category. In string diagrams lines correspond to objects and dots correspond to morphisms. You read such diagrams bottom up. So a morphism

can be drawn as:

I will use dotted letters to denote “points” or morphisms originating in the unit. It is also customary to omit the unit from the picture. It turns out that everything works just fine with implicit units.

A fixed point of a morphism is a global element such that . Here’s the traditional diagam:

And here’s the corresponding string diagram that encodes the commuting condition.

In string diagrams, morphisms are composed by stringing them along lines in the bottom up direction.

Surjections can be generalized in many ways. The one that works here is called surjection on points. A morphism is surjective on points when for every point of (that is a global element ) there is a point of (the domain of ) that is mapped to . In other words

Or string-diagrammatically, for every there exists an such that:

Currying and uncurrying

To formulate Lawvere’s theorem, we’ll replace with the exponential object , that is an object that represents the set of morphisms from to . Conceptually, those morphism will correspond to rows in our table (or characteristic functions, when is ). The mapping:

generates these rows. I will use barred symbols, like for curried morphisms, that is morphisms to exponentials. The object serves as the source of indexes for enumerating the rows of the table (just like the natural numbers in the previous example). The same object also provides indexing within each row.

This is best seen after uncurrying (we assume that we are in a cartesian closed category). The uncurried morphism, uses a product to index simultaneously into rows and columns of the table, just like pairs of natural numbers we used in the previous example.

The currying relationship between these two is given by the universal construction:

with the following commuting condition:

Here, is the evaluation natural transformation (the couinit of the currying adjunction, or the dollar sign operator in Haskell).

This commuting condition can be visualized as a string diagram. Notice that products of objects correspond to parallel lines going up. Morphisms that operate on products, like or , are drawn as dots that merge such lines.

We are interested in mappings that are point-surjective. In this case, we would like to demand that for every point there is a point such that:

or, diagrammatically, for every there exists an such that:

Conceptually, is a point in , which represents some arbitrary function . Surjectivity of means that we can always find this function in our table by indexing into it with some .

This is a very general way of expressing what, in Haskell, would amount to: Every function f :: A -> Y can be obtained by partially applying our g_bar :: X -> A -> Y to some x :: X.

The diagonal

The way to index the diagonal of our table is to use the diagonal morphism . In a cartesian category, such a morphism always exists. It can be defined using the universal property of the product:

By combining this diagram with the diagram that defines the lifting of a pair of points we arrive at a useful identity:

where is the left unitor, which asserts the isomorphism

Here’s the string diagram representation of this identity:

In string diagrams we ignore unitors (as well as associators). Now you see why I like string diagrams. They make things much simpler.

Lawvere’s fixed point theorem

Theorem. (Lawvere) In a cartesian closed category, if there exists a point-surjective morphism then every endomorphism of must have a fixed point.

Note: Lawvere actually used a weaker definition of point surjectivity.

The proof is just a generalization of the diagonal argument.

Suppose that there is an endomorphims that has no fixed point. This generalizes the negation of the original example. We’ll create a special morphism by combining the diagonal entries of our table, and then “negating” them with .

The table is described by (uncurried) ; and we access the diagonal through . So the tricky morphism is just:

or, in diagramatic form:

Since we were guaranteed that our table is an exhaustive listing of all morphisms , our new morphism must be somewhere there. But in order to search the table, we have to first convert to a point in the exponential object .

There is a one-to-one correspondence between points and morphisms given by the universal property of the exponential (noting that is isomorphic to through the left unitor, ).

In other words, is the curried form of , and we have the following commuting codition:

Since is an isomorphism, we can invert it, and get the following formula for in terms of :

In the corresponding string diagram we omit the unitor altogether.

Now we can use our assumption that is point surjective to deduce that there must be a point that will produce , in other words:

So picks the row in which we find our tricky morphism. What we are interested in is “evaluating” this morphism at . That will be our paradoxical diagonal entry. By construction, it should be equal to the corresponding point of , because this row is point-by-point equal to ; after all, we have just found it by searching for ! On the other hand, it should be different, because we’ve build by “negating” diagonal entries of our table using . Something has to give and, since we insist on surjectivity, we conclude that is not doing its job of “negating.” It must have a fixed point at .

Let’s work out the details.

First, let’s apply the function we’ve found in the table at row to itself. Except that what we’ve found is a point in . Fortunately we have figured out earlier how to get from . We apply the result to :

Plugging into it the entry that we have found in the table, we get:

Here’s the corresponding string diagram:

We can now uncurry

And replace a pair of with a :

Compare this with the defining equation for , as applied to :

In other words, the morphism :

is a fixed point of . This contradicts our assumption that had no fixed point.

Conclusion

When I started writing this blog post I though it would be a quick and easy job. After all, the proof of Lawvere’s theorem takes just a few lines both in the original paper and in all other sources I looked at. But then the details started piling up. The hardest part was convincing myself that it’s okay to disregard all the unitors. It’s not an easy thing for a programmer, because without unitors the formulas don’t “type check.” The left hand side may be a morphism from and the right hand side may start at . A compiler would reject such code. I tried to do due diligence as much as I could, but at some point I decided to just go with string diagrams. In the process I got into some interesting discussions and even posted a question on Math Overflow. Hopefully it will be answered by the time you read this post.

One of the things I wasn’t sure about was if it was okay to slide unitors around, as in this diagram:

It turns out this is just naturality condition for , as John Baez was kind to remind me on Twitter (great place to do category theory!).

Acknowledgments

I’m grateful to Derek Elkins for reading the draft of this post.

Literature

1. F. William Lawvere, Diagonal arguments and cartesian closed categories
2. Noson S. Yanofsky, A Universal Approach to Self-Referential Paradoxes, Incompleteness and Fixed Points
3. Qiaochu Yuan, Cartesian closed categories and the Lawvere fixed point theorem