Hot take: optics are better abstraction than lenses, in *all* use cases. Why? They make explicit all the things you're implicitly thinking about anyway when using lenses. I think they are really important in shaping how we think about bidirectional maps. A short thread. 👇 1/9

Optics make explicit 1) the internal state (residual) and 2) the fact that you need to have the base category either be Cartesian, or at the very least have the "get" maps be comonoid homomorphisms. Let's look at the state/residual.
2/9

In lenses, this state is always the same as the input and is implicit. This can be seen by repackaging the get map from get: X → Y to Δₓ;(get×X):X e→ Y×X. Now our new get map (in addition to computing the output) passes through the input. This is good for a few reasons. 3/9

First, this pleasantly symmetric with the put:X×Y'→X'. But also, this new map is now exactly the "left" map of an optic too. (It turns out put was all along the "right" map). This tells us that the passed-through input is actually the state we're remembering. 4/9

But most importantly, this formulation is now explicit in the use of the copy map Δₓ:X → X×X, which you might have not realized is needed if you were just thinking about the standard get-put formulation. Furthermore, when you were composing lenses, ... 5/9