The members of his committee are as follows: David Walker (reader, adviser); Kathleen Fisher (reader - Tufts University), Andrew Appel (examiner), Aarti Gupta (examiner), and Zak Kincaid (examiner)
All are welcome to attend. Please see abstract below.
Bidirectional transformations are groupings of transformations between pairs of data representations. A particularly well-studied class of bidirectional transformations are lenses, bidirectional transformations that satisfy a set of “round-tripping laws”. Lenses 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. As long as an expression is well-typed in these languages, the bidirectional transformation that expression represents is a lens. However, writing in domain-specific lens languages can be hard, requiring the user to reason about fiddly details of the transformations 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 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, symmetric lenses, and quotient lenses. Bijective lenses encode bijections, symmetric lenses encode bidirectional transformations that permit losing information when going from one format to another, and quotient lenses satisfy the round-tripping laws modulo an equivalence relation.
We define a synthesizer that involves two cooperating procedures. One procedure proposes a candidate spaces of lenses, the second procedures searches through that space.
To synthesize symmetric lenses, regular expressions are augmented with probability distributions, and the synthesis algorithm aims to avoid information loss. To synthesize quotient lenses, regular expressions are augmented with equivalence information, and the synthesizer generates lenses between the representative elements of the equivalence classes.
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.