一句话：提出带谓词契约的 contract lens 与双向计算律，用程序演算从规约推导高效双向变换。
双向变换（BX）用于维护相关数据多个表示之间的一致性。基于 lens 组合子的方法因模块化和构造正确而成为 BX 编程主流，但 lens 的双向行为使等式推理与优化比单向程序困难得多。本文将程序演算——一种基于代数律对函数式程序进行构造正确推理的方法——引入双向程序推导。为支持双向程序计算，作者提出 contract lens，在传统 lens 上增加一对谓词，从而支持部分 lens 的安全、模块化组合；并定义 fold、filter、map、scan 等常见计算模式的组合子，建立若干双向计算律用于推理和优化 contract lens。最后通过非平凡例子展示该计算框架的有效性。
Abstract Bidirectional transformations (BXs) are a mechanism for maintaining consistency between multiple representations of related data. The lens framework, which usually constructs BXs from lens combinators, has become the mainstream approach to BX programming because of its modularity and correctness by construction. However, the involved bidirectional behaviors of lenses make the equational reasoning and optimization of them much harder than unidirectional programs. We propose a novel approach to deriving efficient lenses from clear specifications via program calculation, a correct-by-construction approach to reasoning about functional programs by algebraic laws. To support bidirectional program calculation, we propose contract lenses , which extend conventional lenses with a pair of predicates to enable safe and modular composition of partial lenses. We define several contract-lens combinators capturing common computation patterns including $\textit{fold}, \textit{filter},\textit{map}$ , and $\textit{scan}$ , and develop several bidirectional calculation laws to reason about and optimize contract lenses. We demonstrate the effectiveness of our new calculation framework based on contract lenses with nontrivial examples.
@article{paperbot2154,
title = {Contract lenses: Reasoning about bidirectional programs via calculation},
author = {HANLIANG ZHANG and WENHAO TANG and RUIFENG XIE and MENG WANG and ZHENJIANG HU},
journal = {Journal of Functional Programming},
volume = {33},
year = {2023},
doi = {10.1017/s0956796823000059}
}