Everyone is invited to attend his talk. Abstract follows below.
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.