Abstract: I derive free monoidal profunctors as fixed points of a higher order functor acting on profunctors. Monoidal profunctors play an important role in defining traversals.

The beauty of category theory is that it lets us reuse concepts at all levels. In my previous post I have derived a free monoidal functor that goes from a monoidal category to . The current post may then be shortened to: Since profunctors are just functors from to , with the obvious monoidal structure induced by the tensor product in , we automatically get free monoidal profunctors.

Let me fill in the details.

## Profunctors in Haskell

Here’s the definition of a profunctor from Data.Profunctor:

class Profunctor p where dimap :: (s -> a) -> (b -> t) -> p a b -> p s t

The idea is that, just like a functor acts on objects, a profunctor `p`

acts on pairs of objects . In other words, it’s a type constructor that takes two types as arguments. And just like a functor acts on morphisms, a profunctor acts on pairs of morphisms. The only tricky part is that the first morphism of the pair is reversed: instead of going from to , as one would expect, it goes from to . This is why we say that the first argument comes from the opposite category , where all morphisms are reversed with respect to . Thus a morphism from to in is a pair of morphisms .

Just like functors form a category, profunctors form a category too. In this category profunctors are objects, and natural transformations are morphisms. A natural transformation between two profunctors and is a family of functions which, in Haskell, can be approximated by a polymorphic function:

type p ::~> q = forall a b. p a b -> q a b

If the category is monoidal (has a tensor product and a unit object ), then the category has a trivially induced tensor product:

and unit

In Haskell, we’ll use cartesian product (pair type) as the underlying tensor product, and `()`

type as the unit.

Notice that the induced product does not have the usual exponential as the right adjoint. Indeed, the hom-set:

is a set of pairs of morphisms:

If the right adjoint existed, it would be a pair of objects , such that the following hom-set would be isomorphic to the previous one:

While could be the internal hom, there is no candidate for that would produce the isomorphism:

(Consider, for instance, unit for .) This lack of the right adjoint is the reason why we can’t define an analog of `Applicative`

for profunctors. We can, however, define a monoidal profunctor:

class Monoidal p where punit :: p () () (>**<) :: p a b -> p c d -> p (a, c) (b, d)

This profunctor is a map between two monoidal structures. For instance, `punit`

can be seen as mapping the unit in to the unit in :

punit :: () -> p <1, 1>

Operator `>**<`

maps the product in to the induced product in :

(>**<) :: (p <a, b>, p <c, d>) -> p (<a, b> × <c, d>)

Day convolution, which works with monoidal structures, generalizes naturally to the profunctor category:

data PDay p q s t = forall a b c d. PDay (p a b) (q c d) ((b, d) -> t) (s -> (a, c))

## Higher Order Functors

Since profunctors form a category, we can define endofunctors in that category. This is a no-brainer in category theory, but it requires some new definitions in Haskell. Here’s a higher-order functor that maps a profunctor to another profunctor:

class HPFunctor pp where hpmap :: (p ::~> q) -> (pp p ::~> pp q) ddimap :: (s -> a) -> (b -> t) -> pp p a b -> pp p s t

The function `hpmap`

lifts a natural transformation, and `ddimap`

shows that the result of the mapping is also a profunctor.

An endofunctor in the profunctor category may have a fixed point:

newtype FixH pp a b = InH { outH :: pp (FixH pp) a b }

which is also a profunctor:

instance HPFunctor pp => Profunctor (FixH pp) where dimap f g (InH pp) = InH (ddimap f g pp)

Finally, our Day convolution is a higher-order endofunctor in the category of profunctors:

instance HPFunctor (PDay p) where hpmap nat (PDay p q from to) = PDay p (nat q) from to ddimap f g (PDay p q from to) = PDay p q (g . from) (to . f)

We’ll use this fact to construct a free monoidal profunctor next.

## Free Monoidal Profunctor

In the previous post, I defined the free monoidal functor as a fixed point of the following endofunctor:

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

Replacing the functors `f`

and `g`

with profunctors is straightforward:

data FreeP p q s t = DoneP (s -> ()) (() -> t) | MoreP (PDay p q s t)

The only tricky part is realizing that the first term in the sum comes from the unit of Day convolution, which is the type `() -> t`

, and it generalizes to an appropriate pair of functions (we’ll simplify this definition later).

`FreeP`

is a higher order endofunctor acting on profunctors:

instance HPFunctor (FreeP p) where hpmap _ (DoneP su ut) = DoneP su ut hpmap nat (MoreP day) = MoreP (hpmap nat day) ddimap f g (DoneP au ub) = DoneP (au . f) (g . ub) ddimap f g (MoreP day) = MoreP (ddimap f g day)

We can, therefore, define its fixed point:

type FreeMon p = FixH (FreeP p)

and show that it is indeed a monoidal profunctor. As before, the trick is to fist show the following property of Day convolution:

cons :: Monoidal q => PDay p q a b -> q c d -> PDay p q (a, c) (b, d) cons (PDay pxy quv yva bxu) qcd = PDay pxy (quv >**< qcd) (bimap yva id . reassoc) (assoc . bimap bxu id)

where

assoc ((a,b),c) = (a,(b,c)) reassoc (a, (b, c)) = ((a, b), c)

Using this function, we can show that `FreeMon p`

is monoidal for any `p`

:

instance Profunctor p => Monoidal (FreeMon p) where punit = InH (DoneP id id) (InH (DoneP au ub)) >**< frcd = dimap snd (\d -> (ub (), d)) frcd (InH (MoreP dayab)) >**< frcd = InH (MoreP (cons dayab frcd))

`FreeMon`

can also be rewritten as a recursive data type:

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

## Categorical Picture

As I mentioned before, from the categorical point of view there isn’t much to talk about. We define a functor in the category of profunctors:

As previously shown in the general case, its initial algebra defines a free monoidal profunctor.

## Acknowledgments

I’m grateful to Eugenia Cheng not only for talking to me about monoidal profunctors, but also for getting me interested in category theory in the first place through her Catsters video series. Thanks also go to Edward Kmett for numerous discussions on this topic.

February 20, 2018 at 4:07 pm

Thank you for this, great post as always! Where could one find an introduction to the notation used at the end, specifically what things like (1,—) mean? The integral I reason is acting as a categorical forall, but it’s only intuition. Thank you!

February 21, 2018 at 2:12 am

The integral is a coend, so it’s an existential type. The name of the category followed by a pair of objects denotes a hom-set. Here, it’s a hom-set from the unit object (which is a pair ) to a placeholder — meaning both sides are functors in this variable. Some of it was explained in the previous post, and the rest throughout my online book.