Lately there has been a lot of hype around lenses and optics in general, both in the functional programming community and in the category theory community, especially because they are popping up in several different places. This suggest they have an important role that is yet to be completely understood.

One thing that struck me while reading about lenses is the fact that functional programmers tend to consider only lawful lenses, while academics are interested more broadly in generic lenses. Moreover, optics laws, altough very meaningful in practice, appear as something God-given and it is hard to understand where they do come from. Additionally, laws are usually defined only for simple lenses, while it seems reasonable to expect that generic lenses also obey some coherence conditions.

This is why at the Statebox summit I was very curious to talk to other people more skilled than me about lawful generic lenses. It turned out this was a really interesting thing to do, since it seems we now have a good idea on how to solve the above issues. I really need to thank Jules Hedges, David Spivak, Brendan Fong, Christina Vasilakopoulou, Eliana Lorch, Andre Knispel and everyone else who was there for contributing to what follows.

Lens recap

Let’s review briefly what a Lens is. It can be seen as a way to access and update a part of an immutable data structure S, through two functions

data Lens S T A B = Lens
  { g : S -> A
  , p : S -> B -> T
  }

For example we could define a lens cc : Lens (A x M) (B x M) A B defined by

cc : Lens (A x M) (B x M) A B
cc = lens get put
  where
    get : A x M -> A
    get (a, m) = a

    put : (A x M) -> B -> (B x M)
    put (a, m) b = (b, m)

We will call every lens of this form a constant complement lens.

We will call a lens Simple if t = s and b = a, that is if put does not have the ability to change types, but only to update the value of type a inside s.

Lens laws

Traditionally the lens laws are stated for simple lenses as follows:

getput
SgpAS
=
iss

Here • : s -> (s, s) is the function that produces two copies of the input, and i : s -> s is the identity on s.

Alternatively, we could rewrite this as p s (g s) = s.

putget
pSAgSA
=
◦SiAA

Here, ◦ means that we are not using its argument s and i : a -> a is the identity on a.

This could be rewritten as g (p s a) = a

putput
pSAiApSAS
=
S◦AApS

Here ◦ means that we are not using its argument a.

This could be rewritten as p (p s a) = p s.

We say that a simple lens is lawful or very well-behaved if it satisfies the three laws above.

Ramblings on lens laws

I’ve always felt a bit bothered by the three lens laws because, though they make a lot of sense, they still feel a lot like God-given rules without a clear mathematical explanation.

Moreover, as presented above, we are able to state them only for simple lenses, and it feels pretty weird that general lenses do not need to satisfy any rule at all!

Also, lawful lenses seem to be of interest only for programmers, while in academic papers (with some exceptions such as this one) lawful lenses don’t seem to be considered to be very interesting, and generic lenses are usually investigated instead.

Before trying to understand something more about generic lawful lenses, let’s have a look at an easier example of optics, namely adapters.

Generic lawful adapters

An adapter is the simplest of all optics and it encodes the fact that we can adapt data between two different formats. It is defined as

data Adapter S T A B = Adapter
  { f : S -> A
  , t : B -> T
  }

An adapter is said to be simple if S = T and A = B. A simple adapter is lawful if f and t are each other’s inverses, i.e. f (t a) = a and t (f s) = s for any a : A and s : S.

From this point of view, it is clear that we cannot generalise this definition for generic adapters, because we have no way of composing f and t in the generic case.

On the other hand we can easily interpret a simple adapter as follows: it enables us to adapt functions A -> A to functions S -> S, and vice versa, using the isomorphism provided by f and t.

But now we can try to generalize this new point of view to generic adapters: we want a generic adapter to be lawful if it gives us a way to translate functions A -> B to functions S -> T in an isomorphic way, meaning that we can adapt functions A -> B to functions S -> T and vice versa. Hence, we could give the following definition:

A generic adapter is lawful when both f and t are isomorphisms

It is now easy to observe that this definition is equivalent to the previous one when we restict to the simple case, so this new definition is a generalization of the traditional one.

Generalizing to lenses

Now that we were able to state a definition for a generic lawful adapter, let’s see if we can apply this insight to other optics.

If we look at the paper Categories of Optics by Mitchell Riley, we see that a generic optic is defined as

data Optic S T A B = exists M . Optic
  { g : S -> M ⊗ A
  , p : M ⊗ B -> T
  }

where ⊗ is a tensor in a symmetric monoidal category. If you don’t know what that is, don’t worry and interpret it as follows in our relevant examples.

  • For lenses ⊗ is the product, so think to M ⊗ A as (M, A).
  • For prisms ⊗ is the coproduct, or sum. In this case we think to M ⊗ A as Either M A.
  • For adapters ⊗ is just the constant functor, so M ⊗ A is just A.

We can observe that for adapters this definition coincides exactly with the one we gave above. So, we restate our new interpretation of generic lawful adapters in this new more generic setting: an adapter is lawful if both g and p are isomorphisms.

However, with this new interpretation our definition can now be expressed for any possible Optic, not only for adapters! To state it again in its full generality, we say that

An optic o : Optic S T A B is lawful if g and p are isomorphisms

If we now interpret this definition for lenses, where ⊗ is the product, we see that we obtain that lawful lenses are all lenses Lens S T A B where S is isomorphic to (M x A) and T is isomorphic to (M x B). But, up to isomorphism, this is exactly the definition of constant complement lenses we introduced above!

So, to check if our interpretation makes sense, we want to prove that a simple lens is lawful (in the traditional sense, i.e. it respects the three lens laws) if and only if it is constant complement.

Lawful lenses are constanct complement

It is quite easy to check that a simple constant complement lens respects the three lens laws, so we are just going to prove that a lawful lens is constant complement.

The idea of this proof came to us thanks to this hint from Edward Kmett:

Let’s consider a Lens S S A A, defined by functions g : S -> A and p : S -> A -> S, which satisfies getput, putget and putput.

To prove our claim we need to define an M such that S is isomorphic to A x M.

First off, we observe that we can collapse our functions g and p into a single function

g&p : S -> (A, A -> S)
g&p s = (g s, p s)

This actually is really interesting, because it is already sending S into the product of A with something else, where every element of this something else is of the form p s. Hence, we could try to define

M = { m : A -> S | ∃ s : S . m = p s }

At this point let’s try to see if we can prove that S is isomorphic to A x M. Let’s start by defining functions

f : S -> A x M
f s = (g s, p s)

and

h : A x M -> S
h (a, m) = m a

Next, we would like to prove that these two functions f and h are each other’s inverses.

Let’s check first that f;h is the identity on S. We have

(f;h) s = p s g(s)

which is equal to s by getput.

Finally, let’s check that h;f is the identity on A x M.

(h;f) (a, m) = (g(m a), p(m a))

By the definition of the set M, we know that m = p s for some s and hence

(g(m a), p(m a)) = (g(p s a), p(p s a))

which is actually equal to (a, p s) = (a, m) by putget and putput respectively.

QED!

Conclusion

The fact that simple lawful lenses are constant complement lenses is folklore in the functional programming community (e.g. Lenses embody Products, Prisms embody Sums), but a proof of the fact was not easy to find, so I think that writing it down could be useful for future reference.

On the other hand, a definition for a generic lawful optic seems to be not present in the literature, and I think the approach proposed above works really nicely and can help us understand the origin of lens laws.

One interesting question to tackle now would be to understand how this generic notion of lawfulness translates to the profunctor optics encoding.