论文标题
保留镜头
Retentive Lenses
论文作者
论文摘要
基于Foster等人的镜头，已经开发了各种双向编程语言和系统，以帮助用户编写正确的数据同步器。通常采用两种良好的镜头法律，即正确性和狂热性，通常被用作这些系统的保证。虽然镜头旨在在修改视图时将信息保留在源中，但行为良好的信息很少说明信息的保留：Hippocratics仅要求如果不修改视图，则只要求源源不变，并且在更改视图时，没有任何关于信息保留的信息。为了解决该问题，我们提出了原始镜头的扩展，称为保留镜片，该镜头满足了新的保留法，以确保如果部分视图不变，则也保留了源的相应部分。作为保留镜头的具体示例，我们提出了一种特定领域的语言，用于编写树转换。我们证明，DSL中从程序中产生的一对get和放置功能形成了保留镜头。我们通过介绍有关代码重构，Pombrio和Krishnamurthi的重新定位以及XML同步的案例研究来证明保留镜头和DSL的实际使用。
Based on Foster et al.'s lenses, various bidirectional programming languages and systems have been developed for helping the user to write correct data synchronisers. The two well-behavedness laws of lenses, namely Correctness and Hippocraticness, are usually adopted as the guarantee of these systems. While lenses are designed to retain information in the source when the view is modified, well-behavedness says very little about the retaining of information: Hippocraticness only requires that the source be unchanged if the view is not modified, and nothing about information retention is guaranteed when the view is changed. To address the problem, we propose an extension of the original lenses, called retentive lenses, which satisfy a new Retentiveness law guaranteeing that if parts of the view are unchanged, then the corresponding parts of the source are retained as well. As a concrete example of retentive lenses, we present a domain-specific language for writing tree transformations; we prove that the pair of get and put functions generated from a program in our DSL forms a retentive lens. We demonstrate the practical use of retentive lenses and the DSL by presenting case studies on code refactoring, Pombrio and Krishnamurthi's resugaring, and XML synchronisation.
