Beginner's question: additive "information content" of lenses

Summary:

I learned about lenses only recently. I think I'm trying to identify which types of lenses combine in parallel to form other lenses--but there are a lot of types.

Beginner's question: additive "information content" of lenses

J Jakes-Schauer 06 Sep 2019 05:52

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.¹ 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.² 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.³ I hope someone will know what I'm talking about, even if I don't.

Thanks,
Jonathan J-S

Footnotes

1. Perhaps a bit more obvious than in Lisp, in which the relevant syntax is car|cdr versus destructuring-bind.

2. Leaving operations on empty lists undefined for now.

3. I'll toss in the Futamura projections while I'm at it.

Re: Beginner's question: additive "information content" of lenses

Anthony Anjorin 06 Sep 2019 07:48

Hi Jonathan,

I'm not sure what you mean by reversible, or inversion. In general, the "inverse" of a get is not unique — you typically have a choice of many puts that can all be equally "good". Bx frameworks try to hammer out what laws can be used to precisely say what "good" means.

I'm not from the PL/Haskell world but can still suggest [1] for a formal overview of the quite diverse "lens landscape". It might help you identify what you're interested in and provide relevant references and pointers for further reading.
From a more practical, hands-on side, I guess you might be interested in BiGUL [2], a relatively well-documented and mature Haskell library that can be used to easily program your example (and do much more).

The bx community is very diverse and we try hard (struggle?) to leverage this as an advantage. You might find our current bx benchmark interesting as it allows a direct comparison of the different bx approaches applied to the exact same example [3].

Cheers,
Tony

Bibliography

1. Michael Johnson, Robert D. Rosebrugh: Unifying Set-Based, Delta-Based and Edit-Based Lenses. Bx@ETAPS 2016: 1-13

2. Zhenjiang Hu, Hsiang-Shang Ko: Principles and Practice of Bidirectional Programming in BiGUL. Bidirectional Transformations - International Summer School, Oxford, UK, July 25-29, 2016, Tutorial Lectures, pages 100-150

3. Anthony Anjorin, Zinovy Diskin, Frédéric Jouault, Hsiang-Shang Ko, Erhan Leblebici, Bernhard Westfechtel: BenchmarX Reloaded: A Practical Benchmark Framework for Bidirectional Transformations. BX@ETAPS 2017: 15-30

Last edited on 06 Sep 2019 08:02 by Anthony Anjorin Show more

Re: Beginner's question: additive "information content" of lenses

J Jakes-Schauer 23 Sep 2019 03:18

I apologize for the long delay. It's typical, I'm afraid.

I'm not sure what you mean by reversible, or inversion.

I say 'invertible' when talking about things that seem more like mathematical functions, and 'reversible' when describing programs or algorithms, in the 'reversible computing' (q.v.) sense. In the considerable area where they overlap, I tend to use them interchangeably, which may be the source of the confusion.

I'm not from the PL/Haskell world but can still suggest 1 for a formal overview of the quite diverse "lens landscape". It might help you identify what you're interested in and provide relevant references and pointers for further reading.

It did. Johnson and Rosebrugh have another paper, 2, about spans, which helped me to a breakthrough. I think what I was grasping at, in my first post, was that head and tail are 'complementary,' and the combined form $(\mathtt{lhead}\times \mathtt{ltail})$ is a 'span' from head to tail.

The most illuminating paper I've encountered has been 3, which I think is quite elegant. A symmetric lens is the nearest to the-thing-that-I-was-looking-for-that-turned-out-to-be-called-a-lens. The 'lensified cons' which I postulated could be constructed as a symmetric lens.

-Jonathan

Bibliography

1. Michael Johnson, Robert D. Rosebrugh: Unifying Set-Based, Delta-Based and Edit-Based Lenses. Bx@ETAPS 2016: 1-13

2. Johnson, M. & Rosebrugh, Rob. (2014). Spans of lenses. CEUR Workshop Proceedings. 1133. 112-118.

3. Martin Hofmann, Benjamin Pierce, and Daniel Wagner. 2011. Symmetric lenses. SIGPLAN Not. 46, 1 (January 2011), 371-384.