Abstract: I derive a free monoidal (applicative) functor as an initial algebra of a higher-order functor using Day convolution.

I thought I was done with monoids for a while, after writing my Monoids on Steroids post, but I keep bumping into them. This time I read a paper by Capriotti and Kaposi about Free Applicative Functors and it got me thinking about the relationship between applicative and monoidal functors. In a monoidal closed category, the two are equivalent, but monoidal structure seems to be more fundamental. It’s possible to have a monoidal category, which is not closed. Not to mention that monoidal structures look cleaner and more symmetrical than closed structures.

One particular statement in the paper caught my attention: the authors said that the free applicative functors are initial algebras for a very simple higher-order functor:

which, in their own words, “makes precise the intuition that free applicative functors are in some sense lists (i.e. free monoids).” In this post I will decode this statement and then expand it by showing how to implement a free monoidal functor as a higher order fixed point using some properties of Day convolution.

Let me start with some refresher on lists. To define a list all we need is a monoidal category. If we pretend that Hask is a category, then our product is a pair type `(a, b)`

, which is associative up to isomorphism; with `()`

as its unit, also up to isomorphism. We can then define a functor that generates lists:

Notice the similarity with the Capriotti-Kaposi formula. You might recognize this functor in its Haskell form:

data ListF a b = Nil | Cons a b

The fixed point of this functor is the familiar list, a.k.a., the free monoid. So that’s the general idea.

## Day Convolution

There are lots of interesting monoidal structures. Famously (because of the monad quip) the category of endofunctors is monoidal; with functor composition as product and identity functor as identity. What is less known is that functors from a monoidal category to also form a monoidal category. A product of two such functors is defined through Day convolution. I have talked about Day convolution in the context of applicative functors, but here I’d like to give you some more intuition.

What did it for me was Alexander Campbell comment on Stack Exchange. You know how, in a vector space, you can have a set of basis vectors, say , and represent any vector as a linear combination:

It turns out that, under some conditions, there is a basis in the category of functors from to . The basis is formed by representable functors of the form , and the decomposition of a functor is given by the co-Yoneda lemma:

The coend in this formula roughly corresponds to (possibly infinite) categorical sum (coproduct). The product under the integral sign is the cartesian product in .

In pseudo-Haskell, we would write this formula as:

f a ~ exists x . (f x, x -> a)

because a coend corresponds to an existential type. The intuition is that, because the type `x`

is hidden, the only thing the user can do with this data type is to `fmap`

the function over the value `f x`

, and that is equivalent to the value `f a`

.

The actual Haskell encoding is given by the following GADT:

data Coyoneda f a where Coyoneda :: f x -> (x -> a) -> Coyoneda f a

Now suppose that we want to define “multiplication” of two functors that are represented using the coend formula.

Let’s assume that our multiplication interacts nicely with coends. We get:

All that remains is to define the multiplication of our “basis vectors,” the hom-functors. Since we have a tensor product in , the obvious choice is:

This gives us the formula for Day convolution:

We can translate it directly to Haskell:

data Day f g a = forall x y. Day (f x) (g y) ((x, y) -> a)

The actual Haskell library implementation uses GADTs, and also curries the product, but here I’m opting for encoding an existential type using `forall`

in front of the constructor.

For those who like the analogy between functors and containers, Day convolution may be understood as containing a box of s and a bag of s, plus a binary combinator for turning every possible pair into an .

Day convolution lifts the monoidal structure of (the tensor product ) to the functor category . In particular, it lifts the unit object to the hom-functor . We have, for instance:

which, by co-Yoneda, is isomorphic to:

Considering that is isomorphic to , we can apply co-Yoneda again, to indeed get .

In Haskell, the unit object with respect to product is the unit type `()`

, and the hom-functor is isomorphic to the identity functor (a set of functions from unit to is isomorphic to ).

We now have all the tools to understand the formula:

or, more generally:

It’s a sum (coproduct) of the unit under Day convolution and the Day convolution of two functors and .

## Lax Monoidal Functors

Whenever we have a functor between two monoidal categories and , it makes sense to ask how this functor interacts with the monoidal structure. For instance, does it map the unit object in one category to the unit object in another? Does it map the result of a tensor product to a tensor product of mapped arguments?

A lax monoidal functor doesn’t do that, but it does the next best thing. It doesn’t map unit to unit, but it provides a morphism that connects the unit in the target category to the image of the unit of the source category.

It also provides a family of morphisms from the product of images to the image of a product:

which is natural in both arguments. These morphisms must satisfy additional conditions related to associativity and unitality of respective tensor products. If and are isomorphisms then we call a *strong* monoidal functor.

If you look at the way Day convolution was defined, you can see now that we insisted that the hom-functor be strong monoidal:

Since hom-functors define the Yoneda embedding , we can say that Day convolution makes Yoneda embedding strong monoidal.

The translation of the definition of a lax monoidal functor to Haskell is straightforward:

class Monoidal f where unit :: f () (>*<) :: f x -> f y -> f (x, y)

Because Hask is a *closed* monoidal category, `Monoidal`

is equivalent to `Applicative`

(see my post on Applicative Functors).

## Fixed Points

Recursive data structures can be formally defined as fixed points of F-algebras. Lists, in particular, are fixed points of functors of the form:

defined in a monoidal category ( and ) with coproducts (the plus sign).

In general, a fixed point is defined as a point that is fixed under some particular mapping. For instance, a fixed point of a function is some value such that:

Obviously, the function’s codomain has to be the same as its domain, for this equation to make sense.

By analogy, we can define a fixed point of an endofunctor as an object that is isomorphic to its image under :

The isomorphism here is just a pair of morphisms, one the inverse of the other. One of these morphisms can be seen as part of the F-algebra whose carrier is and whose action is:

Lambek’s lemma states that the action of the initial (or terminal) F-algebra is an isomorphism. This explains why a fixed point of a functor is often referred to as an initial (terminal) algebra.

In Haskell, a fixed point of a functor `f`

is called `Fix f`

. It is defined by the property that `f`

acting on `Fix f`

must be isomorphic to `Fix f`

:

which can be expressed as:

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

Notice that the pair is the (initial) algebra for the functor , with the carrier and the action ; and that `out`

is the inverse of `In`

, as prescribed by the Lambek’s lemma.

Here’s another useful intuition about fixed points: they can often be calculated iteratively as a limit of a sequence. For functions, if the following sequence converges to :

then (at least for continuous functions).

We can apply the same idea to our list functor, iteratively replacing with the definition of :

where we assumed associativity and unit laws (up to isomorphism). This formal expansion is in agreement with our intuition that a list is either empty, contains one element, a product of two elements, a product of three elements, and so on…

## Higher Order Functors

Category theory has achieved something we can only dream of in programming languages: reusability of concepts. For instance, functors between two categories and form a category, with natural transformations as morphisms. Therefore everything we said about fixed points and algebras can be immediately applied to the functor category. In Haskell, however, we have to start almost from scratch. For instance, a higher order functor, which takes a functor as argument and returns another functor has to be defined as:

class HFunctor ff where ffmap :: Functor g => (a -> b) -> ff g a -> ff g b hfmap :: (g :~> h) -> (ff g :~> ff h)

The squiggly arrows are natural transformations:

infixr 0 :~> type f :~> g = forall a. f a -> g a

Notice that the definition of `HFunctor`

not only requires a higher-order version of `fmap`

called `hfmap`

, which lifts natural transformations, but also the lower-order `ffmap`

that attests to the fact that the result of `HFunctor`

is again a functor. (Quantified class constraints will soon make this redundant.)

The definition of a fixed point also has to be painstakingly rewritten:

newtype FixH ff a = InH { outH :: ff (FixH ff) a }

Functoriality of a higher order fixed point is easily established:

instance HFunctor f => Functor (FixH f) where fmap h (InH x) = InH (ffmap h x)

Finally, Day convolution is a higher order functor:

instance HFunctor (Day f) where hfmap nat (Day fx gy xyt) = Day fx (nat gy) xyt ffmap h (Day fx gy xyt) = Day fx gy (h . xyt)

## Free Monoidal Functor

With all the preliminaries out of the way, we are now ready to derive the main result.

We start with the higher-order functor whose initial algebra defines the free monoidal functor:

We can translate it to Haskell as:

data FreeF f g t = DoneF t | MoreF (Day f g t)

It is a higher order functor, in that it takes a functor `g`

and produces a new functor `FreeF f g`

:

instance HFunctor (FreeF f) where hfmap _ (DoneF x) = DoneF x hfmap nat (MoreF day) = MoreF (hfmap nat day) ffmap f (DoneF x) = DoneF (f x) ffmap f (MoreF day) = MoreF (ffmap f day)

The claim is that, for any functor `f`

, the (higher order) fixed point of `FreeF f`

:

type FreeMon f = FixH (FreeF f)

is monoidal.

The usual approach to solving such a problem is to express `FreeMon`

as a recursive data structure:

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

and proceed from there. This is fine, but it doesn’t give us any insight about what property of the original higher-order functor makes its fixed point monoidal. So instead, I will concentrate on properties of Day convolution.

To begin with, let’s establish the functoriality of `FreeMon`

using the fact that Day convolution is a functor:

instance Functor f => Functor (FreeMon f) where fmap h (InH (DoneF s)) = InH (DoneF (h s)) fmap h (InH (MoreF day)) = InH (MoreF (ffmap h day))

The next step is based on the list analogy. The free monoidal functor is analogous to a list in which the product is replaced by Day convolution. The proof that it’s monoidal amounts to showing that one can “concatenate” two such lists. Concatenation is a recursive process in which we detach an element from one list and attach it to the other.

When building recursion, the functor in Day convolution will play the role of the tail of the list. We’ll prove monoidality of the fixed point inductively by assuming that the tail is already monoidal. Here’s the crucial step expressed in terms of Day convolution:

cons :: Monoidal g => Day f g s -> g t -> Day f g (s, t) cons (Day fx gy xys) gt = Day fx (gy >*< gt) (bimap xys id) . reassoc)

We took advantage of associativity:

reassoc :: (a, (b, c)) -> ((a, b), c) reassoc (a, (b, c)) = ((a, b), c)

and functoriality (`bimap`

) of the underlying product.

The intuition here is that we have a Day product of the head of the list, which is a box of s; and the tail, which is a container of s. We are appending to it another container of s. We do it by concatenating the two containers into one container of pairs . The new combinator reassociates the nested pairs and applies the old combinator to .

The final step is to show that `FreeMon`

defined through Day convolution is indeed monoidal. Here’s the proof:

instance Functor f => Monoidal (FreeMon f) where unit = InH (DoneF ()) (InH (DoneF s)) >*< frt = fmap (s, ) frt (InH (MoreF day)) >*< frt = InH (MoreF (day `cons` frt))

A lax monoidal functor must also preserve associativity and unit laws. Unlike the corresponding laws for applicative functors, these are pretty straightforward to formulate.

The unit laws are:

fmap lunit (unit () >*< frx) = frx fmap runit (frx >*< unit ()) = frx

where I used the left and right unitors:

lunit :: ((), a) -> a lunit ((), a) = a runit :: (a, ()) -> a runit (a, ()) = a

The associativity law is:

fmap assoc ((frx >*< fry) >*< frz) = (frx >*< (fry >*< frz))

where I used the associator:

assoc :: ((a,b),c) -> (a,(b,c)) assoc ((a,b),c) = (a,(b,c))

Except for the left unit law, I wasn’t able to find simple derivations of these laws.

## Categorical Picture

Translating this construction to category theory, we start with a monoidal category , where is the associator, and and are right and left unitors, respectively. We will be constructing a lax monoidal functors from to , the latter equipped with the usual cartesian product and coproduct.

I will sketch some of the constructions without going into too much detail.

The analogue of `cons`

is a family of natural transformations:

We will assume that is lax monoidal, so the left hand side can be mapped to:

The set of natural transformations can be represented as an end:

A hom-set from a coend is isomorphic to an end of a hom-set:

There is an injection that is a member of this hom-set:

Given a morphism that is a member of , we can construct the morphism , which is a member of .

The free monoidal functor is given as the initial algebra of the (higher-order) endofunctor acting on a functor from :

By Lambek’s lemma, the action of this functor on the fixed point is naturally isomorphic to the fixed point itself:

We want to show that is lax monoidal, that is that there’s a mapping:

and a family of natural transformations:

The first one can be simply chosen as the identity of the singleton set.

Let’s rewrite the type of natural transformations in the second one as an end:

We can expand the first factor using the Lambek’s lemma:

distribute the product over the sum:

and replace functions from coproducts with products of functions:

The first hom-set forms the base of induction and the second is the inductive step. If we call a member of then we can implement the first function as the lifting of acting on , and for the second, we can use .

## Conclusion

The purpose of this post was to explore the formulation of a free lax monoidal functor without recourse to closed structure. I have to admit to a hidden agenda: The profunctor formulation of traversables involves monoidal profunctors, so that’s what I’m hoping to explore in the next post.

## Appendix: Free Monad

While reviewing the draft of this post, Oleg Grenrus suggested that I derive free monad as a fixed point of a higher order functor. The monoidal product in this case is endofunctor composition:

newtype Compose f g a = Compose (f (g a))

The higher-order functor in question can be written as:

or, in Haskell:

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

instance Functor f => HFunctor (FreeMonadF f) where hfmap _ (DoneFM a) = DoneFM a hfmap nat (MoreFM (Compose fg)) = MoreFM $ Compose $ fmap nat fg ffmap h (DoneFM a) = DoneFM (h a) ffmap h (MoreFM (Compose fg)) = MoreFM $ Compose $ fmap (fmap h) fg

The free monad is given by the fixed point:

type FreeMonad f = FixH (FreeMonadF f)

as witnessed by the following instance definition:

instance Functor f => Monad (FreeMonad f) where return = InH . DoneFM (InH (DoneFM a)) >>= k = k a fma >>= k = join (fmap k fma)

join :: Functor f => FreeMonad f (FreeMonad f a) -> FreeMonad f a join (InH (DoneFM x)) = x join (InH (MoreFM (Compose ffr))) = InH $ MoreFM $ Compose $ fmap join ffr