Edit Lenses

Edit Lenses
M. Hofmann, B. Pierce, and D. Wagner
Proceedings of POPL 2012, p. 495-508.


I previously wrote about Diskin et al.'s delta lenses.  That paper explores one approach to bidirectional transformations that takes into account information about the update process changing one state to another.

In this paper, Pierce et al. explore what they call edit lenses.  A delta lens considers a state space as a category, with the arrows of the category being updates describing how to get from one state to another.  An edit lens, by contrast, considers a state space acted upon by a monoid (this idea appears in previous work on algebraic foundations of bidirectional transformations by Stevens, and was mentioned in Pierce et al.'s Symmetric Lenses paper as a natural next step). 



Specifically, let $(M,\cdot,id)$ be a monoid, thus
\begin{eqnarray*}
id \cdot m &=& m = m \cdot id\\
m \cdot (n \cdot k)  &=& (m \cdot n) \cdot k
\end{eqnarray*}
and consider a set $X$ equipped with an $M$-action, that is, a function $\odot : M \times X \to X$ such that
\begin{eqnarray*}id \odot x &=& x\\
(m \cdot n) \odot x& = &m \odot n \odot x
\end{eqnarray*}
(Hofmann et al. actually consider partial actions only, in which case the above equations are Kleene equality: that is, either both sides are defined and equal or both sides are undefined.)

A module is taken to be a structure $(X,init,\partial X, \odot)$ where $\partial X$ acts on $X$ via $\odot$ and $init \in X$ is a specified initial value.

A symmetric edit lens $l : X \leftrightarrow Y$ relating modules $X$ and $Y$ is taken to be a structure $l = (C, init,\Rrightarrow, \Lleftarrow ,K)$, where
\begin{eqnarray*}
\Rrightarrow &:& X \times C \to Y \times C\\
\Lleftarrow &:& Y \times C \to X \times C\\
K &\subseteq & X \times C \times Y
\end{eqnarray*}
Here, $\Rrightarrow$ and $\Lleftarrow$ need to satisfy additional laws, essentially that they preserve the identity function and commute with monoid element composition.  The relation $K$ is a consistency relation on triples $(x,c,y)$.

The next part of the paper explores basic constructions on edit lenses: as one would expect, they include identity and "constant" lenses and are closed under composition.  Tensor product, sum and list constructions are also given, as well as a partition construction relating $(X \oplus Y)^* \leftrightarrow X^* \otimes Y^*$, which retains the ordering of the elements.

This part of the paper switches back and forth between presenting new module constructions (including how to build edit monoids by specifying generators built up out of edits from sub-monoids), which is to some extent detrimental to understanding what is going on.  In particular, the discussion of "generators" on page 500 doesn't actually explain what a generator is (though this is a familiar enough concept in algebra). 

The paper then investigates general edit lens constructions over containers.  More precisely, they consider a variant of the usual presentation of containers: a container type is a structure $(I,P,live)$ where $I$ is a shape set, $P$ is a position set, and for each $i\in I$, $live(I) \subseteq P$ is the set of positions that are "live" in containers of shape $i$.  For example, for lists, one could take $I = \mathbb{N}$ and $P = \mathbb{N}$ and $live(i) = \{0,\ldots,i-1\}$, for trees, one could take $I = \{0,1\}^* = P$ and $live(i) = \{j \mid j \leq i\}$ where $\leq$ denotes string prefix.  The set of shapes is assumed to be ordered.  A container of type $T = (I,P,live)$ with elements from $X$ is then a pair $(i,f)$ where $i \in I$ and $f : live(i) \to X$; the set of such objects is called $T(X)$.

A general class of edits over containers is developed, categorized as pure insertions, pure deletions, or rearrangements.  Edit lens constructions are given that lift a lens relating $X$ and $Y$ to one relating $T(X)$ to $T(Y)$.  (This is a functor in the category of edit lenses.)  Another construction is given that lifts a lens on shapes (from $I$ to $I'$) to one relating containers $T(X)$ and $T'(X)$.

The next section revisits the constructions of modules and considers adding laws to the monoids used in constructions, which leads to simpler-seeming constructions of products and sums, but isn't explored in depth; the last section shows that symmetric lenses are a special case of edit lenses, where the edits are trivial "replace the whole thing" edits.

Stray thoughts:

• What if I want to build a lens of type $T(X) \leftrightarrow T(Y)$ from $l : I\leftrightarrow I'$ and $l' : X \leftrightarrow Y$?  There are two ways to do this using the combinators in figure 8 and 9.  Are they different?
• Generic constructions of bidirectional transformations are also considered elsewhere (for the state-based setting), by Wang et al. (ICFP 2010) and Voigtländer (POPL 2009).  Voigtländer et al. (ICFP 2010) also study techniques for combining different bidirectionalization techniques.  It would be interesting to develop these ideas more systematically. 
• The paper doesn't say much about principles for identifying good classes of edits, or mediating the edits provided by a real system with those that make the theory work well.  It seems safe to assume at least one devil is concealed in these details.