The n-Category Café

Lenses

The most obvious and famous data accessing pattern of this kind is a lens. The origin of lenses in category theory goes back to De Paiva’s Dialectica categories and Oles’ store shapes. Since then, they have appeared on wiring diagrams, supervised learning and compositional game theory; you can read Hedges’ blog post for a history of lenses. Their use as data accessors is described by Pickering, Gibbons and Wu.

In functional programming, a lens between two pairs of types $(S,T)$ and $(A,B)$ consists of two functions $S \to A$ and $S \times B \to T$. We interpret $S$ as the type for the original record; $T$ is the type of the the updated record; $A$ is the type of the part of $S$ to be updated; $B$ is the type of the data that will replace $A$; the function $S \to A$ is the view function; and $S \times B \to T$ is the update.

In a cartesian category $\mathbf{C}$, a lens from a pair of objects $(S,T)$ to a pair of objects $(A,B)$ is given by two morphisms: a view $\mathbf{C}(S , A)$, and an update $\mathbf{C}(S \times B , T)$.

$$\mathbf{Lens} \left( \binom{S}{T}, \binom{A}{B} \right) = \mathbf{C}(S , A) \times \mathbf{C}(S \times B , T).$$

Example: suppose we have a data structure (or a set) representing postal addresses, with the ZIP code being a subfield of any postal address. We want to be able to view the ZIP code inside an address and to modify it, creating a new address. This can be encoded as a lens.

$$\begin{aligned} \mathrm{viewZipCode} \colon & \mathbf{Postal} \to \mathbf{Zip} \\ \mathrm{updateZipCode} \colon & \mathbf{Postal} \times \mathbf{Zip} \to \mathbf{Postal} \end{aligned}$$

Or, in Haskell notation,

viewZip   :: Postal            -> ZipCode
updateZip :: (Postal, ZipCode) -> Postal

Lenses are optics, but not all optics are necessarily lenses. Let us describe other families of optics.

Prisms

As with product types, there is an optic for viewing and updating with sums, called a prism. In functional programming, a prism between two pairs of types $(S,T)$ and $(A,B)$ consists of two functions $S \to A + T$ and $B \to T$. We interpret $S$ as the type for the original, possibly more abstract, data structure; $T$ is the type of its updated version; $A$ is the type of some concrete form $S$ can take; and $B$ is the type that will replace $A$. The function $S \to A + T$ is called a match function and the $B \to T$ is a build function. You can skip the following definition if you note that prisms are precisely lenses in the opposite category.

In a cocartesian category $\mathbf{C}$, a prism from a pair of objects $(S,T)$ to a pair of objects $(A,B)$ is given by two morphisms: a match $S \to A + T$ representing pattern-matching on $A$, and a build $B \to T$ representing the construction of the data structure from one of the alternatives.

$$\mathbf{Prism} \left( \binom{S}{T}, \binom{A}{B} \right) = \mathbf{C}(S , T + A) \times \mathbf{C}(B , T).$$

Example: suppose we have a data structure representing an abstract address. An address is, alternatively, an email address or a postal address like in the previous example. We can try to extract a postal address from a string, returning an abstract address if it fails to match the shape of a postal address. We have also an inclusion of postal addresses into addresses. This can be encoded as a prism.

$$\begin{aligned} \mathrm{matchAddress} \colon & \mathbf{String} \to \mathbf{Address} + \mathbf{Postal} \\ \mathrm{buildAddress} \colon & \mathbf{Postal} \to \mathbf{Address} \end{aligned}$$

In Haskell notation, the example reads as follows.

matchAddress :: String -> Either Address Postal
buildAddress :: Postal -> Address

Traversals

We can go further: optics do not necessarily need to deal with a single focus. Traversals are optics that access a list of foci at the same time. A traversal between two pairs of types $(S,T)$ and $(A,B)$ consists of a single function $S \to \sum_{n \in \mathbb{N}} A^n \times (B^n \to T)$. We again interpret $S$ as the original data structure, that is transformed into $T$ when we replace a list of elements of type $A$ with an equal-length list of elements of type $B$.

In a cartesian closed category with limits and colimits indexed by natural numbers, $\mathbf{C}$, a traversal from a pair of sets $(S,T)$ to $(A,B)$ is given by a single morphism: an extract $\mathbf{C}(S , \sum_{n \in \mathbb{N}} A^n \times (B^n \to T))$ that represents extracting a list of some length and a function that takes a list of the same size to create a new structure. $$\mathbf{Traversal} \left( \binom{S}{T},\binom{A}{B} \right) = \mathbf{C}\left(S , \sum_n A^n \times (B^n \to T)\right).$$

One would think that the traversal can be rewritten in the same style as a lens: that is, as two functions consisting of a get $S \to A^n$ and a put $S \times B^n \to T$. However, the fact that both $n$ must be the same prevents us from writing traversals as a pair of two different functions. This is also what makes a traversal fundamentally different from a lens focusing on a list or tuple type. For the traversal, the length of the output can vary, but we need a list of that same length in each case to be able to update.

Example: suppose we have now a mailing list containing multiple email addresses associated to other data, such as names or subscription options. An accessor for the email addresses is a traversal given by a single function with the following signature:

$$\begin{aligned} \mathrm{extract} \colon & \mathbf{MailList} \to \sum_{n \in \mathbb{N}} \mathbf{Email}^n \times \left(\mathbf{Email}^n \to \mathbf{MailList}\right). \end{aligned}$$

Note that in Haskell we cannot encode the restriction on length without dependent types.

extract :: MailList -> ([Email], [Email] -> MailList)

The problem of modularity

Writing functions as above is not especially difficult. The problem arises when we want to compose multiple accessors to form a new, valid one. For example, we have an accessor that maybe gets a PostalAddress from a given address, and we also have an accessor that gets the ZipCode of the PostalAddress. How can we get an accessor that maybe gets us the ZipCode directly from any Address if it happens to be a PostalAddress?

-- We have these functions.
getPostal :: Address    -> Either Address PostalAddr
setPostal :: PostalAddr -> Address
getZip    :: PostalAddr -> ZipCode
setZip    :: (PostalAddr, ZipCode) -> PostalAddr

-- And we want the following composition.
getZipFromAddr :: Address            -> Either Address ZipCode
setZipAddr     :: (Address, ZipCode) -> Address

The naive solution is not particularly difficult to write, but it adds unnecessarily complex boilerplate code that is difficult to maintain. Moreover, the resulting accessor need not be a lens or a prism. Explicitly, in a bicartesian closed category, assume we have a prism given by $m \in \mathbf{C}(S, T + A)$ and $l \in \mathbf{C}(B,T)$, and a lens given by $v \in \mathbf{C}(A,X)$ and $u \in \mathbf{C}(A \times Y , B)$. We want to compose them into a combined optic from $(S,T)$ to $(X,Y)$. The following would be a suitable composition, although it is tedious to write and not particularly illuminating. Here, we call $\Lambda$ to the product-exponent adjunction (the currying of a morphism).

$$[ \mathrm{id}_T , v \times \Lambda(l \circ u)] \circ m \in \mathbf{C}(S , T + X \times T^Y).$$

Note that $\Lambda(l \circ u) \in \mathbf{C}(A, T^Y)$, and the rest is just a combination of morphisms that uses the product and the coproduct. This approach to composition is not practical: we would need to write down a composition for every pair of optics, and its output could be each time a completely new optic.

This problem is solved using profunctor optics, which we will formally define in the next section. Perhaps surprisingly, some kinds of data accessors have an equivalent formulation in terms of functions that are polymorphic over certain classes of profunctors. For instance, we say that $P \colon \mathbf{C}^{op} \times \mathbf{C} \to \mathbf{Sets}$ is a cartesian profunctor if it is equipped with a natural transformation $\alpha_{C,(A,B)} \colon P(A,B) \to P(C \times A , C \times B)$ such that $\alpha_1 = \mathrm{id}$ and $\alpha_{C_1 \times C_2} = \alpha_{C_1} \circ \alpha_{C_2}$, up to the isomorphisms provided by the unitor and distributor of the cartesian product. All the information that goes into a lens can be encoded into an end over a category $\mathbf{Cartesian}$ of cartesian profunctors; that is,

$$\mathbf{C}(S , A) \times \mathbf{C}(S \times B , T) \cong \int_{P \in \mathbf{Cartesian}} \mathbf{Sets}(P(A,B), P(S,T)).$$

This is convenient because, even if they are equivalent, composition of optics in this representation becomes ordinary function composition.

Example

Assume we have already defined the prism as previously shown (matching a string in a postal address) and the lenses that access the subfields of a postal address. In this example,

1. we input a string;
2. we match it into a postal address using the prism;
3. we compose the prism with a lens, using just function composition in Haskell, to access the street inside the address;
4. update the street with a new value;
5. apply a function to the city part of the postal address.

That is, with this representation, we do not need to worry anymore about boilerplate functions polluting our code. This poses two main questions: first, why and how does this work? and secondly, can we have a unified profunctor representation for some definition of optic?

The existential encoding of optics

A first approximation to the general definition of optic can be found in Milewski’s 2017 post At first, the definition there encompasses only the case where the action is given by (the currying of) a monoidal product $\otimes \colon \mathbf{C} \to [ \mathbf{C} , \mathbf{C} ]$; but towards the end, this is extended to any action given by an inclusion $\mathbf{F} \to [ \mathbf{C} , \mathbf{C} ]$ of some subcategory of endofunctors $\mathbf{F}$. After this, a definition of optic can be found, with slight differences, both in Boisseau and Gibbons’ “What you needa know about Yoneda: Profunctor Optics and the Yoneda Lemma (Functional Pearl)” and in Riley’s “Categories of optics”.

We say that an action of a monoidal category $\mathbf{M}$ on an arbitrary category $\mathbf{C}$ is a strong monoidal functor $\mathbf{M} \to [ \mathbf{C} , \mathbf{C} ]$. In other words, actions are the objects of the slice category $\mathbf{MonCat}/[ \mathbf{C} , \mathbf{C} ]$; and we can consider morphisms between them to be commutative triangles there. Considering that monoidal categories are pseudomonoids in $\mathbf{Cat}$, this is to say that these actions are vertical categorifications of the notion of a monoid action. Associated to any action, we can define an optic as follows.

Definition (from Riley, 2018). Let $(\underline{\phantom{a}}) \colon \mathbf{M} \to [ \mathbf{C} , \mathbf{C} ]$ be a strong monoidal functor and let $S,T,A,B \in \mathbf{C}$. An optic from $(S,T)$ to $(A,B)$ is an element of the following set described as a coend. $$\mathbf{Optic}\left(\binom{S}{T},\binom{A}{B}\right) = \int^{M \in \mathbf{M}} \mathbf{C}(S, \underline{M} A) \times \mathbf{C}(\underline{M} B, T).$$

An intuition for this definition is that the bigger structure, $S$, can be decomposed into the focus, $A$, and some context, $M$, acting on it. We cannot access the context because of the dinaturality of the coend. However, we can use the context to update the original data structure, replacing the current focus by a new element.

It can be shown directly that $\mathbf{Optic}$ can be given the structure of a category, as done by Riley. For our purposes, we will abstain until we reach the section regarding the profunctor representation theorem below so that we can describe $\mathbf{Optic}$ as a particular subcategory of a Kleisli category.

Lenses, prisms, grates and traversals are optics

The definition of optic that we have just given actually captures our motivating examples. We will show that the action of the cartesian product gives lenses, the coproduct gives prisms and the action of functors that can be written as a power series gives traversals. In all of these cases, we will be using the Yoneda lemma to integrate over the coend.

Proposition (from Milewski, 2017). Lenses are optics for the cartesian product.

$\Bigg\{$ $\Bigg\} \cong \Bigg\{$ $\Bigg\}$

$$\begin{aligned} & \int^{C \in \mathbf{C}} \mathbf{C}(S , C \times A) \times \mathbf{C}(C \times B , T) \\ \cong & \qquad{(Product)} \\ & \int^{C \in \mathbf{C}} \mathbf{C}(S , C) \times \mathbf{C}(S , A) \times \mathbf{C}(C \times B , T) \\ \cong & \qquad{\text{(Yoneda lemma)}} \\ & \mathbf{C}(S , A) \times \mathbf{C}(S \times B , T). \end{aligned}$$

Proposition (from Milewski, 2017). Dually, prisms are optics for the cocartesian coproduct.

$\Bigg\{$ $\Bigg\} \cong \Bigg\{$ $\Bigg\}$

$$\begin{aligned} & \int^{C \in \mathbf{C}} \mathbf{C}(S , C + A) \times \mathbf{C}(C + B , T) \\ \cong &\qquad{(Coproduct)} \\ & \int^{C \in \mathbf{C}} \mathbf{C}(S , C + A) \times \mathbf{C}(C , T) \times \mathbf{C}(B , T) \\ \cong &\qquad{\text{(Yoneda lemma)}} \\ & \mathbf{C}(S , T + A) \times \mathbf{C}(B , T). \end{aligned}$$

The final example from Milewski’s blog post requires an action that is not a monoidal product. In a cartesian closed category $\mathbf{C}$, grates from $(S,T)$ to $(A,B)$ are defined as follows, where we use $(\to)$ for the exponential. $$\mathbf{Grate}\left( \binom{S}{T}, \binom{A}{B}\right) = \mathbf{C}((S \to A) \to B, T).$$

Proposition (from Milewski, 2017). Grates are optics for the action of the exponential $( \to ) \colon \mathbf{C}^{op} \to [ \mathbf{C} , \mathbf{C} ]$.

$$\begin{aligned} & \int^{C \in \mathbf{C}^{op}} \mathbf{C}(S , C \to A) \times \mathbf{C}(C \to B , T) \\ \cong & \qquad{\text{(Product-exponential adjunction, and symmetry of the product)}} \\ & \int^{C \in \mathbf{C}^{op}} \mathbf{C}(C , S \to A) \times \mathbf{C}(C \to B , T) \\ \cong & \qquad{(Yoneda)} \\ & \mathbf{C}((S \to A) \to B, T). \end{aligned}$$

This was also interesting because grates are a clear example where indexing category, $\mathbf{C}^{op}$, is not the same as the base category $\mathbf{C}$; and the action is not given by a monoidal product.

Our group’s first goal during this [ACT Adjoint School 2019][act] was to come up with a derivation of the traversal as elementary as possible; and the following is the result of that joint work. Using Yoneda over the category of functors from the discrete category of natural numbers, $[\mathbb{N} , \mathbf{C}]$, we show that traversals are optics for the action that takes any of these functors $C \colon \mathbb{N} \to \mathbf{C}$ into the functor $\mathbf{Poly}(C) \colon \mathbf{C} \to \mathbf{C}$ given by $\mathbf{Poly}(C)(A) = \sum_{n \in \mathbb{N}} C_n \times A^n$. Functors of this form are called polynomial functors in a single variable by Gambino and Kock, or L-species. The monoidal product in $[\mathbb{N} , \mathbf{C}]$ is given by substitution of polynomials and it can be seen as an instance of Faà di Bruno’s formula. That is, $\sum_n C_n \times \left( \sum_m D_m \times X^m \right)^n \cong \sum_n E_n \times X^n$, where $$E_n = \sum_{n = \sum^k_{j=1} m_j} C_k \times \prod^k_{j=1} D_{m_j}$$ with the first sum ranging over all partitions of $n$ as a sum of natural numbers.

$\Bigg\{$ $\Bigg\} \cong \Bigg\{$ $\Bigg\}$

Proposition. Traversals are optics for this power series action $\mathbf{Poly} \colon [\mathbb{N}, \mathbf{C}] \to [\mathbf{C}, \mathbf{C}]$. $$\begin{aligned} & \int^{C \in [ \mathbb{N} , \mathbf{C} ]} \mathbf{C} \left( S , \sum_{n \in \mathbb{N}} C_n \times A^n \right) \times \mathbf{C}\left( \sum_{n \in \mathbb{N}} C_n \times B^n , T\right) \\ \cong & \qquad{(Cocontinuity)} \\ & \int^{C \in [ \mathbb{N} , \mathbf{C} ]} \mathbf{C} \left( S , \sum_{n \in \mathbb{N}} C_n \times A^n \right) \times \prod_{n \in \mathbb{N}} \mathbf{C}\left( C_n \times B^n , T\right) \\ \cong & \qquad{\text{(Adjunction for the exponential)}} \\ & \int^{C \in [ \mathbb{N} , \mathbf{C} ]} \mathbf{C} \left(S , \sum_{n \in \mathbb{N}} C_n \times A^n \right) \times \prod_{n \in \mathbb{N}} \mathbf{C}\left( C_n , B^n \to t\right) \\ \cong & \qquad{\text{(Natural transformation as an end)}}\\ & \int^{C \in [ \mathbb{N} , \mathbf{C} ]} \mathbf{C} \left(S , \sum_{n \in \mathbb{N}} C_n \times A^n \right) \times [ \mathbb{N} , \mathbf{C} ] \left( C_{(-)} , B^{(-)} \to t\right) \\ \cong & \qquad{\text{(Yoneda lemma)}} \\ & \mathbf{C} \left( S, \sum_{n \in \mathbb{N}} A^n \times (B^n \to T) \right). \end{aligned}$$

We also studied how to directly relate this to the usual encoding of profunctor traversals using traversable functors: these that come with a distributive law for every lax monoidal functor for the product. That derivation was described by Riley relying on a result by Jaskelioff and O’Connor. That discussion is, however, outside the scope of this post.

The profunctor encoding

The profunctor representation of optics is based on a generalization of Tambara modules. The original definition, and the one used by Pastro and Street in Doubles for Monoidal Categories, only concerns monoidal products; but both the definition and the main results can be replicated for arbitrary monoidal actions. Let $(\mathbf{M}, \otimes, I)$ be a monoidal category and $(\underline{\phantom{A}}) \colon \mathbf{M} \to [ \mathbf{C} , \mathbf{C} ]$ a strong monoidal functor with structure morphisms $\phi_{M,N} \colon \underline{M} \circ \underline{N} \cong \underline{M \otimes N}$ and $\phi_{I} \colon \mathrm{id} \cong \underline{I}$.

Definition. A (generalized) Tambara module consists of a profunctor $P \colon \mathbf{C}^{op} \times \mathbf{C} \to \mathbf{Sets}$ endowed with a family of morphisms $\alpha(M)_{A,B} \colon P(A,B) \to P(\underline{M} A , \underline{M} B)$ natural in both $A,B \in \mathbf{C}$ and dinatural on $M \in \mathbf{M}$, which additionally satisfy the two equations

$$\alpha(I) = P(\phi_{I}^{-1},\phi_{I})\quad and \quad\alpha(M \otimes N) = P(\phi_{M,N}^{-1},\phi_{M,N}) \circ \alpha(M) \circ \alpha(N).$$

In Doubles for Monoidal Categories, Pastro and Street show that Tambara modules are equivalently coalgebras for a comonad $\Theta \colon [\mathbf{C}^{op} \times \mathbf{C} , \mathbf{Sets}] \to [\mathbf{C}^{op} \times \mathbf{C} , \mathbf{Sets}]$ defined as

$$\Theta(P)(A,B) = \int_{M \in \mathbf{M}} P(\underline{M}A, \underline{M}B).$$

This observation entails that we can consider coalgebra homomorphisms and define the category of Tambara modules, $\mathbf{Tamb}_{\mathbf{M}}$, as the Eilenberg-Moore category for $\Theta$. The $\Theta$ comonad precomposes both components with the image of $M \in \mathbf{M}$ and takes an end; from this description, it can be seen that it has a left adjoint

$$\int^{M \in \mathbf{M}} \mathsf{Lan}_{(\underline{M},\underline{M})} (-) \dashv \int_{M \in \mathbf{M}} (-) \circ (\underline{M} , \underline{M}),$$

which must be a monad. More explicitly, the monad $\Psi \colon [\mathbf{C}^{op} \times \mathbf{C} , \mathbf{Sets}] \to [\mathbf{C}^{op} \times \mathbf{C} , \mathbf{Sets}]$ acts on a profunctor $Q \colon \mathbf{C} \times \mathbf{C}^{op} \to\mathbf{Sets}$ as

$$\Psi(Q)(X,Y) = \int^{M \in \mathbf{M}}\int^{U,V \in \mathbf{C}} \mathbf{C}(X, \underline{M}U) \times \mathbf{C}(\underline{M}V,Y) \times Q(U,V)$$

and the adjunction can be computed as follows for any given $P,Q \colon \mathbf{C}^{op} \times \mathbf{C} \to \mathbf{Sets}$.

$$\begin{aligned} & Q \Rightarrow \Theta P \\ \cong & \qquad{\text{(Natural transformation as an end)}} \\ & \int_{(A,B) \in \mathbf{C}^{op} \times \mathbf{C}} \mathbf{Sets}(Q(A,B) , \Theta P (A,B)) \\ \cong & \qquad{\text{(Fubini rule)}} \\ & \int_{A,B \in \mathbf{C}} \mathbf{Sets}(Q(A,B) , \Theta P (A,B)) \\ \cong & \qquad{\text{(Definition of } \, \Theta \text{)}} \\ & \int_{A,B \in \mathbf{C}} \mathbf{Sets} \left(Q(A,B), \int_{M \in \mathbf{M}}P(\underline{M}A,\underline{M}B)\right) \\ \cong & \qquad{\text{(Continuity of the end)}} \\ & \int_{A,B \in \mathbf{C}} \int_{M \in \mathbf{M}} \mathbf{Sets}(Q(A,B), P (\underline{M}A,\underline{M}B)) \\ \cong & \qquad{\text{(Fubini rule)}} \\ & \int_{M \in \mathbf{M}} \int_{A,B \in \mathbf{C}} \mathbf{Sets}(Q(A,B), P(\underline{M}A,\underline{M}B)) \\ \cong & \qquad{\text{(Yoneda lemma, in the category } \, \mathbf{C}^{op}\times \mathbf{C} \text{)}} \\ & \int_{M \in \mathbf{M}} \int_{A,B \in \mathbf{C}} \mathbf{Sets} \left( Q(A,B) , \int_{X,Y \in \mathbf{C}} \mathbf{Sets} (\mathbf{C}(X,\underline{M}A) \times \mathbf{C}(\underline{M}B,Y) , P(X,Y)) \right) \\ \cong & \qquad{\text{(Continuity of the end)}} \\ & \int_{M \in \mathbf{M}} \int_{A,B \in \mathbf{C}} \int_{X,Y \in \mathbf{C}} \mathbf{Sets} \left( Q(A,B) , \mathbf{Sets} (\mathbf{C}(X,\underline{M}A) \times \mathbf{C}(\underline{M}B,Y) , P(X,Y)) \right) \\ \cong & \qquad{(Currying)} \\ & \int_{M \in \mathbf{M}} \int_{A,B \in \mathbf{C}} \int_{X,Y \in \mathbf{C}} \mathbf{Sets}(Q(A,B) \times \mathbf{C}(X,\underline{M}A) \times \mathbf{C}(\underline{M}B,Y), P(X,Y)) \\ \cong & \qquad{\text{(Fubini rule)}} \\ & \int_{X,Y \in \mathbf{C}} \int_{A,B \in \mathbf{C}} \int_{M \in \mathbf{M}} \mathbf{Sets}(Q(A,B) \times \mathbf{C}(X,\underline{M}A) \times \mathbf{C}(\underline{M}B,Y), P(X,Y)) \\ \cong & \qquad{\text{(Cocontinuity of the coend)}} \\ & \int_{X,Y \in\mathbf{C}} \mathbf{Sets} \left( \int^{M \in \mathbf{M}}\int^{A,B \in \mathbf{C}} Q(A,B) \times \mathbf{C}(X,\underline{M}A) \times \mathbf{C}(\underline{M}B,Y) , P(X,Y) \right) \\ \cong & \qquad{\text{(Definition of } \, \Psi \text{)}} \\ & \int_{X,Y \in \mathbf{C}} \mathbf{Sets}(\Psi Q(X,Y), P(X,Y)) \\ \cong & \qquad{\text{(Natural transformation as an end)}} \\ & \Psi Q \Rightarrow P. \end{aligned}$$

With this in mind, we can go back to the formula for profunctor optics and realize that profunctor optics are exactly optics. The statement of this profunctor representation theorem is the existence of an isomorphism

$$\int_{P \in \mathbf{Tamb}} \mathbf{Sets}(P(A,B) , P(S,T)) \cong \int^{M \in \mathbf{M}} \mathbf{C}(S, \underline{M}A) \times \mathbf{C}(\underline{M}B, T),$$

natural on $A,B,S,T \in \mathbf{C}$. The proof is again a sample of coend-fu. This corresponds to the Yoneda with adjunction described in the original blog post.

$$\begin{aligned} & \int_{P \in \mathbf{Tamb}} \mathbf{Sets}(P(A,B), P(S,T)) \\ \cong & \qquad{\text{(Yoneda lemma)}} \\ & \int_{P \in \mathbf{Tamb}} \mathbf{Sets}\left(\mathrm{Nat}(y_{(A,B)}, P) , P(S,T) \right) \\ \cong & \qquad{\text{(Free-forgetful adjunction for Tambara modules)}} \\ & \int_{P \in \mathbf{Tamb}} \mathbf{Sets}\left( \mathbf{Tamb}(\Psi y_{(A,B)}, P) , P(S,T) \right) \\ \cong & \qquad{\text{(Yoneda lemma)}} \\ & \Psi y_{(A,B)}(S,T) \\ \cong & \qquad{\text{(Definition of } \,\Psi \text{)}} \\ & \int^{M \in \mathbf{M}} \int^{x,y \in \mathbf{C}} \mathbf{C}(S,\underline{M}X) \times \mathbf{C}(\underline{M}Y, T) \times y_{(A,B)}(X,Y) \\ \cong & \qquad{\text{(Yoneda lemma)}} \\ & \int^{M \in \mathbf{M}} \mathbf{C}(S,\underline{M}A) \times \mathbf{C}(\underline{M}B, T)\\ \cong & \qquad{(Definition)} \\ & \mathbf{Optic}\left(\binom{S}{T},\binom{A}{B}\right). \end{aligned}$$

In fact, we can stop midway there and say that an optic for an action is an element of $\Psi y_{(A,B)}(S,T)$, which is, again by Yoneda lemma, the same as a natural transformation $y_{(S,T)} \Rightarrow \Psi y_{(A,B)}$. That is, we could have defined our category of optics to be the full subcategory of representable functors of the Kleisli category for the monad $\Psi$ on the category of profunctors.

We have tried to provide a geodesic path to the proof of the profunctor representation theorem, but the proof proposed in Pastro-Street is slightly different. From that proof, is interesting to remark that we have an identity on objects functor $\mathbf{C}^{op} \times \mathbf{C} \to \mathbf{Optic}$, which is the same as having a promonad, a monoid in the category of endoprofunctors, $\check{\Phi} \colon \mathbf{C}^{op} \times \mathbf{C} \nrightarrow\mathbf{C}^{op} \times \mathbf{C}$, whose Kleisli object is $\mathbf{Optic}$. From the universal property of the Kleisli object, it follows that copresheaves over $\mathbf{Optic}$ are equivalent to modules over that promonad, and it can be shown that these are precisely Tambara modules.

Profunctor optics

Understanding the profunctor representation theorem solves the mystery of the profunctor encoding. The following equivalences are all corollaries of this theorem.

Lenses are optics for the action of a cartesian category $\mathbf{C}$ on itself by the product $(\times) \colon \mathbf{C} \times \mathbf{C} \to \mathbf{C}$ interpreted as $(\times) \colon \mathbf{C} \to [\mathbf{C} , \mathbf{C}]$. That means that they can be written as functions parametric over Tambara modules for the product. We get our motivating result applying the profunctor representation theorem.

$$\mathbf{C}(S , A) \times \mathbf{C}(S \times B,T) \cong \int_{P \in \mathbf{Tamb}(\times)} \mathbf{Sets}(P(A,B) , P(S,T)).$$

Because of this, the following definition is used in Haskell. Note that profunctors endowed with a Tambara module structure for the product are called cartesian profunctors, or strong profunctors in the lens library.

class Strong p where
  strong :: p a b -> p (c,a) (c,b)

type Lens s t a b = forall p. Strong p => p a b -> p s t

Prisms are optics for the coproduct $(+) \colon \mathbf{C} \times \mathbf{C} \to \mathbf{C}$. That means that they can be represented by functions parametric over Tambara modules for the coproduct.

$$\mathbf{C}(S, A + T) \times \mathbf{C}(B,T) \cong \int_{P \in \mathbf{Tamb}(+)} \mathbf{Sets}(P(A,B), P(S,T)).$$

The same applies for them. Note that these Tambara modules were called in Haskell libraries cocartesian profunctors or choice profunctors.

class Choice p where
  choice :: p a b -> p (Either c a) (Either c b)

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

Grates are optics for the action of the exponential $(\to) \colon \mathbf{C}^{op} \times \mathbf{C} \to \mathbf{C}$. That means that they can be represented by Tambara modules for the exponential.

$$\mathbf{C}((S \to A) \to B, T) \cong \int_{P \in \mathbf{Tamb}(\to)} \mathbf{Sets}(P(A,B) , P(S,T)).$$

The implementation in Haskell follows the same idea. Profunctors endowed with a Tambara structure for the exponential are called closed profunctors. In the Discussion section of the blog post, this is called the Related pattern.

class Closed p where
  closed :: p a b -> p (c -> a) (c -> b)

type Grate s t a b = forall p. Closed p => p a b -> p s t

Traversables, are optics for the action of polynomial or power series functors and thus they can be represented by Tambara modules for this action.

$$\mathbf{C}\left(S , \sum_n A^n \times (B^n \to T)\right) \cong \int_{P \in \mathbf{Tamb}(\mathbf{Poly})} \mathbf{Sets}(P(A,B) , P(S,T)).$$

If we want to use this description, one can implement this in Haskell using sized vectors. However, it is more natural to write it in a language with dependent types such as Idris or Agda. The following is Idris code, where the series is described as a dependent pair consisting on a natural number and the monomial for that number.

series : (Nat -> Type) -> Type -> Type
series c a = (n : Nat ** (c n , Vect n a))

interface Polynomial (p : Type -> Type -> Type) where
  polynomial : p a b -> p (series c a) (series c b)

Traversal : Type -> Type -> Type -> Type -> Type
Traversal s t a b = {p : _} -> Polynomial p => (p a b -> p s t)

Composing lenses and prisms

Finally, can we compose optics of different kinds into new optics? In particular, what is the structure we obtain when composing lenses and prisms? The observation is that both lenses and prisms can be seen as particular cases of a different optic: the affine traversal, which has this name because it can be seen as a traversal that has 0 or 1 focus. The composition we discussed at the beginning of the article becomes composition of affine traversals.

Affine traversals

In a bicartesian closed category $\mathbf{C}$, an affine traversal over a pair of sets $(S,T)$ with focus in $(A,B)$ is defined as a morphism with the following signature.

$$\mathbf{Affine} \left( \binom{S}{T}, \binom{A}{B} \right) = \mathbf{C}\left(S , T + A \times (B \to T)\right).$$

Affine traversals are optics for an action that takes a pair $(C,D) \in \mathbf{C} \times \mathbf{C}$ to the functor $F_{(C,D)}(A) = D + C \times A$. Proving that this is indeed a monoidal action requires associativity to show that $F_{(C,D)} \circ F_{(C',D')} = F_{(C\times C' , D + C \times D')}$. The derivation from the existential is again an application of the Yoneda lemma.

$$\begin{aligned} & \int^{C,D \in \mathbf{C}} \mathbf{C}(S , D + C \times A) \times \mathbf{C}(D + C \times B , T) \\ \cong & \qquad{(Coproduct)} \\ & \int^{C,D \in \mathbf{C}} \mathbf{C}(S , D + C \times A) \times \mathbf{C}(D,T) \times \mathbf{C}(C \times B , T) \\ \cong & \qquad{(Yoneda)} \\ & \int^{C \in \mathbf{C}} \mathbf{C}(S , T + C \times A) \times \mathbf{C}(C \times B , T) \\ \cong & \qquad{(Exponential)} \\ & \int^{C \in \mathbf{C}} \mathbf{C}(S , T + C \times A) \times \mathbf{C}(C,B \to T) \\ \cong & \qquad{(Yoneda)} \\ & \mathbf{C}(S , T + (B \to T) \times A). \\ \end{aligned}$$

In Haskell, the typechecker infers the most general type at each step. However, it does not check the Tambara structure axioms. When it composes a lens and a prism, it simply joins the Strong and Choice constraints into a new profunctor optic.

Developments and further work

During the ACT Adjoint school we have related the derivation of the traversal we presented to the description using traversables that can be found in Haskell libraries; we have derived some new concrete optics and studied their application in programming contexts and we have sketched a general categorical account of how composition of optics of different kinds works in general (considering both distributive laws and coproducts of monads). We expect to continue working on this, and there are some interesting directions and related work we have not covered here.

• We have not considered lawful optics on this post. A general description of how to derive these can be found in Riley’s Categories of optics.

• Boisseau and Gibbons’ “What You Needa Know about Yoneda” also describes the approach from functional programming and the description of traversables using traversals.

• The basic theory of optics and the coend calculus we use for the derivations work in a similar way for categories enriched over an arbitrary Benabou cosmos. Enriching over the poset $\{0,1\}$, for instance, yields relations instead of profunctors with Tambara modules being relations preserving some structure.

• Sometimes the Van Laarhoven representation of optics is used instead of the profunctor representation. Again in Riley’s Categories of optics, the question of when this representation is possible for a given optic is discussed.

Our group would like to thank Jeremy Gibbons, Jules Hedges and David Jaz Myers for helpful discussion on the topic. We would also like to thank the organizers of the ACT school for making this collaboration possible. We thank Bartosz Milewski and Daniel Cicala for reading the drafts of this post and suggesting many corrections and improvements to it.