A Coalgebraic Approach to Bidirectional Transformations
James McKinna, Faris Abou-Saleh, Jeremy Gibbons · Edinburgh Research Explorer (University of Edinburgh) · 2014
Bidirectional transformations (bx) are a diverse collection of formalisms for maintaining consistency between two or more related data models, such as (a)symmetric lenses [2] and algebraic bx [3]. In a previous paper [1] we proposed structures called set-bx as a unified framework for studying these formalisms. The main insight was that a bx between data sources A,B could be represented by get and set operations on both A and B – such as getA : MA and setA : A → M(), for some monad M – satisfying four ‘get-set’ laws. Crucially, updates to A may affect B, and vice versa; the operations on A and B will not commute in general, so that the states are entangled. There are two important, related issues such a framework needs to address. The first is how to compose two bx’s x : A ⇔ B and y : B ⇔ C, giving a bx (x ·y) : A⇔ C. The second is that this composition is often only associative, and has identities, up to some notion of equivalence of bx which must be identified. We hope to describe partial answers to these questions in the context of setbx in a companion paper. However, the state monads we often use to describe set-bx, and the corresponding composition and equivalence, also have an interesting interpretation in terms of coalgebras, which we illustrate in this extended abstract.