Reference. Synthesizing bijective lenses

Anders Miltner, Kathleen Fisher, Benjamin C. Pierce, David Walker, Steve Zdancewic · POPL · 2018 · lenses program-synthesis · PDF · DOI · arXiv · pldb
Bidirectional transformations between different data representations occur frequently in modern software systems. They appear as serializers and deserializers, as parsers and pretty printers, as database views and view updaters, and as a multitude of different kinds of ad hoc data converters. 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. We present an alternative approach. Instead of coding transformations manually, we synthesize them from declarative format descriptions and examples. Specifically, we present Optician, a tool for type-directed synthesis of bijective string transformers. The inputs to Optician are a pair of 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. In particular, and 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). Consequently, program synthesis requires search in two dimensions: First, our synthesis algorithm must find a pair of “syntactically compatible types,” and second, using the structure of those types, it must find a type- and example-compliant term. Our key insight is that it is possible to reduce the size of this search space without losing any computational power by defining a new language of lenses designed specifically for synthesis. The new language is free from arbitrary function composition and operates only over types and terms in a new disjunctive normal form. We prove (1) our new language is just as powerful as a more natural, compositional, and declarative language and (2) our synthesis algorithm is sound and complete with respect to the new language. 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, able to synthesize intricate lenses between complex file formats in seconds. We evaluate Optician on a benchmark suite of 39 examples that includes 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.

Cite
Cite as @miltner-2017-synthesizing (helia, typst) · \cite{miltner-2017-synthesizing} (LaTeX)
BibTeX
bibtex · 14 lines
@article{miltner-2017-synthesizing,
  author    = {Anders Miltner and
               Kathleen Fisher and
               Benjamin C. Pierce and
               David Walker and
               Steve Zdancewic},
  title     = {Synthesizing bijective lenses},
  journal   = {{PACMPL}},
  volume    = {2},
  number    = {{POPL}},
  pages     = {1:1--1:30},
  year      = {2018},,
  doi       = {10.1145/3158089},
}
hayagriva YAML (typst)
yaml · 19 lines
miltner-2017-synthesizing:
  type: article
  title: Synthesizing bijective lenses
  author:
  - Miltner, Anders
  - Fisher, Kathleen
  - Pierce, Benjamin C.
  - Walker, David
  - Zdancewic, Steve
  date: 2018
  page-range: 1:1–1:30
  serial-number:
    doi: 10.1145/3158089
  parent:
    type: periodical
    title: PACMPL
    publisher: Association for Computing Machinery (ACM)
    issue: POPL
    volume: 2
Download: miltner-2017-synthesizing.bib · miltner-2017-synthesizing.yml
Cited by (2)

Saggitarius: A DSL for Specifying Grammatical Domains miltner-2023-saggitariusOOPSLA · 2023
Common data types like dates, addresses, phone numbers and tables can have multiple textual representations, and many heavily-used languages, such as SQL, come in several dialects. These variations can cause data to be misinterpreted, leading to silent data corruption, failure of data processing systems, or even security vulnerabilities. Saggitarius is a new language and system designed to help programmers reason about the format of data, by describing grammatical domains—that is, sets of context-free grammars that describe the many possible representations of a datatype. We describe the design of Saggitarius via example and provide a relational semantics. We show how Saggitarius may be used to analyze a data set: given example data, it uses an algorithm based on semi-ring parsing and MaxSAT to infer which grammar in a given domain best matches that data. We evaluate the effectiveness of the algorithm on a benchmark suite of 110 example problems, and we demonstrate that our system typically returns a satisfying grammar within a few seconds with only a small number of examples. We also delve deeper into a more extensive case study on using Saggitarius for CSV dialect detection. Despite being general-purpose, we find that Saggitarius offers comparable results to hand-tuned, specialized tools; in the case of CSV, it infers grammars for 84% of benchmarks within 60 seconds, and has comparable accuracy to custom-built dialect detection tools.
PDF · DOI · arXiv · pldb

Synthesizing symmetric lenses miltner-2019-synthesizingICFP · 2019
Lenses are programs that can be run both “front to back” and “back to front,” allowing updates to either their source or their target data to be transferred in both directions. Since their introduction by Foster et al., lenses have been extensively studied, extended, and applied. Recent work has also demonstrated how techniques from type-directed program synthesis can be used to efficiently synthesize a simple class of lenses—so-called bijective lenses over string data—given a pair of types (regular expressions) and a small number of examples. We extend this synthesis algorithm to a much broader class of lenses, called simple symmetric lenses, including all bijective lenses, all of the popular category of “asymmetric” lenses, and a rich subset of the more powerful “symmetric lenses” proposed by Hofmann et al. Intuitively, simple symmetric lenses allow some information to be present on one side but not the other and vice versa. They are of independent theoretical interest, being the largest class of symmetric lenses that do not rely on persistent internal state. Synthesizing simple symmetric lenses is substantially more challenging than synthesizing bijective lenses: Since some of the information on each side can be “disconnected” from the other side, there will, in general, be many lenses that agree with a given example. To guide the search process, we use stochastic regular expressions and ideas from information theory to estimate the amount of information propagated by a candidate lens, generally preferring lenses that propagate more information, as well as user annotations marking parts of the source and target data structures as either irrelevant or essential. We describe an implementation of simple symmetric lenses and our synthesis procedure as extensions to the Boomerang language. We evaluate its performance on 48 benchmark examples drawn from Flash Fill, Augeas, the bidirectional programming literature, and electronic file format synchronization tasks. Our implementation can synthesize each of these lenses in under 30 seconds.
PDF · DOI · arXiv · pldb
Cites 43 works (1 here)
With notes (1)

A Completeness Theorem for Kleene Algebras and the Algebra of Regular Events KOZEN1994366I&C · 1994
We give a finitary axiomatization of the algebra of regular events involving only equations and equational implications. Unlike Salomaa′s axiomatizations, the axiomatization given here is sound for all interpretations over Kleene algebras.
DOI
External (42)
miltner-2017-synthesizing reference entries/refs/miltner-2017-synthesizing/miltner-2017-synthesizing.hel