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 → Ap : 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 ; hp' : 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 = spᵢ : 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 bp^ : 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*
andL^
inverse of one another? - In the simple lens case, when are
L*
andL^
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) = apπ : 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 getputp*^ : 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 putputp^* : 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 sp° : 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
forL*
andL^
? - How are
L**
,L*^
,L^*
andL^^
related toL
,L*
andL^
? - Is there a relation between
M
being a singleton set and isomorphisms in the category of lenses (it is easy to prove thatM = {*}
implies thatL
satisfiesputput
)? - Are the properties stated for the simple case generalizable to the general case?