Initial Algebra as Directed Colimit
source link: https://bartoszmilewski.com/2020/04/09/initial-algebra-as-directed-colimit/
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.
April 9, 2020
Initial Algebra as Directed Colimit
Posted by Bartosz Milewski under Programming [13] Comments
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
Recommend
About Joyk
Aggregate valuable and interesting links.
Joyk means Joy of geeK