Lenses for Partially-Specified States (Extended Version)

TL;DR

This paper introduces partial-state lenses, a formal framework for managing multiple, partially specified views of data, enabling precise merging of user updates and ensuring consistent, compositional data synchronization.

Contribution

It formalizes partial-state lenses and well-behavedness, providing a novel approach to handling multiple views with partial information in bidirectional transformations.

Findings

Formalization of partial-state lenses and their properties

Demonstration of compositional reasoning with partial updates

Examples illustrating the utility of the proposed framework

Abstract

A bidirectional transformation is a pair of transformations satisfying certain well-behavedness properties: one maps source data into view data, and the other translates changes on the view back to the source. However, when multiple views share a source, an update on one view may affect the others, making it hard to maintain correspondence while preserving the user's update, especially when multiple views are changed at once. Ensuring these properties within a compositional framework is even more challenging. In this paper, we propose partial-state lenses, which allow source and view states to be partially specified to precisely represent the user's update intentions. These intentions are partially ordered, providing clear semantics for merging intentions of updates coming from multiple views and a refined notion of update preservation compatible with this merging. We formalize partial-state lenses, together with partial-specifiedness-aware well-behavedness that supports compositional reasoning and ensures update preservation. In addition, we demonstrate the utility of the proposed system through examples.