Monadic combinators for "Putback" style bidirectional programming
Monadic combinators for "Putback" style bidirectional programming
Date
2014
Authors
Hugo Pereira Pacheco
Hu,Z
Fischer,S
Journal Title
Journal ISSN
Volume Title
Publisher
Abstract
Bidirectional transformations, in particular lenses, are programs with a forward get transformation and a backward putback transformation that keep source and view data types synchronized. Several bidirectional programming languages exist to aid programmers in writing a (sort of) forward transformation, and deriving a backward transformation for free. However, the maintainability offered by such languages comes at the cost of expressiveness and (more importantly) predictability because the ambiguity of synchronization -handled by the putback transformation- is solved by default strategies over which programmers have little control. In this paper, we argue that controlling such ambiguity is essential for bidirectional transformations and propose a novel language in which programmers write a (sort of) putback transformation, and get the unique get transformation for free. Like traditional bidirectional languages, our put-oriented language allows reasoning about the correctness of defined transformations from the properties of their building blocks. But it allows programmers to describe the behavior of a bidirectional transformation much more precisely, while retaining the maintainability of writing a single program. We demonstrate the practical power of the new approach through a series of examples, ranging from simple ones that illustrate traditional lenses to complex ones for which our putback-based approach is central to specifying nontrivial update strategies. Categories and Subject Descriptors D.1.1 [Programming Techniques]: Applicative (Functional) Programming; D.3.1 [Programming Languages]: Formal Definitions and Theory; F.3.2 [Logics and Meanings of Programs]: Semantics of Programming Languages-Algebraic approaches to semantics.