11affiliationtext: Macquarie University,
<EMAIL_ADDRESS>Independent researcher,
<EMAIL_ADDRESS><EMAIL_ADDRESS>University of
Oxford<EMAIL_ADDRESS>Tallinn University of
Technology foscoloregian<EMAIL_ADDRESS>Programming
Cafe<EMAIL_ADDRESS>
# Profunctor optics, a categorical update

Bryce Clarke  Derek Elkins  Jeremy Gibbons  Fosco Loregian  Bartosz Milewski
Emily Pillmore  Mario Román

###### Abstract

Profunctor optics are bidirectional data accessors that capture data
transformation patterns such as accessing subfields or iterating over
containers. They are modular, meaning that we can construct accessors for
complex structures by combining simpler ones. Profunctor optics have been
studied only using $\mathbf{Sets}$ as the enriching category and in the _non-
mixed_ case. However, functional programming languages are arguably better
described by enriched categories and we have found that some structures in the
literature are actually _mixed_ optics. Our work generalizes a classic result
by Pastro and Street on Tambara theory and uses it to describe _mixed_
$\mathcal{V}$-enriched profunctor optics and to endow them with
$\mathcal{V}$-category structure. We provide some original families of optics
and derivations, including an elementary one for _traversals_ that solves an
open problem posed by Milewski. Finally, we discuss a Haskell implementation.

_Keywords:_ lens, profunctor, Tambara module, coend calculus.

###### Contents

  1. 1 Introduction

##  1 Introduction

In functional programming, optics are a compositional representation of many
common patterns in bidirectional data accessing. They are provided by
libraries such as Kmett’s _lens_ [kmett15], O’Connor’s _mezzolens_
[oconnor15], or _purescript profunctor lenses_ by Freeman et al. [freeman15].
Optics, and more concretely _lenses_ , were originally used in functional
programming as a compositional solution to the problem of accessing fields of
nested data structures [foster05]. As the understanding of these data
accessors grew, different families of optics were introduced for a variety of
different types (e.g. _prisms_ for tagged unions or _traversals_ for
containers), each one of them capturing a particular data accessing pattern.
These families are intercomposable and together form a powerful language for
modular data access.

Perhaps surprisingly, optics can be composed using ordinary function
composition; an example can be seen in Figure LABEL:fig:example1. This is
thanks to an alternative encoding called _profunctor representation_. In this
encoding, each optic is written as single function that is polymorphic over
profunctors with a certain algebraic structure. For instance, _lenses_ can be
written as functions polymorphic over _cartesian_ profunctors whereas _prisms_
can be written as functions polymorphic over _cocartesian_ profunctors
[pickering17, §3]. Milewski [milewski17] has identified these structures
(cartesian, cocartesian, …) as _Tambara modules_ [tambara06] and has used a
result by Pastro and Street [pastro08] to propose a unified definition of
optic. That definition has been later extended by Boisseau and Gibbons
[boisseau18] and Riley [riley18], using slightly different techniques and
proposing laws for optics. However, the original result by Pastro and Street
cannot be used directly to unify all the optics that appear in practice. Our
work generalizes their result, going beyond the previous definitions of optic
and covering _mixed_ [riley18, §6.1] and _enriched optics_.

⬇

let home = ”221b Baker St, London, UK”

address :: Prism Address String

street :: Lens String Address

\par>>> home?. address.street

Just ”221b Baker St”

\par>>> home & address.street.~ ”4 Marylebone Rd”

”4 Marylebone Rd, London, UK”

\end{examplecode}

\caption{The composition of a prism (\hask{address}) and a lens
(\hask{street}) is used to parse a string and then access and modify one of
its subfields.}\label{fig:example1}

\end{figure}

\parThe generalized profunctor representation theorem captures optics already
present in the literature and makes it possible to upgrade them to more
sophisticated definitions. For instance, many generalizations of \emph{lenses}
in functional programming are shown to be particular cases of a more refined
definition that uses mixed optics (Definition~\ref{def:lens}). We also show
derivations for some new optics that were not present in the literature.

Finally, Milewski~\cite{milewski17} posed the problem of fitting the three
basic optics (lenses, prisms and traversals) into an elementary pattern;
lenses and prisms had been covered in his work, but traversals were missing.
We present a new description of traversals in terms of power series functors
whose derivation is more direct than the ones based on \emph{traversables} as
studied by Jaskelioff and Rypacek~\cite{rypacek12}.

\par\subsection{Contributions}

\par\begin{itemize}

\itemWe extend the \emph{double} construction from Pastro and Street’s
“Doubles for monoidal categories” to cover mixed optics. In the same way that
they characterize copresheaves of these \emph{doubles} as Tambara modules, we
characterize copresheaves of mixed optics as suitably generalized Tambara
modules~\cite[Proposition 6.1]{pastro08}.

\itemA study of enriched and \emph{mixed} optics~\cite[\S6.1]{riley18},
endowing them with \Vt{category} structure.

\itemAn extension of the result that justifies the profunctor representation
of optics used in functional programming to the case of enriched and mixed
optics.

\itemA new family of optics, which we dub \emph{algebraic lenses}
(Definition~\ref{def:algebraiclens}), that unifies new examples with some
optics already present in the literature, such as Boisseau’s \emph{achromatic
lens}~\cite[\S5.2]{boisseau17}.

\itemA new derivation showing that \emph{monadic lenses}~\cite{AbouSaleh16}
are mixed optics (Proposition~\ref{prop:monadiclens}). Similarly, a new
derivation showing that Myers’ \emph{lenses in a symmetric monoidal
category}~\cite[\S2.2]{spivak19} are mixed optics
(Proposition~\ref{prop:monoidallenses}).

\itemA unified definition of \emph{lenses}, that can be specialized to all of
these previous examples.

\itemA new derivation of the optic known as \emph{traversal}
(Definition~\ref{def:traversal}) in terms of a monoidal structure originally
described by Kelly~\cite[\S8]{kelly05} for the study of non-symmetric operads
(Proposition~\ref{prop:traversal}). Following this, a new family of optics
that arises when we generalize this monoidal structure.

\end{itemize}

\par\subsection{Synopsis}

\parWe introduce the definition of \emph{mixed optic} in
Section~\ref{sec:optics}. Section~\ref{sec:examples} describes examples from
the practice of functional programming and how they are captured by the
definition. Section~\ref{sec:tambaratheory} describes how the theory of
Tambara modules can be applied to obtain a profunctor representation for
optics.

\par\subsection{Setting}

\parWe shall work with categories enriched over a Bénabou cosmos
\\((\V,\otimes,I)\\); that is, a (small)-complete and cocomplete symmetric
monoidal closed category.

In particular, \\(\V\\) is enriched over itself and we write the internal hom-
object between \\(A,B \in\operatorname{Obj}(\V)\\) as \\(\V(A,B)\\) or just
\\([A,B]\\) when it does not cause ambiguity. Our intention is to keep a close
eye on the applications in functional programming: the enriching category
\\(\V\\) should be thought of as the category whose objects model the types of
an idealized programming language and whose morphisms model the programs.
Because of this, \\(\V\\) will be cartesian in many of the examples. We can,
however, remain agnostic as to which specific \\(\V\\) we are addressing.

\parFor calculations, we make significant use of coend calculus as described,
for instance, by Loregian~\cite{loregian19}.

The proofs in this paper can be carried without assuming choice or excluded
middle, but there is an important set-theoretical issue: in some of the
examples, we compute coends over non-small categories. We implicitly fix a
suitable Grothendieck universe and our categories are to be considered small
with respect to that universe. As Riley~\cite[\S2]{riley18} notes, this will
not be a problem in general: even if some coends are indexed by large
categories and we cannot argue their existence using the cocompleteness of
\\(\Sets\\), we will still find them represented by objects in the category.

\par\par\section{Optics}\label{sec:optics}

\parThe structure that is common to all optics is that they divide a bigger
data structure of type \\(S \in\C\\) into some \emph{focus} of type \\(A
\in\C\\) and some \emph{context} or \emph{residual} \\(M \in\M\\) around it.
We cannot access the context but we can still use its shape to update the
original data structure, replacing the current focus by a new one. The
definition will capture this fact imposing a quotient relation on the possible
contexts; this quotient is expressed by the dinaturality condition of a coend.
The category of contexts \\(\M\\) will be monoidal, allowing us to compose
optics with contexts \\(M\\) and \\(N\\) into an optic with context \\(M
\otimesN\\). Finally, we leave open the possibility of the new focus being of
a different type \\(B \in\D\\), possibly in a different category, which yields
a new data structure of type \\(T \in\D\\).

\parLet \\((\M,\otimes,I,a,\lambda,\rho)\\) be a monoidal \Vt{category} as
defined by Day~\cite{day70}. Let it act on two arbitrary \Vt{categories}
\\(\C\\) and \\(\D\\) with strong monoidal \Vt{functors} \\((\actL{}{})
\colon\M\to[ \C, \C]\\) and \\((\actR{}{}) \colon\M\to[\D,\D]\\). We write

\\[\begin{aligned}

& \phi_{A} \colonA \cong\actL{I}{A}, && \phi_{M,N,A}
\colon\actL{M}{\actL{N}{A}} \cong\actL{M \otimesN}{A}, \\\

& \varphi_{B} \colonB \cong\actR{I}{B}, && \varphi_{M, N,B}
\colon\actR{M}{\actR{N}{B}} \cong\actR{M \otimesN}{B},

\end{aligned}\\]

for the structure isomorphisms of the strong monoidal actions \\(\actL{}{}\\)
and \\(\actR{}{}\\).

\par\begin{definition}[{{after \cite[\S6.1]{riley18}, see
also~\cite{milewski17,boisseau18}}}]\label{def:optic}

Let \\(S,A \in\C\\) and \\(T,B \in\D\\). An \textbf{optic} from \\((S,T)\\)
with the focus on \\((A,B)\\) is an element of the following object described
as a coend

\\[\Optic_{\actL{}{},\actR{}{}} ((A, B), (S,T)) \coloneqq\int^{M} \C(S,
\actL{M}{A}) \otimes\D(\actR{M}{B}, T).

\\]

\end{definition}

\parThe two strong monoidal actions \\(\actL{}{}\\) and \\(\actR{}{}\\)
represent the two different ways in which the context interacts with the
focus: one when the data structure is decomposed and another one, possibly
different, when it is reconstructed. Varying these two actions we will cover
many examples from the literature and propose some new ones, as the following
table summarizes.

\par\begin{figure}[h]

\centering\begin{tabular}{ccc}

\hlineName & Description & Ref. \\\

\hlineAdapter \\((\mathbf{Optic}_{\id,\id})\\)

& \\(\C(S,A) \otimes\D(B,T)\\) & {\ref{def:adapter}} \\\

Lens \\((\mathbf{Optic}_{\times,\bullet})\\)

& \\(\C(S,A) \times\D(S \bulletB, T)\\) & {{\ref{def:lens}}} \\\

Monoidal lens \\((\mathbf{Optic}_{\otimes,_\U\times})\\)

& \\(\CCom(S,A) \times\C(\US \otimesB, T)\\) & {{\ref{def:myerslens}}} \\\

Algebraic lens \\((\mathbf{Optic}_{_\U\times,_\U\bullet})\\)

& \\(\C(S,A) \times\D(\PsiS \bulletB, T)\\) & {{\ref{def:algebraiclens}}} \\\

Monadic lens \\((\mathbf{Optic}_{\times,\rtimes})\\)

& \\(\W(S , A) \times\W(S \timesB , \PsiT)\\) & {{\ref{def:monadiclens}}} \\\

Linear lens \\((\mathbf{Optic}_{\otimes,\bullet})\\)

& \\(\C(S, \\{B, T\\} \bulletA)\\) & {{\ref{def:linearlens}}} \\\

Prism \\((\mathbf{Optic}_{\bullet,+})\\)

& \\(\C(S, T \bulletA) \times\D(B,T)\\) & {{\ref{def:prism}}} \\\

Coalg. prism \\((\mathbf{Optic}_{_\U\bullet,_\U+})\\)

& \\(\C(S, \ThetaT \bulletA) \times\D(B,T)\\) &
{{\ref{remark:coalgebraicprism}}} \\\

Grate \\((\mathbf{Optic}_{\\{\\},\bullet})\\)

& \\(\D(\\{S,A\\}\bulletB, T)\\) & {{\ref{def:grate}}} \\\

Glass \\((\mathbf{Optic}_{\times[],\times[]})\\)

& \\(\C(S \times[[S, A], B] , T)\\) & {{\ref{def:glass}}} \\\

Affine traversal \\((\mathbf{Optic}_{+\otimes,+\otimes})\\)

& \\(\C(S, T + A \otimes\\{B, T\\})\\) & {{\ref{def:affine}}} \\\

Traversal \\((\mathbf{Optic}_{\mathrm{Pw},\mathrm{Pw}})\\)

& \\(\V(S, \int\nolimits^n A^n \otimes[B^n, T])\\) & {{\ref{def:traversal}}}
\\\

Kaleidoscope \\((\mathbf{Optic}_{\mathrm{App},\mathrm{App}})\\)

& \\(\int\nolimits_n \V([A^n,B],[S^n, T])\\) & {{\ref{def:kaleidoscope}}} \\\

Setter \\((\mathbf{Optic}_{\mathrm{ev},\mathrm{ev}})\\)

& \\(\V([A,B],[S,T])\\) & {{\ref{def:setter}}} \\\

Fold \\((\mathbf{Optic}_{\mathrm{Foldable},\ast})\\)

& \\(\V(S, \mathcal{L} A)\\) & {{\ref{def:fold}}}

\end{tabular}

\end{figure}

\parThe purpose of an abstract unified definition is twofold: firstly, it
provides a framework to classify existing optics and explore new ones, as we
do in Section~\ref{sec:examples}; and secondly, it enables a unified
profunctor representation,

which we present in Section~\ref{sec:tambaratheory}.

\par\section{Examples of optics}\label{sec:examples}

\subsection{Lenses and prisms}

\parIn functional programming, \textbf{lenses} can be seen as accessors for a
particular subfield of a data structure. Lenses are given by two functions:
the \mintinline[breaklines]{haskell}{view} function that accesses the
subfield; and the \mintinline[breaklines]{haskell}{update} function that
overwrites its contents.

\begin{spec}

view :: s -> a

update :: s -> b -> t

\end{spec}

The definition of \emph{lens} has its origin in Oles’ thesis~\cite{oles82},
but this basic definition has been generalized in many different directions.
\emph{Monadic lenses}~\cite{AbouSaleh16} try to unify many of the already
proposed ways of combining lenses and monadic effects. Myers’ \emph{lenses in
a symmetric monoidal category}~\cite[\S2.2]{spivak19} are a different notion
that provides an analogue of the \mintinline[breaklines]{haskell}{view} and
\mintinline[breaklines]{haskell}{update} functions in arbitrary symmetric
monoidal categories. Riley also describes a notion of \emph{linear lenses}
with their laws in an arbitrary monoidal closed
category~\cite[\S4.8]{riley18}. Boisseau~\cite[\S5.2]{boisseau17} introduced
the \emph{achromatic lens} responding to the fact that sometimes lenses come
endowed with a \mintinline[breaklines]{haskell}{create} function along the
usual \mintinline[breaklines]{haskell}{view} and
\mintinline[breaklines]{haskell}{update}.

\parHowever, these generalizations are not mutually compatible in general.
They use the cartesian or monoidal structure to get the
\mintinline[breaklines]{haskell}{view} function in different ways. Many of
them include a monad at some point in the type signature, and then define a
particular variant of lens composition that takes that monad into account.
Some of them, such as \emph{monoidal lenses} or \emph{lenses in a symmetric
monoidal category} were not presented as \emph{optics}, and a profunctor
representation for them was not considered.

\parWe present two derivations of lenses as mixed optics that capture all of
the variants mentioned before and endow all of them with a unified profunctor
representation (Theorem~\ref{th:profrep}). The first derivation is based on
the cartesian structure. It generalizes the original one by
Milewski~\cite{milewski17} and allows us to show that Myers’ lenses
(Definition~\ref{def:myerslens}) and monadic lenses
(Definition~\ref{def:monadiclens}) are also particular cases of mixed optic.
The derivation can be then refined to also cover \emph{achromatic lenses} and
describe some new variants of optic with potential applications in functional
programming that were missing in the literature. The second derivation uses
the closed structure instead, and slightly generalizes Riley’s \emph{linear
lenses}~\cite[\S4.8]{riley18}.

\par\subsubsection{Lenses}

\parThe key ingredient for most variants of lenses is a cartesian monoidal
structure. Throughout this section, we take a cartesian closed category
\\((\mathcal{W}, \times,1)\\) as our base for enrichment. A monoidal
\Wt{category} \\((\C,\times,1)\\) is cartesian if there exist \Wt{natural}
isomorphisms \\(\C(Z,X \timesY) \cong\C(Z,X) \times\C(Z,Y)\\) and \\(\C(X,1)
\cong1\\).

\par\begin{definition}\label{def:lens}

Let \\(\C\\) be a cartesian \Wt{category} with a monoidal

\Wt{action} \\((\bullet) \colon\C\times\D\to\D\\) to an arbitrary
\Wt{category} \\(\D\\).

A \textbf{lens} is an element of

\\[\mathbf{Lens}((A, B), (S, T)) \coloneqq\C(S,A) \times\D(S \bulletB, T).

\\]

\end{definition}

\begin{proposition}

Lenses are mixed optics (as in Definition~\ref{def:optic}) for the actions of
the cartesian product

\\((\times) \colon\C\times\C\to\C\\) and \\((\bullet)
\colon\C\times\D\to\D\\).

That is, \\(\mathbf{Lens} \cong\Optic_{(\times,\bullet)}\\).

\end{proposition}

\begin{proof}

The product \\((\times) \colon\C^2 \to\C\\) is right adjoint to the diagonal
functor.

\begin{align*}

& \int^{C \in\C} \C(S,C \timesA) \times\D(C \bulletB, T) \\\

\cong& \qquad\mbox{(Product)} \\\

& \int^{C \in\C} \C(S , C) \times\C(S , A) \times\D(C \bulletB , T) \\\

\cong& \qquad\mbox{(coYoneda)} \\\

& \C(S , A) \times\D(S \bulletB , T). \qedhere\end{align*}

\end{proof}

\par\begin{remark}

The previous definition can be specialized to the pair \\(\C(S,A) \times\C(S
\timesB , T)\\) if we take \\(\C= \D\\) and we let \\((\bullet)\\) be the
cartesian product.

\end{remark}

\par\subsubsection{Lenses in a symmetric monoidal category}

\par\begin{definition}[{{\citealp[\S2.2]{spivak19}}}]\label{def:myerslens}

Let \\(\C\\) be a symmetric monoidal category, with \\(\CCom\\) its category
of cocommutative comonoids and \\(\U\colon\CCom\to\C\\) the forgetful functor.
Let \\(S,A \in\CCom\\) and \\(B,T \in\C\\). A \textbf{monoidal lens} is an
element of

\\[\mathbf{mLens}_{\otimes} ((A, B), (S,T)) \coloneqq\CCom(S,A) \times\C(\US
\otimesB, T).

\\]

\end{definition}

\par\begin{proposition}\label{prop:monoidallenses}

Monoidal lenses are a particular case of Definition~\ref{def:lens}.

\end{proposition}

\begin{proof}

The category of cocommutative comonoids \\(\CCom\\) over a category \\(\C\\)
can be given a cartesian structure in such a way that the forgetful functor
\\(\U\colon\CCom\to\C\\) is strict monoidal (see~\cite{fox76}, where a
stronger result is shown). The symmetric structure is needed to endow the
monoidal product of two comonoids with a canonical comonoid structure. We take
the action \\((\bullet)\\) in Definition~\ref{def:lens} to be given by \\(S
\bulletA \coloneqq\US \otimesA\\). That is,
\\(\mathbf{mLens}_\otimes\cong\Optic_{(\otimes, _\U\otimes)}\\).

\end{proof}

\par\subsubsection{Monadic lenses}

\parMonadic lenses~\cite{AbouSaleh16} were proposed for combining lenses with
monadic effects. Their \hask{update} function can be partial or non-
deterministic, and they can account for side effects.

\par\begin{figure}[h]

\centering\begin{examplecode}

box :: (Show b) => MonadicLens Log a b (Box a) (Box b)

\parreturn (Box 42)

>>= mupdate box ”hello”

>>= mupdate box ”world”

\par>>> [box]: contents changed to ”hello”.

>>> [box]: contents changed to ”world”.

>>> Box{”world”}

\end{examplecode}

\caption{A polymorphic family of type-changing monadic lenses for a logging
monad (\hask{Log}) is used to track each time a data holder (\hask{Box}) is
accessed.}\label{fig:exampleBox}

\end{figure}

\par\par\begin{definition}[{{\citealp[\S2.3]{AbouSaleh16}}}]\label{def:monadiclens}

Let \\(\Psi\colon\W\to\W\\) be a \Wt{monad}. A \textbf{monadic lens} for
\\(\Psi\\) is an element of

\\[\mathbf{MndLens}_\Psi((A, B), (S, T)) \coloneqq\W(S , A) \times\W(S \timesB
, \PsiT).\\]

\end{definition}

\par\begin{proposition}\label{prop:monadiclens}

Monadic lenses are a particular case of Definition~\ref{def:lens}.

\end{proposition}

\begin{proof}

First, note that every \Wt{endofunctor} is \textit{strong}. Thus, the
\Wt{monad} \\(\Psi\\) comes with a \Wt{natural} family \\(\theta_{X,Y} \colonX
\times\Psi(Y) \to\Psi(X \timesY)\\). This induces a \Wt{action} \\((\rtimes)
\colon\W\times\operatorname{Kl}(\Psi) \to\operatorname{Kl}(\Psi)\\) defined as
the composite

\\[\begin{tikzcd}[row sep=tiny]

\W(A,\PsiB) \times\W(X,Y) \rar{(\times)} &

\W(X \timesA, Y \times\PsiB) \\\

\phantom{\W(X \timesA, Y \times\PsiB)} \rar{\theta} &

\W(X \timesA, \Psi(Y \timesB)).

\end{tikzcd}\\]

We can note that \\(\operatorname{Kl}_\Psi(S \rtimesB,T) \coloneqq\W(S
\timesB, \PsiT)\\).

Monadic lenses can be rewritten as lenses (as in Definition~\ref{def:lens})
where the action \\((\bullet)\\) is given by \\((\rtimes)
\colon\C\times\operatorname{Kl}(\Psi) \to\operatorname{Kl}(\Psi)\\). That is,
\\(\mathbf{MndLens}_\Psi\cong\Optic_{(\times,\rtimes)}\\).

\end{proof}

\par\begin{remark}

This technique is similar to the one used by Riley to describe a non-mixed
variant called \emph{effectful lenses}~\cite[\S4.9]{riley18}.

\end{remark}

\par\subsubsection{Lenses with algebraic context}

\parWe can further generalize Definition~\ref{def:lens} if we allow the
\textit{context} over which we take the coend to be an algebra for a fixed
monad. The motivation is that lenses with a context like this appear to have
direct applications in programming; for instance, Boisseau’s
\textit{achromatic lens}~\cite[\S5.2]{boisseau17} is a particular case of this
definition. These \textit{algebraic lenses} should not be confused with the
previous \textit{monadic lenses} in Definition~\ref{def:monadiclens}.

\par\begin{definition}\label{def:algebraiclens}

Let \\(\Psi\colon\C\to\C\\) be a \Wt{monad} in a cartesian \Wt{category}
\\(\C\\). Let \\((\bullet) \colon\C\times\D\to\D\\) be a monoidal \Wt{action}
to an arbitrary \Wt{category} \\(\D\\). An \textbf{algebraic lens} is an
element of

\\[\mathbf{Lens}_\Psi((A,B), (S,T))

\coloneqq\C(S, A) \times\D(\PsiS \bulletB, T).

\\]

\end{definition}

\par\begin{proposition}

Algebraic lenses are mixed optics (as in Definition~\ref{def:optic}) for the
actions of the product by the carrier of an algebra \\((_\U\times)
\colon\EM_\Psi\times\C\to\C\\) and \\((_\U\bullet)
\colon\EM_\Psi\times\D\to\D\\). That is,
\\(\mathbf{Lens}_\Psi\cong\Optic_{(_\U\times, _\U\bullet)}\\).

\end{proposition}

\par\begin{proof}

Products in \\(\C\\) induce products in the \Wt{category} of algebras
\\(\EM_\Psi\\) which are preserved by the forgetful functor
\\(\U\colon\EM_\Psi\to\C\\). Thus, the \Wt{category} of algebras is cartesian,
making the forgetful functor monoidal. The functor \\((_\U\times)
\colon\EM_\Psi\times\C\to\C\\), defined by \\(C {_\U\times} A \coloneqq\UC
\timesA\\), is a strong monoidal action.

\begin{align*}

& \int^{C \in\mathbf{\EM_\Psi}}

\C(S, \UC \timesA) \times\D(\UC \bulletB, T) \\\

\cong& \quad\mbox{(Product)} \\\

& \int^{C \in\mathbf{\EM_\Psi}}

\C(S, \UC) \times\C(S, A) \times\D(\UC \bulletB, T) \\\

\cong& \quad\mbox{(Free-forgetful adjunction)} \\\

& \int^{C \in\mathbf{\EM_\Psi}}

\EM_\Psi(\PsiS, C) \times\C(S, A) \times\D(\UC \bulletB, T) \\\

\cong& \quad\mbox{(coYoneda)} \\\

& \C(S, A) \times\D(\PsiS \bulletB, T). \qedhere\end{align*}

\end{proof}

\begin{remark}

Algebraic lenses are a new optic. Let \\(\D= \C\\) and let \\((\bullet)\\) be
the cartesian product. An algebraic lens is given by the usual
\mintinline[breaklines]{haskell}{view} function that accesses the subfield,
and a variant of the \mintinline[breaklines]{haskell}{update} function that
takes an element inside a monad.

\begin{spec}

view :: s -> a

algUpdate :: m s -> b -> t

\end{spec}

\end{remark}

\begin{remark}

In particular, the case where \\(\Psi\\) is the \textit{list monad}
\\(\mathcal{L} \colon\V\to\V\\) defines a new optic, which we dub a
\textbf{classifying lens}. We propose to use them as lenses that can also be
trained to classify a new focus into a complete data structure, as in
Figure~\ref{fig:exampleIris}.

\begin{figure}[H]

\centering\begin{examplecode}

let iris =

[ Iris Setosa 4.9 3.0 1.4, 0.2

, Iris Setosa 4.7 3.2 1.3 0.2

, …

, Iris Virginica 5.9 3.0 5.1 1.8 ]

\parmeasure :: AlgLens [] Measurements Flower

\pariris!!4 ^. measure

>>> (5.0, 3.6, 1.4, 0.2)

\pariris & measure .? Measurements (4.8, 3.2, 3.5, 2.1)

>>> Iris Versicolor (4.8, 3.1, 1.5, 0.1)

\end{examplecode}

\caption{A classifying lens (\hask{measure}) is used both for accessing a the
measurements of a point in the \hask{iris} dataset and to classify new
measurements into a species (\hask{Versicolor}).}\label{fig:exampleIris}

\end{figure}

\parThey are given by two functions, the usual
\mintinline[breaklines]{haskell}{view} function that accesses the focus, and a
\mintinline[breaklines]{haskell}{classify} function that takes a list of
examples together with some piece of data and produces a new example.

\begin{spec}

view :: s -> a

classify :: [s] -> b -> t

\end{spec}

\end{remark}

\par\par\begin{remark}\label{def:achromatic}\label{def:apochromatic}

The case in which \\(\Psi\\) is the \textit{maybe monad} \\(\mathcal{M}
\colon\V\to\V\\) was studied by Boisseau~\cite[\S5.2]{boisseau17} and is known
as the \textbf{achromatic lens}. It is motivated by the fact that, sometimes
in practice, lenses come naturally equipped with a
\mintinline[breaklines]{haskell}{create} function~\cite[\S3]{foster05} along
the usual \mintinline[breaklines]{haskell}{view} and
\mintinline[breaklines]{haskell}{update}.

\begin{spec}

view :: s -> a

update :: s -> b -> t

create :: b -> t

\end{spec}

For this implementation, we note that

\\[\C(S,A) \times\C(\mathcal{M} S \timesB,T) \cong\C(S,A) \times\C(S\timesB,T)
\times\C(B,T).\\]

\end{remark}

\par\begin{remark}

What Riley~\cite[\S4.10]{riley18} calls \textit{achromatic lens},

\\[\C(S,\\{B,T\\}+1) \times\C(S,A) \times\C(B,T),\\]

is actually the optic for the action \\(\odot\colon\C\to[\C,\C]\\) defined by
\\(M \odotA \coloneqq(M + 1) \timesA\\). Perhaps confusingly, this is not
equivalent to Boisseau’s \emph{achromatic lens}, which is the optic for the
action \\((\times) \colon\textrm{\\(\mathcal{M}\\)-Alg} \to[\C,\C]\\) of the
product by pointed objects.

In order to amend this clash of terminology, we call this second optic the
\textbf{apochromatic lens}. It can be implemented by a
\mintinline[breaklines]{haskell}{view} and
\mintinline[breaklines]{haskell}{create} functions, together this time with a
\mintinline[breaklines]{haskell}{maybeUpdate} that is allowed to fail.

\begin{spec}

view :: s -> a

maybeUpdate :: s -> Maybe (b -> t)

create :: b -> t

\end{spec}

\end{remark}

\par\subsubsection{Lenses in a closed category}

\parLinear lenses (as described by Riley~\cite[\S4.8]{riley18}) are a
different generalization of lenses that relies on a closed monoidal structure.
Its advantage is that we do not need to require our enriching category to be
cartesian anymore.

\par\begin{definition}[{{\citealp[\S4.8]{riley18}}}]\label{def:linearlens}

Let \\((\D, \otimes, \\{\\} )\\) be a right closed \Vt{category} with a
monoidal \Vt{action} \\((\bullet) \colon\D\otimes\C\to\C\\) to an arbitrary
\Vt{category} \\(\C\\). A \textbf{linear lens} is an element of

\\[

\mathbf{Lens}_{\\{\\}} ((A, B), (S, T)) \coloneqq\C(S, \\{B , T\\} \bulletA).

\\]

\end{definition}

\par\begin{proposition}

Linear lenses are mixed optics (as in Definition~\ref{def:optic}) for the
actions of the monoidal product \\((\otimes) \colon\D\times\D\to\D\\) and
\\((\bullet) \colon\D\times\C\to\C\\). That is, \\(\Lens_{\\{\\}}
\cong\Optic_{\otimes,\bullet}\\)

\end{proposition}

\begin{proof}

The monoidal product has a right adjoint given by the exponential.

\begin{align*}

& \int^{D \in\D} \C(S,D \bulletA) \otimes\D(D \otimesB, T) \\\

\cong& \qquad\mbox{(Closedness)} \\\

& \int^{D \in\D} \C(S , D \bulletA) \otimes\D(D , \\{B , T\\}) \\\

\cong& \qquad\mbox{(coYoneda)} \\\

& \C(S , \\{B , T\\} \bulletA). \qedhere\end{align*}

\par\end{proof}

\par\subsubsection{Prisms}

\parIn functional programming, \textbf{prisms} pattern match on data
structures, allowing for failure. They are given by a \hask{match} function
that tries to access the matched structure and a \hask{build} function that
constructs an abstract type from one of its alternatives.

\begin{spec}

match :: s -> Either t a

build :: b -> t

\end{spec}

Prisms happen to be lenses in the opposite category. However, they can also be
described as optics in the original category for a different pair of actions.
We will provide a derivation of prisms that is dual to our derivation of
lenses for a cartesian structure. This derivation spcializes to the pair
\\(\C(S,T+A) \times\C(B,T)\\).

\par\begin{definition}\label{def:prism}

Let \\(\D\\) be a cocartesian \Wt{category} with a monoidal \Wt{action}
\\((\bullet) \colon\D\times\C\to\C\\) to an arbitrary category \\(\C\\). A
\textbf{prism} is an element of

\\[\mathbf{Prism}((A, B), (S,T)) \coloneqq\C(S , T \bulletA) \times\D(B , T).

\\]

In other words, a prism from \\((S,T)\\) to \\((A,B)\\) is a lens from
\\((T,S)\\) to \\((B,A)\\) in the opposite categories \\(\D^{op}\\) and
\\(\C^{op}\\). However, they can also be seen as optics from \\((A,B)\\) to
\\((S,T)\\).

\end{definition}

\par\begin{proposition}

Prisms are mixed optics (as in Definition~\ref{def:optic}) for the actions of
the coproduct \\((+) \colon\D\times\D\to\D\\) and \\((\bullet)
\colon\C\times\D\to\D\\). That is, \\(\mathbf{Prism}
\cong\Optic_{(\bullet,+)}\\).

\end{proposition}

\begin{proof}

The coproduct \\((+) \colon\C^2 \to\C\\) is left adjoint to the diagonal
functor.

\begin{align*}

& \int^{D \in\D} \C(S,D \bulletA) \times\D(D + B, T) \\\

\cong& \qquad\mbox{(Coproduct)} \\\

& \int^{D \in\D} \C(S , D \bulletA) \times\D(D , T) \times\D(B , T) \\\

\cong& \qquad\mbox{(coYoneda)} \\\

& \C(S , T \bulletA) \times\D(B , T). \qedhere\end{align*}

\end{proof}

\par\begin{remark}[Prisms in a symmetric monoidal category]

Let \\(\C\\) be a symmetric monoidal (plain) category. Its category of
commutative monoids, \\(\CMon\\), can be given a cocartesian structure in such
a way that the forgetful functor \\(\U\colon\CMon\to\C\\) is strict monoidal.
A \textbf{monoidal prism} is an element of

\\[\mathbf{mPrism}((A, B), (S, T)) \coloneqq\C(S,\UT \otimesA)
\times\CMon(B,T).\\]

\end{remark}

\par\begin{remark}[Prisms with coalgebraic
context]\label{remark:coalgebraicprism}

Let \\(\Theta\\) be a \Wt{comonad} in a cocartesian \Wt{category} \\(\D\\).
Let \\((\bullet) \colon\D\times\C\to\C\\) be a monoidal action to an arbitrary
\Wt{category} \\(\C\\). Coproducts in \\(D\\) induce coproducts in the
category of coalgebras \\(\EM_\Theta\\) which are preserved by the forgetful
\Wt{functor} \\(\U\colon\EM_\Theta\to\D\\). A \textbf{coalgebraic prism} is an
element of

\\[\mathbf{Prism}_\Theta((A, B), (S, T))

\coloneqq\C(S, \ThetaT \bulletA) \times\D(B, T).\\]

The coalgebraic variant for a comonad \mintinline[breaklines]{haskell}{(c)} is
given by a \mintinline[breaklines]{haskell}{cMatch} function, that captures
the failure into a comonad, and the usual
\mintinline[breaklines]{haskell}{build} function.

\begin{spec}

cMatch :: s -> Either (c t) a

build :: b -> t

\end{spec}

\end{remark}

\par\par\subsection{Traversals}

\parIn functional programming, \textbf{traversals} extract the elements of a
container into an ordered list, allowing us to iterate over the elements
without altering the container (Figure~\ref{fig:exampleTraversal}).

\par\begin{figure}[H]

\centering\begin{examplecode}

let mail =

[ ”43 Adlington Rd, Wilmslow, United Kingdom”

, ”26 Westcott Rd, Princeton, USA”

, ”St James’s Square, London, United Kingdom”

]

\pareach :: Traversal String [String]

address :: Prism Address String

city :: Lens String Address

\par>>> mail & each.address.city [ ”43 Adlington Rd, WILMSLOW, United Kingdom”

, ”26 Westcott Rd, PRINCETON, USA”

, ”St James’s Square, LONDON, United Kingdom”

]

\end{examplecode}

\par\par\caption{The composition of a traversal (\hask{each}) with a prism
(\hask{address}) and a lens (\hask{city}) is used to parse a collection of
strings and modify one of their subfields.}\label{fig:exampleTraversal}

\end{figure}

\parTraversals are constructed from a single \hask{extract} function that both
outputs the elements and takes a new list to update them.

\begin{spec}

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

\end{spec}

Usually, we ask the length of the input to the function of type \hask{[b] ->
t} to be the same as the length of \hask{[a]}. This restriction can be also
encoded into the type when dependent types are available.

\par\begin{definition}\label{def:traversal}

A \textbf{traversal} is an element of

\\[\mathbf{Traversal}((A, B), (S, T)) \coloneqq\V\left(S , \int^{n
\in\mathbb{N}} A^n \otimes[B^n, T] \right).

\\]

\end{definition}

\par\begin{remark}

Let \\((\mathbb{N},+)\\) be the free strict monoidal category on one object.
Ends and coends indexed by \\(\mathbb{N}\\) coincide with products and
coproducts, respectively. Here \\(A^{(-)} \colon\mathbb{N} \to\C\\) is the
unique monoidal \Vt{functor} sending the generator of \\(\mathbb{N}\\) to \\(A
\in\C\\). Each functor \\(C \colon\mathbb{N} \to\V\\) induces a \textit{power
series} \\[\operatorname{Pw}_C(A) = \int\nolimits^{n \in\mathbb{N}} A^n
\otimesC_{n}.\\]

This defines an action \\(\operatorname{Pw} \colon[\mathbb{N}, \C]
\to[\C,\C]\\) sending the indexed family to its power series (see
Remark~\ref{remark:series}). We propose a derivation of the \emph{traversal}
as the optic for power series.

\end{remark}

\par\begin{proposition}\label{prop:traversal}

Traversals are optics (as in Definition~\ref{def:optic}) for power series.

That is, \\(\mathbf{Traversal}
\cong\Optic_{\operatorname{Pw},\operatorname{Pw}}\\).

\end{proposition}

\begin{proof}

The derivation generalizes that of linear lenses
(Definition~\ref{def:linearlens}).

\par\noindent\resizebox{\linewidth}{!}{

\begin{minipage}{\linewidth}

\begin{align*}

& \int^{C \in[ \mathbb{N} , \V]}

\V\left(S , \int^{n \in\mathbb{N}} C_n \otimesA^n \right)
\otimes\V\left(\int^{n \in\mathbb{N}} C_n \otimesB^n , T\right) \\\

\cong&\qquad\mbox{{(Continuity)}}\\\

& \int^{C \in[ \mathbb{N} , \V]} \V\left(S , \int^{n \in\mathbb{N}} C_n
\otimesA^n \right) \otimes\int_{n \in\mathbb{N}} \V\left( C_n \otimesB^n ,
T\right) \\\

\cong& \qquad\mbox{{(Currying)}}\\\

& \int^{C \in[ \mathbb{N} , \V]} \V\left(S , \int^{n \in\mathbb{N}} C_n
\otimesA^n \right) \otimes\int_{n \in\mathbb{N}} \V\left( C_n , [B^n ,
T]\right) \\\

\cong& \qquad\mbox{{(Natural transformation as an end)}}\\\

& \int^{C \in[ \mathbb{N} , \V]} \V\left(S , \int^{n \in\mathbb{N}} C_n
\otimesA^n \right) \otimes[ \mathbb{N} , \V] \left(C_{(-)} , [B^{(-)} ,
T]\right) \\\

\cong& \qquad\mbox{{(coYoneda)}}\\\

& \V\left(S , \int^{n \in\mathbb{N}} A^n \otimes[B^n, T] \right).
\qedhere\end{align*}

\end{minipage}}

\end{proof}

\parThe derivation from the general definition of optic to the concrete
description of lenses and prisms in functional programming was first described
by Milewski~\cite{milewski17}, but finding a derivation of traversals like the
one presented here, fitting the same elementary pattern as lenses or prisms,
was left as an open problem. It should be noted, however, that derivations of
the traversal as the optic for a certain kind of functor called
\textbf{Traversables} (which should not be confused with traversals
themselves) have been previously described by Boisseau and
Gibbons~\cite{boisseau18} and Riley~\cite{riley18}. For a derivation using
Yoneda, Riley~\cite{riley18} recalls a parameterised adjunction that has an
equational proof in the work of Jaskelioff and O’Connor~\cite{jaskelioff15}.
These two derivations do not contradict each other: two different classes of
functors can generate the same optic, for instance, if the adjunction
describing both of them gives rise to the same monad. This seems to be the
case here: traversables are coalgebras for a comonad and power series are the
cofree coalgebras for the same comonad~\cite[\S4.2]{roman19}.

\parIn the \\(\mathbf{Sets}\mbox{-based}\\) case, the relation between
traversable functors, applicative functors~\cite{mcbride08} and these power
series functors has been studied by Jaskelioff and
Rypacek~\cite{jaskelioff15}.

\begin{remark}\label{remark:series}

The \Vt{functor} \\(\operatorname{Pw} \colon[\mathbb{N},\V] \to[\V,\V]\\) is
actually a strong monoidal action thanks to the fact that two power series
functors compose into a power series functor.

\begin{align*}

&\int^{m \in\mathbb{N}} \left( \int^{n \in\mathbb{N}} A^n \otimesC_n \right)^m
\otimesD_m \\\

\cong& \quad\mbox{(Product distributes over colimits)} \\\

&\int^{m} \int^{n_1,\dots,n_m} A^{n_1} \otimes\dots\otimesA^{n_m}

\otimesC_{n_1} \otimes\dots\otimesC_{n_m} \otimesD_m \\\

\cong& \quad\mbox{(Rearranging terms)} \\\

&\int^{k \in\mathbb{N}} A^k \otimes\left( \sum_{n_1 + \dots+ n_m = k}

C_{n_1} \otimes\dots\otimesC_{n_m} \otimesD_m \right).

\end{align*}

We are then considering an implicit non-symmetric monoidal structure where the
monoidal product \\((\bullet) \colon[\mathbb{N},\V] \otimes[\mathbb{N},\V]
\to[\mathbb{N},\V]\\) of \\(C_n\\) and \\(D_n\\) can be written as

\\[\int^{m} \int^{n_1,\dots, n_m}

\mathbb{N}(n_1 + \dots+ n_m, k) \otimesC_{n_1} \otimes\dots\otimesC_{n_m}
\otimesD_m.

\\]

This is precisely the structure described by Kelly~\cite[\S8]{kelly05} for the
study of non-symmetric operads. A similar monoidal structure is described
there when we substitute \\(\mathbb{N}\\) by \\((\mathbb{P},+)\\), the
\Vt{\textit{category of permutations}} defined as the free strict symmetric
monoidal category on one object. The same derivation can be repeated with this
new structure to obtain an optic similar to the traversal and given by

\\[\V\left(S , \int^{n \in\mathbb{P}} A^n \otimes[B^n, T] \right).\\]

\end{remark}

\par\subsubsection{Affine traversals}

\par\emph{Affine traversals} strictly generalize prisms and linear lenses in
the non-mixed case allowing a \textit{lens-like} accessing pattern to fail;
they are used to give a concrete representation of the composition between a
lens and a prism. An affine traversal is implemented by a single \hask{access}
function.

\begin{spec}

access :: s -> Either t (a , b -> t)

\end{spec}

\par\par\begin{definition}\label{def:affine}

Let \\(\W\\) be cartesian closed and let \\(\C\\) be a symmetric monoidal
closed \Wt{category} that is also cocartesian. An \textbf{affine traversal} is
an element of

\\[\mathbf{Affine}_{\otimes}\left( (A, B), (S, T) \right)

:= \mathbf{C}(S , T + A \otimes\\{B,T\\}).\\]

\end{definition}

\par\begin{proposition}

Affine traversals are optics (as in Definition~\ref{def:lens}) for the action
\\((+\otimes) \colon\C^2 \to[\C,\C]\\) that sends \\(C, D \in\C\\) to the
functor \\(C + D \otimes(-)\\). That is, \\(\mathbf{Affine}_{\otimes}
\cong\Optic_{(+\otimes),(+\otimes)}\\).

\end{proposition}

\begin{proof}

The action uses that monoidal product distributes over the coproduct.

\begin{align*}

& \int^{C,D} \C(S , C + D \otimesA) \times\C(C + D \otimesB, T) \\\

\cong& \qquad\mbox{{(Coproduct)}} \\\

& \int^{C,D} \C(S , C + D \otimesA) \times\C(C , T) \times\C(D \otimesB, T)
\\\

\cong& \qquad\mbox{{(coYoneda, Exponential)}} \\\

& \int^D \C(S , T + D \otimesA) \times\C(D , \\{B, T\\}) \\\

\cong& \qquad\mbox{{(coYoneda)}} \\\

& \C(S , T + A \otimes\\{B,T\\}). \qedhere\end{align*}

\end{proof}

\par\subsubsection{Kaleidoscopes}

\par\emph{Applicative} functors are commonly considered in functional
programming as they provide a convenient generalization to monads with better
properties for composition. It is a natural then to ask what is the optic
associated to applicative functors. Applicative functors in \\([\V,\V]\\) are
monoids with respect to Day convolution \\((\ast) \colon[\V,\V] \times[\V,\V]
\to[\V,\V]\\), defined as the following coend

\\[

(F \astG)(A) = \int^{X,Y \in\V} \V(X \otimesY, A) \otimesFX \otimesGY.

\\]

Applicative functors form a \Vt{category} of monoids \\(\App\\).
Alternatively, they are lax monoidal \Vt{functors} for the cartesian
structure. It is a basic result in category theory~\cite[\SVII, Theorem
2]{maclane78} that, as the category \\([\V,\V]\\) has denumerable colimits and
Day convolution distributes over them, the free applicative functor can be
computed as \\(I + F + F^{\ast2} + F^{\ast3} + \dots\\).

\par\begin{definition}\label{def:kaleidoscope}

A \textbf{kaleidoscope} is an element of

\\[\mathbf{Kaleidoscope}\left((A, B), (S, T)\right) :=

\prod_{n \in\mathbb{N}} \V\left([A^n, B] , [S^n, T] \right).

\\]

\end{definition}

\par\begin{proposition}

Kaleidoscopes are optics for the action of applicative functors.

\end{proposition}

\begin{proof}

Let \\(\U\colon\App\to[\V,\V]\\) be the forgetful functor from the category of
applicatives.

\begin{align*}

& \int^{F \in\App} \V(S, \UFA) \otimes\V(\UFB,T)

\\\ \cong& \qquad\mbox{{(Yoneda)}} \\\

& \int^{F \in\App} \V\left(S, \int_{C \in\V} [[A,C],\UFC] \right)
\otimes\V(\UFB,T)

\\\ \cong& \qquad\mbox{(Continuity)}\\\

& \int^{F \in\App} \int_{C} \V\left(S, [[A,C],\UFC] \right) \otimes\V(\UFB,T)

\\\ \cong& \qquad\mbox{(Exponential)}\\\

& \int^{F \in\App} \left( \int_{C} \V\left([A,C] \otimesS, \UFC \right)
\right) \otimes\V(\UFB,T)

\\\ \cong& \qquad\mbox{(Natural transformations as ends)}\\\

& \int^{F \in\App} \mathrm{Nat}\left([A,-] \otimesS, \UF \right)
\otimes\V(\UFB,T)

\\\ \cong& \qquad\mbox{(Free applicative)} \\\

& \int^{F \in\App} \App\left(\sum_{n\in\mathbb{N}} [A^n , -] \otimesS , F
\right) \otimes\V(\UFB,T)

\\\ \cong& \qquad\mbox{(coYoneda)} \\\

& \V\left(\sum_{n \in\mathbb{N}} S^n \otimes[A^n , B],T \right)

\\\ \cong& \qquad\mbox{(Continuity and exponential)} \\\

& \prod_{n \in\mathbb{N}} \V\left([A^n , B], [S^n, T] \right).
\qedhere\end{align*}

\end{proof}

\par\begin{remark}

The free applicative we construct here is known in Haskell

programming as the \hask{FunList} applicative. In

the same way that traversables are written in terms of lists, we can

approximate Kaleidoscopes as a single function

\hask{aggregate} that

takes a folding for the foci and outputs a folding for the complete

data structure. Kaleidoscopes are a new optic, and we propose to

use them as accessors for pointwise foldable data structures.

\begin{spec}

aggregate :: ([a] -> b) -> ([s] -> t)

\end{spec}

\end{remark}

\parKaleidoscopes pose a problem on the side of applications: they cannot be
composed with lenses to produce new kaleidoscopes. This is caused by the fact
that the constraint defining them (\mintinline{haskell}{Applicative}) is not a
superclass of the constraint defining lenses: a functor given by a product is
not applicative, in general. However, a functor given by a product \emph{by a
monoid} is applicative. This means that applicatives can be composed with
lenses whose residual is a monoid (Definition~\ref{def:algebraiclens}).

\begin{figure}[H]

\centering\begin{examplecode}

measure :: AlgebraicLens [] Measurements Flower

aggregate :: Kaleidoscope Float Measurements

\pariris & measure.aggregate >- mean

>>> Iris Versicolor; Sepal (5.843, 3.054); Petal (3.758, 1.198)

\end{examplecode}

\caption{Following the previous Example~\ref{fig:exampleIris}, a kaleidoscope
(\hask{aggregate}) is composed with an algebraic lens to create a new point on
the dataset by aggregating measurements with some function (\hask{mean},
\hask{maximum}) and then classifying it.}\label{fig:exampleKaleidoscope}

\end{figure}

\par\subsection{Grates}

\subsubsection{Grates}

\par\emph{Grates} create a new structure provided a way of creating a new
focus from a view function. They are given by a single \hask{grate} function
with the form of a nested continuation.

\begin{spec}

grate :: ((s -> a) -> b) -> t

\end{spec}

\par\begin{definition}\label{def:grate}

Let \\(\C\\) be a symmetric monoidal closed \Vt{category}. Let \\((\bullet)
\colon\C\times\D\to\D\\) be an arbitrary action. A \textbf{grate} is an
element of

\\[\mathbf{Grate}\left((A, B), (S, T)\right) := \D(\\{S,A\\}\bulletB, T).\\]

\end{definition}

\begin{proposition}

Grates are mixed optics for the action of the exponential and \\((\bullet)
\colon\C\times\D\to\D\\). That is, \\(\mathbf{Grate}
\cong\Optic_{\\{\\},\bullet}\\).

\end{proposition}

\begin{proof}

The exponential is right adjoint to the monoidal product.

\begin{align*}

& \int^{C \in\C} \C(S,\\{C,A\\}) \otimes\D(C \bulletB, T) \\\

\cong& \qquad\mbox{(Exponential)} \\\

& \int^{C \in\C} \C(S \otimesC, A) \otimes\D(C \bulletB, T) \\\

\cong& \qquad\mbox{(Exponential)} \\\

& \int^{C \in\C} \C(C,\\{S, A\\}) \otimes\D(C \bulletB, T) \\\

\cong& \qquad\mbox{(coYoneda)} \\\

& \D(\\{S, A\\} \bulletB, T) \qedhere\end{align*}

\end{proof}

\parThe description of a grate and its profunctor representation in terms of
“closed” profunctors was first reported by Deikun and
O’Connor~\cite{deikun15}; it can be seen as a consequence of the profunctor
representation theorem (Theorem~\ref{th:profrep}).

\par\subsubsection{Glasses}

\par\emph{Glasses} are a new optic that strictly generalizes grates and lenses
for the cartesian case. In functional programming, glasses can be implemented
by a single function \hask{glass} that takes a way of transforming
\emph{views} into new foci and uses it to update the data structure. We
propose to use them as a the concrete representation of the composition of
lenses and grates.

\begin{spec}

glass :: ((s -> a) -> b) -> (s -> t)

\end{spec}

\par\begin{definition}\label{def:glass}

Let \\(\W\\) be a cartesian Bénabou cosmos and let \\(\C\\) be a cartesian
closed \Wt{category}. A \textbf{glass} is an element of

\\[\mathbf{Glass} \left( (A, B), (S, T) \right) := \C(S \times[[S, A], B] ,
T).

\\]

\end{definition}

\par\begin{proposition}

Glasses are optics for the action \\((\times[]) \colon\C^{op}
\times\C\to[\C,\C]\\) that sends \\(C, D \in\C\\) to the

\Wt{functor} \\(D \times[C,-]\\).

\end{proposition}

\begin{proof}

\begin{align*}

& \int^{C,D} \C(S, C \times[D,A]) \times\C([D,B] \timesC , T) \\\

\cong& \qquad\mbox{{(Product)}} \\\

& \int^{C,D} \C(S, C) \times\C(S, [D,A]) \times\C([D,B] \timesC , T) \\\

\cong& \qquad\mbox{{(coYoneda)}}\\\

& \int^D \C(S, [D, A]) \times\C([D,B] \timesS, T) \\\

\cong& \qquad\mbox{{(Exponential)}}\\\

& \int^D \C(D, [S , A]) \times\C([D, B] \timesS, T) \\\

\cong& \qquad\mbox{{(coYoneda)}}\\\

& \C([[S,A], B] \timesS , T). \qedhere\end{align*}

\end{proof}

\par\par\subsection{Getters, reviews and folds}

\parSome constructions, such as plain morphisms, are regarded as corner cases
of optics in the \emph{lens} library. We will describe these constructions
(\emph{getters}, \emph{reviews} and \emph{folds}~\cite{kmett15}) as mixed
optics. All of them set one of the two base categories to be the terminal
category and, contrary to most optics, they act only unidirectionally. In some
sense, they are degenerate cases of the definition of mixed optic.

\par\begin{definition}\label{def:getter}\label{def:review}

Let \\(\C\\) be an arbitrary \Vt{category}. \textbf{Getters} are degenerate
optics for the

trivial action on the covariant side. \textbf{Reviews}

are degenerate optics for the trivial action on the contravariant side.

\begin{align*}

\mathbf{Getter}((A,\ast),(S,\ast)) = \C(S, A). \\\

\mathbf{Review}((\ast,B),(\ast,T)) = \C(B, T).

\end{align*}

In other words, we fix the case where \\(\M= \mathbf{1}\\) and \\(\D=
\mathbf{1}\\) or \\(\C= \mathbf{1}\\), respectively.

\end{definition}

\parThe category of \textbf{foldable} functors is the slice category on the
list functor \\(\mathcal{L} \colon\V\to\V\\), also known as the free monoid
functor. Using the fact that \\(\mathcal{L}\\) is a monad, the slice category
can be made monoidal in such a way that the forgetful \\([\V,\V]/\mathcal{L}
\to[\V,\V]\\) becomes strong monoidal.

\par\begin{definition}\label{def:fold}

\textbf{Folds} are degenerate optics for the action of foldable functors.

\\[\mathbf{Fold}((A,\ast), (S,\ast)) = \int^{F \in\mathbf{Foldable} } \V(S , F
A).\\]

\end{definition}

\parFolds admit a concrete description that we can reach by eliminating the
coend. From the definition of coend as colimits, a coend from a diagram
category with a terminal object is determined by the value at the terminal
object.

\\[

\int^{F \in\mathbf{Foldable} } \V(S , F A) \cong\V(S, \mathcal{L} A).

\\]

\par\begin{remark}

The same technique can be used to prove that the optic for the

slice category over a monad \\(\mathcal{G} \colon\V\to\V\\) has a concrete
form

given by \\(\C(S, \mathcal{G}A)\\).

\end{remark}

\par\begin{remark}

We obtain the usual implementations of getters as
\mintinline[breaklines]{haskell}{s -> a}, of reviews as
\mintinline[breaklines]{haskell}{b -> t} and of folds as
\mintinline[breaklines]{haskell}{s -> [a]}. Their profunctor representation
degenerates into a covariant or contravariant \emph{functor representation},
which can be seen as a more direct application of the Yoneda lemma.

\end{remark}

\par\subsection{Setters and adapters}

\par\begin{definition}\label{def:setter}

A \textbf{setter}~\cite{kmett15} is an element of

\\[\mathbf{Setter} ((A, B), (S, T)) \coloneqq\V([A,B], [S,T]).\\]

\end{definition}

\begin{proposition}

Setters are optics for the evaluation of any endofunctor \\(\mathrm{ev}
\colon[\V, \V] \to[\V, \V]\\). That is, \\(\mathbf{Setter}
\cong\Optic_{\mathrm{ev},\mathrm{ev}}\\).

\end{proposition}

\begin{proof}

The concrete derivation described by Riley~\cite[\S4.5.2]{riley18} and his
requirement for strength can be transferred directly to the enriched case.

\begin{align*}

& \int^{F \in[ \V, \V]} \V(S, FA) \otimes\V(FB,T) \\\

\cong& \qquad\mbox{{(Yoneda)}} \\\

& \int^{F \in[ \V, \V]} \left( \int_{C \in\V} [\V(A,C), \V(S, FC)] \right)
\otimes\V(FB,T) \\\

\cong& \qquad\mbox{{(Exponential)}} \\\

& \int^{F \in[ \V, \V]} \left( \int_{C \in\V} \V(S \otimes[A,C], FC) \right)
\otimes\V(FB,T) \\\

\cong& \qquad\mbox{{(Natural transformation as an end)}} \\\

& \int^{F \in[ \V, \V]} [\V,\V](S \otimes[A,-], F) \otimes\V(FB,T) \\\

\cong& \qquad\mbox{{(coYoneda)}} \\\

& \V(S \otimes[A,B], T). \qedhere\end{align*}

\end{proof}

\par\begin{remark}

In functional programming, we implicitly restrict to the case where \\(\V\\)
is a cartesian category, and we curry this description to obtain the usual
representation of setters as a single \mintinline[breaklines]{haskell}{over}
function.

\begin{spec}

over :: (a -> b) -> s -> t

\end{spec}

\end{remark}

\par\begin{definition}\label{def:adapter}

Let \\(\C\\) and \\(\D\\) be any two \Vt{categories};
\textbf{adapters}~\cite{kmett15} are morphisms in \\(\C^{op} \otimes\D\\).
They are optics for the action of the identity functor; \\(\mathbf{Adapter}
\cong\Optic_{\mathrm{id},\mathrm{id}}\\).

\\[\mathbf{Adapter} ((A, B), (S, T)) \coloneqq\C(S,A) \otimes\D(B,T).\\]

\end{definition}

\par\subsection{Optics for (co)free}\label{sec:opticsforcofree}

A common pattern that appears across many optic derivations is that of
computing the optic associated to a class of functors using an adjunction to
allow for an application of the Yoneda lemma. This observation can be
generalized to a class of concrete optics.

\parConsider some \Vt{endofunctor} \\(H \colon\V\to\V\\). Any objects
\\(S,T,A,B \in\V\\) can be regarded as functors from the unit \Vt{category}.
The following isomorphisms are the consequence of the fact that left and right
global Kan extensions are left and right adjoints to precomposition,
respectively.

\begin{align*}

\V(S,HA) \cong[\V,\V]( \mathsf{Lan}_A S,H),\\\

\V(HB,T) \cong[\V,\V](H, \mathsf{Ran}_B T).

\end{align*}

These extensions exist in \\(\V\\) and they are given by the formulas

\\[

\mathsf{Lan}_AS \cong[A,-] \otimesS,

\quad\mathsf{Ran}_BT \cong[[-,B],T].

\\]

\par\begin{proposition}[{{\citealp[\S3.4.7]{roman19}}}]\label{prop:opticfree}

Let the monoidal \Vt{action} \\(\U\colon\M\to[\V,\V]\\) have a left adjoint
\\(\mathcal{L} \colon[\V,\V] \to\M\\), or, dually, let it have a right adjoint
\\(\mathcal{R} \colon[\V,\V] \to\M\\). In both of these cases the optic
determined by that monoidal action has a concrete form, given by

\\[\V(\mathcal{UL}([A,-] \otimesS)(B),T) \quad\mbox{ or
}\quad\V(S,\mathcal{UR} [[-,B],T](A)),\\]

respectively.

\end{proposition}

\begin{proof}

We prove the first case. The second one is dual.

\begin{align*}

& \int^{M \in\M} \V(S, \UMA) \otimes\V(\UMB,T)

\\\ \cong& \qquad\mbox{(Kan extension)} \\\

& \int^{M \in\M} \Nat\left( \mathsf{Lan}_A S , \UM \right) \otimes\V(\UMB,T)

\\\ \cong& \qquad\mbox{(Adjunction)} \\\

& \int^{M \in\M} \M\left(\mathcal{L} \mathsf{Lan}_{A}S , M \right)
\otimes\V(\UMB,T)

\\\ \cong& \qquad\mbox{(coYoneda)} \\\

& \V\left( \mathcal{UL} \mathsf{Lan}_{A}S (B) , T \right). &
\qedhere\end{align*}

\end{proof}

\par\section{Tambara theory}\label{sec:tambaratheory}

\parA fundamental feature of optics is that they can be represented as a
single polymorphic function. Optics that admit this representation are called
\emph{profunctor optics}, and that polymorphic function is their
\emph{profunctor representation}. The benefit of the profunctor representation
is that it makes particularly easy to compose two optics, even if they are
from different families: when optics are represented by polymorphic functions,
composition of optics becomes ordinary function composition, as it happened
with Figure~\ref{fig:example1}.

\parProfunctor optics can be seen as functions polymorphic over profunctors
endowed with some extra algebraic structure. This extra structure depends on
the family of the optic they represent. For instance, \emph{lenses} are
represented by functions polymorphic over \emph{cartesian} profunctors, while
\emph{prisms} are represented by functions polymorphic over \emph{cocartesian}
profunctors~\cite[\S3]{pickering17}. Milewski notes that the algebraic
structures accompanying these profunctors are precisely \emph{Tambara
modules}~\cite{milewski17}, a particular kind of profunctor that had been used
to characterize the monoidal centre of convolution monoidal
categories~\cite{tambara06}. Furthermore, it was shown that, because of this,
categories of lenses or prisms can be obtained as particular cases of the
“Doubles for monoidal categories” defined by Pastro and
Street~\cite[\S6]{pastro08}.

\parThe \emph{double} of an arbitrary monoidal \Vt{category}
\\((\AA,\otimes,I)\\), is a promonoidal \Vt{category} \\(\DA\\) whose hom-
objects are defined as

\\[

\DA((A,B),(S,T)) \coloneqq\int^{C \in\AA} \C(S,C \otimesA) \otimes\C(C
\otimesB, T).

\\]

In the particular case where \\(\AA\\) is cartesian or cocartesian, the
\Vt{category} \\(\DA\\) is precisely the category of lenses or prisms over
\\(\AA\\), respectively.

Moreover, one of the main results of Pastro and Street~\cite[Proposition
6.1]{pastro08} declares that the \Vt{category} of copresheaves over these
\Vt{categories}, \\([\mathcal{D}\C, \V]\\), is equivalent to the \Vt{category}
of Tambara modules on \\(\C\\).

In the case of lenses and prisms, these Tambara modules are precisely
cartesian and cocartesian profunctors, and this justifies their profunctor
representation.

\parSurprisingly, the results of Pastro and Street can be applied to the
theory of optics after the observations of Milewski~\cite{milewski17}.
However, they are not general enough. Milewski~\cite{milewski17} already
proposed a unified description of optics, later extended by
Boisseau~\cite{boisseau18} and Riley~\cite{riley18}, that required a
generalization of the original result by Pastro and Street from monoidal
products to arbitrary monoidal actions. If we want to capture \Vt{enriched}
mixed optics, we need to go even further and generalize Pastro and Street’s
definition of Tambara module~\cite[\S3]{pastro08} in two directions. The
monoidal category \\(\AA\\) in their definition needs to be substituted by a
pair of arbitrary categories \\(\C\\) and \\(\D\\), and the monoidal product
\\((\otimes) \colon\AA\to[\AA,\AA]\\) is substituted by a pair of arbitrary
monoidal actions \\((\actL{}{}) \colon\M\otimes\C\to\C\\) and \\((\actR{}{})
\colon\M\otimes\D\to\D\\), from a common monoidal category \\(\M\\).

\parThis section can be seen both as a partial exposition of one of the main
results from Pastro and Street’s “Doubles for monoidal
categories”~\cite[Proposition 6.1]{pastro08} and a generalization of their
definitions and propositions to the setting that is most useful for
applications in functional programming.

\par\subsection{Generalized Tambara modules}

\parOriginally, \emph{Tambara modules}~\cite{tambara06} were conceived as a
structure on top of certain profunctors that made them interplay nicely with
some monoidal action in both its covariant and contravariant components.

\parIn functional programming, Tambara modules represent the different ways in
which we can use an optic. If $P$ has Tambara module structure for the
monoidal actions defining an optic, we can use that optic to lift the Tambara
module applied to the foci, $P(A,B)$, to the Tambara module applied to the
full structures, $P(S,T)$. For instance, the profunctor $(-) \timesB \to(-)$
can be used to lift the projection $A \timesB \toB$ into the \hask{update}
function $S \timesB \toT$. In other words, that profunctor is a Tambara module
compatible with all the families of optics that admit an \hask{update}
function, such as \emph{lenses}. In programming libraries, this can be used to
define a polymorphic \hask{update} combinator that works across different
optic families.

\parFormally, we want to prove that Tambara modules for the actions
\\(\actL{}{}\\) and \\(\actR{}{}\\) are copresheaves over the category
\\(\Optic_{\actL{}{},\actR{}{}}\\). This will also justify the profunctor
representation of optics in terms of Tambara modules
(Theorem~\ref{th:profrep}).

\par\begin{definition}\label{def:tambara}

Let \\((\M,\otimes,I)\\) be a monoidal \Vt{category} with two monoidal actions
\\((\actL{}{}) \colon\M\otimes\C\to\C\\) and \\((\actR{}{})
\colon\M\otimes\D\to\D\\). A generalized \textbf{Tambara module} consists of a
\Vt{profunctor} \\(P \colon\C^{op} \otimes\mathbf{D} \to\V\\) endowed with a
family of morphisms

\\[\alpha_{M,A,B} \colonP(A,B) \toP(\actL{M}{A} , \actR{M}{B})\\]

\Vt{natural} in \\(A \in\C\\) and \\(B \in\D\\) and \Vt{dinatural} \\(M
\in\M\\), which additionally satisfies the two equations

\begin{align*}

\alpha_{I,A,B} \circP(\phi_{A},\varphi^{-1}_{B}) &= \id, \\\

\alpha_{M \otimesN,A,B} \circP(\phi_{M,N,A},\varphi^{-1}_{M,N,B}) &=

\alpha_{M,\actL{N}{A},\actR{N}{B}} \circ\alpha_{N,A,B},

\end{align*}

for every \\(M,N \in\M\\), every \\(A \in\C\\) and every \\(B \in\D\\). That
is, a family of morphisms making the following two diagrams commute.

\\[\begin{tikzcd}[column sep=4em]

P(A,B) \rar{\alpha_{M \otimesN,A,B}}\dar[swap]{\alpha_{N,A,B}} &

P(\actL{M \otimesN}{A},\actR{M \otimesN}{B}) \dar{P(\phi_{M,N,A},
\varphi_{M,N,B})} \\\

P(\actL{N}{A}, \actR{N}{B}) \rar[swap]{\alpha_{M,\actL{N}{A},\actR{N}{B}}} &

P(\actL{M}{\actL{N}{A}}, \actR{M}{\actR{N}{B}}) \\\

P(A,B) \drar[swap]{\id} \rar{\alpha_{I,A,B}} &

P(\actL{I}{A}, \actR{I}{B}) \dar{P(\phi_{I,A},\varphi^{-1}_{I,B})} \\\

& P(A,B)

\end{tikzcd}\\]

\parWhen \\(\V= \Sets\\), we can define a morphism of Tambara modules as a
natural transformation \\(\eta_{A,B} \colonP(A,B) \toQ(A,B)\\) satisfying
\\[\eta_{\actL{M}{A},\actR{M}{B}} \circ\alpha_{M,A,B} =
\alpha’_{M,A,B}\circ\eta_{A, B}.\\]

For an arbitrary \\(\V\\), Tambara modules are the objects of a \Vt{category}
\\(\mathbf{Tamb}\\) whose hom-object from \\((P,\alpha)\\) to
\\((Q,\alpha’)\\) is computed as the intersection of the equalizers of

\begin{align*}

\int_{A,B} \V(P(A,B),Q(A,B)&) \\\

\xrightarrow{\phantom{AAAAAAA}\pi_{A,B}\phantom{AAAAAAA}}\ & \V(P(A,B),
Q(A,B)) \\\

\xrightarrow{\phantom{AAAAA}\V(\id,\alpha’_{A,B})\phantom{AAAAA}}\ &
\V(P(A,B), Q(\actL{M}{A},\actR{M}{B}))

\end{align*}

and

\begin{align*}

\int_{A,B} \V(P(A,B&),Q(A,B)) \\\

\xrightarrow{\phantom{AA}\pi_{\actL{M}{A},\actR{M}{B}}\phantom{AA}}\ &

\V(P(\actL{M}{A},\actR{M}{B}), Q(\actL{M}{A},\actR{M}{B})) \\\

\xrightarrow{\phantom{xA}\V(\alpha_{A,B},\id)\phantom{Ax}}\ & \V(P(A,B),
Q(\actL{M}{A},\actR{M}{B}))

\end{align*}

for each \\(A \in\C\\), \\(B \in\D\\) and \\(M
\in\M\\)~\cite[\S3.2]{pastro08}.

\end{definition}

\par\begin{remark}

Pastro and Street~\cite{pastro08} follow the convention of omitting the
unitors and the associators of the monoidal category when defining Tambara
modules. These appear in Definition~\ref{def:tambara} replaced by the
structure isomorphisms of the two monoidal actions.

\end{remark}

\par\subsection{Pastro-Street’s “double” comonad}

\parIn order to prove their main result, Pastro and Street characterized
Tambara modules as coalgebras for a particular comonad~\cite[\S5]{pastro08}.
That comonad has a left adjoint that must therefore be a monad, and then
Tambara modules can be equivalently described as algebras for that monad.
Following their same technique, we will describe the \Vt{category} of
\emph{generalized} Tambara modules \\(\Tamb\\) as an Eilenberg-Moore category
first for a comonad and then for its left adjoint monad. This will be the main
lemma (Lemma~\ref{lemma:tambaracoalg}) towards the profunctor representation
theorem (Theorem~\ref{th:profrep}).

\par\begin{definition}\label{def:pastrofunctor}

We start by constructing the underlying \Vt{functor} of the comonad
\\(\Theta\colon\Prof(\C,\D) \to\Prof(\C,\D)\\). Consider first the
\Vt{functor}

\\[T \colon\M^{op} \otimes\M\otimes\C^{op}
\otimes\D\otimes\mathbf{Prof}(\C,\D) \to\V, \\]

given by the composition of the actions \\((\actL{}{})\\) and
\\((\actR{}{})\\) with the evaluation \Vt{functor} \\(\C^{op}
\otimes\D\otimes\Prof(\C,\D) \to\V\\). On objects, this is given by

\\[ T(M,N,A,B,P) \coloneqqP(\actL{M}{A},\actR{N}{B}).

\\]

By the universal property of the end, this induces a \Vt{functor}

\\(\C^{op} \otimes\D\otimes\Prof(\C,\D) \to\V\\)

given by

\\[ T(A,B,P) = \int_{M \in\M} P(\actL{M}{A},\actR{M}{B}),

\\]

which can be curried into the \Vt{functor}

\\[\ThetaP(A,B) \coloneqq\int_{M \in\M} P(\actL{M}{A}, \actR{M}{B}).

\\]

\end{definition}

\par\begin{proposition}\label{prop:pastrocomonad}

The \Vt{functor} \\(\Theta\\) can be endowed with a comonad structure. Its
counit is the \Vt{natural} family of morphisms \\(\varepsilon_{P,A,B}
\colon\ThetaP (A,B) \toP(A,B)\\) obtained by projecting on the monoidal unit
and applying the unitors,

\\[\begin{tikzcd}[column sep=4em]

\ThetaP(A,B) \rar{\pi_{I}} &

P(\actL{I}{A}, \actR{I}{B}) \rar{P(\phi_{A}, \varphi^{-1}_{B})} & P(A,B).

\end{tikzcd}\\]

Its comultiplication is given by \\(\delta_{P,A,B} \colon\ThetaP(A,B)
\to\Theta\ThetaP(A,B)\\), the \Vt{natural} family of transformations obtained
as the unique morphisms factorizing

\\[\begin{tikzcd}[column sep=1.5em]

\displaystyle\ThetaP (A,B)

\ar{r}{P\left(\phi_{M,N,A},\varphi^{-1}_{M,N,B}\right) \circ\pi_{M \otimesN} }

&[18ex] P(\actL{M}{\actL{N}{A}}, \actR{M}{\actR{N}{B}})

\end{tikzcd}\\]

through the projection

\\[\begin{tikzcd}[column sep=4em]

\Theta\ThetaP (A,B)

\rar{\pi_M \circ\pi_N} &

P(\actL{M}{\actL{N}{A}} , \actR{M}{\actR{N}{B}})

\end{tikzcd}\\]

for every \\(M,N \in\M\\).

\end{proposition}

\begin{remark}\label{remark:axiomsmonoidal}

Before the proof, let us recall the axioms for a strong monoidal \Vt{action}
\\(\oslash\colon\M\otimes\C\to\C\\) of a monoidal \Vt{category}
\\((\M,\otimes,I)\\) with coherence isomorphisms \\((a,\lambda,\rho)\\) to an
arbitrary category \\(\C\\). Let

\\[\begin{aligned}

& \phi_{A} \colonA \congI \oslashA, && \phi_{M,N,A} \colonM \oslashN \oslashA
\congM \otimesN \oslashA, \\\

\end{aligned}\\]

be the structure \Vt{natural} isomorphisms of the strong monoidal action.

Note that the following are precisely the axioms for a strong monoidal functor
\\(\M\to[\C,\C]\\) written as \\(\M\otimes\C\to\C\\); they are simplified by
the fact that \\([\C,\C]\\) is strict.

\\[\begin{tikzcd}

I \oslashM \oslashA \dar[swap]{\phi_{I,M,A}} &

M \oslashA \lar[swap]{\phi_{M \oslashA}} \rar{M \oslash\phi_A} \dar{id} &

M \oslashI \oslashA \dar{\phi_{M,I,A}} \\\

I \otimesM \oslashA \rar[swap]{\lambda_M \oslashA}&

M \oslashA &

M \otimesI \oslashA \lar{\rho_M \oslashA}

\end{tikzcd}\\]

\\[\begin{tikzcd}

M \oslashN \oslashK \oslashA \rar{\id} \dar[swap]{\phi_{M,N,K\oslashA}} &

M \oslashN \oslashK \oslashA \dar{M \oslash\phi_{N,K,A}} \\\

M \otimesN \oslashK \oslashA \dar[swap]{\phi_{M \otimesN,K,A}} &

M \oslashN \otimesK \oslashA \dar{\phi_{M,N \otimesK,A}} \\\

(M \otimesN) \otimesK \oslashA \rar[swap]{a_{M,N,K} \oslashA} &

M \otimes(N \otimesK) \oslashA

\end{tikzcd}\\]

\end{remark}

\par\begin{proof}

In order to keep the diagrams in this proof small, we introduce the notation
\\(P[M](A,B) \coloneqqP(\actL{M}{A},\actR{M}{B})\\). We will show that this
construction satisfies the comonad axioms.

\parWe first prove left counitality, \\(\Theta\varepsilon_P \circ\delta_P =
\mathrm{id}_{\ThetaP}\\), which follows from the commutativity of the
following diagram.

\\[\begin{tikzcd}

\ThetaP(A,B) \rar{\delta_P} \ar{dd}[swap]{\pi_{I \otimesM}} &

\Theta\ThetaP(A,B) \rar{(\Theta\varepsilon)_P} \dar{\pi_M} &

\ThetaP(A,B) \dar{\pi_M} \\\

& \ThetaP[M](A,B) \dar{\pi_I} \rar{\varepsilon_{P[M]}} &

P[M](A,B) \dar{\id} \\\

P[I \otimesM](A,B)
\ar[swap]{r}[yshift=-1ex]{P(\phi_{I,M,A},\varphi^{-1}_{I,M,B})} &

P[M][I](A,B)
\ar[swap]{r}[yshift=-1ex]{P(\phi_{\actL{M}{A}},\varphi^{-1}_{\actR{M}{B}})} &

P[M](A,B)

\end{tikzcd}\\]

The left pentagon of this diagram commutes because of the definition of
\\(\delta\\).

The upper right square commutes because of functoriality of ends and
naturality of \\(\pi_M\\). The lower right square commutes because of the
definition of \\(\varepsilon\\). By the axioms of the monoidal actions
(Remark~\ref{remark:axiomsmonoidal}), the lower side of the square can be
rewritten as

\begin{align*}

P(\phi_{I,M,A},\varphi^{-1}_{I,M,B})
\circP(\phi_{\actL{M}{A}},\varphi^{-1}_{\actR{M}{B}}) = P(\lambda^{-1}_M
\oslashA, \lambda_M \oslashB).

\end{align*}

Now, by the wedge condition of the end, one of the sides of the previous
diagram is just the projection \\(\pi_M\\).

\\[\begin{tikzcd}[column sep=small]

& \ThetaP(A,B) \dlar[swap]{\pi_{I \otimesM}} \drar{\pi_M}& \\\

P[I \otimesM](A,B) \drar[swap]{P(\id,\lambda_M \oslashB)} && P[M](A,B)
\dlar{P(\lambda_M \oslashA,\id)} \\\

& P(\actL{I \otimesM}{A},\actL{M}{B}) &

\end{tikzcd}\\]

Finally, by the universal property of the end, that implies that
\\(\Theta\varepsilon_P \circ\delta_P\\) must coincide with the identity.

\parLet us now prove right counitality, \\(\varepsilon_{\ThetaP} \circ\delta_P
= \id_{\ThetaP}\\), which follows from the commutativity of the following
diagram.

\\[\begin{tikzcd}

\ThetaP(A,B) \rar{\delta_P} \ar{dd}[swap]{\pi_{I \otimesM}} &

\Theta\ThetaP(A,B) \rar{ \varepsilon_{\ThetaP}} \dar{\pi_I} &

\ThetaP(A,B) \dar{\id} \\\ &

\ThetaP[I](A,B) \dar{\pi_M} \rar{\ThetaP(\phi_I, \varphi_I^{-1})} &

\ThetaP(A,B) \dar{\pi_M} \\\

P[M \otimesI](A,B)
\ar[swap]{r}[yshift=-1ex]{P(\phi_{M,I,A},\varphi^{-1}_{M,I,B})} &

P[I][M](A,B) \ar[swap]{r}[yshift=-1ex]{P(\phi_A,\varphi_B^{-1})} &

P[M](A,B)

\end{tikzcd}\\]

Again, the definition of \\(\delta\\) makes the left pentagon commute. The
upper right square commutes now because of the definition of
\\(\varepsilon\\), whereas the lower right square commutes because of
functoriality of ends and naturality of \\(\pi\\). By the axioms of the
monoidal actions (Remark~\ref{remark:axiomsmonoidal}), the lower side of the
square can be rewritten as

\\[

P(\phi_A,\varphi_B^{-1}) \circP(\phi_{M,I,A},\varphi^{-1}_{M,I,B}) =
P(\rho_M^{-1} \oslashA, \rho_M \oslashB).

\\]

Now, by the wedge condition of the end, one of the sides of the previous
diagram is just the projection \\(\pi_M\\).

\\[\begin{tikzcd}[column sep=small]

& \ThetaP(A,B) \dlar[swap]{\pi_{I \otimesM}} \drar{\pi_M}& \\\

P[I \otimesM](A,B) \drar[swap]{P(\id,\lambda_M \oslashB)} && P[M](A,B)
\dlar{P(\lambda_M \oslashA,\id)} \\\

& P(\actL{I \otimesM}{A},\actL{M}{B}) &

\end{tikzcd}\\]

Finally, by the universal property of the end, \\(\varepsilon_{\ThetaP}
\circ\delta_P\\) must coincide with the identity.

\parCoassociativity, \\(\Theta\delta_P\circ\delta_{P} =
\delta_{\ThetaP}\circ\delta_P\\), follows from commutativity of the diagram in
Figure~\ref{fig:diagramassoc}. We need to show that the upper diamond
commutes; by the universal property of the ends, this amounts to showing that
it commutes when followed by \\(\pi_M \circ\pi_N \circ\pi_K\\). The lower
pentagon is made of isomorphisms, and it commutes by the axioms of the
monoidal actions (Remark~\ref{remark:axiomsmonoidal}). The two upper
degenerated pentagons commute by definition of \\(\delta\\). The two
trapezoids commute by functoriality of ends and naturality of the projections.

\parFinally, the two outermost morphisms of the diagram correspond to two
projections from \\(\ThetaP(A,B)\\), namely \\(\pi_{(M \otimesN) \otimesK}\\)
and \\(\pi_{M \otimes(N \otimesK)}\\). The wedge condition for the associator
\\(a_{M,N,K}\\) makes the external diagram commute.

\end{proof}

\begin{figure}[!h]

\centering\begin{tikzcd}

& \ThetaP(A,B)

\ar{rd}{\delta_{P}}

\ar[swap]{dl}{\delta_{P}}

& \\\ \Theta\ThetaP(A,B)

\ar[swap]{rd}{\Theta\delta_{P}}

\ar[swap]{ddd}{\pi_K}

&& \Theta\ThetaP(A,B)

\ar{ddd}{\pi_{N \otimesK}}

\ar{ld}{\delta_{\ThetaP}}

\\\ & \Theta\Theta\ThetaP(A,B)

\ar{d}{\pi_K}

\\\ & \Theta\ThetaP[K](A,B)

\ar{dd}{\pi_N}

& \\\ \ThetaP[K](A,B)

\urar{\delta_{P[K]}}

\ar[swap]{ddd}{\pi_{M \otimesN}}

&& \ThetaP[N \otimesK](A,B)

\ar{ddd}{\pi_M}

\dlar[near end]{\ThetaP(\phi_{N,K,A},\varphi_{N,K,B}^{-1})}

\\\ & \ThetaP[K][N](A,B)

\dar{\pi_M}

&\\\ & P[K][N][M](A,B)

\\\ P[K][M \otimesN](A,B)

\urar[near end,xshift=0.5em]{P(\phi_{M,N,\actL{K}{A}},
\varphi_{M,N,\actR{K}{B}}^{-1})}

\dar{P(\phi_{M \otimesN,K,A},\varphi^{-1}_{M \otimesN,K,B})}

&& P[N \otimesK][M](A,B)

\ular[swap, near end]{P(\phi_{N,K,A},\varphi_{N,K,B}^{-1})}

\dar[swap]{P(\phi_{M, N\otimesK,A},\varphi^{-1}_{M, N\otimesK,B})}

\\\ P[(M\otimesN)\otimesK](A,B) \ar{rr}{P(a^{-1}_{M,N,K},a_{M,N,K})} &&
P[M\otimes(N\otimesK)](A,B)

\end{tikzcd}

\caption{Diagram for the coassociativity axiom.}\label{fig:diagramassoc}

\end{figure}

\par\begin{lemma}\label{lemma:tambaracoalg}

Tambara modules are precisely coalgebras for this comonad. There exists an
isomorphism of \Vt{categories} \\(\mathbf{Tamb} \congEM(\Theta)\\) from the
category of Tambara modules to the Eilenberg-Moore category of \\(\Theta\\).

\end{lemma}

\par\begin{proof}

Note that the object of \Vt{natural} transformations from \\(P\\) to
\\(\ThetaP\\) is precisely

\begin{align*}

& \Prof(\C,\D)(P,\ThetaP) \\\

\cong& \quad\mbox{(Definition)} \\\

& \int_{A,B} \V\left(P(A,B),\int_{M \in\M} P(\actL{M}{A}, \actR{M}{B})\right)
\\\

\cong& \quad\mbox{(Continuity)} \\\

& \int_{A,B,M} \V\left(P(A,B), P(\actL{M}{A}, \actR{M}{B})\right)

\end{align*}

whose elements can be seen as a family of morphisms that is natural in both
\\(M \in\M\\) and \\((A,B) \in\C^{op} \otimes\D\\). The two conditions in the
definition of Tambara module can be rewritten as the axioms of the coalgebra.

\end{proof}

\par\begin{proposition}

The \\(\Theta\\) comonad has a left \Vt{adjoint} \\(\Phi\\), which must
therefore be a monad. On objects, it is given by the following formula.

\\[\PhiQ(X,Y) = \int^{M,U,V}

Q(U,V) \otimes\C(X,\actL{M}{U}) \otimes\D(\actR{M}{V},Y).\\]

That is, there exists a \Vt{natural} isomorphism \\(\Nat(\PhiQ,P)
\cong\Nat(Q,\ThetaP)\\).

\end{proposition}

\par\begin{proof}

We can explicitly construct the \Vt{natural} isomorphism using coend calculus.

\par\noindent\resizebox{\linewidth}{!}{

\begin{minipage}{\linewidth}

\begin{align*}

& \int_{A,B} \V\left(Q(A,B), \int_{M}P(\actL{M}{A}, \actR{M}{B})\right)

\\\ \cong& \quad\mbox{(Continuity)}

\\\ & \int_{M,A,B} \V(Q(A,B), P(\actL{M}{A}, \actR{M}{B}))

\\\ \cong& \quad\mbox{(Yoneda, in the category $\C^{op}\otimes\D$)}

\\\ & \int_{M,A,B} \V\left( Q(A,B) , \int_{X,Y} \V\Big(\C(X, \actL{M}{A})
\otimes\D(\actR{M}{B},Y) , P(X,Y)\Big) \right)

\\\ \cong& \quad\mbox{(Continuity)}

\\\ & \int_{M,A,B,X,Y} \V\left( Q(A,B) , \V\Big(\C(X, \actL{M}{A})
\otimes\D(\actR{M}{B},Y) , P(X,Y)\Big) \right)

\\\ \cong& \quad\mbox{(Currying)}

\\\ & \int_{M,A,B,X,Y} \V(Q(A,B) \otimes\C(X, \actL{M}{A})
\otimes\D(\actR{M}{B}, Y), P(X,Y))

\\\ \cong& \quad\mbox{(Continuity)}

\\\ & \int_{X,Y} \V\left( \int^{M,A,B} Q(A,B) \otimes\C(X, \actL{M}{A})
\otimes\D(\actR{M}{B},Y) , P(X,Y) \right). \\\

\end{align*}

\end{minipage}}

\parAlternatively, the adjunction can be deduced from the definition of the
comonad \\(\Theta\\) and the characterization of global Kan extensions as
adjoints to precomposition.

\end{proof}

\par\par\subsection{Pastro-Street’s “double” promonad}

\parThe second part of this proof occurs in the bicategory of
\Vt{profunctors}. In this category, there exists a formal analogue of the
Kleisli construction that, when applied to the Pastro-Street monad \\(\Phi\\),
yields a category whose morphisms are the optics from
Definition~\ref{def:optic}. This is the crucial step of the proof, as the
universal property of that Kleisli construction will imply that copresheaves
over the category of optics there defined are Tambara modules
(Lemma~\ref{lemma:copresheaves}). After that, the last step will be a
relatively straightforward application of the Yoneda lemma
(Lemma~\ref{lemma:doubleyoneda}).

\parLet \\(\Prof\\) be the bicategory of \Vt{profunctors} that has as 0-cells
the \Vt{categories} \\(\C,\D,\E, \dots\\); as 1-cells \\(P \colon\C\nto\D\\)
the \Vt{profunctors} given as \\(P \colon\C^{op} \otimes\D\to\V\\); and as
2-cells the natural transformations between them. The composition of two
\Vt{profunctors} \\(P \colon\C^{op} \otimes\D\to\V\\) and \\(Q \colon\D^{op}
\otimes\E\to\V\\) is the \Vt{profunctor} \\(Q \diamondP \colon\C^{op}
\otimes\E\to\V\\) defined on objects by the coend\footnote{Though, in general,
the composition of two profunctors can fail to exist for size reasons or when
$\V$ lacks certain colimits, we only ever need these composites in a formal
sense. This perspective can be formalized with the notion of virtual
equipment~\cite{cruttwell09}.}

\\[

(Q \diamondP)(C,E) = \int^{D \in\D} P(C,D) \otimesQ(D,E).

\\]

There is, however, an equivalent way of defining profunctor composition if we
interpret each \Vt{profunctor} \\(\C^{op} \otimes\D\to\V\\) as a \Vt{functor}
\\(\C^{op} \to[\D,\V]\\) to the category of copresheaves. In this case, the
composition of two profunctors \\(P \colon\C^{op} \to[\D,\V]\\) and \\(Q
\colon\D^{op} \to[\E,\V]\\) is the \Vt{functor} \\((Q \diamondP) \colon\C^{op}
\to[\E,\V]\\) defined by taking a left Kan extension \\((Q \diamondP)
\coloneqq\Lan_y Q \circP\\) along the Yoneda embedding \\(y \colon\D^{op}
\to[\D,\V]\\). The unit profunctor for composition is precisely the Yoneda
embedding.

\\[\begin{tikzcd}

& \D^{op} \rar{Q} \dar[swap]{y} & \left[\E, \V\right] \\\

\C^{op} \rar{P} & \left[\D, \V\right] \urar[swap]{\Lan_y Q \circP} &

\end{tikzcd}\\]

In the same way that we can construct a Kleisli category over a monad, we will
perform a Kleisli construction over the monoids of the bicategory \\(\Prof\\),
which we call \textbf{promonads}. Promonads over the base category \\(\V\\)
that are also Tambara modules for the product appear frequently in the
literature on functional programming languages under the name of
\emph{arrows}~\cite{hughes00}.

\par\begin{definition}

A \textbf{promonad} is given by a \Vt{category} \\(\A\\), an endoprofunctor
\\(T \colon\A^{op} \otimes\A\to\V\\), and two \Vt{natural} families
\\(\eta_{X,Y} \colon\C(X,Y) \toT(X,Y)\\) and \\(\mu_{X,Y} \colon(T
\diamondT)(X,Y) \toT(X,Y)\\) satisfying the following unitality and
associativity axioms.

\\[\begin{tikzcd}

T \rar{\eta\diamond\id}\drar[swap]{\id} & T\diamondT \dar{\mu} &
\lar[swap]{\id\diamond\eta}\dlar{\id} T &[-2em]

T \diamondT \diamondT\dar[swap]{\id\diamond\mu} \rar{\mu\diamond\id} & T
\diamondT \dar{\mu} \\\

& T && T \diamondT \rar{\mu}& T

\end{tikzcd}\\]

A module for the promonad is a \Vt{profunctor} \\(P \colon\X^{op}
\otimes\A\to\V\\), together with a \Vt{natural} transformation \\(\rho\colonT
\diamondP \toP\\) making the following diagrams commute.

\\[\begin{tikzcd}

P \rar{\eta\diamond\id} \drar[swap]{\id} & T \diamondP \dar{\rho} &

T \diamondT \diamondP \rar{\mu\diamond\id} \dar[swap]{\id\diamond\rho} & T
\diamondP \dar{\rho} \\\

& P & T \diamondP \rar{\rho} & P

\end{tikzcd}\\]

An algebra is a module structure on a \Vt{copresheaf} \\(P \colon\A\to\V\\),
interpreted as a profunctor \\(\mathbf{I}^{op} \otimes\A\to\V\\) from the unit
\Vt{category}.

\end{definition}

\par\begin{lemma}\label{lemma:kleisli}

The bicategory \\(\Prof\\) admits the Kleisli
construction~\cite[\S6]{pastro08}. The Kleisli \Vt{category} \\(\Kl(T)\\) for
a promonad \\((T, \mu, \eta)\\) over \\(\A\\) is constructed as having the
same objects as \\(\A\\) and letting the hom-object between \\(X,Y \in\A\\) be
precisely \\(T(X,Y) \in\V\\).

\end{lemma}

\begin{proof}

The multiplication of the promonad is a \Vt{natural} transformation whose
components can be taken as the definition for the composition of the
\Vt{category} \\(\Kl(T)\\).

\begin{align*}

& \V\left(\int^{Z \in\C} T(X,Z) \otimesT(Z,Y) , T(X,Y)\right) \\\

\cong& \quad\mbox{(Continuity)} \\\

& \int_{Z \in\C} \V\left(T(X,Z) \otimesT(Z,Y) , T(X,Y)\right)

\end{align*}

\par\parLet us show now that this \Vt{category} satisfies the universal
property of the Kleisli construction. Let \\(P \colon\X^{op} \otimes\A\to\V\\)
be a \Vt{profunctor}. A module structure \\(\rho\colonT \diamondP \toP\\)
corresponds to a way of lifting the profunctor \\(P\\) to the Kleisli category
in its second argument.

\begin{align*}

& \int_{X \in\X, Z \in\A} \V\left(\int^{Y \in\A} P(X,Y) \otimesT(Y,Z), P(X,Z)
\right)\\\

\cong& \quad\mbox{(Continuity)} \\\

& \int_{X,Y,Z} \V(P(X,Y) \otimesT(Y,Z), P(X,Z)) \\\

\cong& \quad\mbox{(Exponential)} \\\

& \int_{X,Y,Z} \V(T(Y,Z), [P(X,Y), P(X,Z)]).

\end{align*}

Functoriality of this family follows from the algebra axioms.

\end{proof}

\par\begin{lemma}\label{lemma:copresheaves}

The category of algebras for a promonad is equivalent to the copresheaf
category over its Kleisli object.

\end{lemma}

\begin{proof}

Let \\(\X\\) be any category and \\(\Phi\colon\Y\to\Y\\) a promonad. By the
universal property of the Kleisli construction (see
Lemma~\ref{lemma:kleisli}), \\(\Prof(\X,\operatorname{Kl}(\Phi))\\) is
equivalent to the category of modules on \\(\X\\) for the promonad. In
particular, \Vt{profunctors} from the unit \Vt{category} to the Kleisli object
form precisely the category \\(\EM(\Phi)\\) of algebras for the promonad; thus

\\[[\operatorname{Kl}(\Phi),\V] \cong[\mathbf{I}^{op}
\otimes\operatorname{Kl}(\Phi),\V]
\cong\Prof(\mathbf{I},\operatorname{Kl}(\Phi)) \cong\EM(\Phi).\qedhere\\]

\end{proof}

\par\begin{proposition}\label{prop:cocontinous}

Let \\(T \colon[\A,\V] \to[\A,\V]\\) be a cocontinuous monad. The profunctor
\\(\check{T} \colon\A^{op} \to[\A,\V]\\) defined by \\(\check{T} \coloneqqT
\circy\\) can be given a promonad structure. Moreover, algebras for \\(T\\)
are precisely algebras for the promonad \\(\check{T}\\).

\end{proposition}

\begin{proof}

First, the fact that \\(T\\) is cocontinuous means that it preserves left Kan
extensions and thus,

\\[\Lan_y\check{T} \cong\mathsf{Lan}_y(T \circy) \congT \circ\mathsf{Lan}_y(y)
\congT.\\]

This means that the composition of the profunctor \\(\check{T}\\) with itself
is

\\[\check{T} \diamond\check{T}

\cong\mathsf{Lan}_y \check{T} \circT\circy

\congT \circT \circy.

\\]

The unit and multiplication of the promonad are then obtained by whiskering
the unit and multiplication of the monad with the Yoneda embedding; that is,
\\((\eta\asty) \colony \toT\circy\\) and \\((\mu\asty) \colonT \circy \toT
\circT \circy\\). The diagrams for associativity and unitality for the
promonad are the whiskering by the Yoneda embedding of the same diagrams for
the monad. In fact, the same reasoning yields that, for any \\(P \colon\D^{op}
\to[\A, \V]\\),

\\[\check{T} \diamondP \cong(T \circy) \diamondP \cong\Lan_y(T \circy)\circP
\congT \circP.\\]

As a consequence of this for the case \\(P \colon\mathbf{I}
\to[\A^{op},\V]\\), any \\(T\mbox{-algebra}\\) can be seen as a
\\(\check{T}\mbox{-algebra}\\) and vice versa. The axioms for the promonad
structure on \\(\check{T}\\) coincide with the axioms for the corresponding
monad on \\(T\\).

\end{proof}

\parIn particular, the Pastro-Street monad \\(\Phi\\) is a left adjoint. That
implies that it is cocontinuous and, because of
Proposition~\ref{prop:cocontinous}, it induces a promonad \\({\check\Phi} =
\Phi\circy\\), having Tambara modules as algebras. We can compute by the
Yoneda lemma that

\\[{\check\Phi}(A,B,S,T) = \int^{M} \C(S,\actL{M}{A}) \otimes\D(\actR{M}{B},
T).

\\]

Note that this coincides with Definition~\ref{def:optic}. We now define
\\(\Optic\\) to be the Kleisli \Vt{category} for the promonad
\\({\check\Phi}\\).

\par\subsection{Profunctor representation theorem}

\parLet us zoom out to the big picture again. It has been observed that optics
can be composed using their profunctor representation; that is, profunctor
optics can be endowed with a natural categorical structure. On the other hand,
we have generalized the double construction by Pastro and
Street~\cite{pastro08} to abstractly obtain the category \\(\Optic\\). The
last missing piece that makes both coincide is the \textit{profunctor
representation theorem}, which will justify the profunctor representation of
optics and their composition in profunctor form being the usual function
composition.

\parThe profunctor representation theorem for the case \\(\V= \Sets\\) and
non-mixed optics has been discussed by Boisseau and Gibbons~\cite[Theorem
4.2]{boisseau18}. Although our statement is more general and the proof
technique is different, the main idea is the same. In both cases, the key
insight is the following lemma, already described by
Milewski~\cite{milewski17}.

\par\begin{lemma}[“Double Yoneda” from
Milewski~\cite{milewski17}]\label{lemma:doubleyoneda}

For any \Vt{category} \\(\A\\), the hom-object between \\(X\\) and \\(Y\\) is
\Vt{naturally} isomorphic to the object of \Vt{natural} transformations
between the functors that evaluate copresheaves in \\(X\\) and \\(Y\\); that
is,

\\[\A(X,Y) \cong[ [ \A, \V] , \V](-(X),-(Y)).\\]

The isomorphism is given by the canonical maps \\(\A(X,Y) \to\V(FX,FY)\\) for
each \\(F \in[\A, \V]\\). Its inverse is given by computing its value on the
identity on the \\(\A(X,-)\\) component.

\end{lemma}

\par\begin{proof}

In the functor \Vt{category} \\([ \A, \V]\\), we can apply the Yoneda
embedding to two representable functors \\(\A(Y,-)\\) and \\(\A(X,-)\\) to get

\\[\Nat(\A(Y,-) , \A(X,-)) \cong\int_F \V\Big([\A(X,-),F], [\A(Y,-),F] \Big).

\\]

Here reducing by Yoneda lemma on both the left hand side and the two arguments
of the right hand side, we get the desired result.

\end{proof}

\par\begin{theorem}[Profunctor representation theorem]\label{th:profrep}

\\[\int_{P \in\mathbf{Tamb}} \V(P(A,B) , P(S,T)) \cong\Optic((A,B),(S,T)).

\\]

\end{theorem}

\begin{proof}

We apply Double Yoneda (Lemma~\ref{lemma:doubleyoneda}) to the \Vt{category}
\\(\Optic\\) and then use that copresheaves over it are precisely Tambara
modules (Proposition~\ref{lemma:copresheaves}).

\end{proof}

\par\par\section{Conclusions}

\parWe have extended a result by Pastro and Street to a setting that is useful
for optics in functional programming. Using it, we have refined some of the
optics already present in the literature to mixed optics, providing
derivations for each one of them. We have also described new optics.

\parRegarding functional programming, the work suggests an architecture for a
library of optics that would benefit from these results. Instead of
implementing each optic separately, the general definition can be instantiated
in all the particular cases. We can then just consider specific functions for
constructing the more common families of optics. Tambara modules can be used
to implement each one of the combinators of the library, ensuring that they
work for as many optics as possible. The interested reader can find the
implementation in the Appendix~\ref{sec:implementation}.

\parMany of the other applications of optics may benefit from the flexibility
of enriched and mixed optics. They may be used to capture some
\emph{lens}-like constructions and provide a general theory of how they should
be studied; the specifics remain as future work.

\par\subsection{Van Laarhoven encoding}

This text has focused on the profunctor representation of optics. A similar
representation that also provides the benefit of straightforward composition
is the the \textbf{van Laarhoven encoding}~\cite{laarhoven09}. It is arguably
less flexible than the profunctor representation, being based on representable
profunctors, but it is more common in practice. For instance, traversals admit
a different encoding in terms of profunctors represented by an applicative
functor.

\begin{align*}

& \int_{F \in\mathbf{App}} \V(A, FB) \otimes\V(S,FT) \\\

\cong& \quad\mbox{(Yoneda)} \\\

& \int_{F \in\mathbf{App}} [\V,\V](A \otimes[B,-], F) \otimes\V(S,FT) \\\

\cong& \quad\mbox{(Free applicative)} \\\

& \int_{F \in\mathbf{App}} \App\left(\sum_{n \in\mathbb{N}} A^n
\otimes[B^n,-], F \right) \otimes\V(S,FT) \\\

\cong& \quad\mbox{(coYoneda)} \\\

& \V\left(S, \sum_{n \in\mathbb{N}} A^n \otimes[B^n , T]\right).

\end{align*}

Exactly the same technique yields lenses and \emph{grates}~\cite{deikun15},
using arbitrary representable or corepresentable profunctors, respectively.

\par\subsection{Related work}

\par\begin{itemize}

\itemThe case of mixed optics was first mentioned by
Riley~\cite[\S6.1]{riley18}, but his work targeted a more restricted case.
Specifically, the definitions of \emph{optic} given by Riley~\cite[Definition
2.0.1]{riley18} and Boisseau~\cite[\S4.5]{boisseau18} deal only with the
particular case in which \\(\V= \Sets\\), \\(\C\\) and \\(\D\\) are the same
category, and the two actions coincide. The definition we use
(Definition~\ref{def:optic}) and the proofs we present are then strictly more
general than these other ones~\cite[Proposition 2.0.3]{riley18}, as they
address arbitrary monoidal actions instead of monoidal products, and enriched
\emph{mixed} optics instead of assuming \\(\C=\D\\).

\par\itemPastro and Street~\cite{pastro08} first described the construction of
\Vt{categories} of the form \\(\DA\\) in their study of Tambara theory. These
results can be reused for optics thanks to the observations of
Milewski~\cite{milewski17}. We carry his approach to a more general case.

\par\itemThe profunctor representation theorem and its implications for
functional programming are discussed by Boisseau and
Gibbons~\cite{boisseau18}. We present a different approach to a more general
version of this theorem.

\par\itemWe describe a general derivation for optics assuming a suitable
adjunction (Section~\ref{sec:opticsforcofree}). Riley describes a different
but closely related class of optics and their laws~\cite[\S4.4]{riley18}; ours
makes stronger assumptions but may be easier to apply in programming contexts.

\par\par\itemA central aspect of Riley’s work is the extension of the concept
of \emph{lawful lens} to arbitrary \emph{lawful optics}~\cite[\S3]{riley18}.
Lawfulness is a different topic that we have decided not to address here.

\par\itemFinally, Riley uses the results of Jaskelioff and O’Connor to propose
a description of the traversal in terms of traversable
functors~\cite[\S4.6]{riley18}; our derivation simplifies this approach, which
was in principle not suitable for the enriched case.

\end{itemize}

\par\subsection{Further work}

\par\begin{itemize}

\itemA categorical account of how optics of different kinds compose into
optics is left for further work. Specifically, it should be able to explain
the “lattice of optics” described by Pickering, Gibbons and
Wu~\cite{pickering17} and later by Boisseau and Gibbons~\cite{boisseau18}.
Some preliminary results have been discussed by Román~\cite{roman19}, but the
proposal to model the lattice is still too \emph{ad-hoc} to be satisfactory.

\par\itemThe relation between power series functors and traversables is
implicit across the literature on polynomial functors and containers. It can
be shown that \emph{traversable} structures over an endofunctor \\(T\\)
correspond to certain parameterised coalgebras using the free applicative
construction~\cite{rypacek12}. We believe that it is possible to refine this
result relating the laws of traversables to the derivation in our
Proposition~\ref{prop:traversal}. This could also make our derivation for
traversals more practical for functional programming.

\parIt can be noted that lenses are the optic for products, functors that
distribute over strong functors. Traversals are the optic for traversables,
functors that distribute over applicative functors. Both have a van Laarhoven
representation in terms of strong and applicative functors respectively. A
construction like this needs a certain Kan extension to be given a coalgebra
structure~\cite[Lemma 4.1.3]{roman19}, but it does not necessarily work for
any optic.

\par\itemOptics have numerous applications in the literature, including game
theory~\cite{ghani18}, machine learning~\cite{fong19} or model-driven
development~\cite{stevens10}.

Beyond functional programming, enriched optics open new paths for exploration
on applications of optics. Both mixed optics and enriched optics allow us to
more precisely adjust the existing definitions to match the desired
applications.

\par\itemWe have not addressed the topic of lawfulness. A first reasonable
notion of lawfulness for the case of mixed optics for two actions
\\((\actL{}{}) \colon\M\otimes\C\to\C\\) and \\((\actR{}{})
\colon\N\otimes\D\to\D\\) is to use a cospan \\(\C\to\mathbf{E} \gets\D\\)
\emph{of actions} to push the two parts of the optic into the same category
and then consider lawfulness in \\(\mathbf{E}\\). This can be applied to
monadic lenses, for instance, when the monad is copointed.

\end{itemize}

\par\par\section{Acknowledgements}

This work was started in the last author’s MSc thesis~\cite{roman19};
development continued at the Applied Category School 2019 at Oxford, and we
thank the organizers of the School for that opportunity. We also thank Pawel
Sobocinski for comments on the structure of the paper.

\parFosco Loregian and Mario Román were supported by the European Union
through the ESF funded Estonian IT Academy research measure (project
2014-2020.4.05.19-0001).

Bryce Clarke is supported by the Australian Government Research Training
Program Scholarship.

\par\par\bibliographystyle{alpha}

\bibliography{./optics}

\par\section{Appendix: Haskell implementation}\label{sec:implementation}

\par\ignore{

\begin{code}

{-# LANGUAGE AllowAmbiguousTypes #-}

{-# LANGUAGE ConstraintKinds #-}

{-# LANGUAGE DataKinds #-}

{-# LANGUAGE ExistentialQuantification #-}

{-# LANGUAGE FlexibleContexts #-}

{-# LANGUAGE FlexibleInstances #-}

{-# LANGUAGE FunctionalDependencies #-}

{-# LANGUAGE GADTs #-}

{-# LANGUAGE ImplicitParams #-}

{-# LANGUAGE IncoherentInstances #-}

{-# LANGUAGE KindSignatures #-}

{-# LANGUAGE LiberalTypeSynonyms #-}

{-# LANGUAGE MultiParamTypeClasses #-}

{-# LANGUAGE RankNTypes #-}

{-# LANGUAGE ScopedTypeVariables #-}

{-# LANGUAGE StandaloneDeriving #-}

{-# LANGUAGE TypeApplications #-}

{-# LANGUAGE TypeFamilies #-}

{-# LANGUAGE PolyKinds #-}

{-# LANGUAGE TypeOperators #-}

{-# LANGUAGE TypeSynonymInstances #-}

{-# LANGUAGE UndecidableInstances #-}

{-# LANGUAGE QuantifiedConstraints #-}

{-# LANGUAGE UndecidableSuperClasses #-}

\parimport Prelude hiding (map)

import Data.Constraint

import Data.Void

import Data.Function

import Data.Either

import Control.Monad.Writer hiding (Any)

import Control.Monad

import Data.Char

import Data.List

import Data.Monoid hiding (Any)

import Text.Printf

import Data.Functor.Compose

import Data.Functor.Identity

\end{code}

}

\par\par\parLet \\(\V\\) be a cartesian closed category whose objects model
the types of our programming language and whose points \\(1 \toX\\) represent
programs of type \\(X\\). The following pretends to be an informal translation
of the concepts on enriched category theory to a Haskell implementation where
a single abstract definition of optic is used for a range of different
examples. It can be compiled with GHC version 8.6.5. The source code of this
text includes an implementation of optics and all the examples we have
discussed
(Figures~\ref{fig:example1},~\ref{fig:exampleBox},~\ref{fig:exampleIris} and
\ref{fig:exampleTraversal},~\ref{fig:exampleKaleidoscope}).

\par\subsection{Concepts of enriched category theory}

\par\begin{definition}[{{\citealp[\S1.2]{kelly05}}}]

A \Vt{category} \\(\C\\) consists of a set \\(\mathrm{Obj}(\C)\\) of objects,
a hom-object \\(\C(A,B)\in\V\\) for each pair of objects \\(A,B
\in\mathrm{Obj}(\C)\\), a composition law \\(\C(A,B) \times\C(B,C)
\to\C(A,C)\\) for each triple of objects, and an identity element \\(1
\to\C(A,A)\\) for each object; subject to the usual associativity and unit
axioms.

\end{definition}

\begin{code}

class Category objc c where

unit :: (objc x) => c x x

comp :: (objc x) => c y z -> c x y -> c x z

\end{code}

\par\begin{definition}[{{\citealp[\S1.2]{kelly05}}}]

A \Vt{functor} \\(F \colon\C\to\D\\) consists of a function \\(\Obj(\C)
\to\Obj(\D)\\) together with a map \\(\C(A,B) \to\D(FA,FB)\\) for each pair of
objects; subject to the usual compatibility with composition and units.
\Vt{bifunctors} and \Vt{profunctors} can be defined analogously,

\end{definition}

\begin{code}

class ( Category objc c, Category objd d

, forall x . objc x => objd (f x)

) => VFunctor objc c objd d f where

map :: (objc x, objc y) => c x y -> d (f x) (f y)

\parclass ( Category objc c, Category objd d, Category obje e

, forall x y . (objc x , objd y) => obje (f x y) )

=> Bifunctor objc c objd d obje e f where

bimap :: ( objc x1, objc x2, objd y1, objd y2 )

=> c x1 x2 -> d y1 y2 -> e (f x1 y1) (f x2 y2)

\parclass ( Category objc c, Category objd d )

=> Profunctor objc c objd d p where

dimap :: (objc x1, objc x2, objd y1, objd y2)

=> c x2 x1 -> d y1 y2 -> p x1 y1 -> p x2 y2

\end{code}

\par\begin{definition}[{{\citealp{day70}}}]

A monoidal \Vt{category} is a \Vt{category}

\\(\M\\) together with a \Vt{functor} \\((\otimes) \colon\M\otimes\M\to\M\\),
an object \\(I \in\M\\),

and \Vt{natural} isomorphisms \\(\alpha\colon(A \otimesB) \otimesC \congA
\otimes(B \otimesC)\\),

\\(\rho\colonA \otimesI \congA\\), and \\(\lambda\colonI \otimesA \congA\\),
satisfying the usual coherence axioms for a monoidal category.

\end{definition}

\begin{code}

class ( Category obja a

, Bifunctor obja a obja a obja a o

, obja i )

=> MonoidalCategory obja a o i where

alpha :: (obja x, obja y, obja z)

=> a (x ‘o‘ (y ‘o‘ z)) ((x ‘o‘ y) ‘o‘ z)

alphainv :: (obja x, obja y, obja z)

=> a ((x ‘o‘ y) ‘o‘ z) (x ‘o‘ (y ‘o‘ z))

lambda :: (obja x) => a (x ‘o‘ i) x

lambdainv :: (obja x) => a x (x ‘o‘ i)

rho :: (obja x) => a (i ‘o‘ x) x

rhoinv :: (obja x) => a x (i ‘o‘ x)

\end{code}

\par\begin{definition}

A strong monoidal \Vt{action} \\(F \colon\M\otimes\C\to\C\\) from a monoidal
\Vt{category} \\(\M\\) to an arbitrary category \\(\C\\) is a \Vt{functor}
together with two \Vt{natural} isomorphisms \\(F(I,X) \congX\\) and
\\(F(M,F(N,X))\congF((M \otimesN), X)\\) satisfying associativity and
unitality conditions.

\end{definition}

\begin{code}

class ( MonoidalCategory objm m o i

, Bifunctor objm m objc c objc c f

, Category objc c )

=> MonoidalAction objm m o i objc c f where

unitor :: (objc x) => c (f i x) x

unitorinv :: (objc x) => c x (f i x)

multiplicator :: (objc x, objm p, objm q)

=> c (f p (f q x)) (f (p ‘o‘ q) x)

multiplicatorinv :: (objc x, objm p, objm q)

=> c (f (p ‘o‘ q) x) (f p (f q x))

\end{code}

Definition~\ref{def:optic} has now a direct interpretation. Note how the coend
is modelled with an existential type arising from a \texttt{GADT}.

\begin{code}

data Optic objc c objd d objm m o i f g a b s t where

Optic :: ( MonoidalAction objm m o i objc c f

, MonoidalAction objm m o i objd d g

, objc a, objc s , objd b, objd t , objm x )

=> c s (f x a) -> d (g x b) t

-> Optic objc c objd d objm m o i f g a b s t

\end{code}

\par\subsection{Mixed profunctor optics}

\parWe can implement Tambara modules (Definition~\ref{def:tambara}) and
profunctor optics using the profunctor representation theorem
(Theorem~\ref{th:profrep}).

\begin{code}

class ( MonoidalAction objm m o i objc c f

, MonoidalAction objm m o i objd d g

, Profunctor objc c objd d p )

=> Tambara objc c objd d objm m o i f g p where

tambara :: (objc x, objd y, objm w)

=> p x y -> p (f w x) (g w y)

\partype ProfOptic objc c objd d objm m o i f g a b s t = forall p .

( Tambara objc c objd d objm m o i f g p

, MonoidalAction objm m o i objc c f

, MonoidalAction objm m o i objd d g

, objc a , objd b , objc s , objd t

) => p a b -> p s t

\end{code}

\parThe isomorphism between existential and profunctor optics can be
explicitly constructed from Lemma~\ref{lemma:doubleyoneda}.

\par\ignore{

\begin{code}

– The translation from profunctor to existential optics requires the

– following two isntances to be defined. The first one describes the

– representable copresheaves of the category of optics, that is,

– Optic(A,B,-,-).

instance ( MonoidalAction objm m o i objc c f

, MonoidalAction objm m o i objd d g

, objc a , objd b )

=> Profunctor objc c objd d (Optic objc c objd d objm m o i f g a b) where

dimap f g (Optic l r) = Optic (comp @objc @c l f) (comp @objd @d g r)

\par– The second one shows that these representable copresheaves are

– Tambara modules for their defining actions.

instance ( MonoidalAction objm m o i objc c f

, MonoidalAction objm m o i objd d g

, objc a , objd b )

=> Tambara objc c objd d objm m o i f g (Optic objc c objd d objm m o i f g a
b) where

tambara (Optic l r) = Optic

(comp @objc @c (multiplicator @objm @m @o @i @objc @c @f) (bimap @objm @m
@objc @c @objc @c (unit @objm @m) l))

(comp @objd @d (bimap @objm @m @objd @d @objd @d (unit @objm @m) r)
(multiplicatorinv @objm @m @o @i @objd @d @g))

\end{code}

}

\par\begin{code}

ex2prof :: forall objc c objd d objm m o i f g a b s t .

Optic objc c objd d objm m o i f g a b s t

-> ProfOptic objc c objd d objm m o i f g a b s t

ex2prof (Optic l r) =

dimap @objc @c @objd @d l r .

tambara @objc @c @objd @d @objm @m @o @i

\parprof2ex :: forall objc c objd d objm m o i f g a b s t .

( MonoidalAction objm m o i objc c f

, MonoidalAction objm m o i objd d g

, objc a , objc s

, objd b , objd t )

=> ProfOptic objc c objd d objm m o i f g a b s t

-> Optic objc c objd d objm m o i f g a b s t

prof2ex p = p (Optic

(unitorinv @objm @m @o @i @objc @c @f)

(unitor @objm @m @o @i @objd @d @g))

\end{code}

\par\subsection{Combinators}

\parAfter constructing optics, an implementation should provide ways of using
them. Many optics libraries, such as Kmett’s \emph{lens}~\cite{kmett15},
provide a vast range of combinators. Each of these combinators works on some
group of optics that share a common feature. For instance, we could consider
all the optics that implement a \hask{view} function, and create a single
combinator that lets us view the focus inside a family of optics.

\parThis may seem, at first glance, difficult to model. We do not know, a
priori, which of our optics will admit a given combinator. However, the fact
that Tambara modules are copresheaves over optics suggests that we can use
them to model ways of accessing optics; and in fact, we have found them to be
very satisfactory to describe combinators in their full generality.

\par\par\begin{remark}

As an example, for any fixed \\(A\\) and \\(B\\), consider the profunctor
\\(P_{A,B}(S,T) \coloneqq(S \toA)\\). It can be seen as modelling the
\hask{view} combinator that some optics provide.

\begin{spec}

newtype Viewing a b s t = Viewing { getView :: s -> a }

instance Profunctor Any (->) Any (->) (Viewing a b) where

dimap l _ (Viewing f) = Viewing (f . l)

\end{spec}

If we want to apply this combinator to a particular optic, we need it to be a
Tambara module for the actions describing the optic. For instance, we can show
that it is a Tambara module for the cartesian product, taking \\(\C= \D=
\M\\); this means it can be used with \emph{lenses} in the cartesian case. In
other words, \emph{lenses} can be used to \hask{view} the focus.

\begin{spec}

instance Tambara Any (->) Any (->) Any (->) (,) ()

(,) (,) (Viewing a b) where

tambara (Viewing f) = Viewing (f . snd)

\end{spec}

Optic combinators are usually provided as infix functions that interplay
nicely with the composition operator. Specifically, they have “fixity and
semantics such that subsequent field accesses can be performed with
\hask{Prelude..}”~\cite{kmett15}.

\begin{spec}

infixl 8 ^.

(^.) :: s -> (Viewing a b a b -> Viewing a b s t) -> a

(^.) s l = getView (l $ Viewing id) s

\end{spec}

\end{remark}

\par\ignore{

\begin{code}

– The following code implements instances for some common categories,

– bifunctors and monoidal actions.

\par– Empty constraint. Every type satisfies this constraint. This is

– useful to define categories where the objects are unconstrained.

class Any x

instance Any x

\par– A category modelled by Haskell types.

instance Category Any (->) where

unit = \x-> x

comp = \gf x -> g (f x)

\par– A category of applicative functors with natural transformations

– between them.

newtype Nat f g = Nat { nat :: forall x . f x -> g x }

\parinstance Category Functor Nat where

unit = Nat id

comp (Nat h) (Nat k) = Nat (h . k)

instance Category Applicative Nat where

unit = unit @Functor

comp = comp @Functor

instance Category Traversable Nat where

unit = unit @Functor

comp = comp @Functor

\parnewtype App f a = App { getApp :: f a }

\par– Instances for some common bifunctors.

instance Bifunctor Any (->) Any (->) Any (->) (,) where

bimap f g (x,y) = (f x , g y)

\parinstance Bifunctor Functor Nat Functor Nat Functor Nat Compose where

bimap (Nat h) (Nat k) = Nat (Compose . fmap k . h . getCompose)

instance Bifunctor Applicative Nat Applicative Nat Applicative Nat Compose
where

bimap = bimap @Functor @Nat @Functor @Nat @Functor @Nat @Compose

instance Bifunctor Traversable Nat Traversable Nat Traversable Nat Compose
where

bimap = bimap @Functor @Nat @Functor @Nat @Functor @Nat @Compose

\par\parinstance Bifunctor Any (->) Any (->) Any (->) Either where

bimap f _ (Left x) = Left (f x)

bimap _ g (Right x) = Right (g x)

\parinstance Bifunctor Functor Nat Any (->) Any (->) App where

bimap (Nat h) f = App . fmap f . h . getApp

instance Bifunctor Applicative Nat Any (->) Any (->) App where

bimap = bimap @Functor @Nat @Any @(->) @Any @(->) @App

instance Bifunctor Traversable Nat Any (->) Any (->) App where

bimap = bimap @Functor @Nat @Any @(->) @Any @(->) @App

\par– Instances for some common monoidal categories.

instance MonoidalCategory Any (->) (,) () where

alpha (x,(y,z)) = ((x,y),z)

alphainv ((x,y),z) = (x,(y,z))

lambda (x,_) = x

lambdainv x = (x,())

rho (_,x) = x

rhoinv x = ((),x)

\parinstance MonoidalCategory Any (->) Either Void where

alpha = either (Left . Left) (either (Left . Right) Right)

alphainv = either (either Left (Right . Left)) (Right . Right)

lambda = either (\x-> x) absurd

lambdainv = Left

rho = either absurd (\x-> x)

rhoinv = Right

\parinstance MonoidalCategory Functor Nat Compose Identity where

alpha = Nat (Compose . Compose . fmap getCompose . getCompose)

alphainv = Nat (Compose . fmap Compose . getCompose . getCompose)

lambda = Nat (fmap runIdentity . getCompose)

lambdainv = Nat (Compose . fmap Identity)

rho = Nat (runIdentity . getCompose)

rhoinv = Nat (Compose . Identity)

\parinstance MonoidalCategory Applicative Nat Compose Identity where

alpha = alpha @Functor @Nat @Compose @Identity

alphainv = alphainv @Functor @Nat @Compose @Identity

lambda = lambda @Functor @Nat @Compose @Identity

lambdainv = lambdainv @Functor @Nat @Compose @Identity

rho = rho @Functor @Nat @Compose @Identity

rhoinv = rhoinv @Functor @Nat @Compose @Identity

\parinstance MonoidalCategory Traversable Nat Compose Identity where

alpha = alpha @Functor @Nat @Compose @Identity

alphainv = alphainv @Functor @Nat @Compose @Identity

lambda = lambda @Functor @Nat @Compose @Identity

lambdainv = lambdainv @Functor @Nat @Compose @Identity

rho = rho @Functor @Nat @Compose @Identity

rhoinv = rhoinv @Functor @Nat @Compose @Identity

\parinstance MonoidalAction Functor Nat Compose Identity Any (->) App where

unitor = runIdentity . getApp

unitorinv = App . Identity

multiplicator = App . Compose . fmap getApp . getApp

multiplicatorinv = App . fmap App . getCompose . getApp

\parinstance MonoidalAction Applicative Nat Compose Identity Any (->) App
where

unitor = unitor @Functor @Nat @Compose @Identity @Any @(->) @App

unitorinv = unitorinv @Functor @Nat @Compose @Identity @Any @(->) @App

multiplicator = multiplicator @Functor @Nat @Compose @Identity @Any @(->) @App

multiplicatorinv = multiplicatorinv @Functor @Nat @Compose @Identity @Any
@(->) @App

\parinstance MonoidalAction Traversable Nat Compose Identity Any (->) App
where

unitor = unitor @Functor @Nat @Compose @Identity @Any @(->) @App

unitorinv = unitorinv @Functor @Nat @Compose @Identity @Any @(->) @App

multiplicator = multiplicator @Functor @Nat @Compose @Identity @Any @(->) @App

multiplicatorinv = multiplicatorinv @Functor @Nat @Compose @Identity @Any
@(->) @App

\par– Every V-monoidal action acts on itself via the monoidal product

instance (MonoidalCategory objm m o i) => MonoidalAction objm m o i objm m o
where

unitor = rho @objm @m

unitorinv = rhoinv @objm @m

multiplicator = alpha @objm @m @o @i

multiplicatorinv = alphainv @objm @m @o @i

\par\par– The Eilenberg-Moore category of algebras with algebra morphisms

– between them. The fact that the morphisms are algebra morphisms is

– not checked by the type-system. Most of the instances can then be

– directly copied from the category of types.

class (Monad m) => Algebra m a where

algebra :: m a -> a

\parinstance (Monad m) => Algebra m (m a) where

algebra = join

\parinstance (Monad m) => Category (Algebra m) (->) where

unit = unit @Any

comp = comp @Any

\parinstance (Monad m) => Bifunctor (Algebra m) (->) (Algebra m) (->) (Algebra
m) (->) (,) where

bimap = bimap @Any @(->) @Any @(->) @Any @(->)

\parinstance (Monad m) => Algebra m () where

algebra _ = ()

\parinstance (Monad m, Algebra m x, Algebra m y) => Algebra m (x,y) where

algebra u = (algebra $ fmap fst u, algebra $ fmap snd u)

\parinstance (Monad m) => MonoidalCategory (Algebra m) (->) (,) () where

alpha = alpha @Any @(->) @(,) @()

alphainv = alphainv @Any @(->) @(,) @()

lambda = lambda @Any @(->) @(,) @()

lambdainv = lambdainv @Any @(->) @(,) @()

rho = rho @Any @(->) @(,) @()

rhoinv = rhoinv @Any @(->) @(,) @()

\parinstance (Monad m) => Bifunctor (Algebra m) (->) Any (->) Any (->) (,)
where

bimap = bimap @Any @(->) @Any @(->) @Any @(->) @(,)

\parinstance (Monad m) => MonoidalAction (Algebra m) (->) (,) () Any (->) (,)
where

unitor = unitor @Any @(->) @(,) @() @Any @(->) @(,)

unitorinv = unitorinv @Any @(->) @(,) @() @Any @(->) @(,)

multiplicator = multiplicator @Any @(->) @(,) @() @Any @(->) @(,)

multiplicatorinv = multiplicatorinv @Any @(->) @(,) @() @Any @(->) @(,)

\par\par– FunLists are the free applicatives over Store functors. We

– implement the type-changing FunList.

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

\parinstance Functor (FunList s a) where

fmap f (Done b) = Done (f b)

fmap f (More s l) = More s (fmap (f .) l)

\par– This instance declaration can be seen, for instance, in Pickering,

– Gibbons, Wu.

instance Applicative (FunList s a) where

pure = Done

(Done f) <*> l’ = fmap f l’

(More x l) <*> l’ = More x (fmap flip l <*> l’)

\par\par– Kleisli categories of free algebras. The morphisms Kl(a,b) are

– written in the usual (a -> m b) form.

newtype Kleisli m a b = Kleisli { getKleisli :: (a -> m b) }

\parinstance (Monad m) => Category Any (Kleisli m) where

unit = Kleisli return

comp (Kleisli g) (Kleisli f) = Kleisli (join . fmap g . f)

\parinstance (Monad m) => Bifunctor Any (->) Any (Kleisli m) Any (Kleisli m)
(,) where

bimap f (Kleisli g) = Kleisli (\\(x,y) -> fmap ((,) (f x)) (g y))

\parinstance (Monad m) => MonoidalAction Any (->) (,) () Any (Kleisli m) (,)
where

unitor = unitor @Any @(->) @(,) @() @Any @(Kleisli m) @(,)

unitorinv = unitorinv @Any @(->) @(,) @() @Any @(Kleisli m) @(,)

multiplicator = multiplicator @Any @(->) @(,) @() @Any @(Kleisli m) @(,)

multiplicatorinv = multiplicatorinv @Any @(->) @(,) @() @Any @(Kleisli m) @(,)

\par\par– OPTICS

\par– Lenses are optics for the action of the category on itself via the

– cartesian product.

type Lens a s = ProfOptic Any (->) Any (->) Any (->) (,) () (,) (,) a a s s

mkLens :: (s -> a) -> (s -> a -> s) -> Lens a s

mkLens v u =

ex2prof @Any @(->) @Any @(->) @Any @(->) @(,) @()

$ Optic (\a-> (a , v a)) (\\(s,b) -> u s b)

\par– Prisms are optics for the action of the category on itself via the

– coproduct.

type Prism a s = ProfOptic Any (->) Any (->) Any (->) Either Void Either
Either a a s s

mkPrism :: (s -> Either s a) -> (a -> s) -> Prism a s

mkPrism m b =

ex2prof @Any @(->) @Any @(->) @Any @(->) @Either @Void

$ Optic m (either id b)

\par– Algebraic lenses are optics

type AlgebraicLens m a s = (Monad m) => ProfOptic Any (->) Any (->) (Algebra
m) (->) (,) () (,) (,) a a s s

mkAlgebraicLens :: forall m a s . (Monad m) => (s -> a) -> (m s -> a -> s) ->
AlgebraicLens m a s

mkAlgebraicLens v u =

ex2prof @Any @(->) @Any @(->) @(Algebra m) @(->) @(,) @()

$ Optic (\a-> (return a , v a)) (\\(ms,b) -> u ms b)

\partype Kaleidoscope a s = ProfOptic Any (->) Any (->) Applicative Nat
Compose Identity App App a a s s

mkKaleidoscope :: (([a] -> a) -> ([s] -> s)) -> Kaleidoscope a s

mkKaleidoscope f =

ex2prof @Any @(->) @Any @(->) @Applicative @Nat @Compose @Identity @App @App

$ Optic (App . flip More (Done id)) (uncurry (flip f) . noFun . getApp)

where

noFun :: FunList s a b -> ([s] , ([a] -> b))

noFun (Done b) = ([] , const b)

noFun (More s l) = (\\(u , f) -> (s:u , \\(h:t) -> f t h)) $ noFun l

\partype MonadicLens m a b s t = (Monad m) => ProfOptic Any (->) Any (Kleisli
m) Any (->) (,) () (,) (,) a b s t

mkMonadicLens :: forall m a b s t . (Monad m) => (s -> a) -> (s -> b -> m t)
-> MonadicLens m a b s t

mkMonadicLens v u =

ex2prof @Any @(->) @Any @(Kleisli m) @Any @(->) @(,) @() @(,) @(,)

$ Optic (\a-> (a , v a)) (Kleisli (uncurry u))

\par\par– Traversals as optics for the action of traversable functors.

type Traversal a s = ProfOptic Any (->) Any (->) Traversable Nat Compose
Identity App App a a s s

mkTraversal :: forall a b s t . (s -> [a]) -> ([a] -> s) -> Traversal a s

mkTraversal l r =

ex2prof @Any @(->) @Any @(->) @Traversable @Nat @Compose @Identity @App @App

$ Optic (App . l) (r . getApp)

\par\par– COMBINATORS

\par– The class of profunctors that admit the ’view’ operator.

newtype Viewing a b s t = Viewing { getView :: s -> a }

instance Profunctor Any (->) Any (->) (Viewing a b) where

dimap l _ (Viewing f) = Viewing (f . l)

\parinstance Tambara Any (->) Any (->) Any (->) (,) () (,) (,) (Viewing a b)
where

tambara (Viewing f) = Viewing (f . snd)

\parinstance (Monad m) => Tambara Any (->) Any (->) (Algebra m) (->) (,) ()
(,) (,) (Viewing a b) where

tambara = tambara @Any @(->) @Any @(->) @Any @(->) @(,) @()

\par– The class of profunctors that admit the ’preview’ operator.

newtype Previewing a b s t = Previewing { getPreview :: s -> Maybe a }

instance Profunctor Any (->) Any (->) (Previewing a b) where

dimap l _ (Previewing f) = Previewing (f . l)

\parinstance Tambara Any (->) Any (->) Any (->) (,) () (,) (,) (Previewing a
b) where

tambara (Previewing f) = Previewing (f . snd)

\parinstance Tambara Any (->) Any (->) Any (->) Either Void Either Either
(Previewing a b) where

tambara (Previewing f) = Previewing (either (\_ -> Nothing) f)

\par– The class of profunctors that admit the ’set’ operator.

newtype Setting a b s t = Setting { getSet :: (a -> b) -> (s -> t) }

instance Profunctor Any (->) Any (->) (Setting a b) where

dimap l r (Setting f) = Setting (\u-> r . f u . l)

\parinstance Tambara Any (->) Any (->) Any (->) (,) () (,) (,) (Setting a b)
where

tambara (Setting f) = Setting (\u(w,x) -> (w , f u x))

\parinstance Tambara Any (->) Any (->) Any (->) Either Void Either Either
(Setting a b) where

tambara (Setting f) = Setting (\u-> either Left (Right . f u))

\par– The class of profunctors that admit the ’classify’ operator.

newtype Classifying m a b s t = Classifying

{ getClassify :: (Monad m) => m s -> b -> t }

instance (Monad m) => Profunctor Any (->) Any (->) (Classifying m a b) where

dimap l r (Classifying f) = Classifying (\u-> r . f (fmap l u))

\parinstance (Monad m) => Tambara Any (->) Any (->) (Algebra m) (->) (,) ()
(,) (,) (Classifying m a b) where

tambara (Classifying f) = Classifying (\wb -> (algebra (fmap fst w) , f (fmap
snd w) b))

\par– The class of profunctors that admit the ’aggregate’ operator.

newtype Aggregating a b s t = Aggregate

{ getAggregate :: [s] -> ([a] -> b) -> t }

instance Profunctor Any (->) Any (->) (Aggregating a b) where

dimap l r (Aggregate f) = Aggregate (\vu -> r $ f (fmap l v) u)

\parinstance Tambara Any (->) Any (->) (Algebra []) (->) (,) () (,) (,)
(Aggregating a b) where

tambara (Aggregate u) = Aggregate (\lf -> (algebra (fmap fst l) , u (fmap snd
l) f))

\parinstance Tambara Any (->) Any (->) Applicative Nat Compose Identity App
App (Aggregating a b) where

tambara (Aggregate h) = Aggregate (\uf -> App $ pure (flip h f) <*> sequenceA
(fmap getApp u))

\par– The class of profunctors that admit the ’update’ operator.

newtype Updating m a b s t = Update

{ getUpdate :: (Monad m) => b -> s -> m t }

instance (Monad m) => Profunctor Any (->) Any (->) (Updating m a b) where

dimap l r (Update u) = Update (\bx -> fmap r (u b (l x)))

instance (Monad m) => Profunctor Any (->) Any (Kleisli m) (Updating m a b)
where

dimap l (Kleisli r) (Update u) = Update (\bx -> u b (l x) >>= r)

\parinstance (Monad m) => Tambara Any (->) Any (Kleisli m) (Any) (->) (,) ()
(,) (,) (Updating m a b) where

tambara (Update u) = Update (\b(w , x) -> fmap ((,) w) $ u b x)

\par– The class of profunctors that admit the ’over’ operator.

newtype Replacing a b s t = Replace

{ getReplace :: (a -> b) -> (s -> t) }

instance Profunctor Any (->) Any (->) (Replacing a b) where

dimap l r (Replace u) = Replace (\f-> r . u f . l)

\parinstance Tambara Any (->) Any (->) Any (->) (,) () (,) (,) (Replacing a b)
where

tambara (Replace u) = Replace (fmap . u)

instance Tambara Any (->) Any (->) Any (->) Either Void Either Either
(Replacing a b) where

tambara (Replace u) = Replace (fmap . u)

instance Tambara Any (->) Any (->) Functor Nat Compose Identity App App
(Replacing a b) where

tambara (Replace u) = Replace ((\f-> App . fmap f . getApp) . u)

instance Tambara Any (->) Any (->) Applicative Nat Compose Identity App App
(Replacing a b) where

tambara = tambara @Any @(->) @Any @(->) @Functor @Nat @Compose @Identity @App
@App @(Replacing a b)

instance Tambara Any (->) Any (->) Traversable Nat Compose Identity App App
(Replacing a b) where

tambara = tambara @Any @(->) @Any @(->) @Functor @Nat @Compose @Identity @App
@App @(Replacing a b)

\par\par– Inspired by the ”view” operator of Kmett et al’s lens library. The

– fixity and semantics are such that subsequent field accesses can be

– performed with ’Prelude..’.

infixl 8 ^.

(^.) :: s -> (Viewing a b a b -> Viewing a b s t) -> a

(^.) s l = getView (l $ Viewing id) s

\par– Inspired by the ”preview” operator of Kmett et al’s lens library. The

– fixity and semantics are such that subsequent field accesses can be

– performed with ’Prelude..’.

infixl 8 ?.

(?.) :: s -> (Previewing a b a b -> Previewing a b s t) -> Maybe a

(?.) s l = getPreview (l $ Previewing return) s

\par– Inspired by the ”set” operator of Kmett et al’s lens library. The

– fixity and semantics are such that subsequent field accesses can be

– performed with ’Prelude..’.

infixl 8 .~

(.~) :: (Setting a b a b -> Setting a b s t) -> b -> s -> t

(.~) l b = getSet (l $ Setting id) (\_ -> b)

\par– Inspired by the ”over” operator of Kmett et al’s lens library. The

– fixity and semantics are such that subsequent field accesses can be

– performed with ’Prelude..’.

infixl 8 ((\par– A ”classify” operator. The fixity and semantics are such that

– subsequent field accesses can be performed with ’Prelude..’.

infixl 8 .?

(.?) :: (Monad m) => (Classifying m a b a b -> Classifying m a b s t) -> b ->
m s -> t

(.?) l b ms = getClassify (l $ Classifying (\ab -> b)) ms b

\par– An ”aggregate” operator. The fixity and semantics are such that

– subsequent field accesses can be performed with ’Prelude..’.

infixl 8 >\-

(>-) :: (Aggregating a b a b -> Aggregating a b s t) -> ([a] -> b) -> [s] -> t

(>-) l = flip $ getAggregate (l $ Aggregate $ flip ($))

\par– An ”mupdate” operator. It is prepared to be used with do notation.

mupdate :: (Monad m) => (Updating m a b a b -> Updating m a b s t) -> b -> s
-> m t

mupdate f = getUpdate $ f (Update (\ba -> return b))

\par\par– EXAMPLE 1: Lenses and prisms.

data Address = Address

{ street’ :: String

, city’ :: String

, country’ :: String

} deriving (Show)

\parhome :: String

home = ”221b Baker St, London, UK”

\parstreet :: Lens String Address

street = mkLens street’ (\xy -> x {street’ = y})

\parcity :: Lens String Address

city = mkLens city’ (\xy -> x {city’ = y})

\paraddress :: Prism Address String

address = mkPrism matchPostal buildPostal

where

matchPostal :: String -> Either String Address

matchPostal a = maybe (Left a) Right $ do

(street, b) <- readUntil ’,’ a

(city, c) <- readUntil ’,’ (tail $ tail b)

return $ Address street city (tail $ tail c)

buildPostal :: Address -> String

buildPostal (Address s t c) = s ++ ”, ” ++ t ++ ”, ” ++ c

\parreadUntil :: Char -> String -> Maybe (String , String)

readUntil c a = if elem c a

then Just (takeWhile (/= c) a, dropWhile (/= c) a)

else Nothing

\par\par– EXAMPLE 2: Kaleidoscope and algebraic lenses

data Species = None | Setosa | Versicolor | Virginica | Mixed

\pardata Measurements = Measurements

{ sepalLe :: Float

, sepalWi :: Float

, petalLe :: Float

, petalWi :: Float

}

\pardata Flower = Flower

{ measurements :: Measurements

, species :: Species

}

\parinstance Show Flower where

show (Flower m s) = show s ++ ” ” ++ show m

\parinstance Show Species where

show None = ”No Species”

show Setosa = ”Iris Setosa”

show Versicolor = ”Iris Versicolor”

show Virginica = ”Iris Virginica”

\parinstance Show Measurements where

show (Measurements sl sw pl pw) =

”(” ++ show sl ++ ”, ” ++ show sw ++ ”, ”

++ show pl ++ ”, ” ++ show pw ++ ”)”

\par\parmeasure :: AlgebraicLens [] Measurements Flower

measure = mkAlgebraicLens @[] measurements learn

where

distance :: Measurements -> Measurements -> Float

distance (Measurements a b c d) (Measurements x y z w) =

sqrt . sum . fmap (**2) $ [a-x,b-y,c-z,d-w]

\parlearn :: [Flower] -> Measurements -> Flower

learn l m = Flower m $

species (minimumBy (compare ‘on‘ (distance m . measurements)) l)

\paraggregate :: Kaleidoscope Float Measurements

aggregate = mkKaleidoscope $ \fl -> Measurements

(f $ fmap sepalLe l)

(f $ fmap sepalWi l)

(f $ fmap petalLe l)

(f $ fmap petalWi l)

\parmean :: [Float] -> Float

mean l = (sum l) / (fromIntegral $ length l)

\pariris :: [Flower]

iris = [

Flower (Measurements 5.1 3.5 1.4 0.2) Setosa,

Flower (Measurements 4.9 3.0 1.4 0.2) Setosa,

Flower (Measurements 4.7 3.2 1.3 0.2) Setosa,

Flower (Measurements 4.6 3.1 1.5 0.2) Setosa,

Flower (Measurements 5.0 3.6 1.4 0.2) Setosa,

Flower (Measurements 5.4 3.9 1.7 0.4) Setosa,

Flower (Measurements 4.6 3.4 1.4 0.3) Setosa,

Flower (Measurements 5.0 3.4 1.5 0.2) Setosa,

Flower (Measurements 4.4 2.9 1.4 0.2) Setosa,

Flower (Measurements 4.9 3.1 1.5 0.1) Setosa,

Flower (Measurements 5.4 3.7 1.5 0.2) Setosa,

Flower (Measurements 4.8 3.4 1.6 0.2) Setosa,

Flower (Measurements 4.8 3.0 1.4 0.1) Setosa,

Flower (Measurements 4.3 3.0 1.1 0.1) Setosa,

Flower (Measurements 5.8 4.0 1.2 0.2) Setosa,

Flower (Measurements 5.7 4.4 1.5 0.4) Setosa,

Flower (Measurements 5.4 3.9 1.3 0.4) Setosa,

Flower (Measurements 5.1 3.5 1.4 0.3) Setosa,

Flower (Measurements 5.7 3.8 1.7 0.3) Setosa,

Flower (Measurements 5.1 3.8 1.5 0.3) Setosa,

Flower (Measurements 5.4 3.4 1.7 0.2) Setosa,

Flower (Measurements 5.1 3.7 1.5 0.4) Setosa,

Flower (Measurements 4.6 3.6 1.0 0.2) Setosa,

Flower (Measurements 5.1 3.3 1.7 0.5) Setosa,

Flower (Measurements 4.8 3.4 1.9 0.2) Setosa,

Flower (Measurements 5.0 3.0 1.6 0.2) Setosa,

Flower (Measurements 5.0 3.4 1.6 0.4) Setosa,

Flower (Measurements 5.2 3.5 1.5 0.2) Setosa,

Flower (Measurements 5.2 3.4 1.4 0.2) Setosa,

Flower (Measurements 4.7 3.2 1.6 0.2) Setosa,

Flower (Measurements 4.8 3.1 1.6 0.2) Setosa,

Flower (Measurements 5.4 3.4 1.5 0.4) Setosa,

Flower (Measurements 5.2 4.1 1.5 0.1) Setosa,

Flower (Measurements 5.5 4.2 1.4 0.2) Setosa,

Flower (Measurements 4.9 3.1 1.5 0.1) Setosa,

Flower (Measurements 5.0 3.2 1.2 0.2) Setosa,

Flower (Measurements 5.5 3.5 1.3 0.2) Setosa,

Flower (Measurements 4.9 3.1 1.5 0.1) Setosa,

Flower (Measurements 4.4 3.0 1.3 0.2) Setosa,

Flower (Measurements 5.1 3.4 1.5 0.2) Setosa,

Flower (Measurements 5.0 3.5 1.3 0.3) Setosa,

Flower (Measurements 4.5 2.3 1.3 0.3) Setosa,

Flower (Measurements 4.4 3.2 1.3 0.2) Setosa,

Flower (Measurements 5.0 3.5 1.6 0.6) Setosa,

Flower (Measurements 5.1 3.8 1.9 0.4) Setosa,

Flower (Measurements 4.8 3.0 1.4 0.3) Setosa,

Flower (Measurements 5.1 3.8 1.6 0.2) Setosa,

Flower (Measurements 4.6 3.2 1.4 0.2) Setosa,

Flower (Measurements 5.3 3.7 1.5 0.2) Setosa,

Flower (Measurements 5.0 3.3 1.4 0.2) Setosa,

Flower (Measurements 7.0 3.2 4.7 1.4) Versicolor,

Flower (Measurements 6.4 3.2 4.5 1.5) Versicolor,

Flower (Measurements 6.9 3.1 4.9 1.5) Versicolor,

Flower (Measurements 5.5 2.3 4.0 1.3) Versicolor,

Flower (Measurements 6.5 2.8 4.6 1.5) Versicolor,

Flower (Measurements 5.7 2.8 4.5 1.3) Versicolor,

Flower (Measurements 6.3 3.3 4.7 1.6) Versicolor,

Flower (Measurements 4.9 2.4 3.3 1.0) Versicolor,

Flower (Measurements 6.6 2.9 4.6 1.3) Versicolor,

Flower (Measurements 5.2 2.7 3.9 1.4) Versicolor,

Flower (Measurements 5.0 2.0 3.5 1.0) Versicolor,

Flower (Measurements 5.9 3.0 4.2 1.5) Versicolor,

Flower (Measurements 6.0 2.2 4.0 1.0) Versicolor,

Flower (Measurements 6.1 2.9 4.7 1.4) Versicolor,

Flower (Measurements 5.6 2.9 3.6 1.3) Versicolor,

Flower (Measurements 6.7 3.1 4.4 1.4) Versicolor,

Flower (Measurements 5.6 3.0 4.5 1.5) Versicolor,

Flower (Measurements 5.8 2.7 4.1 1.0) Versicolor,

Flower (Measurements 6.2 2.2 4.5 1.5) Versicolor,

Flower (Measurements 5.6 2.5 3.9 1.1) Versicolor,

Flower (Measurements 5.9 3.2 4.8 1.8) Versicolor,

Flower (Measurements 6.1 2.8 4.0 1.3) Versicolor,

Flower (Measurements 6.3 2.5 4.9 1.5) Versicolor,

Flower (Measurements 6.1 2.8 4.7 1.2) Versicolor,

Flower (Measurements 6.4 2.9 4.3 1.3) Versicolor,

Flower (Measurements 6.6 3.0 4.4 1.4) Versicolor,

Flower (Measurements 6.8 2.8 4.8 1.4) Versicolor,

Flower (Measurements 6.7 3.0 5.0 1.7) Versicolor,

Flower (Measurements 6.0 2.9 4.5 1.5) Versicolor,

Flower (Measurements 5.7 2.6 3.5 1.0) Versicolor,

Flower (Measurements 5.5 2.4 3.8 1.1) Versicolor,

Flower (Measurements 5.5 2.4 3.7 1.0) Versicolor,

Flower (Measurements 5.8 2.7 3.9 1.2) Versicolor,

Flower (Measurements 6.0 2.7 5.1 1.6) Versicolor,

Flower (Measurements 5.4 3.0 4.5 1.5) Versicolor,

Flower (Measurements 6.0 3.4 4.5 1.6) Versicolor,

Flower (Measurements 6.7 3.1 4.7 1.5) Versicolor,

Flower (Measurements 6.3 2.3 4.4 1.3) Versicolor,

Flower (Measurements 5.6 3.0 4.1 1.3) Versicolor,

Flower (Measurements 5.5 2.5 4.0 1.3) Versicolor,

Flower (Measurements 5.5 2.6 4.4 1.2) Versicolor,

Flower (Measurements 6.1 3.0 4.6 1.4) Versicolor,

Flower (Measurements 5.8 2.6 4.0 1.2) Versicolor,

Flower (Measurements 5.0 2.3 3.3 1.0) Versicolor,

Flower (Measurements 5.6 2.7 4.2 1.3) Versicolor,

Flower (Measurements 5.7 3.0 4.2 1.2) Versicolor,

Flower (Measurements 5.7 2.9 4.2 1.3) Versicolor,

Flower (Measurements 6.2 2.9 4.3 1.3) Versicolor,

Flower (Measurements 5.1 2.5 3.0 1.1) Versicolor,

Flower (Measurements 5.7 2.8 4.1 1.3) Versicolor,

Flower (Measurements 6.3 3.3 6.0 2.5) Virginica,

Flower (Measurements 5.8 2.7 5.1 1.9) Virginica,

Flower (Measurements 7.1 3.0 5.9 2.1) Virginica,

Flower (Measurements 6.3 2.9 5.6 1.8) Virginica,

Flower (Measurements 6.5 3.0 5.8 2.2) Virginica,

Flower (Measurements 7.6 3.0 6.6 2.1) Virginica,

Flower (Measurements 4.9 2.5 4.5 1.7) Virginica,

Flower (Measurements 7.3 2.9 6.3 1.8) Virginica,

Flower (Measurements 6.7 2.5 5.8 1.8) Virginica,

Flower (Measurements 7.2 3.6 6.1 2.5) Virginica,

Flower (Measurements 6.5 3.2 5.1 2.0) Virginica,

Flower (Measurements 6.4 2.7 5.3 1.9) Virginica,

Flower (Measurements 6.8 3.0 5.5 2.1) Virginica,

Flower (Measurements 5.7 2.5 5.0 2.0) Virginica,

Flower (Measurements 5.8 2.8 5.1 2.4) Virginica,

Flower (Measurements 6.4 3.2 5.3 2.3) Virginica,

Flower (Measurements 6.5 3.0 5.5 1.8) Virginica,

Flower (Measurements 7.7 3.8 6.7 2.2) Virginica,

Flower (Measurements 7.7 2.6 6.9 2.3) Virginica,

Flower (Measurements 6.0 2.2 5.0 1.5) Virginica,

Flower (Measurements 6.9 3.2 5.7 2.3) Virginica,

Flower (Measurements 5.6 2.8 4.9 2.0) Virginica,

Flower (Measurements 7.7 2.8 6.7 2.0) Virginica,

Flower (Measurements 6.3 2.7 4.9 1.8) Virginica,

Flower (Measurements 6.7 3.3 5.7 2.1) Virginica,

Flower (Measurements 7.2 3.2 6.0 1.8) Virginica,

Flower (Measurements 6.2 2.8 4.8 1.8) Virginica,

Flower (Measurements 6.1 3.0 4.9 1.8) Virginica,

Flower (Measurements 6.4 2.8 5.6 2.1) Virginica,

Flower (Measurements 7.2 3.0 5.8 1.6) Virginica,

Flower (Measurements 7.4 2.8 6.1 1.9) Virginica,

Flower (Measurements 7.9 3.8 6.4 2.0) Virginica,

Flower (Measurements 6.4 2.8 5.6 2.2) Virginica,

Flower (Measurements 6.3 2.8 5.1 1.5) Virginica,

Flower (Measurements 6.1 2.6 5.6 1.4) Virginica,

Flower (Measurements 7.7 3.0 6.1 2.3) Virginica,

Flower (Measurements 6.3 3.4 5.6 2.4) Virginica,

Flower (Measurements 6.4 3.1 5.5 1.8) Virginica,

Flower (Measurements 6.0 3.0 4.8 1.8) Virginica,

Flower (Measurements 6.9 3.1 5.4 2.1) Virginica,

Flower (Measurements 6.7 3.1 5.6 2.4) Virginica,

Flower (Measurements 6.9 3.1 5.1 2.3) Virginica,

Flower (Measurements 5.8 2.7 5.1 1.9) Virginica,

Flower (Measurements 6.8 3.2 5.9 2.3) Virginica,

Flower (Measurements 6.7 3.3 5.7 2.5) Virginica,

Flower (Measurements 6.7 3.0 5.2 2.3) Virginica,

Flower (Measurements 6.3 2.5 5.0 1.9) Virginica,

Flower (Measurements 6.5 3.0 5.2 2.0) Virginica,

Flower (Measurements 6.2 3.4 5.4 2.3) Virginica,

Flower (Measurements 5.9 3.0 5.1 1.8) Virginica]

\par\par– EXAMPLE 3: Updating with monadic lenses.