Two kinds of Prisms

If you’re a functional programmer, you’ve probably heard of prisms. A prism is a bidirectional data structure that often said to be dual to a lens. You might know lenses and prisms from Haskell’s lens library, the recent paper on Profunctor Optics, or other places (such as my my previous blog post).

While lenses are pretty extensively written about (here, and here, for instance), prisms are more mysterious. What does a prism do? What does it mean to be dual to a lens? I’ve been thinking about this recently, and in this short blog post I want to share an interesting find: there are two different ways of being dual to a lens. This feels worthwhile to mention, and as far as I know, is novel.

Let’s just quickly recap what a lens is, and how it’s related to an optic. Given a cartesian category , a lens consists of the forward map and the backward map .¹ Lenses are morphisms in the category whose objects are pairs of objects in . This is their concrete definition. You can also see lenses as special cases of optics. An optic over a monoidal category is defined as an element of the following coend . If you set the monoidal category to be the previously defined cartesian category , then you can reduce the above representation to lenses.²

Great, so how is a prism dual to a lens? Well, it turns out there’s two ways. Given a cocartesian category , you can define a prism as either:

• an element of the hom-set , or
• an element of the hom-set .

The first definition is dual to a lens because we’re instantiating optics for a cocartesian (instead of a cartesian) category, and the second definition is dual because we’re instantiating lenses in the opposite category. Many people casually reference prisms as being dual to lenses, but they seldom reference which duality they’re referring to. And as it turns out, these dualities are different. Let’s see why that is.

If we unpack the prism-as-optic definition, we have the following chain of isomorphisms:

where the first isomorphism is given by the universal property of coproduct, and second one by Yoneda reduction. This gives us two types of maps in which we’ll call and . Alternatively, if we unpack the second way of defining a prism:

we obtain two maps that are also often called and . Let’s write them both down side by side.

It’s clear that they’re different! Even though they have the same “shape”, the way the ports and are bound to parts of the two maps are different in these two cases.

So what does this mean, and why is this important? Well, I’m trying to understand what prisms really do. I like to have a clear picture of where information enters, what happens to it, all the branchings that can possibly happen, and so on. But I only have a clear picture for one of the definitions. It’s the one that sees them as optics.

I wrote about this definition in my previous blog post. I also animated it below: we start at , and then we either a) short-circuit the computation by moving straight down back to , or b) we query the environment with a and wait for a response , subsequently turning it into an .

The other picture doesn’t give us anything like that. In it a prism is supposed to consist of maps and . But which way does the information flow here? Does happen before ? Do we start at , and then build an , meaning we go backwards? Or is there something else at play? It’s not clear. People usually say “prisms are lenses in the opposite category” and then stop there, without telling us how to think about the internal data flow.

This is one reason I prefer the former definition. The other reason is that if we think of prisms as optics, then we get a clear recipe for composing prisms with lenses to obtain affine traversals. But this recipe is missing from the other picture.

This makes me skeptical about it. I haven’t been able to find any nice stories about the other definition, and at this point, I’m starting to wonder whether the fact that “prisms are lenses in the opposite category” is just a misleading coincidence.