Reference. Retentive Lenses

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.

Cite

Cite as @zhu-2020-retentive (helia, typst) · \cite{zhu-2020-retentive} (LaTeX)
BibTeX
bibtex · 8 lines
@misc{zhu-2020-retentive,
  author = {Zirun Zhu and Zhixuan Yang and Hsiang-Shang Ko and Zhenjiang Hu},
  title = {Retentive Lenses},
  year = {2020},
  month = {1},
  eprint = {2001.02031},
  archiveprefix = {arXiv}
}
hayagriva YAML (typst)
yaml · 11 lines
zhu-2020-retentive:
  type: misc
  title: Retentive Lenses
  author:
  - Zhu, Zirun
  - Yang, Zhixuan
  - Ko, Hsiang-Shang
  - Hu, Zhenjiang
  date: 2020-01
  serial-number:
    arxiv: '2001.02031'
zhu-2020-retentive reference entries/refs/zhu-2020-retentive/zhu-2020-retentive.hel