Bidirectional Program Calculation with Effects

Bidirectional transformations (BXs) are a widely adopted approach for data synchronisation. It has many interesting applications, including the synchronization of replicated data in different formats, presentation-oriented structured document development, interactive user interface design, and coupled software transformation. Although several BX languages have been proposed for programming bidirectional transformations, writing complex bidirectional transformations that are both correct and efficient in those languages remains very challenging. Besides, in traditional BX theories, the two transformations in opposite directions must not have side-effects. While a few frameworks aim to lift this restriction by using monads, they are still quite limited, e.g., allowing only side-effects in the backwards transformation.In this research project, we aim to develop a reliable and effective method of program construction for bidirectional transformations by bringing the strength of program calculation techniques to the bidirectional world. This way programmers can write a straightforward and correct-by-construction transformation first and then systematically derive an efficient implementation from it while preserving correctness. Many practical bidirectional transformations are not pure functions in the mathematical sense, because they involve computational effects such as partiality, nondeterminism, mutable state, probabilistic behaviour, etc. We also plan to extend the theory with generic support for computational effects and formulate suitable descriptions so that it is possible to reason about bidirectional programs with these computational effects, and furthermore to optimize them.

Keywords:program calculation, bidirectional transformation, lens, algebraic effects

Disciplines:Language design, constructs and features

Project type:PhD project