Synthesizing bijective lenses
Synthesizing bijective lenses
复制标题
合成双射透镜
DOI：
10.1145/3158089
复制
发表时间：
2017
影响因子：
--
通讯作者：
Steve Zdancewic
中科院分区：
文献类型：
--
作者：
Anders Miltner;Kathleen Fisher;B. Pierce;D. Walker;Steve Zdancewic
不同数据表示之间的双向转换在现代软件系统中经常发生。它们以序列化和避难所的形式出现，作为解析器和漂亮的打印机，数据库视图和查看更新器，以及多种不同类型的临时数据转换器。手动构建双向转换 - - 通过编写两个单独的函数，这些功能旨在对抗 - - 繁琐而错误。一种更好的方法是使用特定领域的语言，在该语言中，这两个方向都可以写为单个表达式。但是，这些特定于域的语言可能很难编程，要求程序员在复杂类型的系统中工作时管理巧合的细节。我们提出了另一种方法。我们没有手动编码转换，而是从声明格式的描述和示例中综合了它们。具体而言，我们提出了Optician，这是一种用于类型定向的conignive String Transformers合成的工具。 Optician的输入是一对代表两种数据格式和一些具体示例的普通正则表达式。该输出是Boomerang（基于镜头理论的双向语言）的一个良好的程序。主要的技术挑战涉及有效地导航庞大的计划搜索空间。特别是，与大多数先前在类型定向合成方面的工作不同，我们的系统在一种语言的背景下运行，与类型具有丰富的等价关系（正则表达理论）。因此，程序合成需要在两个维度上进行搜索：首先，我们的合成算法必须找到一对“语法兼容类型”，其次，使用这些类型的结构，必须找到一个符合类型和示例的术语。我们的关键见解是，可以通过定义专门为合成设计的新镜头语言来减少此搜索空间的大小而不会失去任何计算能力。新语言不受任意函数组成的含量，并仅以新的分离正常形式进行类型和术语。我们证明（1）我们的新语言与一种更自然，构图和声明性语言一样强大，并且（2）我们的综合算法在新语言方面是合理且完整的。我们还从经验上证明，我们的新语言将综合问题从接受棘手的解决方案的综合问题转变为一种接受高效解决方案的解决方案，能够以几秒钟的时间在复杂的文件格式之间合成复杂的镜头。我们在39个示例的基准套件上评估了光学师，其中包括微型计算和现实示例，这些示例包括来自其他数据管理系统，包括Flash Fill，一种用于综合电子表格中的字符串转换工具，以及Augeas，这是Linux System System配置文件的双向处理工具。
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.