合成双射透镜

现代软件系统中频繁出现不同数据表示之间的双向变换。它们表现为序列化器与反序列化器、数据库视图与视图更新器等。手动构建双向变换——即编写两个旨在互为逆函数的独立函数——既繁琐又易错。一种更好的方法是使用领域特定语言，使得两个方向均可写为单一表达式。然而，这些领域特定语言可能难以编程，要求程序员在复杂的类型系统中处理繁琐的细节。为解决此问题，我们提出了 Optician，一个用于类型导向合成双射字符串转换器的工具。Optician 的输入是代表两种数据格式的两个普通正则表达式以及若干用于消歧的具体示例。输出则是 Boomerang（一种基于透镜理论的双向语言）中的一个良类型程序。主要技术挑战涉及足够高效地探索庞大的程序搜索空间。与以往大多数类型导向合成工作不同，我们的系统运行于类型具有丰富等价关系（正则表达式理论）的语言上下文中。我们合成一种等价语言的项，并将生成的项转换为我们的透镜语言。我们证明了合成算法的正确性。我们还通过实验证明，我们的新语言将合成问题从存在不可解方案的问题转变为存在高效方案的问题。我们在包含 39 个示例的基准套件上评估了 Optician，其中包括微型基准测试以及源自其他数据管理系统的现实示例，如用于在电子表格中合成字符串转换的 Flash Fill 工具，以及用于双向处理 Linux 系统配置文件的 Augeas 工具。