Inspired by my former colleague Arif Wider, I had a closer look on lenses recently. I started with reading some papers by Nate Foster et alii. You can find a bibliography including these papers at researchr.org. Next, I implemented some lenses in Stratego. These lenses work on terms. In an upcoming series of blog posts, I like to share some insights. This post starts the series with the overall idea of lenses.
Lenses provide means to specify well-behaved bidirectional transformations between more concrete “things” — let’s say models — and more abstract models. Given a set C of concrete models and a set A of abstract models, a lens comprises three total functions:
- get: C → A
- put: A × C → C
- create: A → C
The get function derives an abstract model from a concrete model. This abstract model is basically a view on the concrete model. The put function takes an updated abstract model and its original concrete model as arguments, yielding an updated concrete model which reflects the updates of the abstract model. If no concrete model exists, the create function constructs a concrete model from an abstract one. To ensure well-behaveness these functions must obey the following round-tripping laws:
- get(put(a, c)) = a
- get(create(a)) = a
- put(get(c), c) = c
If we update an abstract model and propagate this update back into an old concrete model by a lens’ put function, we expect that the new concrete model reflects this update completely. The first law — the PutGet law — guarantees this. It requires that applying the lens’ get function to the new concrete model must yield exactly the updated abstract model. That is, no update detail is lost during the put. Similarly, we expect a concrete model which is initially created from an abstract model by a lens’ create function to contain all the information of the abstract model. We must be able to derive the very same abstract model from the concrete model by the lens’ get function. This is ensured by the second law — the CreateGet law. Finally, if we derive an abstract model from a concrete one by a lens’ get function and put this abstract model without any modifications back into the original concrete model, we expect the concrete model to stay unmodified, too. The third law — the GetPut law — enforces this behaviour.
Well, this is simply what we expect from a bidirectional transformation. We can implement the three functions of a lens in any programming language and have to prove the three round-tripping laws. The first step might be quite easy and the second one might become a nightmare, particularly if implementation changes. So what is so special about lenses? Where is the benefit? The idea is to use lenses as first class citizens in a bidirectional transformation language. This language provides a set of basic lenses and combinators for these lenses as means to specify bidirectional transformations. You can simply define new lenses by combining existing lenses. The round-tripping laws are proven for the basic lenses and the static semantics of the language guarantee that a combination of lenses is well-formed and the round-tripping laws hold for the combination as well. Dynamic semantics of the language specify how the three functions of a combined lens can be derived from its constituting base lenses and combinators. Thus, dynamic semantics release you from writing separate functions for your bidirectional transformation while static semantics release you from proving the round-tripping laws.
Coming up next: How to specify lenses in Stratego.
