A LENS is a bi-directional program.  When read from left to right, it denotes an ordinary function.  When read from right to left, it denotes an “update translator” that takes an input to this function together with an UPDATED output and produces a new input reflecting the update.

Many variants of this idea have been explored, but none deal fully with ORDERED data.  If, for example, an update involves a change in the order of a list in the output, the correspondence between the items in the output list and the items in the input list can be lost, leading to loss or corruption of data.

We propose a refined semantic space of RESOURCEFUL LENSES, enriching the WELL-BEHAVED LENSES of Foster, Greenwald, Moore, Pierce, and Schmitt (2005) with an equivalence relation embodying a notion of “reordering.”  A new behavioral law states that the translation of updates must be invariant with respect to reordering.  We then develop a regular-expression-like syntax for resourceful lenses over string data.  The key technical challenge is devising an intermediate semantic space that (a) supports global matching of corresponding chunks of input and output structures and (b) provides suitable denotations for a compositional language of lens combinators.  A simple static type system for this language guarantees that the behavioral laws are satisfied.  We show how our language can be used to build bi-directional string transformations for some real-world data formats.

Principles of Programming Seminars