Symmetric polymorphic lenses (maybe)

Whereas ordinary directed lenses go from a source to a view, symmetric lenses relate two different views of an internal source. I’ve been thinking about how to smoosh together symmetric lenses with polymorphic lenses, which are the sort used in functional programming. My actual goal is to invent “symmetric open games” (without relying on non-well-founded recursion like I did in this paper). But with the right definition, I think symmetric polymorphic lenses could be a useful tool to programmers as well.

Normally when I’m playing with an idea like this I mock it up in Haskell and play around with it to check it works, before committing to too much hard work on the proofs. But this would be very difficult (and maybe impossible) to write in Haskell, so the idea of this post is to give enough detail that some folks could try it in Agda or Idris, and give me feedback on whether it feels like something useful. (In the meantime, I will try an extremely fast and loose Haskell version by pretending that pullbacks and pushouts are products and coproducts, and see what happens.)

What I’ll write about here is actually symmetric bimorphic lenses, the word I made up for when the lens laws don’t even typecheck. In what is now a fine tradition, I’ll figure out how the lens laws come into it later. (I have a nasty feeling that the lens laws might be what kills this idea.)

Rather than starting from the original concrete definition of symmetric lenses, I’m starting from their characterisation as spans of directed lenses (modulo a hack, because the category of lenses doesn’t quite have pullbacks).

The other ingredient is the fact that the category of bimorphic lenses embeds canonically into the category of containers. (This was first pointed out to me by Fred Nordvall Forsberg.) Morphisms of containers can be viewed as dependently typed lenses, as in this paper. The category of containers has extremely nice properties: it is complete, cocomplete and locally cartesian closed, making it a model of a big chunk of type theory.

With this, I can give my proposed definition in a maximally slick way: a symmetric bimorphic lens is a span of container morphisms whose feet are in the image of the category of lenses (or equivalently: whose feet have only constant type dependence).

Here’s an unpacked definition. A symmetric bimorphic lens between and consists of 6 things:

• A type (thought of as the type of initial sources)
• A type dependent on (thought of as the types of updated sources)
• Left-view and right-view functions and
• Left-update and right-update functions and

I think that the types really should be bound by an existential quantifier, and not by a — in category theory I think of them as bound by a coend. But probably nothing will go seriously wrong if it’s implemented as a type.

The remaining thing is how to compose them. Suppose we have symmetric lenses between and with internal state , and another between and with internal state . Then:

• The type of initial sources is , in other words, the pairs of initial sources which agree on their common view
• The updated sources indexed by is the pushout

I could try to write down the new view and update maps, but if you’re hacking this up I expect it’s easier to just follow the types.

Update: After writing a simple Haskell implementation (see this thread), I spotted the fairly big problem with existential quantification: Since you can’t get at the type of initial states, you can never actually make the lens do anything. So, types it probably is then.