Strategic Lenses, Episode I: Two Simple Lenses

In my last post, I discussed lenses as means to specify well-behaved bidirectional transformations. In this post, I introduce two very simple lenses: identity and composition. Both lenses are part of a bidirectional transformation language working on terms. Its syntax is specified in SDF while its semantics is defined by term rewriting rules in Stratego.

Identity

This is a very simple lens. It maps between identical concrete and abstract models. From concrete to abstract models, get simply copies the concrete model. In the opposite direction, put and create copy the abstract model:

1. id.get(c) = c
2. id.put(a, c) = a
3. id.create(a) = a

The notion l.f refers to the function f of a particular lens l of interest. id denotes the identity lens. This lens obeys all three round-tripping laws:

1. id.get(id.put(a, c)) = id.get(a) = a
2. id.get(id.create(a)) = id.get(a) = a
3. id.put(id.get(c), c) = id.put(c, c) = c

Composition

This lens combines two lenses l1 and l2 sequentially to a new lens (l1 ; l2). To get an abstract model from a concrete model c, l1.get and l2.get are applied sequentially. The put function of the combined lens is slightly more difficult. First, l2.put is applied to put back the abstract model into the temporary model l2.get was applied to. This temporary model is the result of l1.get. This step yields an updated temporary model. In the next step, the updated temporary model is put back into the original concrete model by applying l1.put. The create function is simple again. First, l2.create is applied to the abstract model. Afterwards, l1.create is applied to the result:

1. (l1 ; l2).get(c) = l2.get(l1.get(c))
2. (l1 ; l2).put(a, c) = l1.put(l2.put(a, l1.get(c)), c)
3. (l1 ; l2).create(a) = l1.create(l2.create(a))

The composition (l1 ; l2) fulfils the round-tripping laws if l1 and l2 do so:

1. (l1 ; l2).get((l1 ; l2).put(a, c)) =
   l2.get(l1.get(l1.put(l2.put(a, l1.get(c)), c))) =
   l2.get(l2.put(a, l1.get(c))) = a
2. (l1 ; l2).get((l1 ; l2).create(a)) =
   l2.get(l1.get(l1.create(l2.create(a)))) =
   l2.get(l2.create(a)) = a
3. (l1 ; l2).put((l1 ; l2).get(c), c) =
   l1.put(l2.put(l2.get(l1.get(c)), l1.get(c)), c) =
   l1.put(l1.get(c)), c) = c

Defining a DSL

We now take identity and composition as a starting point for a bidirectional transformation language working on terms. First, we need to define a concrete syntax for this language. For this purpose, the metalanguage of choice is SDF which integrates lexical and context-free syntax in one formalism, supports arbitrary context-free grammars, and enables language reuse by a module system. Here is an SDF module defining a concrete syntax for the two lenses discussed so far:

module StrategicLenses

imports Common

exports context-free syntax
"id"          -> Lens     {cons("Id")}
Lens ";" Lens -> Lens     {left, cons("Comp")}


This module reuses another module called Common which provides definitions for syntactic sorts like ID, INT and STRING as well as typical layout definitions including comments. For each lens, there is a rule defining the syntactic sort Lens. The second rule is attributed being left associative to avoid ambiguity. Finally, both rules are attributed with a constructor name for nodes in abstract syntax trees. With SDF, abstract syntax trees are represented as terms. A signature for such terms can be derived from a SDF syntax definition. Here is the signature for our transformation language:

module StrategicLenses

signature constructors
Comp : Lens * Lens -> Lens
Id   : Lens


We rely on such term representations when we specify the dynamic semantics of both lenses by term rewriting rules in Stratego. Here are the rules for identity:

module Semantics

imports libstratego-lib StrategicLenses

rules
get    : (Id(), c)    -> c
put    : (Id(), a, c) -> a
create : (Id(), a)    -> a

This module imports the Stratego standard library and the signature  StrategicLenses mentioned before. There is a rewrite rule for each lens function. The fundamental idea is to rewrite tuples consisting of a lens and the arguments of the function into the result of the function. The first rule specifies the get function. It rewrites a pair consisting of the identity lens and a concrete model c to c. The second rule specifies the put function. Since this function takes two arguments — an abstract model a and a concrete model c, it rewrites a triple consisting of the identity lens, a, and c to the abstract model a. The third rule specifies the create function analogously.

Here are the rules for composition:

rules
get    : (Comp(l1, l2), c)    -> <get> (l2, <get> (l1, c))
put    : (Comp(l1, l2), a, c) -> <put> (l1, <put> (l2, a, <get> (l1, c)), c)
create : (Comp(l1, l2), a)    -> <create> (l1, <create> (l2, a))

Note that these rules have the same name as for identity. But they distinguish in the matching pattern for the lens. Here, a composition lens is matched and the two sub-lenses are bound to l1 and l2, respectively. To specify the result of the functions, we need to apply rewriting rules recursively. Application of a rule is denoted by angle brackets. For example, the right-hand side of the first rule reads: Apply get to a pair consisting of l2 and the result of applying get to the pair (l1, c). This enables us to specify the three lens functions in a notation very similar to the one in the beginning of this post.

Coming up next: Some useful lenses working on terms.

Advertisement