More (Categorical) Thoughts on Lawful Lenses

In the previous post we discussed how we could state a definition for generic lawful optics and we proved that lawful lenses are exactly constant complement lenses.

In this post we will revisit the ideas presented there in a more categorical fashion, but focusing on lenses in particular.

What we will present in this post is a series of results which were obtained at the third Statebox Summit with the collaboration of the participants, out of which I ought to mention Jules Hedges, David Spivak, Brendan Fong, Christina Vasilakopoulou, Eliana Lorch, Andre Knispel and Stefano Gogioso for taking active part in this discussion.

The Category of Lenses

Let’s start by defining the category of lenses. The objects of our category will be pairs of sets (S, T), morphisms between (S, T) and (A, B) will be lenses of type Lens S T A B, which are described by pairs of functions

g : S → A
p : S → B → T

The composition of two morphisms, i.e. two lenses, (g, p) : (S, T) → (A, B) and (h, q) : (A, B) → (C, D) is a new lens (g', p') : Lens S T C D defined by functions

g' : S → C
g' = g ; h
p' : S → D → T
p' s d = p s (q (g s) d)

where p' can be represented by the following diagram

where ∙ : S → S × S is the copy operation.

Given any object of our category, which is a pair (S, T), the identity morphism on it is the lens (gᵢ, pᵢ) : (S, T) → (S, T) defined by

gᵢ : S → S
gᵢ s = s
pᵢ : S → T → T
pᵢ s t = t

It can be checked that the above definitions satisfy the axioms for a category.

Associated Lenses

Given a generic lens L := (g, p) : (S, T) → (A, B), we saw in this post that we can define a set

M = { m ∈ B → T | ∃ s : S . m = p s }

which turns out to be really helpful in proving that lawful lenses are exactly the constant complement ones. In fact, this set allows us to define two new lenses associated to the lens L.

First off, we can define L* : (S, T) → (A × M, B × M) by

g*: S → A × M
g* s = (g s, p s)
p* : S → B × M → T
p* s (b, m) = m b

Moreover, we can also define L^ : (B × M, A × M) → (T, S) by

g^ : B × M → T
g^ (b, m) = m b
p^ : B × M → S → A × M
p^ (b, m) s = (g s, p s)

Notice how ^ (pronounced “hat”) produces a swap between A and B and between S and T. In their generic form, L* and L^ are not composable. However, if we restrict them to simple lenses, they are!

So, with these two new lenses at hand, some questions arise naturally

• In the simple lens case, when are L* and L^ inverse of one another?
• In the simple lens case, when are L* and L^ lawful?
• In the generic case, if we consider π : (A × M, B × M) → (A, B) to be the lens defined by

gπ : A × M → A
gπ (a, m) = a
pπ : A × M → B → B × M 
pπ (a, m) b = (b, m)

is it always true that L = L* ; π?

Are L* and L^ Inverses?

Let us first consider the composition L* ; L^. In this case we have

g*^ : S → S
g*^ s = p s (g s) = s -- by getput
p*^ : S → S → S
p*^ s₁ s₂ = p s₂ (g s₂) = s₂ -- by getput

Therefore L^ ; L^ = id on (S, S) if and only if getput holds for L.

On the other hand, consider L^ ; L*. We obtain

g^* : A × M → A × M
g^* (a, m) = (g (m a), p (m a))
p^* : A × M → A × M → A × M
p^* (a₁, m₁) (a₂, m₂) = (g (m₂ a₂), p (m₂ a₂))

Remember that by definition of M we have that any m ∈ M is of the form p s for some s ∈ S. Hence we get

g^* : A × M → A × M
g^* (a, p s) = (g (p s a), p (p s a))
             = (a, p s) -- by putget and putput
p^* : A × M → A × M → A × M
p^* (a₁, p s₁) (a₂, p s₂) = (g (p s₂ a₂), p (p s₂ a₂))
                          = (a₂, p s₂) -- by putget and putput

We then obtain that L^ ; L* = id on (M × A) whenever L satisfies putget and putput.

We conclude by saying that L* and L^ are each other’s inverses if and only if L is a lawful lens.

Are L* and L^ Lawful?

In this section we will check whether L* and L^ are lawful lenses in the simple case, and which conditions we do need to assume on L for them to satisfy the lens laws.

Let’s start with L*

getput

p* s (g* s) = p s (g s) = s -- by getput

putget

g* (p* s₁ (a, p s₂)) = g* (p s₂ a)
                     = (g (p s₂ a), p (p s₂ a))
                     = (a, p s₂) -- by putget and putput

putput

p* (p* s (a₁, m₁)) (a₂, m₂) = p* (m₁ a₁) (a₂, m₂)
                            = m₂ a₂
                            = p* s (a₂, m₂) -- always holds

Hence L* always satisfies putput, satisfies getput if L satisfies getput and satisfies putget if L satisfies putget and putput. Therefore L* is lawful if and only if L is.

Let’s now have a look at L^.

getput

p^ (a, p s) (g^ (a, p s)) = p^ (a, p s) (p s a)
                          = (g (p s a), p (p s a))
                          = (a, p s) -- by putget and putput

putget

g^ (p^ (a, m) s) = g^ (g s, p s)
                 = p s (g s)
                 = s -- by getput

putput

p^ (p^ (a, m) s₁) s₂ = p^ (g s₁, p s₁) s₂
                     = (g s₂, p s₂)
                     = p^ (a, m) s₂ -- always

Therefore also L^ always satisfies putput, and it satisfies getput if L satisfies putget and putput and satisfies putget if L satisfies getput. So also L^ is lawful if and only if L is.

Decomposing L

One question remains: whether L = L* ; π holds. It is not hard to check that it actually always does; in fact if we compute the components g° and p° for the composed lens, we get

g° : S → A
g° s = gπ (g* s) = gπ (g s, p s) = g s
p° : S → B → T
p° s b = p* (s, pπ (g* s, b))
       = p* (s, pπ ((g s, p s), b))
       = p* (s, (b, p s)) = p s b

In conclusion, we can always decompose L into L* ; π, where π is always lawful.

Conclusion

In this post we investigated the role of M more closely, as well as the lenses L* and L^ which are generated from it. We saw that L* and L^ are strictly related to L, and that they satisfy the lens laws only if L satisfies other lens laws.

Putting together the three results presented above, we can also recover a more formal proof that a simple lens is lawful if and only if it is isomorphic to a constant complement lens.

Some further questions we might consider

• What is M for L* and L^ ?
• How are L**, L*^, L^* and L^^ related to L, L* and L^?
• Is there a relation between M being a singleton set and isomorphisms in the category of lenses (it is easy to prove that M = {*} implies that L satisfies putput)?
• Are the properties stated for the simple case generalizable to the general case?