*A PDF of this post is available on github*

# Motivation

Lenses seem to pop up in most unexpected places. Recently a new type of lens showed up as a set of morphisms between polynomial functors. This lens seemed to not fit the usual classification of optics, so it was not immediately clear that it had an existential representation using coends and, consequently a profunctor representation using ends. A profunctor representation of optics is of special interest since it lets us compose optics using standard function composition. In this post I will show how the polynomial lens fits into the framework of general optics.

# Polynomial Functors

A polynomial functor in can be written as a sum (coproduct) of representables:

The two families of sets, and are indexed by elements of the set (in particular, you may think of it as a set of natural numbers, but any set will do). In other words, they are fibrations of some sets and over . In programming we call such families *dependent types*. We can also think of these fibrations as functors from a discrete category to .

Since, in , the internal hom is isomorphic to the external hom, a polynomial functor is sometimes written in the exponential form, which makes it look more like an actual polynomial or a power series:

or, by representing all sets as sums of singlentons:

I will also use the notation for the internal hom:

Polynomial functors form a category in which morphisms are natural transformations.

Consider two polynomial functors and . A natural transformation between them can be written as an end. Let’s first expand the source functor:

The mapping out of a sum is isomorphic to a product of mappings:

We can see that a natural transformation between polynomials can be reduced to a product of natural transformations out of monomials. So let’s consider a mapping out of a monomial:

We can use the currying adjunction:

or, in :

We can now use the Yoneda lemma to eliminate the end. This will simply replace with in the target of the natural transformation:

The set of natural transformation between two arbitrary polynomials and is called a polynomial lens. Combining the previous results, we see that it can be written as:

Notice that, in general, the sets and are different.

Using dependent-type language, we can describe the polynomial lens as acting on a whole family of types at once. For a given value of type it determines the index . The interesting part is that this index and, consequently, the type of the focus and the type on the new focus depends not only on the type but also on the *value* of the argument .

Here’s a simple example: consider a family of node-counted trees. In this case is a type of a tree with nodes. For a given node count we can still have trees with a different number of leaves. We can define a poly-lens for such trees that focuses on the leaves. For a given tree it produces a counted vector of leaves and a function that takes a counted vector (same size, but different type of leaf) and returns a new tree .

# Lenses and Kan Extensions

After publishing an Idris implementation of the polynomial lens, Baldur Blöndal (Iceland Jack) made an interesting observation on Twitter: The sum type in the definition of the lens looks like a left Kan extension. Indeed, if we treat and as co-presheaves, the left Kan extension of along is given by the coend:

A coend over a discrete category is a sum (coproduct), since the co-wedge condition is trivially satisfied.

Similarly, an end over a discrete category becomes a product. An end of hom-sets becomes a natural transformation. A polynomial lens can therefore be rewritten as:

Finally, since the left Kan extension is the left adjoint of functor pre-composition, we get this very compact formula:

which works for arbitrary categories and for which the relevant Kan extensions exist.

# Existential Representation

A lens is just a special case of optics. Optics have a very general representation as existential types or, categorically speaking, as coends.

The general idea is that optics describe various modes of decomposing a type into the focus (or multiple foci) and the residue. This residue is an existential type. Its only property is that it can be combined with a new focus (or foci) to produce a new composite.

The question is, what’s the residue in the case of a polynomial lens? The intuition from the counted-tree example tells us that such residue should be parameterized by both, the number of nodes, and the number of leaves. It should encode the shape of the tree, with placeholders replacing the leaves.

In general, the residue will be a doubly-indexed family and the existential form of poly-lens will be implemented as a coend over all possible residues:

To see that this representation is equivalent to the previous one let’s first rewrite a mapping out of a sum as a product of mappings:

and use the currying adjunction to get:

The main observation is that, if we treat the sets and as a discrete categories and , a product of mappings can be considered a natural transformation between functors. Functors from a discrete category are just mappings of objects, and naturality conditions are trivial.

A double product can be considered a natural transformation from a product category. And since a discrete category is its own opposite, we can (anticipating the general profunctor case) rewrite our mappings as natural transformations:

The indexes were replaced by placeholders. This notation underscores the interpretation of as a functor (co-presheaf) from to , as a functor from to , and as a profunctor on .

We can therefore use the co-Yoneda lemma to eliminate the coend over . The result is that can be wrtitten as:

which is exactly the original polynomial-to-polynomial transformation.

# Acknowledgments

I’m grateful to David Spivak, Jules Hedges and his collaborators for sharing their insights and unpublished notes with me, especially for convincing me that, in general, the two sets and should be different.

## Leave a Reply