Previously: Profunctors.

# Traversals

A traversal is a kind of optic that can focus on zero or more items at a time. Naively, we would expect to have a getter that returns a list of values, and a setter that replaces a list of values. Think of a tree with $N$ leaves: a traversal would return a list of leaves, and it would allow you to replace them with a new list. The problem is that the size of the list you pass to the setter cannot be arbitrary—it must match the number of leaves in the particular tree. This is why, in Haskell, the setter and the getter are usually combined in a single function:

s -> ([b] -> t, [a])


Still, Haskell is not able to force the sizes of both lists to be equal.

Since a list type can be represented as an infinite sum of tuples, I knew that the categorical version of this formula must involve a power series, or a polynomial functor:

$\mathbf{Set} \big(s, \sum_{n} \mathbf{Set}(b^n, t) \times a^n\big)$

but was unable to come up with an existential form for it.

Pickering, Gibbons, and Wu came up with a representation for traversals using profunctors that were cartesian, cocartesian, and monoidal at the same time, but the monoidal constraint didn’t fit neatly into the Tambara scheme:

class Profunctor p => Monoidal p where
par   :: p a b -> p c d -> p (a, c) (b, d)
empty :: p () ()


We’ve been struggling with this problem, when one of my students, Mario Román came up with the ingenious idea to make $n$ existential.

The idea is that a coend in the existential representation of optics acts like a sum (or like an integral—hence the notation). A sum over natural numbers is equivalent to the coend over the category of natural numbers.

At the root of all optics there is a monoidal action. For lenses, this action is given by “scaling”

$a \to a \times c$

For prisms, it’s the “translation”

$a \to a + c$

For grates it’s the exponentiation

$a \to a^c$

The composition of a prism and a lens is an affine transformation

$a \to c_0 + a \times c_1$

A traversal is similarly generated by a polynomial functor, or a power series functor:

$a \to \sum_n c_n \times a^n$

The key observation here is that there is a different object $c_n$ for every power of $a$, which can only be expressed using dependent types in programming. For every multiplicity of foci, the residue is of a different type.

In category theory, we can express the whole infinite sequence of residues as a functor from the monoidal category $\mathbb{N}$ of natural numbers to $\mathbf{Set}$. (The sum is really a coend over $\mathbb{N}$.)

The existential version of a traversal is thus given by:

$\int^{c \colon [\mathbb{N}, \mathbf{Set}]} \mathbf{Set}\big(s, \sum_n c_n \times a^n\big) \times \mathbf{Set}\big( \sum_m c_m \times b^m, t\big)$

We can now use the continuity of the hom-set to replace the mapping out of a sum with a product of mappings:

$\int^{c \colon [\mathbb{N}, \mathbf{Set}]} \mathbf{Set}\big(s, \sum_n c_n \times a^n\big) \times \prod_m \mathbf{Set}\big( c_m \times b^m, t\big)$

$\int^{c \colon [\mathbb{N}, \mathbf{Set}]} \mathbf{Set}\big(s, \sum_n c_n \times a^n\big) \times \prod_m \mathbf{Set}\big( c_m, \mathbf{Set}( b^m, t)\big)$

The product of hom-sets is really an end over $\mathbb{N}$, or a set of natural transformations in $[\mathbb{N}, \mathbf{Set}]$

$\int^{c \colon [\mathbb{N}, \mathbf{Set}]} \mathbf{Set}\big(s, \sum_n c_n \times a^n\big) \times [\mathbb{N}, \mathbf{Set}]\big( c_-, \mathbf{Set}( b^-, t)\big)$

and we can apply the Yoneda lemma to “integrate” over $c$ to get:

$\mathbf{Set}(s, \sum_n (\mathbf{Set}(b^n, t) \times a^n)\big)$

which is exactly the formula for traversals.

Once we understood the existential representation of traversals, the profunctor representation followed. The equivalent of Tambara modules for traversals is a category of profunctors equipped with the monoidal action parameterized by objects in $[\mathbb{N}, \mathbf{Set}]$:

$\alpha_{c, \langle a, b \rangle} \colon p \langle a, b \rangle \to p\langle \sum_n c_n \times a^n, \sum_m c_m \times b^m \rangle$

The double Yoneda trick works for these profunctors as well, proving the equivalence with the existential representation.

# Generalizations

As hinted in my blog post and formalized by Mitchell Riley, Tambara modules can be generalized to an arbitrary monoidal action. We have also realized that we can combine actions in two different categories. We could take an arbitrary monoidal category $\mathcal{M}$, define its action on two categories, $\mathcal{C}$ and $\mathcal{D}$ using strong monoidal functors:

$F \colon \mathcal{M} \to [\mathcal{C}, \mathcal{C}]$

$G \colon \mathcal{M} \to [\mathcal{D}, \mathcal{D}]$

These actions define the most general existential optic:

$\mathbf{Optic} \langle s, t \rangle \langle a, b \rangle = \int^{m \colon \mathcal{M}} \mathcal{C}(s, F_m a) \times \mathcal{D}(G_m b, t)$

Notice that the pairs of arguments are heterogenous—e.g., in $\langle a, b \rangle$, $a$ is from $\mathcal{C}$, and $b$ is from $\mathcal{D}$.

We have also generalized Tambara modules:

$\alpha_{m, \langle a, b \rangle} \colon p \langle a, b \rangle \to p \langle F_m a, G_m b\rangle$

and the Pastro Street derivation of the promonad. That lead us to a more general proof of isomorphism between the profunctor formulation and the existential formulation of optics. Just to be general enough, we did it for enriched categories, replacing $\mathbf{Set}$ with an arbitrary monoidal category.

Finally, we described some new interesting optics like algebraic and monadic lenses.

# The Physicist’s Explanation

The traversal result confirmed my initial intuition from general relativity that the most general optics are generated by the analog of diffeomorphisms. These are the smooth coordinate transformations under which Einstein’s theory is covariant.

Physicists have long been using symmetry groups to build theories. Laws of physics are symmetric with respect to translations, time shifts, rotations, etc.; leading to laws of conservation of momentum, energy, angular momentum, etc. There is an uncanny resemblance of these transformations to some of the monoidal actions in optics. The prism is related to translations, the lens to rotations or scaling, etc.

There are many global symmetries in physics, but the real power comes from local symmetries: gauge symmetries and diffeomorphisms. These give rise to the Standard Model and to Einstein’s theory of gravity.

A general monoidal action seen in optics is highly reminiscent of a diffeomorphism, and the symmetry behind a traversal looks like it’s generated by an analytical function.

In my opinion, these similarities are a reflection of a deeper principle of compositionality. There is only a limited set of ways we can decompose complex problems, and sooner or later they all end up in category theory.

The main difference between physics and category theory is that category theory is more interested in one-way mappings, whereas physics deals with invertible transformations. For instance, in category theory, monoids are more fundamental than groups.

Here’s how categorical optics might be seen by a physicist.

In physics we would start with a group of transformations. Its representations would be used, for instance, to classify elementary particles. In optics we start with a monoidal category $\mathcal{M}$ and define its action in the target category $\mathcal{C}$. (Notice the use of a monoid rather than a group.)

$F \colon \mathcal{M} \to [\mathcal{C}, \mathcal{C}]$

In physics we would represent the group using matrices, here we use endofunctors.

A profunctor is like a path that connects the initial state to the final state. It describes all the ways in which $a$ can evolve into $b$.

If we use mixed optics, final states come from a different category $\mathcal{D}$, but their transformations are parameterized by the same monoidal category:

$G \colon \mathcal{M} \to [\mathcal{D}, \mathcal{D}]$

A path may be arbitrarily extended, at both ends, by a pair of morphisms. Given a morphism in $\mathcal{C}$:

$f \colon a' \to a$

and another one in $\mathcal{D}$

$g \colon b \to b'$

the profunctor uses them to extend the path:

$p \langle a, b \rangle \to p \langle a', b' \rangle$

A (generalized) Tambara module is like the space of paths that can be extended by transforming their endpoints.

$\alpha_{m, \langle a, b \rangle} \colon p \langle a, b \rangle \to p \langle F_m a, G_m b\rangle$

If we have a path that can evolve $a$ into $b$, then the same path can be used to evolve $F_m a$ into $G_m b$. In physics, we would say that the paths are “invariant” under the transformation, but in category theory we are fine with a one-way mapping.

The profunctor representation is like a path integral:

$\int_{p \colon \mathbf{Tam}} \mathbf{Set}( p \langle a, b \rangle, p \langle s, t \rangle)$

We fix the end-states but we vary the paths. We integrate over all paths that have the “invariance” or extensibility property that defines the Tambara module.

For every such path, we have a mapping that takes the evolution from $a$ to $b$ and produces the evolution (along the same path) from $s$ to $t$.

The main theorem of profunctor optics states that if, for a given collection of states, $\langle a, b \rangle, \langle s, t \rangle$, such a mapping exists, then these states are related. There exists a transformation and a pair of morphisms that are secretly used in the path integral to extend the original path.

$\int^{m \colon \mathcal{M}} \mathcal{C}(s, F_m a) \times \mathcal{D}(G_m b, t)$

Again, the mappings are one-way rather than both ways. They let us get from $s$ to $F_m a$ and from $G_m b$ to $t$.

This pair of morphisms is enough to extend any path $p \langle a, b \rangle$ to $p \langle s, t \rangle$ by first applying $\alpha_m$ and then lifting the two morphisms. The converse is also true: if every path can be extended then such a pair of morphisms must exist.

What seems unique to optics is the interplay between transformations and decompositions: The way $m$ can be interpreted both as parameterizing a monoidal action and the residue left over after removing the focus.

# Conclusion

For all the details and a list of references you can look at our paper “Profunctor optics, a categorical update.” It’s the result of our work at the Adjoint School of Applied Category Theory in Oxford in 2019. It’s avaliable on arXiv.

I’d like to thank Mario Román for reading the draft and providing valuable feedback.

Previously: Existentials.

# Double Yoneda

If you squint hard enough, the Yoneda lemma:

$\int_{x} \mathbf{Set}\big(\mathcal{C}(a, x), f x\big) \cong f a$

could be interpreted as the representable functor $\mathcal{C}(a, -)$ acting as the unit with respect to taking the end. It takes an $f$ and returns an $f$. Let’s keep this in mind.

We are going to need an identity that involves higher-order natural transformations between two higher-order functors. These are actually the functors $R_a$ that we’ve encountered before. They are parameterized by objects in $\mathcal{C}$, and their action on functors (co-presheaves) is to apply those functors to objects. They are the “give me a functor and I’ll apply it to my favorite object” kind of functors.

We need a natural transformation between two such functors, and we can express it as an end:

$\int_f \mathbf{Set}( R_a f, R_s f) = \int_f \mathbf{Set}( f a, f s)$

Here’s the trick: replace these functors with their Yoneda equivalents:

$\int_f \mathbf{Set}( f a, f s) \cong \int_f \mathbf{Set}\Big(\int_{x} \mathbf{Set}\big(\mathcal{C}(a, x), fx), \int_{y} \mathbf{Set}\big(\mathcal{C}(s, y), f y\big)\Big)$

Notice that this is now a mapping between two hom-sets in the functor category, the first one being:

$\int_{x} \mathbf{Set}\big(\mathcal{C}(a, x), fx\big) = [\mathcal{C}, \mathbf{Set}]\big(\mathcal{C}(a, -), f\big)$

We can now use the corollary of the Yoneda lemma to replace the set of natural transformation between these two hom-functors with the hom-set:

$[\mathcal{C}, \mathbf{Set}]\big(\mathcal{C}(s, -), \mathcal{C}(a, -) \big)$

But this is again a natural transformation between two hom-functors, so it can be further reduced to $\mathcal{C}(a, s)$. The result is:

$\int_f \mathbf{Set}( f a, f s) \cong \mathcal{C}(a, s)$

We’ve used the Yoneda lemma twice, so this trick is called the double-Yoneda.

# Profunctors

It turns out that the prism also has a functor-polymorphic representation, but it uses profunctors in place of regular functors. A profunctor is a functor of two arguments, but its action on arrows has a twist. Here’s the Haskell definition:

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


It lifts a pair of functions, where the first one goes in the opposite direction.

In category theory, the “twist” is encoded by using the opposite category $\mathcal{C}^{op}$, so a profunctor is defined a functor from $\mathcal{C}^{op} \times \mathcal{C}$ to $\mathbf{Set}$.

The prime example of a profunctor is the hom-functor which, on objects, assigns the set $\mathcal{C}(a, b)$ to every pair $\langle a, b \rangle$.

Before we talk about the profunctor representation of prisms and lenses, there is a simple optic called Iso. It’s defined by a pair of functions:

from :: s -> a
to   :: b -> t


The key observation here is that such a pair of arrows is an element of the hom set in the category $\mathcal{C}^{op} \times \mathcal{C}$ between the pair $\langle a, b \rangle$ and the pair $\langle s, t \rangle$:

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

The “twist” of using $\mathcal{C}^{op}$ reverses the direction of the first arrow.

Iso has a simple profunctor representation:

type Iso s t a b = forall p. Profunctor p => p a b -> p s t


This formula can be translated to category theory as an end in the profunctor category:

$\int_p \mathbf{Set}(p \langle a, b \rangle, p \langle s, t \rangle)$

Profunctor category is a category of co-presheaves $[\mathcal{C}^{op} \times \mathcal{C}, \mathbf{Set}]$. We can immediately apply the double Yoneda identity to it to get:

$\int_p \mathbf{Set}(p \langle a, b \rangle, p \langle s, t \rangle) \cong (\mathcal{C}^{op} \times \mathcal{C})( \langle a, b \rangle, \langle s, t \rangle)$

which shows the equivalence of the two representations.

# Tambara Modules

Here’s the profunctor representation of a prism:

type Prism s t a b = forall p. Choice p => p a b -> p s t


It looks almost the same as Iso, except that the quantification goes over a smaller class of profunctors called Choice (or cocartesian). This class is defined as:

class Profunctor p => Choice where
left'  :: p a b -> p (Either a c) (Either b c)
right' :: p a b -> p (Either c a) (Either c b)


Lenses can also be defined in a similar way, using the class of profunctors called Strong (or cartesian).

class Profunctor p => Strong where
first'  :: p a b -> p (a, c) (b, c)
second' :: p a b -> p (c, a) (c, b)


Profunctor categories with these structures are called Tambara modules. Tambara formulated them in the context of monoidal categories, for a more general tensor product. Sum (Either) and product (,) are just two special cases.

A Tambara module is an object in a profunctor category with additional structure defined by a family of morphisms:

$\alpha_{c, \langle a, b \rangle} \colon p \langle a, b \rangle \to p\langle c \otimes a, c \otimes b \rangle$

with some naturality and coherence conditions.

Lenses and prisms can thus be defined as ends in the appropriate Tambara modules

$\int_{p \colon \mathbf{Tam}} \mathbf{Set}(p \langle a, b \rangle, p \langle s, t \rangle)$

We can now use the double Yoneda trick to get the usual representation.

The problem is, we don’t know in what category the result should be. We know the objects are pairs $\langle a, b \rangle$, but what are the morphisms between them? It turns out this problem was solved in a paper by Pastro and Street. The category in question is the Kleisli category for a particular promonad. This category is now better known as $\mathbf{Optic}$. Let me explain.

The double Yoneda trick worked for an unconstrained category of functors. We need to generalize it to a category with some additional structure (for instance, a Tambara module).

Let’s say we start with a functor category $[\mathcal{C}, \mathbf{Set}]$ and endow it with some structure, resulting in another functor category $\mathcal{T}$. It means that there is a (higher-order) forgetful functor $U \colon \mathcal{T} \to [\mathcal{C}, \mathbf{Set}]$ that forgets this additional structure. We’ll also assume that there is the right adjoint functor $F$ that freely generates the structure.

We will re-start the derivation of double Yoneda using the forgetful functor

$\int_{f \colon \mathcal{T}} \mathbf{Set}( (U f) a, (U f) s)$

Here, $a$ and $s$ are objects in $\mathcal{C}$ and $(U f)$ is a functor in $[\mathcal{C}, \mathbf{Set}]$.

We perform the Yoneda trick the same way as before to get:

$\int_{f \colon \mathcal{T}} \mathbf{Set}\Big(\int_{x \colon C} \mathbf{Set}\big(\mathcal{C}(a, x),(U f) x), \int_{y \colon C} \mathbf{Set}\big(\mathcal{C}(s, y),(U f) y\big)\Big)$

Again, we have two sets of natural transformations, the first one being:

$\int_{x \colon C} \mathbf{Set}\big(\mathcal{C}(a, x), (U f) x\big) = [\mathcal{C}, \mathbf{Set}]\big(\mathcal{C}(a, -), U f\big)$

$[\mathcal{C}, \mathbf{Set}]\big(\mathcal{C}(a, -), U f\big) \cong \mathcal{T}\Big(F\big(\mathcal{C}(a, -)\big), f\Big)$

The right-hand side is a hom-set in the functor category $\mathcal{T}$. Plugging this back into the original formula, we get

$\int_{f \colon \mathcal{T}} \mathbf{Set}\Big(\mathcal{T}\Big(F\big(\mathcal{C}(a, -)\big), f\Big), \mathcal{T}\Big(F\big(\mathcal{C}(s, -)\big), f\Big) \Big)$

This is the set of natural transformations between two hom-functors, so we can use the corollary of the Yoneda lemma to replace it with:

$\mathcal{T}\Big( F\big(\mathcal{C}(s, -)\big), F\big(\mathcal{C}(a, -)\big) \Big)$

We can then use the adjunction again, in the opposite direction, to get:

$[\mathcal{C}, \mathbf{Set}] \Big( \mathcal{C}(s, -), (U \circ F)\big(\mathcal{C}(a, -)\big) \Big)$

or, using the end notation:

$\int_{c \colon C} \mathbf{Set} \Big(\mathcal{C}(s, c), (U \circ F)\big(\mathcal{C}(a, -)\big) c \Big)$

Finally, we use the Yoneda lemma again to get:

$(U \circ F) \big( \mathcal{C}(a, -) \big) s$

This is the action of the higher-order functor $(U \circ F)$ on the hom-functor $\mathcal{C}(a, -)$, the result of which is applied to $s$.

The composition of two functors that form an adjunction is a monad $\Phi$. This is a monad in the functor category $[\mathcal{C}, \mathbf{Set}]$. Altogether, we get:

$\int_{f \colon \mathcal{T}} \mathbf{Set}( (U f) a, (U f) s) \cong \Phi \big( \mathcal{C}(a, -) \big) s$

# Profunctor Representation of Lenses and Prisms

The previous formula can be immediately applied to the category of Tambara modules. The forgetful functor takes a Tambara module and maps it to a regular profunctor $p$, an object in the functor category $[\mathcal{C}^{op} \times \mathcal{C}, \mathbf{Set}]$. We replace $a$ and $s$ with pairs of objects. We get:

$\int_{p \colon \mathbf{Tam}} \mathbf{Set}(p \langle a, b \rangle, p \langle s, t \rangle) \cong \Phi \big( (\mathcal{C}^{op} \times \mathcal{C})(\langle a, b \rangle, -) \big) \langle s, t \rangle$

The only missing piece is the higher order monad $\Phi$—a monad operating on profunctors.

The key observation by Pastro and Street was that Tambara modules are higher-order coalgebras. The mappings:

$\alpha \colon p \langle a, b \rangle \to p\langle c \otimes a, c \otimes b \rangle$

can be thought of as components of a natural transformation

$\int_{\langle a, b \rangle, c} \mathbf{Set} \big( p \langle a, b \rangle, p\langle c \otimes a, c \otimes b \rangle \big)$

By continuity of hom-sets, we can move the end over $c$ to the right:

$\int_{\langle a, b \rangle} \mathbf{Set} \Big( p \langle a, b \rangle, \int_c p\langle c \otimes a, c \otimes b \rangle \Big)$

We can use this to define a higher order functor that acts on profunctors:

$(\Theta p)\langle a, b \rangle = \int_c p\langle c \otimes a, c \otimes b \rangle$

so that the family of Tambara mappings can be written as a set of natural transformations $p \to (\Theta p)$:

$\int_{\langle a, b \rangle} \mathbf{Set} \big( p \langle a, b \rangle, (\Theta p)\langle a, b \rangle \big)$

Natural transformations are morphisms in the category of profunctors, and such a morphism $p \to (\Theta p)$ is, by definition, a coalgebra for the functor $\Theta$.

Pastro and Street go on showing that $\Theta$ is more than a functor, it’s a comonad, and the Tambara structure is not just a coalgebra, it’s a comonad coalgebra.

$(\Phi p) \langle s, t \rangle = \int^{\langle x, y \rangle, c} (\mathcal{C}^{op} \times \mathcal{C})\big(\langle c \otimes x, c \otimes y \rangle, \langle s, t \rangle \big) \times p \langle x, y \rangle$

When a monad is adjoint to a comonad, the comonad coalgebras are isomorphic to monad algebras—in this case, Tambara modules. Indeed, the algebras $(\Phi p) \to p$ are given by natural transformations:

$\int_{\langle s, t \rangle} \mathbf{Set}\Big( (\Phi p) \langle s, t \rangle, p\langle s, t \rangle \Big)$

Substituting the formula for $\Phi$,

$\int_{\langle s, t \rangle} \mathbf{Set}\Big( \int^{\langle x, y \rangle, c} (\mathcal{C}^{op} \times \mathcal{C})\big(\langle c \otimes x, c \otimes y \rangle, \langle s, t \rangle \big) \times p \langle x, y \rangle, p\langle s, t \rangle \Big)$

by continuity of the hom-set (with the coend in the negative position turning into an end),

$\int_{\langle s, t \rangle} \int_{\langle x, y \rangle, c}\mathbf{Set}\Big( (\mathcal{C}^{op} \times \mathcal{C})\big(\langle c \otimes x, c \otimes y \rangle, \langle s, t \rangle \big) \times p \langle x, y \rangle, p\langle s, t \rangle \Big)$

$\int_{\langle s, t \rangle, \langle x, y \rangle, c}\mathbf{Set}\Big( (\mathcal{C}^{op} \times \mathcal{C})\big(\langle c \otimes x, c \otimes y \rangle, \langle s, t \rangle \big), \mathbf{Set}\big( p \langle x, y \rangle, p\langle s, t \rangle \big) \Big)$

and the Yoneda lemma, we get

$\int_{\langle x, y \rangle, c} \mathbf{Set}\big( p \langle x, y \rangle, p\langle c \otimes x, c \otimes y \rangle \big)$

which is the Tambara structure $\alpha$.

$\Phi$ is exactly the monad that appears on the right-hand side of the double-Yoneda with adjunctions. This is because every monad can be decomposed into a pair of adjoint functors. The decomposition we’re interested in is the one that involves the Kleisli category of free algebras for $\Phi$. And now we know that these algebras are Tambara modules.

All that remains is to evaluate the action of $\Phi$ on the represesentable functor:

$\Phi \big( (\mathcal{C}^{op} \times \mathcal{C})(\langle a, b \rangle, -) \big) \langle s, t \rangle$

It’s a matter of simple substitution:

$\int^{\langle x, y \rangle, c} (\mathcal{C}^{op} \times \mathcal{C})\big(\langle c \otimes x, c \otimes y \rangle, \langle s, t \rangle \big) \times (\mathcal{C}^{op} \times \mathcal{C})(\langle a, b \rangle, \langle x, y \rangle)$

and using the Yoneda lemma to replace $\langle x, y \rangle$ with $\langle a, b \rangle$. The result is:

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

This is exactly the existential represenation of the lens and the prism:

$\int^c \mathcal{C}(s, c \otimes a) \times \mathcal{C}(c \otimes b, t)$

This was an encouraging result, and I was able to derive a few other optics using the same approach.

The idea was that Tambara modules were just one example of a monoidal action, and it could be easily generalized to other types of optics, like Grate, where the action $c \otimes a$ is replaced by the (contravariant in $c$) action $a^c$ (or c->a, in Haskell).

There was just one optic that resisted that treatment, the Traversal. The breakthrough came when I was joined by a group of talented students at the Applied Category Theory School in Oxford.

Next: Traversals.