Notions of Bidirectional Computation and Entangled State Monads

Abstract. Bidirectional transformations (bx) support principled consistency maintenance among data sources. Each data source corresponds to one perspective on a composite system, manifested by oper-ations to ‘get ’ and ‘put ’ a view of the whole from that perspective. Bx are important in a wide range of settings, including databases, interactive applications, and model-driven development. We show that bx are naturally modelled in terms of mutable state; in particular, the ‘put ’ operations are stateful functions. This leads naturally to considering bx that exploit other computational effects too, such as I/O, nondeterminism, and failure, which have largely been ignored in the bx literature to date. We present a semantic foundation for symmetric bidirectional transformations with effects. We build on the mature theory of monadic encapsulation of effects in functional programming, develop the equa-tional theory and important combinators, and provide a prototype implementation in Haskell along with several illustrative examples.