Optics for the Working Mathematician |   Bartosz Milewski's Programming Cafe

Category theory extracts the essence of structure and composition. At its foundation it deals with the composition of arrows. Building on composition of arrows it then goes on describing the ways objects can be composed: we have products, coproducts and, at a higher level, tensor products. They all describe various modes of composing objects. In monoidal categories any two objects can be composed.

Unlike composition, which can be described uniformly, decomposition requires case-by-case treatment. It’s easy to decompose a cartesian product using projections. A coproduct (sum) can be decomposed using pattern matching. A generic tensor product, on the other hand, has no standard means of decompositon.

Optics is the essence of decomposition. It answers the question of what it means to decompose a composite.

We consider an object decomposable when:

• We can split it into the focus and the complement,
• We can replace the focus with something else, without changing the complement, to get a new composite object,
• We can zoom in; that is, if the focus is decomposable, we can compose the two decompositions,
• It’s possible for the whole object to be the focus.

Let’s translate these requirements into the language of category theory. We’ll start with the standard example: the lens, which is the optic for decomposing cartesian products.

The splitting means that there is a morphism from the composite object to the product , where is the complement and is the focus. This morphism is a member of the hom-set .

To replace the focus we need another morphism that takes the same complement , combines it with the new focus to produce the new composite . This morphism is a member of the hom-set

Here’s the important observation: We don’t care what the complement is. We are “focusing” on the focus. We carry the complement over to combine it with the new focus, but we don’t use it for anything else. It’s a featureless black box.

To erase the identity of the complement, we hide it inside a coend. A coend is a generalization of a sum, so it is written using the integral sign (see the Appendix for details). Programmers know it as an existential type, logicians call it an existential quantifier. We say that there exists a complement , but we don’t care what it is. We “integrate” over all possible complements.

Here’s the existential definition of the lens:

Just like we construct a coproduct using one of the injections, so the coend is constructed using one of (possibly infinite number of) injections. In our case we construct a lens by injecting a pair of morphisms from the two hom-sets sharing the same . But once the lens is constructed, there is no way to extract the original from it.

It’s not immediately obvious that this representation of the lens reproduces the standard setter/getter form. However, in a cartesian closed category, we can use the currying adjunction to transform the second hom-set:

Here, is the internal hom, or the function object representing morphisms from to . We can then use the co-Yoneda lemma to reduce the coend:

The first part of this product is the setter: it takes the source object and the new focus to produce the new target . The second part is the getter that extracts the focus .

Even though all optics have similar form, each of them reduces differently.

Here’s another example: the prism. We just replace the product with the coproduct (sum).

This time the reduction goes through the universal property of the coproduct: a mapping out of a sum is a product of mappings:

Again, we use the co-Yoneda to reduce the coend:

The first one extracts the focus , if possible, otherwise it constructs a (by secretly injecting a ). The second constructs a by injecting a .

We can easily generalize existential optics to an arbitrary tensor product in a monoidal category:

In general, though, this form cannot be further reduced using the co-Yoneda trick.

But what about the third requirement: the zooming-in property of optics? In the case of the lens and the prism it works because of associativity of the product and the sum. In fact it works for any tensor product. If you can decompose into , and further decompose into , then you can decompose into . Zooming-in is made possible by the associativity of the tensor product.

Focusing on the whole object plays the role of the unit of zooming.

These two properties are used in the definition of the category of optics. The objects in this category are pairs of object in . A morphism from a pair to is the optic . Zooming-in is the composition of morphisms.

But this is still not the most general setting. The useful insight is that the multiplication (product) in a lens, and addition (coproduct) in a prism, look like examples of linear transformations, with the residue playing the role of a parameter. In fact, a composition of a lens with a prism produces a 2-parameter affine transformation, which also behaves like an optic. We can therefore generalize optics to work with an arbitrary monoidal action (first hinted in the discussion at the end of this blog post). Categories with such actions are known as actegories.

The idea is that you define a family of endofunctors in that is parameterized by objects from a monoidal category . So far we’ve only discussed examples where the parameters were taken from the same category and the action was either multiplication or addition. But there are many examples in which is not the same as .

The zooming principles are satisfied if the action respects the tensor product in :

(Here, is the unit object with respect to the tensor product in , and is the identity endofunctor.)

The actegorical version of the optic doesn’t deal directly with the residue. It tells us that the “unimportant” part of the composite object can be parameterized by some .

This additional abstraction allows us to transport the residue between categories. It’s enough that we have one action in and another in to create this mixed optics (first introduced by Mitchell Riley):

The separation of the focus from the complement using monoidal actions is reminiscent of what physicists call the distinction between “physical”  and “gauge” degrees of freedom.

An in-depth presentation of optics, including their profunctor representation, is available in this paper.

Appendix: Coends and the Co-Yoneda Lemma

A coend is defined for a profunctor, that is a functor of two variables, one contravariant and one covariant, . It’s a cross between a coproduct and a trace, as it’s constructed using injections of diagonal elements (with some identifications):

Co-Yoneda lemma is the identity that works for any covariant functor (copresheaf) :