Synthesizing Lenses

Abstract

Lenses are bidirectional functions that satisfy a set of "round-tripping laws." Lenses arise in a number of domains, and can implement serializer/deserializer pairs, parser/pretty printer pairs, and incremental data structure transformers.

Domain-specific languages like Boomerang, Augeas, GRoundTram, BiFluX, BiYacc, Brul, BiGUL, and HOBiT allow programmers to write both transformations with a single program, and guarantee the transformations satisfy the round-tripping laws. However, writing in domain-specific lens languages can be hard, requiring the user to reason about fiddly details of the transformations, often within the context of a complex type system.

In this work we introduce Optician, which provides an alternative method of developing lenses -- synthesis. We develop a synthesis engine for Boomerang, a lens language for string transformations. Pairs of regular expressions serve as types for Boomerang lenses, which transform strings between the languages of those regular expressions. Instead of manually writing Boomerang lenses, programmers merely need to provide the type of the desired lens and a set of input/output examples describing the lens's behavior. Optician will then synthesize a lens between the provided types that exhibits the demonstrated behavior. We demonstrate how to synthesize three classes of lenses: bijective lenses, quotient lenses, and symmetric lenses. Bijective lenses encode bijections, quotient lenses encode bijections modulo an equivalence relation, and symmetric lenses encode bidirectional transformations that may discard information when going from one format to another.

We define a synthesizer that involves two cooperating procedures. One procedure proposes a candidate space of lenses, the second procedure searches through that space.

To synthesize quotient lenses, regular expressions are augmented with equivalence information, and the synthesizer generates lenses that translate between the representative elements of the equivalence classes. To synthesize symmetric lenses, regular expressions are augmented with probability distributions, and the synthesis algorithm aims to avoid information loss.

We evaluate Optician from a variety of benchmarks taken from the lens and synthesis literature, and find that we are able to synthesize all the lenses in our benchmark suite. We have integrated Optician into the Boomerang codebase, enabling users to either synthesize their lenses or write them by hand.