There is a lot of folklore about various data types that pop up in discussions about lenses. For instance, it’s known that `FunList`

and `Bazaar`

are equivalent, although I haven’t seen a proof of that. Since both data structures appear in the context of `Traversable`

, which is of great interest to me, I decided to do some research. In particular, I was interested in translating these data structures into constructs in category theory. This is a continuation of my previous blog posts on free monoids and free applicatives. Here’s what I have found out:

`FunList`

is a free applicative generated by the`Store`

functor. This can be shown by expressing the free applicative construction using Day convolution.- Using Yoneda lemma in the category of applicative functors I can show that
`Bazaar`

is equivalent to`FunList`

Let’s start with some definitions. `FunList`

was first introduced by Twan van Laarhoven in his blog. Here’s a (slightly generalized) Haskell definition:

data FunList a b t = Done t | More a (FunList a b (b -> t))

It’s a non-regular inductive data structure, in the sense that its data constructor is recursively called with a different type, here the function type `b->t`

. `FunList`

is a functor in `t`

, which can be written categorically as:

where is a shorthand for the hom-set .

Strictly speaking, a recursive data structure is defined as an initial algebra for a higher-order functor. I will show that the higher order functor in question can be written as:

where is the (indexed) store comonad, which can be written as:

Here, is the constant functor, and is the hom-functor. In Haskell, this is equivalent to:

newtype Store a b s = Store (a, b -> s)

The standard (non-indexed) `Store`

comonad is obtained by identifying `a`

with `b`

and it describes the objects of the slice category (morphisms are functions that make the obvious triangles commute).

If you’ve read my previous blog posts, you may recognize in the functor that generates a free applicative functor (or, equivalently, a free monoidal functor). Its fixed point can be written as:

The star stands for Day convolution–in Haskell expressed as an existential data type:

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

Intuitively, is a “list of” `Store`

functors concatenated using Day convolution. An empty list is the identity functor, a one-element list is the `Store`

functor, a two-element list is the Day convolution of two `Store`

functors, and so on…

In Haskell, we would express it as:

data FunList a b t = Done t | More ((Day (Store a b) (FunList a b)) t)

To show the equivalence of the two definitions of `FunList`

, let’s expand the definition of Day convolution inside :

The coend corresponds, in Haskell, to the existential data type we used in the definition of `Day`

.

Since we have the hom-functor under the coend, the first step is to use the co-Yoneda lemma to “perform the integration” over , which replaces with everywhere. We get:

We can then evaluate the constant functor and use the currying adjunction:

to get:

Applying the co-Yoneda lemma again, we replace with :

This is exactly the functor that generates `FunList`

. So `FunList`

is indeed the free applicative generated by `Store`

.

All transformations in this derivation were natural isomorphisms.

Now let’s switch our attention to `Bazaar`

, which can be defined as:

type Bazaar a b t = forall f. Applicative f => (a -> f b) -> f t

(The actual definition of `Bazaar`

in the lens library is even more general–it’s parameterized by a profunctor in place of the arrow in `a -> f b`

.)

The universal quantification in the definition of `Bazaar`

immediately suggests the application of my favorite double Yoneda trick in the functor category: The set of natural transformations (morphisms in the functor category) between two functors (objects in the functor category) is isomorphic, through Yoneda embedding, to the following end in the functor category:

The end is equivalent (modulo parametricity) to Haskell `forall`

. Here, the sets of natural transformations between pairs of functors are just hom-functors in the functor category and the end over is a set of higher-order natural transformations between them.

In the double Yoneda trick we carefully select the two functors and to be either representable, or somehow related to representables.

The universal quantification in `Bazaar`

is limited to applicative functors, so we’ll pick our two functors to be free applicatives. We’ve seen previously that the higher-order functor that generates free applicatives has the form:

Here’s the version of the Yoneda embedding in which varies over all applicative functors in the category , and and are arbitrary functors in :

The free functor is the left adjoint to the forgetful functor :

Using this adjunction, we arrive at:

We’re almost there–we just need to carefuly pick the functors and . In order to arrive at the definition of `Bazaar`

we want:

The right hand side becomes:

where I represented natural transformations as ends. The first term can be curried:

and the end over can be evaluated using the Yoneda lemma. So can the second term. Altogether, the right hand side becomes:

In Haskell notation, this is just the definition of `Bazaar`

:

forall f. Applicative f => (a -> f b) -> f t

The left hand side can be written as:

Since we have chosen to be the hom-functor , we can use the Yoneda lemma to “perform the integration” and arrive at:

With our choice of , this is exactly the free applicative generated by `Store`

–in other words, `FunList`

.

This proves the equivalence of `Bazaar`

and `FunList`

. Notice that this proof is only valid for -valued functors, although a generalization to the enriched setting is relatively straightforward.

There is another family of functors, `Traversable`

, that uses universal quantification over applicatives:

class (Functor t, Foldable t) => Traversable t where traverse :: forall f. Applicative f => (a -> f b) -> t a -> f (t b)

The same double Yoneda trick can be applied to it to show that it’s related to `Bazaar`

. There is, however, a much simpler derivation, suggested to me by Derek Elkins, by changing the order of arguments:

traverse :: t a -> (forall f. Applicative f => (a -> f b) -> f (t b))

which is equivalent to:

traverse :: t a -> Bazaar a b (t b)

In view of the equivalence between `Bazaar`

and `FunList`

, we can also write it as:

traverse :: t a -> FunList a b (t b)

Note that this is somewhat similar to the definition of `toList`

:

toList :: Foldable t => t a -> [a]

In a sense, `FunList`

is able to freely accumulate the effects from `traversable`

, so that they can be interpreted later.

## Acknowledgments

I’m grateful to Edward Kmett and Derek Elkins for many discussions and valuable insights.

November 19, 2018 at 6:29 pm

Is use of the indexing variables for the Store functor consistent throughout this article? It looks ‘a’ and ‘b’ occasionally swap roles, sometimes being in negative position, sometimes being in positive position.

November 20, 2018 at 3:35 am

I try to be consistent: a positive, b negative. Could you point out the place where they are swapped?

November 20, 2018 at 1:57 pm

Perhaps I’m mistaken, but the roles of ‘a’ and ‘b’ appear to be swapped when the store functor is written as the product of a constant functor and hom-functor —

specifically, between the lines

(

) “To show the equivalence of the two definitions of FunList…”) “…we just need to carefully pick the functors g and h”.and

(

November 20, 2018 at 2:19 pm

Brilliant article by the way. I’ve really enjoyed it.

I’ve noticed that you recommend Emily Riehl’s “Category Theory in Context” elsewhere. Are there any other category-theory or topos-theory books (aside from the MacLane’s staple, of course) that you might recommend?

December 12, 2018 at 1:54 pm

Barr and Wells, Toposes, Triples, and Theories is a great book.