Generic recursive lens combinators and their calculation laws

• Published in: Theoretical computer science 2022-04, Vol.913, p.113-137
• Main Authors: Xie, Ruifeng, Hu, Zhenjiang
• Format: Article
• Language: English
• Subjects: Bidirectional transformations; Program calculation; Programming language theory
• ISSN: 0304-3975; 1879-2294
• DOI: 10.1016/j.tcs.2022.02.019

•We provide a set of generic recursive lens combinators for constructing bidirectional programs.•We extend existing recursive lens combinators to support contract lenses.•We provide various calculation laws for reasoning about contract lenses.•We define new contract-lens combinators for upwards and downwards accumulations. Bidirectional transformation is a generic method for synchronizing two related data structures, with applications in databases, software model transformation, graph transformation, etc. Since the data to synchronize often have complicated and disparate structures, bidirectional transformations are hard to develop, correctly comprehend, reason about, or maintain. Programming language researchers have invested much efforts to invent new frameworks and paradigms, to aid the development of complex bidirectional transformations. However, these frameworks are not always applicable due to certain subtleties in the problem specification; some bidirectional programs become too complicated and unstructured to verify their correctness, not to mention their poor efficiency. In this paper, we propose a collection of generic recursion patterns for bidirectional transformations, and develop corresponding calculation laws. With these generic recursion patterns, we can develop structured bidirectional transformations, which are easy to understand and maintain. With these calculation laws, we can effectively optimize bidirectional programs, while preserving its very semantics. We demonstrate, through calculation of bidirectional transformations on trees, the expressiveness of the combinators and the effectiveness of the calculation laws.