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 `a`

s

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

- Adamek, Introduction to coalgebra
- Michael Barr, Terminal coalgebras for endofunctors on sets