How are you, ladies & gentlemen?

I'm interested in source-to-source program transformations, which I think should be reversible, implying monomorphism. To do this, one needs to be able to invert the components of these transformations, so I was happy to discover the idea of *lenses*, which plugged a hole in my mental compendium about a decade old.

Allow me to raise the very simple example of list decomposition, using Haskell notation. There's an obvious sense in which the inverse of the `cons` operation is pattern-matching on the the list head|tail, with the same notation, `(:)`, used for both.^{1} Similarly, one can say that destructuring is "the same" as the `(head⨯tail)` joint operation. By another abuse of notation, in the form of entropy: $H(\text{<destructuring>}) = H(\mathtt{head}) + H(\mathtt{tail})$.

Now let me "lift" `head` and `tail` into the category of very well behaved (VWB?) lenses, which I'll call `lhead` and `ltail`, as

```
lhead⭧ = head
lhead⭨ x (_:xs) = x:xs
ltail⭧ = tail
ltail⭨ xs (x:_) = x:xs
```

where the `Get` operations are the original `head` and `tail`.^{2} Intuitively, the joint information provided by `lhead|ltail` is "the same" as that of `cons` plus pattern-matching, in that we could transform programs written in one syntactic convention into the other. There's probably a symmetric argument to show that a lensified `cons` has equivalent expressive power as well. If I were a category theorist, I might draw a little diagram.

Unfortunately, I'm asking questions on several topics, here, about which my knowledge level is abecedarian. Are there particular subcategories of lenses which show the algebraic behavior I'm suggesting? Is there a domain-theoretic way of describing the special relationship between `lhead⭨`, `ltail⭨` and `cons`? I have the impression that some kind of higher-order functor should exist to map regular functions to these lenses.^{3} I hope someone will know what I'm talking about, even if I don't.

Thanks,

Jonathan J-S