Lenses are a very powerful and practically useful functional construct. They represent “first class” fields for a data structure.
Lenses arose in work on bidirectional programming (for example, in Boomerang), and in Haskell, people have given many different definitions of lenses, but the simplest and easiest to replicate in type theory is probably the one based on getters and setters.
- a function
, the “getter”;
- a function
, the “setter”;
subject to the following laws:
This definition makes sense for general types
The problem with this definition becomes apparent if, following Russell O’Connor, we think of the pair
The laws that we specified are only enough to show that
Unfortunately, it is not yet clear how to define
One possible idea is the following: a function
So we arrive at the following definition: a higher lens is a function
At this point, we need to show that for any two sets
Therefore, for any
We can now define:
and obtain the setter and the first law at the same time.
To get the other laws, we observe that the
from which the third law follows easily. For the second law, it is enough to observe that coherence implies that
So, any higher lens is also a lens, regardless of truncation levels.
Nicolai Kraus and I are currently working on a paper on precisely the topic of factoring maps through truncations, where we give, for any
In our case, we have
and then a “coherence” property for
To show that
and showing that it is functorial, in the sense that we have functions:
These can be obtained simply by reversing the above derivation of a lens from a higher lens and using the fact that both
We haven’t shown that these two mappings are inverses of each other. I haven’t checked this in detail, but I think it’s true. To prove it, one would need to rearrange the above proof into a chain of simple equivalences, which would directly show that the two notions are equivalent.