Functors from a monoidal category C to Set form a monoidal category with Day convolution as product. A monoid in this category is a lax monoidal functor. We define an initial algebra using a higher order functor and show that it corresponds to a free lax monoidal functor.

Recently I’ve been obsessing over monoidal functors. I have already written two blog posts, one about free monoidal functors and one about free monoidal profunctors. I followed some ideas from category theory but, being a programmer, I leaned more towards writing code than being preoccupied with mathematical rigor. That left me longing for more elegant proofs of the kind I’ve seen in mathematical literature.

I believe that there isn’t that much difference between programming and math. There is a whole spectrum of abstractions ranging from assembly language, weakly typed languages, strongly typed languages, functional programming, set theory, type theory, category theory, and homotopy type theory. Each language comes with its own bag of tricks. Even within one language one starts with some relatively low level encodings and, with experience, progresses towards higher abstractions. I’ve seen it in Haskell, where I started by hand coding recursive functions, only to realize that I can be more productive using bulk operations on types, then building recursive data structures and applying recursive schemes, eventually diving into categories of functors and profunctors.

I’ve been collecting my own bag of mathematical tricks, mostly by reading papers and, more recently, talking to mathematicians. I’ve found that mathematicians are happy to share their knowledge even with outsiders like me. So when I got stuck trying to clean up my monoidal functor code, I reached out to Emily Riehl, who forwarded my query to Alexander Campbell from the Centre for Australian Category Theory. Alex’s answer was a very elegant proof of what I was clumsily trying to show in my previous posts. In this blog post I will explain his approach. I should also mention that most of the results presented in this post have already been covered in a comprehensive paper by Rivas and Jaskelioff, Notions of Computation as Monoids.

Lax Monoidal Functors

To properly state the problem, I’ll have to start with a lot of preliminaries. This will require some prior knowledge of category theory, all within the scope of my blog/book.

We start with a monoidal category C, that is a category in which you can “multiply” objects using some kind of a tensor product \otimes. For any pair of objects a and b there is an object a \otimes b; and this mapping is functorial in both arguments (that is, you can also “multiply” morphisms). A monoidal category will also have a special object I that is the unit of multiplication. In general, the unit and associativity laws are satisfied up to isomorphism:

\lambda : I \otimes a \cong a

\rho : a \otimes I \cong a

\alpha : (a \otimes b) \otimes c \cong a \otimes (b \otimes c)

These isomorphisms are called, respectively, the left and right unitors, and the associator.

The most familiar example of a monoidal category is the category of types and functions, in which the tensor product is the cartesian product (pair type) and the unit is the unit type ().

Let’s now consider functors from C to the category of sets, Set. These functors also form a category called [C, Set], in which morphisms between any two functors are natural transformations.

In Haskell, a natural transformation is approximated by a polymorphic function:

type f ~> g = forall x. f x -> g x

The category Set is monoidal, with cartesian product \times serving as a tensor product, and the singleton set 1 as the unit.

We are interested in functors in [C, Set] that preserve the monoidal structure. Such a functor should map the tensor product in C to the cartesian product in Set and the unit I to the singleton set 1. Accordingly, a strong monoidal functor F comes with two isomorphisms:

F a \times F b \cong F (a \otimes b)

1 \cong F I

We are interested in a weaker version of a monoidal functor called lax monoidal functor, which is equipped with a one-way natural transformation:

\mu : F a \times F b \to F (a \otimes b)

and a one-way morphism:

\eta : 1 \to F I

A lax monoidal functor must also preserve unit and associativity laws.

laxassoc

Associativity law: \alpha is the associator in the appropriate category (top arrow, in Set; bottom arrow, in C).

Right unit law. ρ is the right unitor in the appropriate category.
Left unit law. λ is the left unitor in the appropriate category.

In Haskell, a lax monoidal functor can be defined as:

class Monoidal f where
  eta :: () -> f ()
  mu  :: (f a, f b) -> f (a, b)

It’s also known as the applicative functor.

Day Convolution and Monoidal Functors

It turns out that our category of functors [C, Set] is also equipped with monoidal structure. Two functors F and G can be “multiplied” using Day convolution:

(F \star G) c = \int^{a b} C(a \otimes b, c) \times F a \times G b

Here, C(a \otimes b, c) is the hom-set, or the set of morphisms from a \otimes b to c. The integral sign stands for a coend, which can be interpreted as a generalization of an (infinite) coproduct (modulo some identifications). An element of this coend can be constructed by injecting a triple consisting of a morphism from C(a \otimes b, c), an element of the set F a, and an element of the set G b, for some a and b.

In Haskell, a coend corresponds to an existential type, so the Day convolution can be defined as:

data Day f g c where
  Day :: ((a, b) -> c, f a, g b) -> Day f g c

(The actual definition uses currying.)

The unit with respect to Day convolution is the hom-functor:

C(I, -)

which assigns to every object c the set of morphisms C(I, c) and acts on morphisms by post-composition.

The proof that this is the unit is instructive, as it uses the standard trick: the co-Yoneda lemma. In the coend form, the co-Yoneda lemma reads, for a covariant functor F:

\int^x C(x, a) \times F x \cong F a

and for a contravariant functor H:

\int^x C(a, x) \times H x \cong H a

(The mnemonics is that the integration variable must appear twice, once in the negative, and once in the positive position. An argument to a contravariant functor is in a negative position.)

Indeed, substituting C(I, -) for the first functor in Day convolution produces:

(C(I, -) \star G) c = \int^{a b} C(a \otimes b, c) \times C(I, a) \times G b

which can be “integrated” over a using the Yoneda lemma to yield:

\int^{b} C(I \otimes b, c) \times G b

and, since I is the unit of the tensor product, this can be further “integrated” over b to give G c. The right unit law is analogous.

To summarize, we are dealing with three monoidal categories: C with the tensor product \otimes and unit I, Set with the cartesian product and singleton 1, and a functor category [C, Set] with Day convolution and unit C(I, -).

A Monoid in [C, Set]

A monoidal category can be used to define monoids. A monoid is an object m equipped with two morphisms — unit and multiplication:

\eta : I \to m

\mu : m \otimes m \to m

monoid-1

These morphisms must satisfy unit and associativity conditions, which are best illustrated using commuting diagrams.

monunit

Unit laws. λ and ρ are the unitors.

monassoc

Associativity law: α is the associator.

This definition of a monoid can be translated directly to Haskell:

class Monoid m where
  eta :: () -> m
  mu  :: (m, m) -> m

It so happens that a lax monoidal functor is exactly a monoid in our functor category [C, Set]. Since objects in this category are functors, a monoid is a functor F equipped with two natural transformations:

\eta : C(I, -) \to F

\mu : F \star F \to F

At first sight, these don’t look like the morphisms in the definition of a lax monoidal functor. We need some new tricks to show the equivalence.

Let’s start with the unit. The first trick is to consider not one natural transformation but the whole hom-set:

[C, Set](C(I, -), F)

The set of natural transformations can be represented as an end (which, incidentally, corresponds to the forall quantifier in the Haskell definition of natural transformations):

\int_c Set(C(I, c), F c)

The next trick is to use the Yoneda lemma which, in the end form reads:

\int_c Set(C(a, c), F c) \cong F a

In more familiar terms, this formula asserts that the set of natural transformations from the hom-functor C(a, -) to F is isomorphic to F a.

There is also a version of the Yoneda lemma for contravariant functors:

\int_c Set(C(c, a), H c) \cong H a

The application of Yoneda to our formula produces F I, which is in one-to-one correspondence with morphisms 1 \to F I.

We can use the same trick of bundling up natural transformations that define multiplication \mu.

[C, Set](F \star F, F)

and representing this set as an end over the hom-functor:

\int_c Set((F \star F) c, F c)

Expanding the definition of Day convolution, we get:

\int_c Set(\int^{a b} C(a \otimes b, c) \times F a \times F b, F c)

The next trick is to pull the coend out of the hom-set. This trick relies on the co-continuity of the hom-functor in the first argument: a hom-functor from a colimit is isomorphic to a limit of hom-functors. In programmer-speak: a function from a sum type is equivalent to a product of functions (we call it case analysis). A coend is a generalized colimit, so when we pull it out of a hom-functor, it turns into a limit, or an end. Here’s the general formula, in which p x y is an arbitrary profunctor:

Set(\int^x p x x, y) \cong \int_x Set(p x x, y)

Let’s apply it to our formula:

\int_c \int_{a b} Set(C(a \otimes b, c) \times F a \times F b, F c)

We can combine the ends under one integral sign (it’s allowed by the Fubini theorem) and move to the next trick: hom-set adjunction:

Set(a \times b, c) \cong Set(a, b \to c)

In programming this is known as currying. This adjunction exists because Set is a cartesian closed category. We’ll use this adjunction to move F a \times F b to the right:

\int_{a b c} Set(C(a \otimes b, c), (F a \times F b) \to F c)

Using the Yoneda lemma we can “perform the integration” over c  to get:

\int_{a b} (F a \times F b) \to F (a \otimes b))

This is exactly the set of natural transformations used in the definition of a lax monoidal functor. We have established one-to-one correspondence between monoidal multiplication and lax monoidal mapping.

Of course, a complete proof would require translating monoid laws to their lax monoidal counterparts. You can find more details in Rivas and Jaskelioff, Notions of Computation as Monoids.

We’ll use the fact that a monoid in the category [C, Set] is a lax monoidal functor later.

Alternative Derivation

Incidentally, there are shorter derivations of these formulas that use the trick borrowed from the proof of the Yoneda lemma, namely, evaluating things at the identity morphism. (Whenever mathematicians speak of Yoneda-like arguments, this is what they mean.)

Starting from F \star F \to F and plugging in the Day convolution formula, we get:

\int^{a' b'} C(a' \otimes b', c) \times F a' \times F b' \to F c

There is a component of this natural transformation at (a \otimes b) that is the morphism:

\int^{a' b'} C(a' \otimes b', a \otimes b) \times F a' \times F b' \to F (a \otimes b)

This morphism must be defined for all possible values of the coend. In particular, it must be defined for the triple (id_{a \otimes b}, F a, F b), giving us the \mu we seek.

There is also an alternative derivation for the unit: Take the component of the natural transformation \eta at I:

\eta_I : C(I, I) \to L I

C(I, I) is guaranteed to contain at least one element, the identity morphism id_I. We can use \eta_I \, id_I as the (only) value of the lax monoidal constraint at the singleton 1.

Free Monoid

Given a monoidal category C, we might be able to define a whole lot of monoids in it. These monoids form a category Mon(C). Morphisms in this category correspond to those morphisms in C that preserve monoidal structure.

Consider, for instance, two monoids m and m'. A monoid morphism is a morphism f : m \to m' in C such that the unit of m' is related to the unit of m:

\eta' = f \circ \eta

munit

and similarly for multiplication:

\mu' \circ (f \otimes f) = f \circ \mu

Remember, we assumed that the tensor product is functorial in both arguments, so it can be used to lift a pair of morphisms.

mmult

There is an obvious forgetful functor U from Mon(C) to C which, for every monoid, picks its underlying object in C and maps every monoid morphism to its underlying morphism in C.

The left adjoint to this functor, if it exists, will map an object a in C to a free monoid L a.

The intuition is that a free monoid L a is a list of a.

In Haskell, a list is defined recursively:

data List a = Nil | Cons a (List a)

Such a recursive definition can be formalized as a fixed point of a functor. For a list of a, this functor is:

data ListF a x = NilF | ConsF a x

Notice the peculiar structure of this functor. It’s a sum type: The first part is a singleton, which is isomorphic to the unit type (). The second part is a product of a and x. Since the unit type is the unit of the product in our monoidal category of types, we can rewrite this functor symbolically as:

\Phi a x = I + a \otimes x

It turns out that this formula works in any monoidal category that has finite coproducts (sums) that are preserved by the tensor product. The fixed point of this functor is the free functor that generates free monoids.

I’ll define what is meant by the fixed point and prove that it defines a monoid. The proof that it’s the result of a free/forgetful adjunction is a bit involved, so I’ll leave it for a future blog post.

Algebras

Let’s consider algebras for the functor F. Such an algebra is defined as an object x called the carrier, and a morphism:

f : F x \to x

called the structure map or the evaluator.

In Haskell, an algebra is defined as:

type Algebra f x = f x -> x

There may be a lot of algebras for a given functor. In fact there is a whole category of them. We define an algebra morphism between two algebras (x, f : F x \to x) and (x', f' : F x' \to x') as a morphism \nu : x \to x' which commutes with the two structure maps:

\nu \circ f = f' \circ F \nu

algmorph

The initial object in the category of algebras is called the initial algebra, or the fixed point of the functor that generates these algebras. As the initial object, it has a unique algebra morphism to any other algebra. This unique morphism is called a catamorphism.

In Haskell, the fixed point of a functor f is defined recursively:

newtype Fix f = In { out :: f (Fix f) }

with, for instance:

type List a = Fix (ListF a)

A catamorphism is defined as:

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

A list catamorphism is called foldr.

We want to show that the initial algebra L a of the functor:

\Phi a x = I + a \otimes x

is a free monoid. Let’s see under what conditions it is a monoid.

Initial Algebra is a Monoid

In this section I will show you how to concatenate lists the hard way.

We know that function type b \to c (a.k.a., the exponential c^b) is the right adjoint to the product:

Set(a \times b, c) \cong Set(a, b \to c)

The function type is also called the internal hom.

In a monoidal category it’s sometimes possible to define an internal hom-object, denoted [b, c], as the right adjoint to the tensor product:

curry : C(a \otimes b, c) \cong C(a, [b, c])

If this adjoint exists, the category is called closed monoidal.

In a closed monoidal category, the initial algebra L a of the functor \Phi a x = I + a \otimes x is a monoid. (In particular, a Haskell list of a, which is a fixed point of ListF a, is a monoid.)

To show that, we have to construct two morphisms corresponding to unit and multiplication (in Haskell, empty list and concatenation):

\eta : I \to L a

\mu : L a \otimes L a \to L a

What we know is that L a is a carrier of the initial algebra for \Phi a, so it is equipped with the structure map:

I + a \otimes L a \to L a

which is equivalent to a pair of morphisms:

\alpha : I \to L a

\beta : a \otimes L a \to L a

Notice that, in Haskell, these correspond the two list constructors: Nil and Cons or, in terms of the fixed point:

nil :: () -> List a
nil () = In NilF

cons :: a -> List a -> List a
cons a as = In (ConsF a as)

We can immediately use \alpha to implement \eta.

The second one, \beta, one can be rewritten using the hom adjuncion as:

\bar{\beta} = curry \, \beta

\bar{\beta} : a \to [L a, L a]

Notice that, if we could prove that [L a, L a] is a carrier for the same algebra generated by \Phi a, we would know that there is a unique catamorphism from the initial algebra L a:

\kappa_{[L a, L a]} : L a \to [L a, L a]

which, by the hom adjunction, would give us the desired multiplication:

\mu : L a \otimes L a \to L a

Let’s establish some useful lemmas first.

Lemma 1: For any object x in a closed monoidal category, [x, x] is a monoid.

This is a generalization of the idea that endomorphisms form a monoid, in which identity morphism is the unit and composition is multiplication. Here, the internal hom-object [x, x] generalizes the set of endomorphisms.

Proof: The unit:

\eta : I \to [x, x]

follows, through adjunction, from the unit law in the monoidal category:

\lambda : I \otimes x \to x

(In Haskell, this is a fancy way of writing mempty = id.)

Multiplication takes the form:

\mu : [x, x] \otimes [x, x] \to [x, x]

which is reminiscent of composition of edomorphisms. In Haskell we would say:

mappend = (.)

By adjunction, we get:

curry^{-1} \, \mu : [x, x] \otimes [x, x] \otimes x \to x

We have at our disposal the counit eval of the adjunction:

eval : [x, x] \otimes x \cong x

We can apply it twice to get:

\mu = curry (eval \circ (id \otimes eval))

In Haskell, we could express this as:

mu :: ((x -> x), (x -> x)) -> (x -> x)
mu (f, g) = \x -> f (g x)

Here, the counit of the adjunction turns into simple function application.

\square

Lemma 2: For every morphism f : a \to m, where m is a monoid, we can construct an algebra of the functor \Phi a with m as its carrier.

Proof: Since m is a monoid, we have two morphisms:

\eta : I \to m

\mu : m \otimes m \to m

To show that m is a carrier of our algebra, we need two morphisms:

\alpha : I \to m

\beta : a \otimes m \to m

The first one is the same as \eta, the second can be implemented as:

\beta = \mu \circ (f \otimes id)

In Haskell, we would do case analysis:

mapAlg :: Monoid m => ListF a m -> m
mapAlg NilF = mempty
mapAlg (ConsF a m) = f a `mappend` m

\square

We can now build a larger proof. By lemma 1, [L a, L a] is a monoid with:

\mu = curry (eval \circ (id \otimes eval))

We also have a morphism \bar{\beta} : a \to [L a, L a] so, by lemma 2, [L a, L a] is also a carrier for the algebra:

\alpha = \eta

\beta = \mu \circ (\bar{\beta} \otimes id)

It follows that there is a unique catamorphism \kappa_{[L a, L a]} from the initial algebra L a to it, and we know how to use it to implement monoidal multiplication for L a. Therefore, L a is a monoid.

Translating this to Haskell, \bar{\beta} is the curried form of Cons and what we have shown is that concatenation (multiplication of lists) can be implemented as a catamorphism:

concat :: List a -> List a -> List a
conc x y = cata alg x y
  where alg NilF        = id
        alg (ConsF a t) = (cons a) . t

The type:

List a -> (List a -> List a)

(parentheses added for emphasis) corresponds to L a \to [L a, L a].

It’s interesting that concatenation can be described in terms of the monoid of list endomorphisms. Think of turning an element a of the list into a transformation, which prepends this element to its argument (that’s what \bar{\beta} does). These transformations form a monoid. We have an algebra that turns the unit I into an identity transformation on lists, and a pair a \otimes t (where t is a list transformation) into the composite \bar{\beta} a \circ t. The catamorphism for this algebra takes a list L a and turns it into one composite list transformation. We then apply this transformation to another list and get the final result: the concatenation of two lists. \square

Incidentally, lemma 2 also works in reverse: If a monoid m is a carrier of the algebra of \Phi a, then there is a morphism f : a \to m. This morphism can be thought of as inserting generators represented by a into the monoid m.

Proof: if m is both a monoid and a carrier for the algebra \Phi a, we can construct the morphism a \to m by first applying the identity law to go from a to a \otimes I, then apply id_a \otimes \eta to get a \otimes m. This can be right-injected into the coproduct I + a \otimes m and then evaluated down to m using the structure map for the algebra on m.

a \to a \otimes I \to a \otimes m \to I + a \otimes m \to m

insertion

In Haskell, this corresponds to a construction and evaluation of:

ConsF a mempty

\square

Free Monoidal Functor

Let’s go back to our functor category. We started with a monoidal category C and considered a functor category [C, Set]. We have shown that [C, Set] is itself a monoidal category with Day convolution as tensor product and the hom functor C(I, -) as unit. A monoid is this category is a lax monoidal functor.

The next step is to build a free monoid in [C, Set], which would give us a free lax monoidal functor. We have just seen such a construction in an arbitrary closed monoidal category. We just have to translate it to [C, Set]. We do this by replacing objects with functors and morphisms with natural transformations.

Our construction relied on defining an initial algebra for the functor:

I + a \otimes b

Straightforward translation of this formula to the functor category [C, Set] produces a higher order endofunctor:

A_F G = C(I, -) + F \star G

It defines, for any functor F, a mapping from a functor G to a functor A_F G. (It also maps natural transformations.)

We can now use A_F to define (higher-order) algebras. An algebra consists of a carrier — here, a functor T — and a structure map — here, a natural transformation:

A_F T \to T

The initial algebra for this higher-order endofunctor defines a monoid, and therefore a lax monoidal functor. We have shown it for an arbitrary closed monoidal category. So the only question is whether our functor category with Day convolution is closed.

We want to define the internal hom-object in [C, Set] that satisfies the adjunction:

[C, Set](F \star G, H) \cong [C, Set](F, [G, H])

We start with the set of natural transformations — the hom-set in [C, Set]:

[C, Set](F \star G, H)

We rewrite it as an end over c, and use the formula for Day convolution:

\int_c Set(\int^{a b} C(a \otimes b, c) \times F a \times G b, H c)

We use the co-continuity trick to pull the coend out of the hom-set and turn it into an end:

\int_{c a b} Set(C(a \otimes b, c) \times F a \times G b, H c)

Keeping in mind that our goal is to end up with F a on the left, we use the regular hom-set adjunction to shuffle the other two terms to the right:

\int_{c a b} Set(F a, C(a \otimes b, c) \times G b \to H c)

The hom-functor is continuous in the second argument, so we can sneak the end over b c under it:

\int_{a} Set(F a, \int_{b c} C(a \otimes b, c) \times G b \to H c)

We end up with a set of natural transformations from the functor F to the functor we will call:

[G, H] = \int_{b c} (C(- \otimes b, c) \times G b \to H c)

We therefore identify this functor as the right adjoint (internal hom-object) for Day convolution. We can further simplify it by using the hom-set adjunction:

\int_{b c} (C(- \otimes b, c) \to (G b \to H c))

and applying the Yoneda lemma to get:

[G, H] = \int_{b} (G b \to H (- \otimes b))

In Haskell, we would write it as:

newtype DayHom f g a = DayHom (forall b . f b -> g (a, b))

Since Day convolution has a right adjoint, we conclude that the fixed point of our higher order functor defines a free lax monoidal functor. We can write it in a recursive form as:

Free_F = C(I, -) + F \star Free_F

or, in Haskell:

data FreeMonR f t =
      Done t
    | More (Day f (FreeMonR f) t)

Free Monad

This blog post wouldn’t be complete without mentioning that the same construction works for monads. Famously, a monad is a monoid in the category of endofunctors. Endofunctors form a monoidal category with functor composition as tensor product and the identity functor as unit. The fact that we can construct a free monad using the formula:

FreeM_F = Id + F \circ FreeM_F

is due to the observation that functor composition has a right adjoint, which is the right Kan extension. Unfortunately, due to size issues, this Kan extension doesn’t always exist. I’ll quote Alex Campbell here: “By making suitable size restrictions, we can give conditions for free monads to exist: for example, free monads exist for accessible endofunctors on locally presentable categories; a special case is that free monads exist for finitary endofunctors on Set, where finitary means the endofunctor preserves filtered colimits (more generally, an endofunctor is accessible if it preserves \kappa-filtered colimits for some regular cardinal number \kappa).”

Conclusion

As we acquire experience in programming, we learn more tricks of trade. A seasoned programmer knows how to read a file, parse its contents, or sort an array. In category theory we use a different bag of tricks. We bunch morphisms into hom-sets, move ends and coends, use Yoneda to “integrate,” use adjunctions to shuffle things around, and use initial algebras to define recursive types.

Results derived in category theory can be translated to definitions of functions or data structures in programming languages. A lax monoidal functor becomes an Applicative. Free monoidal functor becomes:

data FreeMonR f t =
      Done t
    | More (Day f (FreeMonR f) t)

What’s more, since the derivation made very few assumptions about the category C (other than that it’s monoidal), this result can be immediately applied to profunctors (replacing C with C^{op}\times C) to produce:

data FreeMon p s t where
     DoneFM :: t -> FreeMon p s t
     MoreFM :: p a b -> FreeMon p c d -> 
                        (b -> d -> t) -> 
                        (s -> (a, c)) -> FreeMon p s t

Replacing Day convolution with endofunctor composition gives us a free monad:

data FreeMonadF f g a = 
    DoneFM a 
  | MoreFM (Compose f g a)

Category theory is also the source of laws (commuting diagrams) that can be used in equational reasoning to verify the correctness of programming constructs.

Writing this post has been a great learning experience. Every time I got stuck, I would ask Alex for help, and he would immediately come up with yet another algebra and yet another catamorphism. This was so different from the approach I would normally take, which would be to get bogged down in inductive proofs over recursive data structures.