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

s at any level remain untouched; only the contents of bottom `Node`

s 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 `Leaf`

s.

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

s, but there is no possibility of having terminal `Node`

s). 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

- Adamek, Milius, Moss, Initial Algebras, Terminal Coalgebras, and

the Theory of Fixed Points of Functors

April 10, 2020 at 3:50 am

ι

0 : 0 -> μF(F0) : F0 -> μFF! : F0 -> F²0

ι

It seems that we can’t compose ι

(F0) and F!. It should be ι_0 = ι(F0)∘! ?Thank you for writing this series!

April 10, 2020 at 8:40 am

Good catch! I’m glad somebody’s paying attention. Fixed!

April 10, 2020 at 11:39 am

How about looking at Graphs and Graph Databases from Category Theory point-of-view!

April 13, 2020 at 1:25 pm

Why “Stream Void” is not an uninhabited type? How can it be constructed?

April 13, 2020 at 1:46 pm

Stream Void is indeed uninhabited. But in general (Stream a) is inhabited, whereas the initial algebra for (StreamF a) is not.

April 13, 2020 at 1:57 pm

Oh, I see, thanks.

The part when you say “…will produce an uninhabited type (empty set).

Notice that this is differentfrom its terminal coalgebra…” got me confused. But I am not a native English speaker, so…Btw, I’d like to thank you for this blog and your youtube lessons, invaluable materials that are helping me a lot getting my mind around category theory.

Thanks!

April 16, 2020 at 9:53 am

[…] Перевод статьи Бартоша Милевски «Initial Algebra as Directed Colimit» (исходный текст расположен по адресу — Текст оригинальной статьи). […]

April 17, 2020 at 3:51 am

In Haskell the newtype

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

is referred to as the least fix point. How do you show that it corresponds exactly to the colimit you’re talking about in this post?April 17, 2020 at 9:04 am

It doesn’t. You can see that by applying it to the stream functor. The initial algebra is empty, but the fixed point exists and it is the type of infinite streams. I’ll show the details in the next post about coalgebras.

Could you point me to the source of the statement that Fix f is the least fixed point?

April 17, 2020 at 9:40 am

I don’t have a precise reference at the moment. The things which are closer to that are this paper (https://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt) by Wadler where he shows that

`Mu`

is the least fixed point and these answers (https://stackoverflow.com/questions/45580858/what-is-the-difference-between-fix-mu-and-nu-in-ed-kmetts-recursion-scheme-pac and https://stackoverflow.com/questions/61083423/fix-and-mu-isomorphic) which deal with the isomorphism between`Mu`

,`Fix`

and`Nu`

. Moreover in Purescript you have “`Mu f = In (f (Mu f))`

is the least fixed point of a functor f, when it exists” (from https://pursuit.purescript.org/packages/purescript-fixed-points/5.1.0/docs/Data.Functor.Mu#t:Mu)April 17, 2020 at 9:52 am

I’ll talk more about it in the upcoming post. The short story is that Mu is the least fixed point and Nu is the greatest fixed point. They don’t have to be isomorphic. That’s category theory.

So which one is Fix f? It depends on the programming language, in particular, is it lazy or eager? Haskell is lazy, Purescript is eager.

July 21, 2020 at 12:18 am

Referencing the link “Terminal Coalgebras, and the Theory of Fixed Points of Functors” produces “Page not found”. Can this article be accessed?

July 21, 2020 at 12:30 am

Yes, it looks like the link has disappeared.