19-Tambara.tex

\documentclass[DaoFP]{subfiles}
\begin{document}
\setcounter{chapter}{18}

\chapter{Tambara Modules}

It's not often that an obscure corner of category theory gains sudden prominence in programming. Tambara modules got a new lease on life in their application to profunctor optics. They provide a clever solution to the problem of composing optics. We've seen that, in the case of lenses, the getters compose nicely using function composition, but the composition of setters involves some shenanigans. The existential representation doesn't help much. The profunctor representation, on the other hand, makes composition a snap. 

The situation is somewhat analogous to the problem of composing geometric transformations in graphics programming. For instance, if you try to compose two rotations around two different axes, the formula for the new axis and the angle is quite complicated. But if you represent rotations as matrices, you can use matrix multiplication; or, if you represent them as quaternions, you can use quaternion multiplication. Profunctor representation lets you compose optics using straightforward function composition.


\section{Tannakian Reconstruction}

\subsection{Monoids and their Representations}

The theory or representations is a science in itself. Here, we'll approach it from the categorical perspective. Instead of groups, we'll consider monoids. A monoid can be defined as a special object in a monoidal category, but it can also be thought of as a single-object category $\cat M$. We call its object $*$, and the only hom-set $\cat M( *, *)$ contains all the information we need. 

What we called ``product'' in a monoid is replaced by the composition of morphisms. By the laws of a category, it's associative and unital---the identity morphism playing the role of the monoidal unit.

In this sense, every single-object category is automatically a monoid and all monoids can be made into single-object categories. 

For instance, a monoid of the whole numbers with addition can be thought of as a category with a single abstract object $*$ and a different morphism for every number. To compose two such morphisms, you add their numbers, as in the example below:
\[
 \begin{tikzcd}
  *
  \arrow[r, bend left, "2"]
  \arrow[rr, bend right, "5"']
 & *
 \arrow[r, bend left, "3"]
 & *
  \end{tikzcd}
\]
The morphism corresponding to zero is automatically the identity morphism. 

We can \emph{represent} a monoid as transformations of a set. Such a representation is given by a functor $F \colon \cat M \to \Set$. It maps the single object $*$ to some set $S$, and it maps the hom-set $\cat M(*, *)$ to a set of functions $S \to S$. By functor laws, it maps identity to identity and composition to composition, so it preserves the structure of the monoid. 

If the functor is fully faithful, its image contains exactly the same information as the monoid and nothing more. But in general functors tend to cheat. The hom-set $\Set (S, S)$ may contain some other functions that are not in the image of $\cat M(*, *)$; and multiple morphisms in $\cat M$ may be mapped to a single function. 

In the extreme, the whole hom-set $\cat M(*, *)$ may be mapped to the identity function $id_S$. So, just by looking at the set $S$---the image of $*$ under the functor $F$---we cannot dream of reconstructing the original monoid.

Not all is lost, though, if we are allowed to look at all the representations of a given monoid simultaneously. Such representations form a category---the functor category $[\cat M, \Set]$, a.k.a. the co-presheaf category over $\cat M$. Arrows in this category are natural transformations. 

Since the source category $\cat M$ contains only one object, naturality conditions take a particularly simple form. A natural transformation $\alpha \colon F \to G$ has only one component, a function $\alpha \colon F *\; \to \;G *$. Given a morphism $m \colon * \to *$, the naturality square reads:

\[
 \begin{tikzcd}
 F *
 \arrow[r, "\alpha"]
 \arrow[d, "F m"]
 & G *
  \arrow[d, "G m"]
\\
 F *
 \arrow[r, "\alpha"]
 & G *
 \end{tikzcd}
\]
It's a relationship between three functions acting on two sets:
\[
 \begin{tikzcd}
 F *
  \arrow[loop, "F m"']
  \arrow[rr, bend right, "\alpha"']
 && G *
  \arrow[loop, "G m"']
  \end{tikzcd}
\]
The naturality condition tells us that:
\[ \alpha \circ (F m) = (G m) \circ \alpha \]

In other words, if you pick any element $x$ in the set $F *$, you can map it to $G *$ using $\alpha$ and then apply the transformation $G m$ corresponding to $m$; or you can first apply the transformation $F m$ and then map the result using $\alpha$. The result must be the same.

Such functions are called \index{equivariant function}\emph{equivariant}. We often call $F m$ the \index{monoid action}\emph{action} of $m$ on the set $F *$. An equivariant function connects an action on one set to its corresponding action on another set using either pre-composition or post-composition. 

\subsection{Cayley's theorem}

In group theory, Cayley's theorem states that every group is isomorphic to a (subgroup of the) group of permutations. A \index{group}\emph{group} is just a monoid in which every element $g$ has an inverse $g^{-1}$. Permutations are bijective functions that map a set to itself. They \emph{permute} the elements of a set.

In category theory, Cayley's theorem is practically built into the definition of a monoid and its representations. 

The connection between the single-object interpretation and the more traditional ``set of elements'' interpretation of a monoid is easy to establish. We do this by constructing the functor $F \colon \cat M \to \Set$ that maps $*$ to the special set $S$ that is equal to the hom-set: $S = \cat M(*, *)$. Elements of this set are identified with morphisms in $\cat M$. We define the action of $F$ on morphisms as post-composition:
\[ (F m) n = m \circ n \]
Here $m$ is a morphism in $\cat M$ and $n$ is an element of $S$, which happens to also be a morphism in $\cat M$.

We can take this particular representation as an alternative definition of a monoid in the monoidal category $\Set$. All we need is to implement unit and multiplication:
\begin{align*}
\eta &\colon 1 \to S
\\
\mu &\colon S \times S \to S
\end{align*}
The unit picks the element of $S$ that corresponds to $id_*$ in $\cat M(*, *)$. Multiplication of two elements $m$ and $n$ is given by the element that corresponds to $m \circ n$. 

At the same time we can look at $S$ as an image of $F \colon \cat M \to \Set$, in which case it's the functions $S \to S$ that form a representation of the monoid. This is the essence of the Cayley's theorem: Every monoid can be represented by a set of endo-functions.

In programming, the best example of applying the Cayley's theorem is in the efficient implementation of \index{list reversal}list reversal. Recall the naive recursive implementation of reversal:
\begin{haskell}
reverse :: [a] -> [a]
reverse [] = []
reverse (a : as) = reverse as ++ [a]
\end{haskell}
It splits the list into the head and the tail, reverses the tail, and appends a singleton made out of the head to the result. The problem is that every append has to traverse the growing list resulting in $O(N^2)$ performance.

Remember, however, that a list is a (free) monoid:
\begin{haskell}
instance Monoid [a] where
  mempty = []
  mappend as bs = as ++ bs
\end{haskell}
We can use Cayley's theorem to represent this monoid as functions on lists:
\begin{haskell}
type DList a = [a] -> [a]
\end{haskell}
To represent a list, we turn it into a function. It's a function (a closure) that prepends this list \hask{as} to its argument \hask{xs}:
\begin{haskell}
rep :: [a] -> DList a
rep as = \xs -> as ++ xs
\end{haskell}
This representation is called a \index{difference list}\emph{difference list}.

To turn a function back to a list, it's enough to apply it to an empty list:
\begin{haskell}
unRep :: DList a -> [a]
unRep f = f []
\end{haskell}
It's easy to check that the representation of an empty list is an identity function, and that the representation of a concatenation of two lists is a composition of representations:
\begin{haskell}
rep [] = id
rep (xs ++ ys) = rep xs . rep ys
\end{haskell}
So this is exactly the Cayley representation of the list monoid.

We can now translate the reversal algorithm to produce this new representation:
\begin{haskell}
rev :: [a] -> DList a
rev [] = rep []
rev (a : as) = rev as . rep [a]
\end{haskell}
and turn it back to a list:
\begin{haskell}
fastReverse :: [a] -> [a]
fastReverse = unRep . rev
\end{haskell}
At first sight it might seem like we haven't done much except add a layer of conversions on top of our recursive algorithm. Except that the new algorithm has $O(N)$ rather than $O(N^2)$ performance. To see that, consider reversing a simple list \hask{[1, 2, 3]}. The function \hask{rev} turns this list into a composition of functions:
\begin{haskell}
 rep [3] . rep [2] . rep [1]
\end{haskell}
It does it in linear time. The function \hask{unRep} executes this composite acting on an empty list. But notice that each \hask{rep} \emph{prepends} its argument to the cumulative result. In particular, the final \hask{rep [3]} executes:
\begin{haskell}
 [3] ++ [2, 1]
\end{haskell}
Unlike appending, prepending is a constant-time operation, so the whole algorithm takes $O(N)$ time. 

Another way of looking at it is to realize that \hask{rev} queues up the actions in the order of the elements of the list, starting at the head. But the queue of functions is executed in the first-in-first-out (FIFO) order. 

Because of Haskell's laziness, list reversal using \hask{foldl} has similar performance:
\begin{haskell}
reverse = foldl (\as a -> a : as) []
\end{haskell}
This is because \hask{foldl}, before returning the result, traverses the list left-to-right accumulating functions (closures). It then executes them as necessary, in the FIFO order.

\subsection{Tannakian reconstruction of a monoid}

How much information do we need to reconstruct a monoid from its representations? Just looking at the sets is definitely not enough, since any monoid can be represented on any set. But if we include structure-preserving functions between those sets, we might have a chance. 

The usual approach of category theory is to look at the big picture, rather than concentrating on individual cases. So, instead of focusing on a single functor, let's look at the totality of representations of a given monoid $\cat M$---the functor category $[\cat M, \Set]$. 

We can define a forgetful functor called the \index{fiber functor}fiber functor, $\mathvar{fib} \colon [\cat M, \Set] \to \Set$. It's action on objects (here, functors) extracts the underlying set:
\[ \mathvar{fib} F = F *\]
Its action on arrows (here, natural transformations) produces the corresponding equivariant function. Acting on $\alpha \colon F \to G$ we get:
\[\mathop{\mathvar{fib}} \alpha \colon F *\; \to G * \]

The functor $\mathvar{fib}$ is a member of a functor category $[[\cat M, \Set], \Set]$. In this category arrows are natural transformations, which are families of functions in $\Set$ parameterized by functors. For Tannakian reconstruction, we will focus on the set of natural transformations from $\mathvar{fib}$ to itself. We can write it as an end over the functor category $[\cat M, \Set]$:
\[ \int_F \Set(\mathvar{fib} F, \mathvar{fib} F) \]
or, expanding the definition of $\mathvar{fib}$:
\[ \int_F \Set(F *, F *) \]

Here are some details. The profunctor under the end is a functor of the form:
\[ P \colon [\cat M, \Set]^{op} \times [\cat M, \Set] \to \Set \]
whose action on objects (pairs of functors from $\cat M$ to $\Set$)  is:
\[ P \langle G, H \rangle = \Set (G *, H *) \]

Let's define its action on morphisms, that is pairs of natural transformations. Given any pair:
\begin{align*}
\alpha &\colon G' \to G \\ 
\beta &\colon H \to H'
\end{align*}
their lifting is a function:
\[ P\langle \alpha, \beta \rangle \colon  \Set ( G*, H*)  \to \Set (G'*, H'*)\] that is implemented by precomposing with $\alpha$ and postcomposing with $\beta$. 

The end is a gigantic product, that is a tuple of functions picked from hom-sets $\Set ( F*, F*)$, one per each functor. These tuples are further constrained by the wedge condition. We can extract this constraint by instantiating the universal condition for the singleton set (terminal object). Here we pick $g$ as an element of $\Set (G*, G*)$ and $h$ as an element of $\Set (H*, H*)$,
\[
 \begin{tikzcd}
 & 1
 \arrow[ddl, bend right,  "g"']
 \arrow[ddr, bend left, "h"]
 \arrow[d, dashed, ""]
 \\
 & \int_F \Set (F *, F *)
 \arrow[dl, "\pi_G"']
 \arrow[dr, "\pi_H"]
 \\
 \Set(G *, G *)
 \arrow[dr, "\alpha \circ -"']
 && \Set (H *, H *)
  \arrow[dl, "- \circ \alpha"]
\\
 & \Set (G *, H *)
 \end{tikzcd}
\]
We get the following condition:
\[  \alpha \circ g = h \circ \alpha  \]
for any equivariant $\alpha \colon G *\; \to H *$ satisfying the condition:
\[ \alpha \circ (G m) = (H m) \circ \alpha \]

The Tannakian reconstruction theorem in this case tells us that:
\[ \int_F \Set(F *, F *) \cong \cat M (*, *) \]
In other words, we can recover the monoid from its representations. 

We'll see the proof of this theorem in the context of a more general statement, but here's the general idea. Among all possible representations there is one that is full and faithful. Its underlying set is the hom-set $\cat M (*, *)$ and the monoid action is that of post-composition $(m \circ -)$. The only functions from this set to itself that satisfy the wedge condition are the monoidal actions themselves, and they are in one-to-one correspondence with the elements of $\cat M (*, *)$.


\subsection{Proof of Tannakian reconstruction}

Monoid reconstruction is a special case of a more general theorem in which, instead of the single-object category, we use a regular category. As in the monoid case, we'll reconstruct the hom-set, only this time it will be a regular hom-set between a pair of objects. We'll prove the formula:
\[ \int_{F \colon [\cat C, \Set]} \Set (F a, F b) \cong \cat C(a, b) \]
The trick is to use the Yoneda lemma to represent the action of $F$:
\[ F a \cong [\cat C, \Set] ( \cat C (a ,-), F) \]
and the same for $F b$. We get:
\[ \int_{F \colon [\cat C, \Set]} \Set ([\cat C, \Set] ( \cat C (a ,-), F), [\cat C, \Set] ( \cat C (b ,-), F)) \]
Notice that the two sets of natural transformations here are hom-sets in $[\cat C, \Set]$. 

Recall the corollary to the Yoneda lemma that works for any category $\cat A$:
\[ [\cat A, \Set] (\cat A (x, -), \cat A (y, -)) \cong \cat A (y, x) \]
We can write it using an end:
\[ \int_{z \colon \cat C} \Set (\cat A (x, z), \cat A (y, z)) \cong \cat A (y, x) \]
In particular, we can replace $\cat A$ with the functor category $[\cat C, \Set]$. We get:
\[ \int_{F \colon [\cat C, \Set]} \Set ([\cat C, \Set] ( \cat C (a ,-), F), [\cat C, \Set] ( \cat C (b ,-), F)) \cong [\cat C, \Set](\cat C (b ,-), \cat C (a ,-))\]
We can then apply the Yoneda lemma again to the right hand side and get:
\[ \cat C (a, b) \]
which is exactly the sought after result.

It's important to realize how the structure of the functor category enters the end through the wedge condition. It does that through natural transformations. Every time we have a natural transformation between two functors $\alpha \colon G \to H$, the following diagram must commute:
\[
 \begin{tikzcd}
 & \int_F \Set (F a, F b)
 \arrow[dl, "\pi_G"']
 \arrow[dr, "\pi_H"]
 \\
 \Set(G a, G b)
 \arrow[dr, "{\Set(id, \alpha)}"']
 && \Set (H a, H b)
  \arrow[dl, "{\Set (\alpha, id)}"]
\\
 & \Set (G a, H b)
 \end{tikzcd}
\]

To get some intuition about Tannakian reconstruction, you may recall that $\Set$-valued functors have the interpretation as \index{proof-relevant subset}proof-relevant subsets. A functor $F \colon \cat C \to \Set$ (a co-presheaf) defines a subset of the objects of (a small category) $\cat C$. We say that an object $a$ is in that subset only if $F a$ is non-empty. Each element of $F a$ can then be interpreted as a proof of that. 

But unless the category in question is discrete, not all subsets will correspond to co-presheaves. In particular, whenever there is an arrow $f \colon a \to b$, there also is a function $F f \colon F a \to F b$. According to our interpretation, such function maps every proof that $a$ is in the subset  defined by $F$ to a proof that $b$ is in that subset. Co-presheaves thus define proof-relevant subsets that are compatible with the structure of the category.

Let's reinterpret Tannakian reconstruction in the same spirit. 
\[ \int_{F \colon [\cat C, \Set]} \Set (F a, F b) \cong \cat C(a, b) \]
An element of the left-hand side is a proof that for every subset that is compatible with the structure of $\cat C$, if $a$ belongs to that subset, so does $b$. That is only possible if there is an arrow from $a$ to $b$. 

\begin{exercise}
Apply to proof of Tannakian reconstruction to a single-object category $\cat M$ from the previous section.
\end{exercise}

\subsection{Tannakian reconstruction in Haskell}

We can immediately translate this result to Haskell. We replace the end by \hask{forall}. The left hand side becomes:
\begin{haskell}
forall f. Functor f => f a -> f b
\end{haskell}
and the right hand side is the function type \hask{a->b}. 

We've seen polymorphic functions before: they were functions defined for all types, or sometimes for classes of types. Here we have a function that is defined for all functors. It says: give me a functorful of \hask{a}'s and I'll produce a functorful of \hask{b}'s---no matter what functor you use. The only way this can be implemented (using parametric polymorphism) is if this function has secretly captured a function of the type \hask{a->b} and is applying it using \hask{fmap}. 

Indeed, one direction of the isomorphism is just that: capturing a function and \hask{fmap}ping it over the argument:
\begin{haskell}
toTannaka :: (a -> b) -> (forall f. Functor f => f a -> f b)
toTannaka g fa = fmap g fa
\end{haskell}
The other direction uses the Yoneda trick:
\begin{haskell}
fromTannaka :: (forall f. Functor f => f a -> f b) -> (a -> b)
fromTannaka g a = runIdentity (g (Identity a))
\end{haskell}
where the \index{identity functor}identity functor is defined as:
\begin{haskell}
data Identity a = Identity a 
  
runIdentity :: Identity a -> a
runIdentity (Identity a) = a

instance Functor Identity where
  fmap g (Identity a) = Identity (g a)
\end{haskell}

This kind of reconstruction might seem trivial and pointless. Why would anyone want to replace function type \hask{a->b} with a much more complicated type:
\begin{haskell}
type Getter a b = forall f. Functor f => f a -> f b
\end{haskell}
It's instructive, though, to think of \hask{a->b} as the precursor of all optics. It's a lens that focuses on the $b$ part of $a$. It tells us that $a$ contains enough information, in one form or another, to construct a $b$. It's a ``getter'' or an ``accessor.'' 

Obviously, functions compose. What's interesting though is that functor representations also compose, and they compose using simple function composition, as seen in this example:
\begin{haskell}
boolToStrGetter :: Getter Bool String
boolToStrGetter = toTannaka (show) . toTannaka (bool (-1) 1)
\end{haskell}
where:
\begin{haskell}
bool :: a -> a -> Bool -> a
bool f _ False = f
bool _ t True  = t
\end{haskell}

Other optics don't compose so easily, but their functor (and profunctor) representations do. 

\subsection{Tannakian reconstruction with adjunction}

The trick in generalizing the Tannakian reconstruction is to define the end over some specialized functor category $\cat T$ (we'll later apply it to the Tambara category). 

Let's assume that we have the free/forgetful adjunction $F \dashv U$ between two functor categories $\cat T$ and $[\cat C, \Set]$:
\[ \cat T (F Q, P) \cong  [\cat C, \Set] ( Q, U P )\]
where $Q$ is a functor in $[\cat C, \Set]$ and $P$ a functor in $\cat T$.

Our starting point for Tannakian reconstruction is the following end:
\[ \int_{P \colon \cat T} \Set \big((U P) a, (U P) s\big) \]
The mapping $\cat T \to \Set$ parameterized by the object $a$, and given by the formula:
\[ P \mapsto (U P) a \]
is the \index{fiber functor}\emph{fiber functor}, so the end formula can be interpreted as a set of natural transformations between two fiber functors. 

Conceptually, a fiber functor describes an ``infinitesimal neighborhood'' of an object. It maps functors to sets but, more importantly, it maps natural transformations to functions. These functions probe the environment in which the object lives. In particular, natural transformations in $\cat T$ are involved in wedge conditions that define the end. (In calculus, stalks of sheaves play a very similar role.)

As we did before, we first apply the Yoneda lemma to the co-presheaves $(U P)$:
\[ \int_{P \colon \cat T} \Set \Big([\cat C, \Set] \big( \cat C (a ,-), U P\big), [\cat C, \Set] \big( \cat C (s ,-), U P\big)\Big) \]
We can now use the adjunction:
\[ \int_{P \colon \cat T} \Set \Big(\cat T \big( F \cat C (a ,-), P\big), \cat T \big( F \cat C (s ,-), P\big)\Big) \]
We end up with a mapping between two natural transformations in the functor category $\cat T$. We can perform the ``integration'' using the corollary to the Yoneda lemma, giving us:
\[ \cat T\big( F \cat C (s ,-), F \cat C (a ,-) \big) \]
We can apply the adjunction once more:
\[ \Set \big( \cat C (s ,-), (U\circ F) \cat C (a ,-) \big) \]
and the Yoneda lemma again:
\[ \big( (U\circ F) \cat C (a ,-) \big) s \]
The final observation is that the composition $U \circ F$ of adjoint functors is a monad in the functor category. Let's call this monad $\Phi$. The result is the following identity that will serve as the foundation for profunctor optics:
\[ \int_{P \colon \cat T} \Set \big((U P) a, (U P) s\big) \cong \big( \Phi \cat C (a ,-) \big) s \]
The right-hand side is the action of the monad $\Phi = U \circ F$ on the representable functor $\cat C (a, -)$, which is then evaluated at $s$. Using the Yoneda functor notation, this can be written as $(\Phi \mathcal Y^a) s$.

Compare this with the earlier formula for Tannakian reconstruction, especially if we rewrite it in the following form:
\[ \int_{F \colon [\cat C, \Set]} \Set (F a, F s) \cong \cat C(a, -) s\]

Keep in mind that, in the derivation of optics, we'll replace $a$ and $s$ with pairs of objects $\langle a, b \rangle$ and $\langle s, t \rangle$  from $\cat C^{op} \times \cat C$. Our functors will then become profunctors.

\section{Profunctor Lenses}

Our goal is to find a functor representation for optics. We've seen before that, for instance, type-changing lenses can be seen as hom-sets in the $\mathbf{Lens}$ category. The objects in $\mathbf{Lens}$ are pairs of objects from some cartesian category $\cat C$, and a hom-set from one such pair $\langle s, t \rangle$ to another  $\langle a, b \rangle$ is given by the coend formula:
\[ \mathcal{L}\langle s, t\rangle \langle a, b \rangle = \int^{c} \mathcal{C}(s, c \times a) \times  \mathcal{C}(c \times b, t) \]
Notice that the pair of hom-sets in this formula can be seen as a single hom-set in the product category $\cat C^{op} \times \cat C$:
\[  \mathcal{L}\langle s, t\rangle \langle a, b \rangle =  \int^{c} (\cat C^{op} \times \cat C )(c \bullet \langle a, b \rangle, \langle s, t \rangle)  \]
where we define the action of $c$ on a pair $\langle a, b \rangle$ as:
\[ c \bullet \langle a, b \rangle = \langle c \times a, c \times b \rangle \]
This is a shorthand notation for the diagonal part of a more general action of $\cat C^{op} \times \cat C$ on itself given by:
 \[ \langle c, c' \rangle \bullet \langle a, b \rangle = \langle c \times a, c' \times b \rangle \]


This suggests that, to represent such optics, we should be looking at co-presheaves on the category $\cat C^{op} \times \cat C$, that is, we should be considering profunctor representations. 

\subsection{Iso}
As a quick test of this idea, let's apply our reconstruction formula to the simple case of $\cat T = [\cat C^{op} \times \cat C, \Set]$ with no additional structure. In that case we don't need to use the forgetful functors, or the monad $\Phi$, and we just get the straightforward application of Tannakian reconstruction:
\[  \mathcal{O}\langle s, t\rangle \langle a, b \rangle =\int_{P \colon \cat T} \Set \big(P \langle a, b\rangle, P \langle s, t\rangle \big) \cong \big( (\cat C^{op} \times \cat C) (\langle a, b\rangle ,-) \big) \langle s, t\rangle \]
The right hand side evaluates to:
\[ (\cat C^{op} \times \cat C) (\langle a, b\rangle , \langle s, t\rangle) = \cat C (s, a) \times \cat C (b, t) \]

This optic is known in Haskell as \hask{Iso} (or an adapter):
\begin{haskell}
type Iso s t a b = (s -> a, b -> t)
\end{haskell}
and it, indeed, has a profunctor representation corresponding to the following end:
\begin{haskell}
type IsoP s t a b = forall p. Profunctor p => p a b -> p s t
\end{haskell}

Given a pair of functions it's easy to construct this profunctor-polymorphic function:
\begin{haskell}
toIsoP :: (s -> a, b -> t) -> IsoP s t a b
toIsoP (f, g) = dimap f g
\end{haskell}
This is simply saying that any profunctor can be used to lift a pair of functions. 

Conversely, we may ask the question: How can a single polymorphic function map the set $P \langle a, b \rangle$ to the set $P \langle s, t \rangle$ for \emph{every} profunctor imaginable? The only thing this function knows about the profunctor is that it can lift a pair of functions. Therefore it must be a closure that either contains or is able to produce a pair of functions \hask{(s -> a, b -> t)}. 

\begin{exercise}
Implement the function:
\begin{haskell}
fromIsoP :: IsoP s t a b -> (s -> a, b -> t)
\end{haskell}
Hint: Show that this is a profunctor:
\begin{haskell}
newtype Adapter a b s t = Ad (s -> a, b -> t)
\end{haskell}
and construct \hask{Adapter a a s s} using a pair of identity functions.
\end{exercise}

\subsection{Profunctors and lenses}

Let's try to apply the same logic to lenses. We have to find a class of profunctors to plug into our profunctor representation. Let's assume that the forgetful functor $U$ only forgets additional structure but doesn't change the sets, so the set $P \langle a, b \rangle$ is the same as the set $(U P) \langle a, b \rangle$. 

Let's start with the existential representation. We have at our disposal an object $c$ and a pair of functions:
\[  \langle f, g \rangle \colon \cat C(s, c \times a) \times \cat C(c \times b, t) \]
We want to build a profunctor representation, so we have to be able to map the set $P \langle a, b \rangle$ to the set $P \langle s, t \rangle$. We could get $P \langle s, t \rangle$ by lifting these two functions, but only if start from $P \langle c \times a, c \times b \rangle$. Indeed:
\[ P \langle f, g \rangle \colon P \langle c \times a, c \times b \rangle \to P \langle s, t \rangle \]
What we are missing is the mapping:
\[ P \langle a, b \rangle \to P \langle c \times a, c \times b \rangle \]
And this is exactly the additional structure we shall demand from our profunctor class. 

\subsection{Tambara module}

A profunctor $P$ equipped with the family of transformations:
\[ \alpha_{\langle a, b\rangle, c} \colon P \langle a, b \rangle \to P \langle c \times a, c \times b \rangle \]
is called a \emph{Tambara module}. 

We want this family to be natural in $a$ and $b$, but what should we demand from $c$? The problem with $c$ is that it appears twice, once in the contravariant, and once in the covariant position. So, if we want to interact nicely with arrows like $h \colon c \to c'$, we have to modify the naturality condition. We may consider a more general profunctor $P \langle c' \times a, c \times b \rangle$ and treat $\alpha$ as producing its diagonal elements, ones in which $c'$ is the same as $c$. 

A transformation $\alpha$ between diagonal parts of two profunctors $P$ and $Q$ is called a \index{dinatural transformation}\emph{dinatural transformation} (\emph{di}-agonally natural) if the following diagram commutes for any $f \colon c \to c'$:

\[
 \begin{tikzcd}
 & P \langle c', c \rangle
 \arrow[dl, "{P \langle f, c \rangle}"']
 \arrow[dr, "{P \langle c', f \rangle}"]
 \\
 P \langle c, c \rangle 
  \arrow[d, "\alpha_c"']
 && P \langle c', c' \rangle
 \arrow[d, "\alpha_{c'}"]
 \\
 Q \langle c, c \rangle
   \arrow[dr, "{P \langle c, f \rangle}"']
 &&  Q \langle c', c' \rangle
 \arrow[dl,"{P \langle f, c \rangle}"]
\\
&Q \langle c, c' \rangle
 \end{tikzcd}
\]
(I used the common shorthand $P \langle f, c \rangle$, reminiscent of whiskering, for $P \langle f, id_c \rangle$.)

In our case, the dinaturality condition simplifies to:
\[
 \begin{tikzcd}
 & P \langle a, b \rangle
 \arrow[dl, "{\alpha_{\langle a, b \rangle, c}}"']
 \arrow[dr, "{\alpha_{\langle a, b \rangle, c'}}"]
 \\
 P \langle c \times a, c \times b \rangle
   \arrow[dr, "{P \langle c \times a, f \times b \rangle}"']
 &&  P \langle c' \times a, c'  \times b\rangle
 \arrow[dl,"{P \langle f \times b, c \times b \rangle}"]
\\
&P \langle c \times a, c' \times b \rangle
 \end{tikzcd}
\]
(Here, again $P \langle f \times b, c \times b \rangle$ stands for $P \langle f \times id_b, id_{c \times b} \rangle$.)

There is one more consistency condition on Tambara modules: they must preserve the monoidal structure. The action of multiplying by $c$ makes sense in a cartesian category: we have to have a product for any pair of objects, and we want to have the terminal object to serve as the unit of multiplication. Tambara modules have to respect unit and preserve multiplication. For the unit (terminal object), we impose the following condition:
\[ \alpha_{\langle a, b \rangle, 1} = id _{P \langle a, b \rangle}\]
For multiplication, we have:
\[ \alpha_{\langle a, b \rangle, c' \times c} \cong  \alpha_{\langle c \times a, c \times b \rangle, c'} \circ  \alpha_{\langle a, b \rangle, c}\]
or, pictorially:
\[
 \begin{tikzcd}
 P \langle a, b \rangle
 \arrow[rr, "{\alpha_{\langle a, b \rangle, c' \times c } }"]
 \arrow[rdd, "{ \alpha_{\langle a, b \rangle, c}}"']
 &&
 P \langle c' \times c \times a, c' \times c \times b \rangle
 \\
 \\
 & P \langle c \times a, c \times b \rangle
  \arrow[ruu, "{\alpha_{\langle c \times a, c \times b \rangle, c'}}"']
\end{tikzcd}
\]
(Notice that the product is associative up to isomorphism, so there is a hidden associator in this diagram.)

Since we want Tambara modules to form a category, we have to define morphisms between them. These are natural transformations that preserve the additional structure. Let's say we have a natural transformation $\rho$ between two Tambara modules $\rho \colon (P, \alpha) \to (Q, \beta) $. We can either apply $\alpha$ and then $\rho$, or do $\rho$ first and then  $\beta$. We want the result to be the same:
\[
 \begin{tikzcd}
  P \langle a, b \rangle
 \arrow[d, "{ \rho_{\langle a, b \rangle}}"']
 \arrow[r, "{ \alpha_{\langle a, b \rangle, c}}"]
  &  P \langle c \times a, c \times b \rangle
  \arrow[d, "{ \rho_{\langle c \times a, c \times b \rangle}}"]
\\
   Q \langle a, b \rangle
 \arrow[r, "{ \beta_{\langle a, b \rangle, c}}"]
 &  Q \langle c \times a, c \times b \rangle
 \end{tikzcd}
\]
Keep in mind that the structure of the Tambara category is encoded in these natural transformations. They will determine, through the wedge condition, the shape of the ends that enter the definition of profunctor lenses.

\subsection{Profunctor lenses}

Now that we have some intuition about how Tambara modules are related to lenses, let's go back to our main formula:
\[  \mathcal{L}\langle s, t\rangle \langle a, b \rangle =\int_{P \colon \cat T} \Set \big((U P) \langle a, b\rangle, (U P) \langle s, t\rangle \big) \cong \big( \Phi (\cat C^{op} \times \cat C) (\langle a, b\rangle ,-) \big) \langle s, t\rangle \]
This time we're taking the end over the Tambara category. The only missing part is the monad $\Phi = U \circ F$ or the functor $F$ that freely generates Tambara modules.

It turns out that, instead of guessing the monad, it's easier to guess the comonad. There is a comonad in the category of profunctors that takes a profunctor $P$ and produces another profunctor $\Theta P$. Here's the formula:
\[(\Theta P) \langle a, b \rangle = \int_c P \langle c \times a, c \times b \rangle \]
You can check that this is indeed a comonad by implementing $\varepsilon$ and $\delta$ (\hask{extract} and \hask{duplicate}). For instance, $\varepsilon$ maps $\Theta P \to P$ using the projection $\pi_1$ for the terminal object (the unit of cartesian product).

What's interesting about this comonad is that its coalgebras are Tambara modules. Again, these are coalgebras that map profunctors to profunctors. They are natural transformations $P \to \Theta P$. We can write such a natural transformation as an element of the end:
\[\int_{a, b} \Set \big (P \langle a, b \rangle, (\Theta P) \langle a, b \rangle \big) = \int_{a, b} \int_c \Set \big( P\langle a, b \rangle , P \langle c \times a, c \times b \rangle \big) \]
I used the continuity of the hom-functor to pull out the end over $c$. The resulting end encodes a set of natural (dinatural in $c$) transformations that define a Tambara module:
\[ \alpha_{\langle a, b\rangle, c} \colon P \langle a, b \rangle \to P \langle c \times a, c \times b \rangle \]
In fact, these coalgebras are \emph{comonad} coalgebras, that is they are compatible with the comonad $\Theta$. In other words, Tambara modules form the Eilenberg-Moore category of coalgebras for the comonad $\Theta$.

The left adjoint to $\Theta$ is a monad $\Phi$ given by the formula:
\[(\Phi P)  \langle s, t \rangle = \int^{u, v, c} (\cat C^{op} \times \cat C) \big(c \bullet \langle u, v\rangle , \langle s, t \rangle\big) \times P \langle u, v \rangle \]
where I used the shorthand notation:
\[ (\cat C^{op} \times \cat C) \big(c \bullet \langle u, v\rangle , \langle s, t \rangle\big) = \cat C(s, c \times u) \times \cat C(c \times v, t) \]

This adjunction can be easily verified using some end/coend manipulations: The mapping out of $\Phi P$ to some profunctor $Q$ can be written as an end. The coends in $\Phi$ can then be taken out using co-continuity of the hom-functor. Finally, applying the ninja-Yoneda lemma produces the mapping into $\Theta Q$. We get:
\[ [(\cat C^{op} \times \cat C, \Set] (P \Phi, Q) \cong [(\cat C^{op} \times \cat C, \Set] (P, \Theta Q) \]

Replacing $Q$ with $P$ we immediately see that the set of algebras for $\Phi$ is isomorphic to the set of coalgebras for $\Theta$. In fact they are monad algebras for $\Phi$. This means that the Eilenberg-Moore category for the monad $\Phi$ is the same as the Tambara category.

Recall that the Eilenberg-Moore construction factorizes a monad into a free/forgetful adjunction. This is exactly the adjunction we were looking for when deriving the formula for profunctor optics. 

What remains is to evaluate the action of $\Phi$ on the representable functor:
\[ \big( \Phi (\cat C^{op} \times \cat C) (\langle a, b\rangle ,-) \big) \langle s, t\rangle = \int^{u, v, c} (\cat C^{op} \times \cat C) \big(c \bullet \langle u, v\rangle , \langle s, t \rangle \big) \times  (\cat C^{op} \times \cat C) \big(\langle a, b\rangle , \langle u, v\rangle \big)\]
Applying the co-Yoneda lemma, we get:
\[ \int^c (\cat C^{op} \times \cat C) \big(c \bullet \langle a, b\rangle , \langle s, t \rangle\big) = \int^c \cat C(s, c \times a) \times \cat C (c \times b, t)\]
which is exactly the existential representation of the lens.

\subsection{Profunctor lenses in Haskell}

To define profunctor representation in Haskell we introduce a class of profunctors that are Tambara modules with respect to cartesian product (we'll see more general Tambara modules later). In the Haskell library this class is called \hask{Strong}. It also appears in the literature as \hask{Cartesian}:
\begin{haskell}
class Profunctor p => Cartesian p where
  alpha :: p a b -> p (c, a) (c, b)
\end{haskell}
The polymorphic function \hask{alpha} has all the relevant naturality properties guaranteed by parametric polymorphism. 

The profunctor lens is just a type synonym for a function type that is polymorphic in \hask{Cartesian} profunctors:
\begin{haskell}
type LensP s t a b = forall p. Cartesian p => p a b -> p s t
\end{haskell}

The easiest way to implement such a function is to start from the existential representation of a lens and apply \hask{alpha} followed by \hask{dimap} to the profunctor argument:
\begin{haskell}
toLensP :: LensE s t a b -> LensP s t a b
toLensP (LensE from to) = dimap from to . alpha
\end{haskell}

Because profunctor lenses are just functions, we can compose them as such:
\begin{haskell}
lens1 :: LensP s t x y 
-- p s t -> p x y
lens2 :: LensP x y a b 
-- p x y -> p a b
lens3 :: LensP s t a b 
-- p s t -> p a b
lens3 = lens2 . lens1
\end{haskell}

The converse mapping from a profunctor representation to the set/get representation of the lens is also possible. For that we need to guess the profunctor that we can feed into \hask{LensP}. It turns out that the get/set representation of the lens is such a profunctor, when we fix the pair of types \hask{a} and \hask{b}. We define:
\begin{haskell}
data FlipLens a b s t = FlipLens (s -> a) (s -> b -> t)
\end{haskell}
It's easy to show that it's indeed a profunctor:
\begin{haskell}
instance Profunctor (FlipLens a b) where
  dimap f g (FlipLens get set) = FlipLens (get . f) (fmap g . set . f)
\end{haskell}
Not only that---it is also a \hask{Cartesian} profunctor:
\begin{haskell}
instance Cartesian (FlipLens a b) where
  alpha(FlipLens get set) = FlipLens get' set'
    where get' = get . snd
          set' = \(x, s) b -> (x, set s b)
\end{haskell}
We can now initialize \hask{FlipLens} with a trivial pair of a getter and a setter and feed it to our profunctor representation:
\begin{haskell}
fromLensP :: LensP s t a b -> (s -> a, s -> b -> t)
fromLensP pp = (get', set')
  where FlipLens get' set' = pp (FlipLens id (\s b -> b))
\end{haskell}

\section{General Optics}
Tambara modules were originally defined for an arbitrary monoidal category\footnote{In fact, Tambara modules were originally defined for a category enriched over vector spaces} with a tensor product $\otimes$ and a unit object $I$. Their structure maps have the form:
\[ \alpha_{\langle a, b\rangle, c} \colon P \langle a, b \rangle \to P \langle c \otimes a, c \otimes b \rangle \]
You can easily convince yourself that all coherency laws translate directly to this case, and the derivation of profunctor optics works without a change.

\subsection{Prisms}

From the programming point of view there are two obvious monoidal structures to explore: the product and the sum. We've seen that the product gives rise to lenses. The sum, or the coproduct, gives rise to prisms. 

We get the existential representation simply by replacing the product by the sum in the definition of a lens:
\[ \mathcal{P}\langle s, t\rangle \langle a, b \rangle = \int^{c} \mathcal{C}(s, c + a) \times  \mathcal{C}(c + b, t) \]
To simplify this, notice that the mapping out of a sum is equivalent to the product of mappings:
\[ \int^{c} \mathcal{C}(s, c + a) \times  \mathcal{C}(c + b, t) \cong  \int^{c} \mathcal{C}(s, c + a) \times  \mathcal{C}(c, t) \times  \mathcal{C}(b, t) \]
Using the co-Yoneda lemma, we can get rid of the coend to get:
\[ \mathcal{C}(s, t + a) \times  \mathcal{C}(b, t) \]

In Haskell, this defines a pair of functions:
\begin{haskell}
match :: s -> Either t a
build :: b -> t
\end{haskell}

To understand this, let's first translate the existential form of the prism:
\begin{haskell}
data Prism s t a b where
  Prism :: (s -> Either c a) -> (Either c b -> t) -> Prism s t a b
\end{haskell}
Here \hask{s} either contains the focus \hask{a} or the residue \hask{c}. Conversely, \hask{t} can be built either from the new focus \hask{b}, or from the residue \hask{c}. 

This logic is reflected in the conversion functions:
\begin{haskell}
toMatch :: Prism s t a b -> (s -> Either t a)
toMatch (Prism from to) s =
  case from s of
    Left  c -> Left (to (Left c))
    Right a -> Right a
\end{haskell}

\begin{haskell}
toBuild :: Prism s t a b -> (b -> t)
toBuild (Prism from to) b = to (Right b)
\end{haskell}

\begin{haskell}
toPrism :: (s -> Either t a) -> (b -> t) -> Prism s t a b
toPrism match build = Prism from to
  where
    from = match
    to (Left  c) = c
    to (Right b) = build b
\end{haskell}

The profunctor representation of the prism is almost identical to that of the lens, except for swapping the product for the sum. 

The class of Tambara modules for the sum type is called \hask{Choice} in the Haskell library, or \hask{Cocartesian} in the literature:
\begin{haskell}
class Profunctor p => Cocartesian p where
  alpha' :: p a b -> p (Either c a) (Either c b)
\end{haskell}
The profunctor representation is a polymorphic function type:
\begin{haskell}
type PrismP s t a b = forall p. Cocartesian p => p a b -> p s t
\end{haskell}

The conversion from the existential prism is virtually identical to that of the lens:
\begin{haskell}
toPrismP :: Prism s t a b -> PrismP s t a b
toPrismP (Prism from to) = dimap from to . alpha'
\end{haskell}

Again, profunctor prisms compose using function composition.
\subsection{Traversals}
A traversal is a type of optic that focuses on multiple foci at once. Imagine, for instance, that you have a tree that can have zero or more leaves of type \hask{a}. A traversal should be able to get you a list of those nodes. It should also let you replace these nodes with a new list. And here's the problem: the length of the list that delivers the replacements must match the number of nodes, otherwise bad things happen. 

A type-safe implementation of a traversal would require us to keep track of the sizes of lists. In other words, it would require dependent types.

In Haskell, a (non-type-safe) traversal is often written as:
\begin{haskell}
type Traversal s t a b = s -> ([b] -> t, [a])
\end{haskell}
with the understanding that the sizes of the two lists are determined by \hask{s} and must be the same. 

When translating traversals to categorical language, we'll express this condition using a sum over the sizes of the list. A counted list of size $n$ is an $n$-tuple, or an element of $a^n$, so we can write:
\[ \mathbf{Tr} \langle s, t\rangle \langle a, b \rangle = \Set \big( s, \sum_n (\Set (b^n, t) \times a^n) \big) \]
We interpret a traversal as a function that, given a source $s$ produces an existential type that is hiding an $n$. It says that there exists an $n$ and a pair consisting of a function $b^n \to t$ and an $n$-tuple $a^n$. 

The existential form of a traversal must take into account the fact that the residues for different $n$'s will have, in principle, different types. For instance, you can decompose a tree into an n-tuple of leaves $a^n$ and the residue $c_n$ with $n$ holes. So the correct existential representation for a traversal must involve a coend over all sequences $c_n$ that are indexed by natural numbers:
\[ \mathbf{Tr} \langle s, t\rangle \langle a, b \rangle = \int^{c_n} \cat C (s, \sum_m c_m \times a^m) \times \cat C (\sum_k c_k \times b^k, t) \]
The sums here are coproducts in $\cat C$.

One way to look at sequences $c_n$ is to interpret them as fibrations. For instance, in $\Set$ we would start with a set $C$ and a projection $p \colon C \to \mathbb N$, where $\mathbb N$ is a set of natural numbers. Similarly $a^n$ could be interpreted as a fibration of the free monoid on $a$ (the set of lists of $a$'s) with the projection that extracts the length of the list.

Or we can look at $c_n$'s as mappings from the set of natural numbers to $\cat C$. In fact, we can treat natural numbers as a discrete category $\cat N$, in which case $c_n$'s are functors $\cat N \to \cat C$.

\[ \mathbf{Tr} \langle s, t\rangle \langle a, b \rangle = \int^{c \colon [\cat N, \cat C]} \cat C (s, \sum_m c_m \times a^m) \times \cat C (\sum_k c_k \times b^k, t) \]

To show the equivalence of the two representations, we first rewrite the mapping out of a sum as a product of mappings:
\[\int^{c \colon [\cat N, \cat C]} \cat C (s, \sum_m c_m \times a^m) \times \prod_k \cat C (c_k \times b^k, t) \]
and then use the currying adjunction:
\[\int^{c \colon [\cat N, \cat C]} \cat C (s, \sum_m c_m \times a^m) \times \prod_k \cat C (c_k,  [b^k, t]) \]
Here, $[b^k, t]$ is the internal hom, which is an alternative notation for the exponential object $t^{b^k}$.

The next step is to recognize that a product in this formula represents a set of natural transformations in $[\cat N, \cat C]$. Indeed, we could write it as an end:
 \[ \prod_k \cat C (c_k,  [b^k, t] \cong \int_{k : \cat N} C (c_k,  [b^k, t]) \]
This is because an end over a discrete category is just a product. Alternatively, we could write it as a hom-set in the functor category:
\[ [\cat N, \cat C](c_{-}, [b^{-}, t]) \]
with placeholders replacing the arguments to the two functors in question:
\[ k \mapsto c_k \]
\[ k \mapsto [b^k, t] \]

We can now use the co-Yoneda lemma in the functor category $[\cat N, \cat C]$:
\[\int^{c \colon [\cat N, \cat C]} \cat C (s, \sum_m c_m \times a^m) \times  [\cat N, \cat C]\big(c_{-}, [b^{-}, t]\big) \cong \cat C(s, \sum_m [b^m, t] \times a^m)\]
This result is more general than our original formula, but it turns into it when restricted to the category of sets.

To derive a profunctor representation for traversals, we should look more closely at the kind of transformations that are involved. We define the action of a functor $c \colon [\cat N, \cat C]$ on $a$ as:
\[ c \bullet a = \sum_m c_m \times a^m \]
These actions can be composed by expanding the formula using distributivity laws:
\[ c \bullet (c' \bullet a) = \sum_m c_m \times (\sum_n c'_n \times a^n)^m \]
If the target category is $\Set$, this is equivalent to the following Day convolution (for non-$\Set$ categories, one could use the enriched version of the Day convolution):
\[ (c \star c')_k = \int^{m, n} \cat N (m + n, k) \times c_m \times c'_n \]
This gives monoidal structure to the category $[\cat N, \cat C]$. 

The existential representation of traversals can be written is terms of the action of this monoidal category on $\cat C$:
\[ \mathbf{Tr} \langle s, t\rangle \langle a, b \rangle = \int^{c \colon [\cat N, \cat C]} \cat C (s, c \bullet a) \times \cat C (c \bullet b, t) \]

To derive the profunctor representation of traversals, we have to generalize Tambara modules to the action of a monoidal category:
\[ \alpha_{\langle a, b\rangle, c} \colon P \langle a, b \rangle \to P \langle c \bullet a, c \bullet b \rangle \]
It turns out that the original derivation of profunctor optics still works for these generalized Tambara modules, and traversals can be written as polymorphic functions:
\[  \mathbf{Tr}\langle s, t \rangle \langle a, b \rangle 
 =\int_{P \colon \cat T} \Set \big((U P) \langle a, b\rangle, (U P) \langle s, t\rangle \big) \]
where the end is taken over a generalized Tambara module.

\section{Mixed Optics}

Whenever we have an action of a monoidal category $\cat M$ on $\cat C$ we can define the corresponding optic. A category with such an action is called an \index{actegory}\emph{actegory}. We can go even further by considering two separate actions. Suppose that $\cat M$ can act on both $\cat C$ and $\cat D$. We'll use the same notation for both actions:
\[ \bullet \colon \cat M \times \cat C \to \cat C \]
\[ \bullet \colon \cat M \times \cat D \to \cat D \]
We can then define the \index{mixed optics}\emph{mixed optics} as:
\[ \mathcal{O} \langle s, t \rangle \langle a, b \rangle = \int^{m \colon \cat M} \cat C(s, m \bullet a) \times \cat D(m \bullet b, t) \]
These mixed optics have profunctor representations in terms of profunctors:
\[ P \colon \cat C ^{op} \times \cat D \to \Set \]
and the corresponding Tambara modules that use two separate actions:
\[ \alpha_{\langle a, b\rangle, m} \colon P \langle a, b \rangle \to P \langle m \bullet a, m \bullet b \rangle \]
with $a$ an object of $\cat C$, $b$ and object of $\cat D$, and $m$ and object of $\cat M$.

\begin{exercise}
What are the mixed optics for the action of the cartesian product when one of the categories is the terminal category? What if the first category is $\cat C^{op} \times \cat C$ and the second is terminal?
\end{exercise}

\end{document}