## Quotient Lenses

### J. Nathan Foster, Alexandre Pilkiewicz and Benjamin C. Pierce

**The 13th ACM SIGPLAN International Conference on Functional Programming (ICFP 2008)**
Victoria, British Columbia, Canada, September 22-24, 2008

## Abstract

There are now a plethora of bidirectional programming languages, in which every program can be read both as a transformation from one data structure to another and as a reverse transformation mapping an edited version of its output to a corresponding edited version of its input. Besides notational parsimony---representing two related transformations by a single expression---such languages are attractive because they generally come with behavioral laws offering strong guarantees about how the two transformations must fit together. However, it has repeatedly been discovered that, in practice, these laws are too strong: we do not actually want them to hold ``on the nose,'' but only up to some equivalence, permitting inessential details such as whitespace to be different after a round trip. Several bidirectional languages loosen their behavioral laws in this way, but only for specific, baked-in equivalences.

We propose a general theory of quotient lenses---bidirectional transformations that are well-behaved modulo specified equivalences. Semantically, quotient lenses are a natural refinement of lenses, which we have studied in previous work. At the level of syntax, we develop a rich set of mechanisms for programming with canonizers and for quotienting lenses by canonizers. We track equivalences explicitly, with each expression's type specifying the equivalences it respects.

We have implemented quotient lenses as a refinement of the bidirectional string processing language Boomerang. The result is a very expressive system for transforming real-world ad hoc data formats. We present a number of useful primitive canonizers for the domain of strings, show how quotient lenses can be checked statically using a simple extension of Boomerang's regular-expression-based type system, and develop an extended example, based on the UniProt genome database format, showing the power of the notation. Finally, we illustrate the generality of the approach, we discuss how programs in some other bidirectional languages can be translated into our notation.

START
Conference Manager (V2.54.6)