February | 2018 | Bartosz Milewski's Programming Cafe

February 2018

Monthly Archive

February 20, 2018

Free Monoidal Profunctors

Posted by Bartosz Milewski under Category Theory, Haskell
[4] Comments

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 $C$ to $Set$ . The current post may then be shortened to: Since profunctors are just functors from $C^{op} \times C$ to $Set$ , with the obvious monoidal structure induced by the tensor product in $C$ , 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 $\langle a, b \rangle$ . 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 $a$ to $s$ , as one would expect, it goes from $s$ to $a$ . This is why we say that the first argument comes from the opposite category $C^{op}$ , where all morphisms are reversed with respect to $C$ . Thus a morphism from $\langle a, b \rangle$ to $\langle s, t \rangle$ in $C^{op} \times C$ is a pair of morphisms $\langle s \to a, b \to t \rangle$ .

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 $p$ and $q$ 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 $C$ is monoidal (has a tensor product $\otimes$ and a unit object $1$ ), then the category $C^{op} \times C$ has a trivially induced tensor product:

$\langle a, b \rangle \otimes \langle c, d \rangle = \langle a \otimes c, b \otimes d \rangle$

and unit $\langle 1, 1 \rangle$

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:

$(C^{op} \times C) \, ( \langle a, b \rangle \otimes \langle c, d \rangle, \langle s, t \rangle )$

is a set of pairs of morphisms:

$\langle s \to a \otimes c, b \otimes d \to t \rangle$

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

$\langle X \to a, b \to Y \rangle$

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

$s \to a \otimes c \cong X \to a$

(Consider, for instance, unit $()$ for $a$ .) 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 $Set$ to the unit in $C^{op} \times C$ :

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

Operator >**< maps the product in $Set$ to the induced product in $C^{op} \times C$ :

(>**<) :: (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:

$A_p q = (C^{op} \times C) (1, -) + \int^{ a b c d } p a b \times q c d \times (C^{op} \times C) (\langle a, b \rangle \otimes \langle c, d \rangle, -)$

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 17, 2018

Free Monoidal Functors

Posted by Bartosz Milewski under Programming
[6] Comments

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 $x$ s and a bag of $y$ s, 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 $x$ s; and the tail, which is a container of $y$ s. We are appending to it another container of $t$ s. 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

Bartosz Milewski's Programming Cafe

February 2018

Free Monoidal Profunctors

Profunctors in Haskell

Higher Order Functors

Free Monoidal Profunctor

Categorical Picture

Acknowledgments

Free Monoidal Functors

Day Convolution

Lax Monoidal Functors

Fixed Points

Higher Order Functors

Free Monoidal Functor

Categorical Picture

Conclusion

Appendix: Free Monad

Top Posts

License

Blogroll

Follow Me

Archives