Title: Synthesizing Bijective Lenses,
Abstract: Bidirectional transformations between different data representations occur
frequently in modern software systems. They appear as serializers and
deserializers, as database views and view updaters, and more. Manually building
bidirectional transformations---by writing two separate functions that are
intended to be inverses---is tedious and error prone. A better approach is to
use a domain-specific language in which both directions can be written as a
single expression. However, these domain-specific languages can be difficult to
program in, requiring programmers to manage fiddly details while working in a
complex type system.
To solve this, we present Optician, a tool for type-directed synthesis of
bijective string transformers. The inputs to Optician are two ordinary regular
expressions representing two data formats and a few concrete examples for
disambiguation. The output is a well-typed program in Boomerang (a
bidirectional language based on the theory of lenses). The main technical
challenge involves navigating the vast program search space efficiently enough.
Unlike most prior work on type-directed synthesis, our system operates in the
context of a language with a rich equivalence relation on types (the theory of
regular expressions). We synthesize terms of a equivalent language and convert
those generated terms into our lens language. We prove the correctness of our
synthesis algorithm. We also demonstrate empirically that our new language
changes the synthesis problem from one that admits intractable solutions to one
that admits highly efficient solutions. We evaluate Optician on a benchmark
suite of 39 examples including both microbenchmarks and realistic examples
derived from other data management systems including Flash Fill, a tool for
synthesizing string transformations in spreadsheets, and Augeas, a tool for
bidirectional processing of Linux system configuration files.