Bidirectional transformations (BXs) are a widely adopted approach for data synchronisation that is usually based on two functions, one from the source to the view and one back. Traditionally, these functions must not have side effects. While a few frameworks aim to lift this restriction by introducing monads into lenses, they are still quite limited, e.g., allowing only side effects in the backwards transformation. In this paper, we propose a much more general framework for effectful lenses. Our effectful lenses can have different effects in their two directions, and the effects need not be cancellable. We also define the round-trip relations and use them to generalise the two well-known round-trip properties to effectful lenses. Moreover, composition preserves the two well-known round-trip properties, and we also provide a rich combinator language, which enables compositional programming for effectful lenses. Finally, we present a case study to illustrate the flexibility and expressivity of our framework.

Parsers and printers are vital for data synchronisation between different serialisation formats. As they are tightly related, much research has been devoted to showing that both can be derived from a single definition. It, however, turns out to be challenging to extend this work with exact-printing , which recovers the original source text for the parsed data. In this paper, we propose a new approach to tackling the challenge that considers a parser-printer pair as a mechanism to synchronize the input text string with the data, and formalizes them as a bidirectional program (lens). We propose the first biparser framework to support exact-printing with non-injective parsers, provide a library of combinators for common patterns, and demonstrate its usefulness with biparsers for subsets of JSON and YAML.

Bidirectional live programming systems (BLP) enable developers to modify a program by directly manipulating the program output, so that the updated program can produce the manipulated output. One state-of-the-art approach to BLP systems is operation-based, which captures the developer's intention of program modifications by taking how the developer manipulates the output into account. The program modifications are usually hard coded for each direct manipulation in these BLP systems, which are difficult to extend. Moreover, to reflect the manipulations to the source program, these BLP systems trace the modified output to appropriate code fragments and perform corresponding code transformations. Accordingly, they require direct manipulation users be aware of the source code and how it is changed, making “direct” manipulation (on output) be “indirect”. In this paper, we resolve this problem by presenting a novel operation-based framework for bidirectional live programming, which can automatically fuse direct manipulations into the source code, thus supporting code-insensitive direct manipulations. Firstly, we design a simple but expressive delta language DM capable of expressing common direct manipulations for output values. Secondly, we present a fusion algorithm that propagates direct manipulations into the source functional programs and applies them to the constants whenever possible; otherwise, the algorithm embeds manipulations into the “proper positions” of programs. We prove the correctness of the fusion algorithm that the updated program executes to get the manipulated output. To demonstrate the expressiveness of DM and the effectiveness of our fusion algorithm, we have implemented FuseDM, a prototype SVG editor that supports GUI-based operations for direct manipulation, and successfully designed 14 benchmark examples starting from blank code using FuseDM.

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.