paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Synthesizing symmetric lenses

合成对称 lens
ICFP 3(ICFP)2019匹配度 2/10 · 论文属于程序合成/双向编程(lens)领域,虽涉及DSL、形式化与工程实现,但与用户核心关注的静态分析、LLM/Agent、浮点程序分析及贝叶斯程序分析均无直接关联。引用 17 inbox
Anders Miltner, Solomon Maina, Kathleen Fisher, Benjamin C. Pierce, David Walker, Steve Zdancewic
crossref: 2026-09-10

AI 速览

一句话:将类型导向程序合成扩展到简单对称 lens,借助信息论和用户标注从示例合成 Boomerang lens。

Lens 是可双向运行的程序,用于在源与目标间传播更新。已有工作能用类型导向合成,从类型和少量示例高效合成字符串上的双射 lens。本文把该合成算法扩展到更广的简单对称 lens:包含双射 lens、常见非对称 lens,以及 Hofmann 等人对称 lens 的一个丰富子集;它们允许信息仅存在于一侧,且不依赖持久内部状态。由于两侧信息可能互不连通,同一组示例常有多个候选,合成难度增加。作者用随机正则表达式和信息论度量候选 lens 传播的信息量,偏好传播更多信息者,并利用用户标注标出无关或必需的数据部分。实现作为 Boomerang 扩展,在 48 个基准上均可在 30 秒内合成。

问题
如何从一对类型(正则表达式)和少量示例自动合成比双射 lens 更广的简单对称 lens,后者允许信息仅存在于源或目标一侧。
方法
扩展类型导向程序合成,使用随机正则表达式与信息论估计候选 lens 传播的信息量,并支持用户标注源/目标中无关或必需的部分;实现为 Boomerang 语言扩展。
评估
在 48 个来自 Flash Fill、Augeas、双向编程文献和电子文件格式同步的基准上评估,所有 lens 均可在 30 秒内合成。
原文摘要(Abstract)

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.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@article{paperbot579,
  title = {Synthesizing symmetric lenses},
  author = {Anders Miltner and Solomon Maina and Kathleen Fisher and Benjamin C. Pierce and David Walker and Steve Zdancewic},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {3},
  number = {ICFP},
  year = {2019},
  doi = {10.1145/3341699}
}