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:

A G = Id + F \star G

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:

A_a b = () + (a, b)

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 \mathscr{C} to \mathscr{S}et 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 \vec{e}_i, and represent any vector as a linear combination:

\vec{v} = \sum \limits_{i = 1}^n v_i \vec{e}_i

It turns out that, under some conditions, there is a basis in the category of functors from \mathscr{C} to \mathscr{S}et. The basis is formed by representable functors of the form \mathscr{C}(x, -), and the decomposition of a functor F is given by the co-Yoneda lemma:

F a = \int^x F x \times \mathscr{C}(x, a)

The coend in this formula roughly corresponds to (possibly infinite) categorical sum (coproduct). The product under the integral sign is the cartesian product in \mathscr{S}et.

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.

(F \star G) a \cong \int^x F x \times \mathscr{C}(x, a) \star \int^y G y \times \mathscr{C}(y, a)

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

\int^{x y} F x \times G y \times (\mathscr{C}(x, a) \star \mathscr{C}(y, a))

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

\mathscr{C}(x, -) \star \mathscr{C}(y, -) \cong \mathscr{C}(x \otimes y, -)

This gives us the formula for Day convolution:

(F \star G) a = \int^{x y} F x \times G y \times \mathscr{C}(x \otimes y, a)

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 xs and a bag of ys, plus a binary combinator for turning every possible pair (x, y) into an a.

Day convolution lifts the monoidal structure of \mathscr{C} (the tensor product \otimes) to the functor category [\mathscr{C}, \mathscr{S}et]. In particular, it lifts the unit object 1 to the hom-functor \mathscr{C}(1, -). We have, for instance:

(F \star \mathscr{C}(1, -)) a = \int^{x y} F x \times \mathscr{C}(1, y) \times \mathscr{C}(x \otimes y, a)

which, by co-Yoneda, is isomorphic to:

\int^{x} F x \times \mathscr{C}(x \otimes 1, a)

Considering that x \otimes 1 is isomorphic to x, we can apply co-Yoneda again, to indeed get F a.

In Haskell, the unit object with respect to product is the unit type (), and the hom-functor \mathscr{C}(1, -) is isomorphic to the identity functor Id (a set of functions from unit to x is isomorphic to x).

We now have all the tools to understand the formula:

A G = Id + F \star G

or, more generally:

A_F G = \mathscr{C}(1, -) + F \star G

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

Lax Monoidal Functors

Whenever we have a functor between two monoidal categories \mathscr{C} and \mathscr{D}, 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.

\epsilon : 1_\mathscr{D} \to F 1_\mathscr{C}

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

\mu_{a b} : F a \otimes_\mathscr{D} F b \to F (a \otimes_\mathscr{C} b)

which is natural in both arguments. These morphisms must satisfy additional conditions related to associativity and unitality of respective tensor products. If \epsilon and \mu are isomorphisms then we call F 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:

\mathscr{C}(x, -) \star \mathscr{C}(y, -) \cong \mathscr{C}(x \otimes y, -)

Since hom-functors define the Yoneda embedding \mathscr{C} \to [\mathscr{C}, \mathscr{S}et], 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:

F_a b = 1 + a \otimes b

defined in a monoidal category (\otimes and 1) 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 f(x) is some value x_0 such that:

f(x_0) = x_0

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 F as an object that is isomorphic to its image under F:

F x \cong x

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 (x, f) whose carrier is x and whose action is:

f : F x \to x

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:

Fix f \cong f (Fix f)

which can be expressed as:

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

Notice that the pair (Fix f, In) is the (initial) algebra for the functor f, with the carrier Fix f and the action In; 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 x:

x_{n+1} = f (x_n)

then f(x) = x (at least for continuous functions).

We can apply the same idea to our list functor, iteratively replacing b with the definition of F_a b = 1 + a \otimes b:

1 + a \otimes b\\ 1 + a \otimes (1 + a \otimes b)\\ 1 + a + a \otimes a \otimes (1 + a \otimes b)\\ 1 + a + a \otimes a + a \otimes a \otimes a + ...

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 C and D 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:

A_F G = Id + F \star G

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 g 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 xs; and the tail, which is a container of ys. We are appending to it another container of ts. We do it by concatenating the two containers (gy >*< gt) into one container of pairs (y \otimes t). The new combinator reassociates the nested pairs (x \otimes (y \otimes t)) and applies the old combinator to (x \otimes y).

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 (\mathscr{C}, \otimes, 1, \alpha, \rho, \lambda), where \alpha is the associator, and \rho and \lambda are right and left unitors, respectively. We will be constructing a lax monoidal functors from \mathscr{C} to \mathscr{S}et, 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:

\beta_{s t} = \int^{x y} f x \times g y \times \mathscr{C}(x \otimes y, s) \times g t \to \int^{u v} f u \times g v \times \mathscr{C}(u \otimes v, s \otimes t)

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

\int^{x y} f x \times g (y \otimes t) \times \mathscr{C}(x \otimes y, s)

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

\int_{s t} Set(\int^{x y} f x \times g (y \otimes t) \times \mathscr{C}(x \otimes y, s), \int^{u v} f u \times g v \times \mathscr{C}(u \otimes v, s \otimes t))

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

\int_{s t x y} Set(f x \times g (y \otimes t) \times \mathscr{C}(x \otimes y, s), \int^{u v} f u \times g v \times \mathscr{C}(u \otimes v, s \otimes t))

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

i_{x, y \otimes t} : f x \times g (y \otimes t) \times \mathscr{C}(x \otimes (y \otimes t), -) \to \int^{u v} f u \times g v \times \mathscr{C}(u \otimes v, -)

Given a morphism h that is a member of \mathscr{C}(x \otimes y, s), we can construct the morphism (h \otimes id) \circ \alpha^{-1}, which is a member of \mathscr{C}(x \otimes (y \otimes t), s \otimes t).

The free monoidal functor Free_f is given as the initial algebra of the (higher-order) endofunctor acting on a functor g from [\mathscr{C}, \mathscr{S}et]:

A_f g = \mathscr{C}(1, -) + f \star g

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

\mathscr{C}(1, -) + (f \star Free_f) \cong Free_f

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

\epsilon : 1 \to Free_f \, 1

and a family of natural transformations:

\mu_{s t} : Free_f\, s \times Free_f\, t \to Free_f\, (s \otimes t)

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

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

\int_{s t} \mathscr{S}et(Free_f\, s \times Free_f\, t, Free_f\, (s \otimes t))

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

\int_{s t} \mathscr{S}et((\mathscr{C}(1,s) + (f \star Free_f) s) \times Free_f\, t, Free_f\, (s \otimes t))

distribute the product over the sum:

\int_{s t} \mathscr{S}et(\mathscr{C}(1,s)\times Free_f\, t + (f \star Free_f) s \times Free_f\, t, Free_f\, (s \otimes t))

and replace functions from coproducts with products of functions:

\int_{s t} \mathscr{S}et(\mathscr{C}(1,s)\times Free_f\, t, Free_f\, (s \otimes t)) \times

\int_{s t} \mathscr{S}et((f \star Free_f) s \times Free_f\, t, Free_f\, (s \otimes t))

The first hom-set forms the base of induction and the second is the inductive step. If we call a member of \mathscr{C}(1,s) h then we can implement the first function as the lifting of (h 1 \otimes -) acting on Free_f\, t, and for the second, we can use \beta_{s t}.

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:

A_f g = Id + f \circ g

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