|START Conference Manager|
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)