TY - GEN

T1 - Notions of bidirectional computation and entangled state monads

AU - Abou-Saleh, Faris

AU - Cheney, James

AU - Gibbons, Jeremy

AU - McKinna, James

AU - Stevens, Perdita

PY - 2015

Y1 - 2015

N2 - Bidirectional transformations (bx) support principled consistency maintenance between data sources. Each data source corresponds to one perspective on a composite system, manifested by operations to ‘get’ and ‘set’ a view of the whole from that particular 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 ‘set’ operations are stateful functions. This leads naturally to considering bx that exploit other computational effects too, such as I/O, nondeterminism, and failure, all largely 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 equational theory and important combinators for effectful bx, and provide a prototype implementation in Haskell along with several illustrative examples.

AB - Bidirectional transformations (bx) support principled consistency maintenance between data sources. Each data source corresponds to one perspective on a composite system, manifested by operations to ‘get’ and ‘set’ a view of the whole from that particular 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 ‘set’ operations are stateful functions. This leads naturally to considering bx that exploit other computational effects too, such as I/O, nondeterminism, and failure, all largely 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 equational theory and important combinators for effectful bx, and provide a prototype implementation in Haskell along with several illustrative examples.

UR - http://www.scopus.com/inward/record.url?scp=84937438634&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-19797-5_9

DO - 10.1007/978-3-319-19797-5_9

M3 - Conference contribution

AN - SCOPUS:84937438634

SN - 9783319197968

T3 - Lecture Notes in Computer Science

SP - 187

EP - 214

BT - Mathematics of Program Construction. MPC 2015

A2 - Voigtländer, Janis

A2 - Hinze, Ralf

PB - Springer

T2 - 12th International Conference on Mathematics of Program Construction 2015

Y2 - 29 June 2015 through 1 July 2015

ER -