Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

January 29, 2020

Profunctor Optics: The Categorical View

Posted by John Baez

guest post by Emily Pillmore and Mario Román

In functional programming, optics are a compositional representation of bidirectional data accessors provided by libraries such as Kmett’s lens, or O’Connor’s mezzolens. Optics were originally called accessors or generalized functional references and appeared as a compositional solution to accessing fields of nested product types. As the understanding of functional references grew, different families of optics were introduced for a variety of different types (e.g. prisms for tagged unions or traversals for containers), culminating in a whole “glassery” of intercomposable accessors.

More recently, Milewski explained the profunctor formulation of these optics in terms of Tambara modules: profunctors endowed with additional structure that makes it interplay nicely with a monoidal action. Milewski explains how a unified profunctor representation of optics can be obtained following Pastro and Street’s “Doubles for monoidal categories”.

In this twelfth post for the Applied Category Theory School we will be presenting Bartosz Milewski’s post “Profunctor optics: the categorical view”. We will give an introduction to the topic of optics, and discuss some of the ideas developed during the course of the ACT Adjoint School 2019.

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)(S,T) and (A,B)(A,B) consists of two functions SAS \to A and S×BTS \times B \to T. We interpret SS as the type for the original record; TT is the type of the the updated record; AA is the type of the part of SS to be updated; BB is the type of the data that will replace AA; the function SAS \to A is the view function; and S×BTS \times B \to T is the update.

A lens from (S,T) to (A,B), consisting on a pair of view and update functions.

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

Lens((ST),(AB))=C(S,A)×C(S×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.

viewZipCode: PostalZip updateZipCode: Postal×ZipPostal\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)(S,T) and (A,B)(A,B) consists of two functions SA+TS \to A + T and BTB \to T. We interpret SS as the type for the original, possibly more abstract, data structure; TT is the type of its updated version; AA is the type of some concrete form SS can take; and BB is the type that will replace AA. The function SA+TS \to A + T is called a match function and the BTB \to T is a build function. You can skip the following definition if you note that prisms are precisely lenses in the opposite category.

A prism, consisting on a pair of match and build functions.

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

Prism((ST),(AB))=C(S,T+A)×C(B,T).\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.

matchAddress: StringAddress+Postal buildAddress: PostalAddress\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)(S,T) and (A,B)(A,B) consists of a single function S nA n×(B nT)S \to \sum_{n \in \mathbb{N}} A^n \times (B^n \to T). We again interpret SS as the original data structure, that is transformed into TT when we replace a list of elements of type AA with an equal-length list of elements of type BB.

A traversal, consisting on an extract function.

In a cartesian closed category with limits and colimits indexed by natural numbers, C\mathbf{C}, a traversal from a pair of sets (S,T)(S,T) to (A,B)(A,B) is given by a single morphism: an extract C(S, nA n×(B nT))\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. Traversal((ST),(AB))=C(S, nA n×(B nT)).\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 SA nS \to A^n and a put S×B nTS \times B^n \to T. However, the fact that both nn 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:

extract: MailList nEmail n×(Email nMailList).\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 mC(S,T+A)m \in \mathbf{C}(S, T + A) and lC(B,T)l \in \mathbf{C}(B,T), and a lens given by vC(A,X)v \in \mathbf{C}(A,X) and uC(A×Y,B)u \in \mathbf{C}(A \times Y , B). We want to compose them into a combined optic from (S,T)(S,T) to (X,Y)(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).

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

Note that Λ(lu)C(A,T Y)\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:C op×CSetsP \colon \mathbf{C}^{op} \times \mathbf{C} \to \mathbf{Sets} is a cartesian profunctor if it is equipped with a natural transformation α C,(A,B):P(A,B)P(C×A,C×B)\alpha_{C,(A,B)} \colon P(A,B) \to P(C \times A , C \times B) such that α 1=id\alpha_1 = \mathrm{id} and α C 1×C 2=α C 1α C 2\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 Cartesian\mathbf{Cartesian} of cartesian profunctors; that is,

C(S,A)×C(S×B,T) PCartesianSets(P(A,B),P(S,T)).\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.

An example showing how optics work.

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 :C[C,C]\otimes \colon \mathbf{C} \to [ \mathbf{C} , \mathbf{C} ]; but towards the end, this is extended to any action given by an inclusion F[C,C]\mathbf{F} \to [ \mathbf{C} , \mathbf{C} ] of some subcategory of endofunctors F\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 M\mathbf{M} on an arbitrary category C\mathbf{C} is a strong monoidal functor M[C,C]\mathbf{M} \to [ \mathbf{C} , \mathbf{C} ]. In other words, actions are the objects of the slice category MonCat/[C,C]\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 Cat\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 (a̲):M[C,C](\underline{\phantom{a}}) \colon \mathbf{M} \to [ \mathbf{C} , \mathbf{C} ] be a strong monoidal functor and let S,T,A,BCS,T,A,B \in \mathbf{C}. An optic from (S,T)(S,T) to (A,B)(A,B) is an element of the following set described as a coend. Optic((ST),(AB))= MMC(S,M̲A)×C(M̲B,T).\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, SS, can be decomposed into the focus, AA, and some context, MM, 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 Optic\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 Optic\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\{An existential lens. }{\Bigg\} \cong \Bigg\{ A lens. }\Bigg\}

CCC(S,C×A)×C(C×B,T) (Product) CCC(S,C)×C(S,A)×C(C×B,T) (Yoneda lemma) C(S,A)×C(S×B,T).\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\{An existential prism. }{\Bigg\} \cong \Bigg\{ A prism. }\Bigg\}

CCC(S,C+A)×C(C+B,T) (Coproduct) CCC(S,C+A)×C(C,T)×C(B,T) (Yoneda lemma) C(S,T+A)×C(B,T).\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 C\mathbf{C}, grates from (S,T)(S,T) to (A,B)(A,B) are defined as follows, where we use ()(\to) for the exponential. Grate((ST),(AB))=C((SA)B,T).\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 ():C op[C,C]( \to ) \colon \mathbf{C}^{op} \to [ \mathbf{C} , \mathbf{C} ].

CC opC(S,CA)×C(CB,T) (Product-exponential adjunction, and symmetry of the product) CC opC(C,SA)×C(CB,T) (Yoneda) C((SA)B,T).\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, C op\mathbf{C}^{op}, is not the same as the base category C\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, [,C][\mathbb{N} , \mathbf{C}], we show that traversals are optics for the action that takes any of these functors C:CC \colon \mathbb{N} \to \mathbf{C} into the functor Poly(C):CC\mathbf{Poly}(C) \colon \mathbf{C} \to \mathbf{C} given by Poly(C)(A)= nC n×A n\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 [,C][\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, nC n×( mD m×X m) n nE n×X n\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= n= j=1 km jC k× j=1 kD m jE_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 nn as a sum of natural numbers.

{\Bigg\{An existential traversal. }{\Bigg\} \cong \Bigg\{ A traversal. }\Bigg\}

Proposition. Traversals are optics for this power series action Poly:[,C][C,C]\mathbf{Poly} \colon [\mathbb{N}, \mathbf{C}] \to [\mathbf{C}, \mathbf{C}]. C[,C]C(S, nC n×A n)×C( nC n×B n,T) (Cocontinuity) C[,C]C(S, nC n×A n)× nC(C n×B n,T) (Adjunction for the exponential) C[,C]C(S, nC n×A n)× nC(C n,B nt) (Natural transformation as an end) C[,C]C(S, nC n×A n)×[,C](C (),B ()t) (Yoneda lemma) C(S, nA n×(B nT)).\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 (M,,I)(\mathbf{M}, \otimes, I) be a monoidal category and (A̲):M[C,C](\underline{\phantom{A}}) \colon \mathbf{M} \to [ \mathbf{C} , \mathbf{C} ] a strong monoidal functor with structure morphisms ϕ M,N:M̲N̲MN̲\phi_{M,N} \colon \underline{M} \circ \underline{N} \cong \underline{M \otimes N} and ϕ I:idI̲\phi_{I} \colon \mathrm{id} \cong \underline{I}.

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

α(I)=P(ϕ I 1,ϕ I)andα(MN)=P(ϕ M,N 1,ϕ M,N)α(M)α(N).\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 Θ:[C op×C,Sets][C op×C,Sets]\Theta \colon [\mathbf{C}^{op} \times \mathbf{C} , \mathbf{Sets}] \to [\mathbf{C}^{op} \times \mathbf{C} , \mathbf{Sets}] defined as

Θ(P)(A,B)= MMP(M̲A,M̲B).\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, Tamb M\mathbf{Tamb}_{\mathbf{M}}, as the Eilenberg-Moore category for Θ\Theta. The Θ\Theta comonad precomposes both components with the image of MMM \in \mathbf{M} and takes an end; from this description, it can be seen that it has a left adjoint

MMLan (M̲,M̲)() MM()(M̲,M̲),\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 Ψ:[C op×C,Sets][C op×C,Sets]\Psi \colon [\mathbf{C}^{op} \times \mathbf{C} , \mathbf{Sets}] \to [\mathbf{C}^{op} \times \mathbf{C} , \mathbf{Sets}] acts on a profunctor Q:C×C opSetsQ \colon \mathbf{C} \times \mathbf{C}^{op} \to\mathbf{Sets} as

Ψ(Q)(X,Y)= MM U,VCC(X,M̲U)×C(M̲V,Y)×Q(U,V)\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:C op×CSetsP,Q \colon \mathbf{C}^{op} \times \mathbf{C} \to \mathbf{Sets}.

QΘP (Natural transformation as an end) (A,B)C op×CSets(Q(A,B),ΘP(A,B)) (Fubini rule) A,BCSets(Q(A,B),ΘP(A,B)) (Definition of Θ) A,BCSets(Q(A,B), MMP(M̲A,M̲B)) (Continuity of the end) A,BC MMSets(Q(A,B),P(M̲A,M̲B)) (Fubini rule) MM A,BCSets(Q(A,B),P(M̲A,M̲B)) (Yoneda lemma, in the category C op×C) MM A,BCSets(Q(A,B), X,YCSets(C(X,M̲A)×C(M̲B,Y),P(X,Y))) (Continuity of the end) MM A,BC X,YCSets(Q(A,B),Sets(C(X,M̲A)×C(M̲B,Y),P(X,Y))) (Currying) MM A,BC X,YCSets(Q(A,B)×C(X,M̲A)×C(M̲B,Y),P(X,Y)) (Fubini rule) X,YC A,BC MMSets(Q(A,B)×C(X,M̲A)×C(M̲B,Y),P(X,Y)) (Cocontinuity of the coend) X,YCSets( MM A,BCQ(A,B)×C(X,M̲A)×C(M̲B,Y),P(X,Y)) (Definition of Ψ) X,YCSets(ΨQ(X,Y),P(X,Y)) (Natural transformation as an end) ΨQP.\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

PTambSets(P(A,B),P(S,T)) MMC(S,M̲A)×C(M̲B,T),\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,TCA,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.

PTambSets(P(A,B),P(S,T)) (Yoneda lemma) PTambSets(Nat(y (A,B),P),P(S,T)) (Free-forgetful adjunction for Tambara modules) PTambSets(Tamb(Ψy (A,B),P),P(S,T)) (Yoneda lemma) Ψy (A,B)(S,T) (Definition of Ψ) MM x,yCC(S,M̲X)×C(M̲Y,T)×y (A,B)(X,Y) (Yoneda lemma) MMC(S,M̲A)×C(M̲B,T) (Definition) Optic((ST),(AB)).\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 Ψy (A,B)(S,T)\Psi y_{(A,B)}(S,T), which is, again by Yoneda lemma, the same as a natural transformation y (S,T)Ψy (A,B)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 C op×COptic\mathbf{C}^{op} \times \mathbf{C} \to \mathbf{Optic}, which is the same as having a promonad, a monoid in the category of endoprofunctors, Φˇ:C op×CC op×C\check{\Phi} \colon \mathbf{C}^{op} \times \mathbf{C} \nrightarrow\mathbf{C}^{op} \times \mathbf{C}, whose Kleisli object is Optic\mathbf{Optic}. From the universal property of the Kleisli object, it follows that copresheaves over Optic\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 C\mathbf{C} on itself by the product (×):C×CC(\times) \colon \mathbf{C} \times \mathbf{C} \to \mathbf{C} interpreted as (×):C[C,C](\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.

C(S,A)×C(S×B,T) PTamb(×)Sets(P(A,B),P(S,T)).\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 (+):C×CC(+) \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.

C(S,A+T)×C(B,T) PTamb(+)Sets(P(A,B),P(S,T)).\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 ():C op×CC(\to) \colon \mathbf{C}^{op} \times \mathbf{C} \to \mathbf{C}. That means that they can be represented by Tambara modules for the exponential.

C((SA)B,T) PTamb()Sets(P(A,B),P(S,T)).\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.

C(S, nA n×(B nT)) PTamb(Poly)Sets(P(A,B),P(S,T)).\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 C\mathbf{C}, an affine traversal over a pair of sets (S,T)(S,T) with focus in (A,B)(A,B) is defined as a morphism with the following signature.

Affine((ST),(AB))=C(S,T+A×(BT)).\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)C×C(C,D) \in \mathbf{C} \times \mathbf{C} to the functor F (C,D)(A)=D+C×AF_{(C,D)}(A) = D + C \times A. Proving that this is indeed a monoidal action requires associativity to show that F (C,D)F (C,D)=F (C×C,D+C×D)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.

C,DCC(S,D+C×A)×C(D+C×B,T) (Coproduct) C,DCC(S,D+C×A)×C(D,T)×C(C×B,T) (Yoneda) CCC(S,T+C×A)×C(C×B,T) (Exponential) CCC(S,T+C×A)×C(C,BT) (Yoneda) C(S,T+(BT)×A). \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}\{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.

Posted at January 29, 2020 6:28 AM UTC

TrackBack URL for this Entry:   https://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/3191

7 Comments & 0 Trackbacks

Re: Profunctor Optics: The Categorical View

Small typo: in the statement of the “profunctor representation theorem” you want C(S,M̲A)\mathbf{C}(S,\underline{M}A). (In the derivation it appears correctly.)

Posted by: Tom Ellis on January 30, 2020 7:18 AM | Permalink | Reply to this

Re: Profunctor Optics: The Categorical View

I’ve attempted to fix that; someone should let me know if it’s not right.

Posted by: John Baez on January 30, 2020 8:03 PM | Permalink | Reply to this

Re: Profunctor Optics: The Categorical View

Your fix is correct! Thank you for pointing that out Tom, and fixing it, John.

Posted by: Emily Pillmore on January 30, 2020 8:59 PM | Permalink | Reply to this

Re: Profunctor Optics: The Categorical View

I really like this approach because it classifies “opticable types” by associating them with a functor. For example, types which support a lens (“lensable types”) are associated with cartesian product and types which support a traversal (“traversalable types”, or just “traversable types”!) are associated with Poly\mathbf{Poly}. Every lens is also a traversal, and this presumably arises from the natural transformation from ×\cdot \times \cdot to Poly(iifi=1thenelse1)()\mathbf{Poly}(i \to if i = 1 \, then \cdot else \, \mathbf{1})(\cdot) (if you’ll excuse the notation).

I can’t work out what the functors for getters and setters should be. I have a hypothesis that a setter should correspond to the functor for all algebraic datatypes (i.e. not just sums and products, like Poly\mathbf{Poly} but also exponentials). I haven’t made much progress with that.

Posted by: Tom Ellis on February 3, 2020 1:10 PM | Permalink | Reply to this

Re: Profunctor Optics: The Categorical View

Yes, that sounds right :) Usually, we associate each optic with a family of endofunctors (products by an object, traversables, and so on). In this sense, Setters are associated to the family of all endofunctors (see, for instance, Riley, 4.5.1).

Getters are not optics in this sense but something we call mixed optics. The article we wrote after the ACT school targets precisely these (“Profunctor optics, a categorical update”, Section 3.4).

Posted by: Mario Román on March 11, 2020 5:32 PM | Permalink | Reply to this

Re: Profunctor Optics: The Categorical View

At the top you briefly mentioned Dialectica categories as an early appearance of lenses (by another name). But arguably one of the main points of Dialectica categories is that they are monoidal categories, or at least multicategories. Does this monoidal/multi structure generalize to any of these other notions of optics?

Posted by: Mike Shulman on February 18, 2020 6:31 PM | Permalink | Reply to this

Re: Profunctor Optics: The Categorical View

If (𝒞,,I)(\mathcal{C},\otimes,I) is symmetric monoidal, then optics for the action ():𝒞[𝒞,𝒞](\otimes) \colon \mathcal{C} \to [\mathcal{C},\mathcal{C}] of the monoidal product form a symmetric monoidal category. In fact, the construction of the category of optics extends to a endofunctor on SymmMonCat\mathbf{SymmMonCat} (Riley, Theorem 2.0.8, and all of Section 2 is devoted to this case).

However, this is a very particular case that will not work in general. I guess we would need to ask the action ():[𝒞,𝒞](\oslash) \colon \mathcal{M} \to [\mathcal{C},\mathcal{C}] giving rise to the optic to be such that (MA)(NB)(MN)(AB)(M \oslash A) \otimes (N \oslash B) \cong (M \otimes N) \oslash(A \otimes B), or something along those lines, and that is something that will not work for most of our examples.

Posted by: Mario Román on March 11, 2020 5:22 PM | Permalink | Reply to this

Post a New Comment