Optics

An optic is a bidirectional accessor; a lens focuses a field, whereas a prism matches a case, and the categorical presentation is what makes the zoo of them one construction. An optic splits off a private residual, exposes an interface, and later rebuilds the whole from a new value. The choice of how much context it carries is quotiented away by a coend, and the same data reappears as a profunctor-polymorphic map, as the value of a functor on monoidal categories, and as a box with a hole in a string diagram.

Work in a monoidal category . An optic from to is an element of the coend

a pair “split off a residual and expose ” / “given a new and the residual, rebuild ” (the coend presentation of Riley’s “Categories of Optics” and Clarke et al.’s “Profunctor Optics, a Categorical Update”), with existentially quantified. Two optics agree when they differ only by how much context they carry, the coequaliser of the coend quotienting away that choice. Concrete families are recovered by choosing the acting structure. A lens takes the complement and (get/put), whereas a prism dualises to a coproduct (match/build).

An optic is written in bra–ket notation with a forward leg and a backward leg . The terminology splits the data three ways. The residue is hidden state, the focus is the exposed interface, and the outer is the whole seen from outside.

Definition. The profunctor form

Equivalently an optic is a profunctor-polymorphic map, a transformation natural in every profunctor carrying the relevant algebraic structure (a Tambara module, after Pastro–Street). The double-Yoneda / Tambara-module theorem identifies this end of natural transformations with the coend above, so the two presentations name the same optic.

Theorem. Optics as a functor

Optics are not a list of gadgets but the value of a functor , . It sends a symmetric monoidal category to the symmetric monoidal category whose objects are pairs and whose homs are the coend above. When has finite products and this specialises to .

Remark. Actegory generalisation

Replacing by an actegory action of a monoidal on gives , so the residue and the focus need not live in the same category. The residual is then drawn from the acting category while the interface stays in .

Remark. Coend calculus and open diagrams

The existential is coend calculus doing bookkeeping. Composition of optics is composition of the residuals, and the coend’s coequaliser quotients away the choice of . This is the “open diagrams” reading, in which an optic is a process with an open slot, drawn as a box with a hole through which the continuation is threaded, composing by plugging holes.

Remark. Local state (Román)

Román reads an optic as a local-state transformer, with the residual private state a process hides from its environment, exposed only through the interface. Message-passing and monadic/stateful lenses fall out by varying and the acting monoidal structure, which is why the coend definition subsumes the concrete optic families rather than listing them.

Remark. The surface-diagram reading

Drawn as a string diagram, an optic is two boxes and with the residue threaded “over the top” from the first to the second. The residue is a wire that leaves the surface, arcs over, and re-enters, so the focus flows through the front while the state passes behind. This is the cover / wall / wire / point tower: the point is a value, the wire its type, the wall the residue channel separating forward from backward, and the cover the whole surface on which composition glues optics edge to edge.

Lenses as store-comonad coalgebras

The three folklore lens laws are not axioms imposed by hand but exactly the equations a coalgebra of the store comonad already satisfies, a characterisation that lives outside the coend and Tambara presentations above because it is special to the product lens where the residual is an actual function space. A lens on with view is a pair of a getter and a putter , the latter taking a whole and a new view and returning an updated whole. Currying the putter to and pairing with collapses the bidirectional data into one map

a coalgebra of the store comonad . The backward, derivative-like leg is what places lenses in a differential-category when the base carries a differential structure.

Theorem. Store-comonad coalgebra laws are the lens laws

is a store-comonad coalgebra iff it is a lawful lens, matched law-for-law. The counit law is get-put , since putting back what was read changes nothing. The comultiplication law splits into two equations, put-get reading back what was written, whereas put-put makes a second write override the first. The two comonad axioms thus encode the lens laws.

Pre-lenses and learners

Milewski’s iteration of the Tambara construction lifts an optic to the shape of a learner, whose update is parametric and runs in both directions. A pre-lens keeps visible the residual that the coend above hides, exposing the parameter rather than quotienting it away. A triple Tambara module then carries three actegory actions at once, one for the parameter over and above the forward and backward data, whereas an ordinary Tambara module carries a single action. Capucci’s open direction lets those actions vary over one another as a dependent actegory, in which the backward action’s category depends on the forward object, organised as a triple category that Capucci and Myers package as contextads.