Profunctor Optics, a Categorical Update

TL;DR

This work generalizes profunctor optics to enriched and mixed settings, unifying lenses, prisms, traversals and related patterns under a single coend-based definition. It extends Pastro-Street Tambara theory to enable generalized Tambara modules for two independent monoidal actions, yielding an enriched category of mixed optics and a profunctor representation theorem that justifies composing optics as ordinary function composition. The paper also presents new optics (e.g., algebraic lenses, glasses) and elementary derivations (e.g., traversals via power-series functors), plus a Haskell implementation that materializes the framework for practical programming. By connecting coend calculus, Tambara modules, and the Double Yoneda lemma, the approach provides a principled, modular architecture for building and composing optics in functional programming with enriched categories. The results offer a robust foundation for future work on lawfulness, Kan extensions, and library design for optics in real-world languages.

Abstract

Optics are bidirectional data accessors that capture data transformation patterns such as accessing subfields or iterating over containers. Profunctor optics are a particular choice of representation supporting modularity, meaning that we can construct accessors for complex structures by combining simpler ones. Profunctor optics have previously been studied only in an unenriched and non-mixed setting, in which both directions of access are modelled in the same category. 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, with access directions modelled in different categories. Our work generalizes a classic result by Pastro and Street on Tambara theory and uses it to describe mixed V-enriched profunctor optics and to endow them with V-category structure. We provide some original families of optics and derivations, including an elementary one for traversals. Finally, we discuss a Haskell implementation.

Figures (11)

• Figure 1: Lenses are pairs of 'view' and 'update' functions that capture the repeating pattern of accessing subfields. Here, extracts a field from a record, and updates that field.
• Figure 2: A prism is given by a pair of functions and that account for the possiblity of failure on pattern matching. In the figure, we verify whether a string can be parsed as an address. The combinator returns the results using the monad (see § \ref{['sec:tablecombinators']}).
• Figure 3: The composition of a prism (asAddress) and a lens (street) produces a composite optic (asAddress . street). This optic (an "affine traversal", see §\ref{['def:affine']}) is used to parse a string and then access and modify one of its subfields.
• Figure 4: A type-variant lens that targets the contents of a value paired with creation and modification timestamps. The lens is constructed from two functions viewContents and updateContents.
• Figure 5: The common structure of an optic. We could provide semantics for diagram of this kind in terms of profunctors, see roman21.

Theorems & Definitions (92)

• Definition 1.1: Ends and coends
• Proposition 1.2
• Proposition 1.3
• Proposition 1.4
• Proposition 1.5
• Definition 2.1
• Definition 3.1
• Proposition 3.2
• proof
• Definition 3.3