=Paper=
{{Paper
|id=Vol-1396/p16-abousaleh
|storemode=property
|title=Coalgebraic Aspects of Bidirectional Computation
|pdfUrl=https://ceur-ws.org/Vol-1396/p16-abousaleh.pdf
|volume=Vol-1396
|dblpUrl=https://dblp.org/rec/conf/staf/Abou-SalehMG15
}}
==Coalgebraic Aspects of Bidirectional Computation==
https://ceur-ws.org/Vol-1396/p16-abousaleh.pdf
Coalgebraic Aspects of Bidirectional Computation
Faris Abou-Saleh1 James McKinna2 Jeremy Gibbons1
1. Department of Computer Science 2. School of Informatics
University of Oxford, UK University of Edinburgh, UK
{Faris.Abou-Saleh,Jeremy.Gibbons}@cs.ox.ac.uk James.McKinna@ed.ac.uk
Abstract
We have previously (Bx, 2014; MPC, 2015) shown that several state-
based bx formalisms can be captured using monadic functional pro-
gramming, using the state monad together with possibly other monadic
effects, giving rise to structures we have called monadic bx (mbx). In
this paper, we develop a coalgebraic theory of state-based bx, and relate
the resulting coalgebraic structures (cbx) to mbx. We show that cbx
support a notion of composition coherent with, but conceptually sim-
pler than, our previous mbx definition. Coalgebraic bisimulation yields
a natural notion of behavioural equivalence on cbx, which respects com-
position, and essentially includes symmetric lens equivalence as a spe-
cial case. Finally, we speculate on the applications of this coalgebraic
perspective to other bx constructions and formalisms.
1 Introduction
Many scenarios in computer science involve multiple, partially overlapping, representations of the same data,
such that whenever one representation is modified, the others must be updated in order to maintain consistency.
Such scenarios arise for example in the context of model-driven software development, databases and string
parsing [6]. Various formalisms, collectively known as bidirectional transformations (bx), have been developed
to study them, including (a)symmetric lenses [8, 16], relational bx [30], and triple-graph grammars [27].
In recent years, there has been a drive to understand the similarities and differences between these formalisms
[18]; and a few attempts have been made to give a unified treatment. In previous work [5, an extended abstract]
and [1, to appear], we outlined a unified theory, with examples, of various accounts of bx in the literature, in
terms of computations defined monadically using Haskell’s do-notation. The idea is to interpret a bx between two
data sources A and B (subject to some consistency relation R ⊆ A × B ) relative to some monad M representing
computational effects, in terms of operations, getL : MA and setL : A → M (), and similarly getR , setR for B ,
which allow lookups and updates on both A and B while maintaining R. We defined an effectful bx over a
monad M in terms of these four operations, written as t : A ⇐⇒M B , subject to several equations in line with
the Plotkin–Power equational theory of state [23]. The key difference is that in a bidirectional context, the
sources A and B are interdependent, or entangled : updates to A (via setL ) should in general affect B , and vice
versa. Thus we must abandon some of the Plotkin–Power equations; for instance, one no longer expects setL to
commute with setR . To distinguish our earlier effectful bx from the coalgebraic treatment to be developed in
this paper, we will refer to them as monadic bx, or simply mbx, from now on.
We showed that several well-known bx formalisms may be described by monadic bx for the particular case
of the state monad, MS X = S → (X × S ), called State S in Haskell. Moreover, we introduced a new class
of bx: monadic bx with effects, expressed in terms of the monad transformer counterpart TSM to MS (called
StateT S M in Haskell), where TSM X = S → M (X × S ) builds on some monad M , such as I/O. We defined
Copyright c by the paper’s authors. Copying permitted for private and academic purposes.
In: A. Cunha, E. Kindler (eds.): Proceedings of the Fourth International Workshop on Bidirectional Transformations (Bx 2015),
L’Aquila, Italy, July 24, 2015, published at http://ceur-ws.org
16
composition t1 # t2 for those mbx with transparent get operations – i.e. gets which are effect-free and do not
modify the state. The definition is in terms of StateT -monad morphisms derived from lenses (see Section 5),
adapting work of Shkaravska [28]. As with symmetric lenses, composition can only be well-behaved up to some
notion of equivalence, due to the different state-spaces involved. We showed that our definition of composition
was associative and had identities up to an equivalence defined by monad morphisms – in particular, given by
isomorphisms of state-spaces.
Although this equivalence is adequate for analysing such properties, it proves unsuitably fine-grained for
comparing other aspects of bx behaviour. For instance, one may be interested in optimisation; one would then
like some means of reasoning about different implementations, to check that they indeed have the same behaviour.
Such reasoning is not possible based solely on state-space isomorphisms. As most of our work considers state-
based bx, it is natural to ask whether one can identify an alternative, less ad-hoc, notion of equivalence.
In this paper, we present a coalgebraic treatment of our earlier work on monadic bx, inspired by Power
and Shkaravska’s work on variable arrays and comodels [24] for the theory of mutable state. Previously, we
considered structure relative to the categories Set, Hask (Haskell types and functions); in particular, we argued
that the composite mbx operations we defined on the underlying simple types respected appropriate set-theoretic
invariants. Here, the coalgebraic approach has several benefits: firstly, it gives a more direct categorical treatment
of bx composition, in terms of pullbacks. More importantly, it allows us to improve on our earlier notion of
equivalence given by state-space isomorphism, appealing instead to the theory of coalgebraic bisimularity [26];
in particular, we relate it to the equivalence on symmetric lenses [16].
The technical contributions and structure of this paper are as follows. Firstly, in Section 2 we identify a
categorical setting, and useful properties, for interpreting bx in terms of coalgebras. In Section 3, we introduce
an equivalence on coalgebras, namely pointed coalgebraic bisimulation, and demonstrate how this equivalence
relates to that of symmetric lenses, in addition to various effectful bx scenarios. (Pointedness identifies initial
states, with respect to which coalgebra behaviours are compared.) In Section 4 we give a detailed account of
composition of coalgebraic bx in terms of pullbacks, which is both more direct and categorically general than
our earlier definition [1], highlighting subtleties in the definitions (such as Remark 4.8). We prove that our
coalgebraic notion of composition is associative, and has identities, up to the equivalence we have introduced.
Finally, in Section 5 we show that coalgebraic bx composition is coherent with that of [1].
NB We discuss only key ideas and techniques; an extended version with detailed proofs is available at
http://groups.inf.ed.ac.uk/bx/cbx-tr.pdf.
2 Coalgebraic bx
2.1 Categorical Prerequisites
1. We will assume an ambient category C with finite products X × Y and exponentials X Y (essentially,
the space of functions from Y to X ), on which a strong monad M is defined. (See for example Moggi’s
original paper [21] for a discussion of the need for such structure.) This allows us to make free use of the
equational theory of do-notation as the internal language of the Kleisli category Kl(M ) (see [9] for more
detail). Rather than using pointfree strength and associativity isomorphisms, do-notation is convenient for
representing value-passing between functions using pointwise syntax.
2. In order to define coalgebraic bx composition in Section 4, we further require that C have pullbacks, and
that M weakly preserve them [11]; we say “M is wpp”, for short. The following diagrams make this more
explicit. Recall that a pullback of two arrows f : X → B and g : Y → B is an object P and span of arrows
pX : P → X , pY : P → Y making the below-left diagram commute, such that for any object Q and span
cX , cY making the outermost ‘square’ in the middle diagram commute, there is a unique arrow h making the
whole diagram commute. Finally, the wpp property (for M ) asserts that the span M pX , M pY forms a weak
pullback of Mf and Mg: for any object S and span dX , dY making the outermost ‘square’ in the right-hand
diagram commute, there is an arrow k , not necessarily unique, making the whole diagram commute.
pX
P /X Q cX S dX
∃!h ∃k
pY pY " M pY "
f / MX
P /X MP
cY dY
g X p f M pX Mf
Y /B ! g ! Mg
Y /B MY / MB
17
3. For technical reasons, we assume that the return of the monad M is monic: this allows us to observe the
value x wrapped in an effect-free computation return x . Most computational monads (we are unaware of
natural counterexamples) have this property: e.g. global state, I/O, non-determinism, and exceptions [22].
4. Lastly, we assume an object I , such that arrows x : I → X represent “elements” x of an object X . Typically,
as in Set, I might be the terminal object 1, but if C is symmetric monoidal closed (e.g. pointed cpos and
strict maps), then I could be the monoidal unit.
Remark 2.1. The wpp condition lets us consider (at least for C = Set) monads M of computational interest
such as (probabilistic) non-determinism [12, 29], which are wpp but do not preserve pullbacks; more generally,
we can include I/O, exceptions, and monoid actions, by appealing to a simple criterion to check wpp holds for
such M [11, Theorem 2.8].
2.2 Bx as Pointed Coalgebras
We now give a coalgebraic description of bx, i.e. as state-based systems. We begin by noting that many bx
formalisms, such as (a)symmetric lenses and relational bx, often involve an initialised state. The behaviours of
two such bx are compared relative to their initial states. Hence, to reason about such behaviour, throughout
this paper we concern ourselves with pointed coalgebras with designated initial state. Coalgebras with the
same structure, but different initial states, are considered distinct (see [3] for more general considerations).
Corollary 4.14 makes explicit the categorical structure of bx represented by such structures.
Definition 2.2. For an endofunctor F on a category C, a pointed F -coalgebra is a triple (X , α, α ) consisting
of: an object X of C – the carrier or state-space; an arrow α : X → FX – its structure map or simply structure;
and an arrow α : I → X picking out a distinguished initial state. We abuse notation, typically writing α for the
pointed coalgebra itself.
Now we define the behaviour functors we use to describe bx coalgebraically; as anticipated above, we incorpo-
rate a monad M into the definition from the outset to capture effects, although for many example classes, such
as symmetric lenses, it suffices to take M = Id , the identity monad. Here are several example settings, involving
more interesting monads, to which we return in Section 3.2:
• Interactive I/O. In [1] we gave an example of an mbx which notifies the user whenever an update occurred.
Extending this example further, after an update to A or B , in order to restore consistency (as specified e.g.
by a consistency relation R ⊆ A × B ) the bx might prompt the user for a new B or A value respectively
until a consistent value is supplied. Such behaviour may be described in terms of a simplified version of the
I/O monad MX = νY . X + (O × Y ) + Y I given by a set O of observable output labels, and a set of inputs
I that the user can provide. Note that the ν-fixpoint permits possibly non-terminating I/O interactions.
• Failure. Sometimes it may be simply impossible to propagate an update on A across to B , or vice versa;
there is no way to restore consistency. In this case, the update request should simply fail; and we may model
this with the Maybe monad MX = 1 + X .
• Non-determinism. There may be more than one way of restoring consistency between A and B after
an update. In this case, rather than prompting the user at every such instance, it may be preferable for
a non-deterministic choice to be made. We may model this situation by taking the monad M to be the
(finitary) powerset monad.
M A B
Definition 2.3. For objects A and B , define the functor FAB (−) = A × (M (−)) × B × (M (−)) .
M
For a given choice of objects A and B , we will use the corresponding functor FAB to characterise the behaviour
M
of those bx between A and B , as FAB -coalgebras. By taking projections, we can see the structure map α : X →
M M
FAB X of a pointed FAB -coalgebra as supplying four pieces of data: a function X → A which observes the
A
A-value in a state X ; a function X → (MX ) which, uncurried into the form X × A → MX , gives us the side-
effectful result MX of updating the A-value in the state X ; and two similar functions for B . These respectively
correspond to the getL , setL , getR , and setR functions of a monadic bx with respect to the state monad MX
(with state-space X ), as outlined above. Note that in this coalgebraic presentation, the behaviour functor makes
clear that the get operations are pure functions of the coalgebra state – corresponding to ‘transparent’ bx [1].
M A
Convention 2.4. Given α : X → FAB X , we write α.getL : X → A, and α.setL : X → (MX ) , for the
B
corresponding projections, called ‘left’- or L-operations, and similarly α.getR : X → B , α.setR : X → (MX ) for
the other projections, called R-operations. Where α may be inferred, and we wish to draw attention to the carrier
X , we also write x .getL for α.getL x , and similarly for the other L-, R-operations.
18
M S
Remark 2.5. Note that FAB may be defined in terms of the costore comonad S × (−) , used in [24] to describe
arrays of independent variables. However, we differ in not allowing simultaneous update of each source (which
would take S = A × B ), because updates to A may affect B , and vice versa.
M
To ensure that pointed FAB -coalgebras provide sensible implementations of reading and writing to A and B ,
we impose laws restricting their behaviour. We call such well-behaved coalgebras coalgebraic bx, or cbx.
M M
Definition 2.6. A coalgebraic bx is a pointed FAB -coalgebra (X , α : X → FAB X , α ) for which the following
laws hold at L (writing x .getL for α.getL x , etc. as per Convention 2.4):
(CGetSetL ) (α) : x .setL (x .getL ) = return x
(CSetGetL ) (α) : do {x ← x .setL a; return (x , x .getL )} = do {x 0 ← x .setL a; return (x 0 , a)}
0 0 0
and the corresponding laws (CSetGetR ) and (CGetSetR ) hold at R.
These laws are the analogues of the (GS), (SG) laws [1] which generalise those for well-behaved lenses [8, see
also Section 5.2 below]. They also correspond to a subset of the laws for coalgebras of the costore comonad
S × (−)S , again for S = A and S = B independently, but excluding the analogue of ‘Put-Put’ or very-well-
behavedness of lenses [10]. We typically refer to a cbx by its structure map, and simply write α : A −X B , where
−
we may further omit explicit mention of X .
Here is a simple example of a cbx, which will provide identities for cbx composition as defined in Section 4
below. Note that there is a separate identity bx for each pair of an object A and initial value e : A.
Example 2.7. Given (A, e : A), there is a trivial cbx structure ι(e) : A − A A defined by ι(e) = e; a.getL = a =
−
a.getR ; a.setL a 0 = return a 0 = a.setR a 0 .
Remark 2.8. Our definition does not make explicit any consistency relation R ⊆ A × B on the observable A
and B values; however, one obtains such a relation from the get functions applied to all possible states, viz.
R = {(a, b) : ∃x . getL x = a ∧ getR x = b }. One may then show that well-behaved cbx do, indeed, maintain
consistency wrt R.
3 Behavioural Equivalence and Bisimulation
In this section, we introduce the notion of pointed coalgebraic bisimulation, which defines a behavioural equiva-
lence ≡ for pointed cbx. In Section 3.1 we compare this equivalence to the established notion of equivalence for
symmetric lenses. We then discuss in Section 3.2 the behavioural equivalences induced for the classes of effectful
bx described in Section 2.2: interactive I/O, failure, and non-determinism.
Definition 3.1. A pointed (F -)coalgebra morphism h between pointed coalgebras (X , α, α ) and (Y , β, β ) is a
map h : X → Y such that β ◦ h = Fh ◦ α and h ◦ α = β .
M
Remark 3.2. In terms of do notation, h : X → Y being an FAB -coalgebra morphism between α and β is
equivalent to the following laws (where we again write x .setL for α.setL x , and so on):
(CGetPL )(h) : x .getL = (h x ).getL
(CSetPL )(h) : do {x 0 ← x .setL a; return (h x 0 )} = do {let y = (h x ); y 0 ← y.setL a; return y 0 }
We now define a modest generalisation to C of the standard Set-based definition of (coalgebraic) bisimulation
relations [19]. (Since we are concerned only with the existence of bisimulations between X and Y , we may
consider them to be given non-uniquely by some jointly monic pair, as follows).
Definition 3.3. A bisimulation between pointed coalgebras α and β is a pointed coalgebra ζ and a span (p, q)
of pointed coalgebra morphisms p : ζ → α, q : ζ → β which is jointly monic (in C) – meaning that whenever
p ◦ f = p ◦ f 0 and q ◦ f = q ◦ f 0 , we have f = f 0 .
Definition 3.3 characterises bisimulation in the concrete case C = Set and M = Id as follows:
Id
Proposition 3.4. A pointed FAB -bisimulation R on a pair of coalgebraic bxs α, β is equivalent to a relation
R ⊆ X × Y such that (α , β ) ∈ R, and (x , y) ∈ R implies, for all a : A and b : B ,
• x .getL = y.getL and x .getR = y.getR ;
• (x .setL a, y.setL a) ∈ R, and (x .setR b, y.setR b) ∈ R.
Definition 3.5. We say that two cbx α, α0 are behaviourally equivalent, and write α ≡ α0 , if there exists a
pointed coalgebraic bisimulation (ζ, p, q) between α and α0 .
19
3.1 Relationship with Symmetric Lens Equivalence
In this subsection, we describe symmetric lenses (SL) [16] in terms of cbx, and relate pointed bisimilarity between
cbx and symmetric lens (SL-)equivalence [ibid., Definition 3.2]. First of all, it is straightforward to describe a
symmetric lens between A and B with complement C – given by a pair of functions putr :: A × C → B × C ,
putl :: B × C → A × C and initial state C together satisfying two laws – as a cbx: take M = Id and state-
space X = A × C × B , encapsulating the current value of the lens complement C , as well as those of A and B
(cf. [5, Section 4]). We now define the analogues of the SL-operations for a cbx between A and B :
Definition 3.6. (Note that this is the opposite L-R convention from [16]!)
x .put L : A → (B × X ) x .put L a = let x 0 = x .setL a in (x 0 .getR , x 0 )
x .put R : B → (A × X ) x .put R b = let x 0 = x .setR b in (x 0 .getL , x 0 )
Proposition 3.7. Taking C = Set and M = Id , a pointed FAB Id
-bisimulation R between cbxs α, β is equivalent
to a relation R ⊆ X × Y such that (α , β ) ∈ R, and (x , y) ∈ R implies the following:
• x .getL = y.getL and x .getR = y.getR ;
• for all a : A, x .put L a = (b 0 , x 0 ) and y.put L a = (b 0 , y 0 ) for some b 0 and (x 0 , y 0 ) ∈ R;
• for all b : B , x .put R b = (a 0 , x 0 ) and y.put R b = (a 0 , y 0 ) for some a 0 and (x 0 , y 0 ) ∈ R.
Expressing cbx equivalence in these terms reveals that it is effectively identical to SL-equivalence. The
cosmetic difference is that we are able to observe the ‘current’ values of A and B in any given state, via the
get functions. This information is also implicitly present in SL-equivalence, where a sequence of putr or putl
operations amounts to a sequence of sets to A and B , but where we cannot observe which values have been set.
Here, the get operations make this information explicit. We say more about the categorical relationship between
cbx and SLs in Corollary 4.15 below.
3.2 Coalgebraic Bisimilarity with Effects
By introducing effects through M , our coalgebraic definition of behavioural equivalence allows us to characterise
a wide class of behaviours in a uniform manner, and we illustrate with the examples anticipated in Section 2.2.
3.2.1 Interactive I/O
We take MX = νY . X + (O × Y ) + Y I , where O is a given set of observable outputs, and I inputs the user
can provide. The components of the disjoint union induce monadic return : X → MX and algebraic operations
out : O × MX → MX and in : (I → MX ) → MX (c.f. [23]). In the context of cbx that exhibit I/O effects in this
A
way, an operation like setL : X → (MX ) maps a state x : X and an A-value a : A to a value m : MX , where m
describes some path in an (unbounded) tree of I/O actions, either terminating eventually and returning a new
state in X , or diverging (depending on the user’s input).
One may characterise pointed bisimulations on such cbx as follows. Intuitively, behaviourally equivalent
states must “exhibit the same observable I/O activity” during updates setL and setR , and subsequently arrive at
behaviourally equivalent states. To formalise this notion of I/O activity, we need an auxiliary definition (which
derives from the greatest-fixpoint definition of M ):
Definition 3.8. With respect to an I/O monad M and a relation R ⊆ X × Y , the I/O-equivalence relation ∼R
⊆ MX × MY induced by R is the greatest equivalence relation such that m ∼R n whenever:
• m = return x , n = return y, and (x , y) ∈ R for some x , y; or
• m = out (o, m 0 ) and n = out (o, n 0 ) for some o : O and m 0 ∼R n 0 ; or
• m = in (λi → m(i )) and n = in (λi → n(i )), where m(i ) ∼R n(i ) for all i : I .
M
One may now show that a pointed FAB -bisimulation R on a pair of such cbxs α, β is equivalent to a relation
R ⊆ X × Y such that (α , β ) ∈ R, and (x , y) ∈ R iff
• x .getL = y.getL and x .getR = y.getR ;
• for all a : A and b : B , (x .setL a) ∼R (y.setL a) and (x .setR b) ∼R (y.setR b).
Such an equivalence guarantees that, following any sequence of updates in α or β, the user experiences exactly
the same sequence of I/O actions; and when the sequence is complete, they observe the same values of A and B
for either bx. Thus, pointed bisimulation asserts that α, β are indistinguishable from the user’s point of view.
20
3.2.2 Failure
Here we take MX = 1 + X , and write None and Just x for the corresponding components of the coproduct. This
induces a simple equivalence on pairs of bx, asserting that sequences of updates to either bx will succeed or fail
in the same way. More formally, a pointed bisimulation R on a pair of coalgebraic bxs α, β is equivalent to a
relation R ⊆ X × Y such that (α , β ) ∈ R, and (x , y) ∈ R iff for all a : A and b : B ,
• x .getL = y.getL and x .getR = y.getR ;
• if x .setL a = None then y.setL a = None – and vice versa;
• if x .setL a = Just x 0 , then y.setL a = Just y 0 for some y 0 with (x 0 , y 0 ) ∈ R – and vice versa;
• two analogous clauses with B and setR substituted for A and setL .
3.2.3 Non-determinism
Taking M to be the finitary powerset monad, the resulting behavioural equivalence on bx comes close to the
standard notion of strong bisimulation on labelled transition systems – and as we will see, shares its excessive
M
fine-grainedness. A pointed FAB -bisimulation R on a pair of cbxs α, β is equivalent to a relation R ⊆ X × Y
such that (α , β ) ∈ R, and (x , y) ∈ R iff for all a : A and b : B ,
• x .getL = y.getL ;
• for all a : A and x 0 ∈ x .setL a, there is some y 0 ∈ y.setL a with (x 0 , y 0 ) ∈ R;
• for all a : A and y 0 ∈ y.setL a, there is some x 0 ∈ x .setL a with (x 0 , y 0 ) ∈ R;
• three analogous clauses with B and getR /setR substituted for A and getL /setL .
In contrast with the case of user I/O, this equivalence may be too fine for comparing bx behaviours, as it
exposes too much information about when non-determinism occurs. Here is a prototypical scenario: consider the
effect of two successive L-updates. In one implementation, suppose an update setL a changes the system state
from s to t, and a second update setL a 0 changes it to either u or u 0 . Each state-change is only observable to
the user through the values of getL and getR ; so suppose u.getR = u 0 .getR = b. (Note that u.getL = u 0 .getL = a 0
by (CGetSetL )). This means u and u 0 cannot be distinguished by their get values.
In a different implementation, suppose setL a instead maps s to one of two states t 0 or t 00 (both with the same
values of getR and getL as state t above), and then setL a 0 maps these respectively to u and u 0 again. The states
called s in both implementations, although indistinguishable to any user by observing their get values, are not
bisimilar. In such situations, a coarser ‘trace-based’ notion of equivalence may be more appropriate [14].
4 Coalgebraic bx Composition
A cbx α : A − X B describes how changes to a data source A are propagated across X to B (and vice versa).
−
It is then natural to suppose, given another such β : B − Y C , that we may propagate these changes to C (and
−
vice versa), raising the question of whether there exists a composite cbx α • β : A −Z C for some Z . Here, we
−
give a more general, coalgebraic definition of cbx composition than our previous account for mbx [1]; this lets us
reason about behavioural equivalence of such compositions in Section 4.1.
First, we introduce some necessary technical details regarding weak pullback preserving (wpp) functors. Wpp
functors are closed under composition, and we also exploit the following fact:
Lemma 4.1. A wpp functor preserves monomorphisms, or “monos” (maps f which are ‘right cancellable’:
g.f = h.f implies g = h) [25, Lemma 4.4].
M
Remark 4.2. The following technical observation will also be useful for reasoning about FAB -coalgebras. As M
M A
is wpp (assumption 2 of Section 2.1), so too is FAB , using the fact that A × (−) and (−) preserve pullbacks,
M
and hence are wpp. Then by Lemma 4.1, FAB also preserves monos.
Finally, we will employ the following in proofs, where k x a is a block of statements referring to x and a:
Lemma 4.3. (CSetGetL ) and (CGetSetL ) are equivalent to the following ‘continuation’ versions:
(CGetSetL ) (α) : do {let a = x .getL ; x 0 ← x .setL a; k x 0 a } = do {let a = x .getL ; k x a }
(CSetGetL ) (α) : do {x 0 ← x .setL a; k x 0 (x 0 .getL )} = do {x 0 ← x .setL a; k x 0 a }
Similarly, there are continuation versions of the coalgebra-morphism laws (CGetPL )(h), (CSetPL )(h), etc. in
Remark 3.2, which we omit. We are now ready to define cbx composition; we do this in four stages.
21
(i) Defining a State-space for the Composition of α and β
The state-spaces of coalgebraic bx α : A − X B , β : B −
− Y C both contain information about B , in addition to
−
A and C respectively. As indicated above, we define the state-space Z of the composite as consisting of those
(x , y) pairs which are ‘B -consistent’, in that x .getR = y.getL . We must also identify an initial state in Z ; the
obvious choice is the pair (α , β ) of initial states from α and β. To lie in Z , this pair itself must be B -consistent:
α .getR = β .getL . We may only compose cbx whose initial states are B -consistent in this way.
We now give the categorical formulation of these ideas, in terms of pullbacks:
Definition 4.4. Given two pointed cbx α:A − X B and β :B −
− Y C , we define a state-space for their composition
−
α • β to be the pullback Pα,β in the below-left diagram. It is straightforward to show that this also makes the
below-right diagram (also used in Step ((iii)) below) into a pullback, where eα,β is defined to be hpα , pβ i.
pβ eα,β =hpα ,pβ i
Pα,β /Y Pα,β / X ×Y
pα β.getL pα α.getR ×β.getL
α.getR hα.getR ,α.getR i
X /B X / B ×B
For instance, in the category Set, these definitions may be interpreted as follows:
Pα,β = {(x , y) | x .getR = y.getL } = {(x , y) | (x .getR , y.getL ) = (x .getR , x .getR )}
and α•β is the pair of initial states (α , β ), assuming α .getR = β .getL .
Remark 4.5. Towards proving properties of the composition α • β in Section 3, we note that eα,β is also the
equalizer of the parallel pair of arrows α.getR ◦ π1 , β.getL ◦ π2 : X × Y → B . Hence, a fortiori eα,β is monic (i.e.
M
left-cancellable), and thus by Lemma 4.1, so too is its image under the wpp functors M and FAB .
This allows us to pick out an initial state for Z , by noting that the arrow (α , β ) : I → X × Y equalizes the
parallel pair of morphisms in Remark 4.5; universality then gives the required arrow α•β : I → Z .
(ii) Defining Pair-based Composition α β
M
Definition 4.6. (X × Y , α β) is an FAC -coalgebra with L-operations (similarly for R):
(x , y).getL = x .getL (x , y).setL a = do {x 0 ← x .setL a; y 0 ← y.setL (x 0 .getR ); return (x 0 , y 0 )}
(iii) Inducing the Coalgebra α • β on the Pullback
We now prove that the set operations of α β produce B -consistent pairs – even if the input pairs (x , y) were not
B -consistent (because the set operations involve retrieving a B -value from one bx, and setting the same value
in the other). Note that this implies α β will generally fail to be a coalgebraic bx, as it will not satisfy the
coalgebraic bx law (CGetSet): getting and then setting A or C in a B -inconsistent state will result in a different,
B -consistent state, in contrast to the law’s requirement that this should not change the state.
Lemma 4.7. The following equation (†L ) holds at L for the setL operation of Definition 4.6, and a corresponding
property (†R ) for setR . (The last two occurrences of x 0 .getR may equivalently be replaced with y 0 .getL .)
do {(x 0 , y 0 ) ← (x , y).setL a; return (x 0 .getR , y 0 .getL )}
(†L )
= do {(x 0 , y 0 ) ← (x , y).setL a; return (x 0 .getR , x 0 .getR )}
Proof. We prove (†L ); the argument for (†R ) is symmetric.
do {(x 0 , y 0 ) ← (x , y).setL a; return (x 0 .getR , y 0 .getL )}
= [[ definition of (x , y).setL ]]
do {x 0 ← x .setL a; let b = x 0 .getR ; y 0 ← y.setL b; return (x 0 .getR , y 0 .getL )}
= [[ (CSetGet) (β), where k y 0 b is return (x 0 .getR , b) (N.B. k doesn’t use y 0 ) ]]
do {x 0 ← x .setL a; let b = x 0 .getR ; y 0 ← y.setL b; return (x 0 .getR , b)}
= [[ undo inlining of let b = x 0 .getR ]]
do {x 0 ← x .setL a; let b = x 0 .getR ; y 0 ← y.setL b; return (x 0 .getR , x 0 .getR )}
= [[ definition of (x , y).setL ]]
do {(x 0 , y 0 ) ← (x , y).setL a; return (x 0 .getR , x 0 .getR )}
22
Remark 4.8. In general, this is a stronger constraint than the corresponding equation
do {(x 0 , y 0 ) ← (x , y).setL a; return (x 0 .getR )} = do {(x 0 , y 0 ) ← (x , y).setL a; return (y 0 .getL )} (†∗L )
although it is equivalent if the monad M preserves jointly monic pairs (Definition 3.3). To illustrate the difference,
suppose B = {0, 1} and consider a non-deterministic setting, where M is the (finitary) powerset monad on Set
(and indeed, it does not preserve jointly monic pairs). In state (x , y), suppose that (setL a) can land in either
of two new states (x1 , y1 ) or (x2 , y2 ), where x2 .getR = y1 .getL = 0 and x1 .getR = y2 .getL = 1. Then (†∗L ) holds
at (x , y) as both sides give {0, 1}, but (†L ) does not, because the left side gives {(0, 1), (1, 0)} and the right gives
{(0, 0), (1, 1)}. We require the stronger version (†L ) to correctly define composition below.
Our goal is to show that the properties (†L ) and (†R ) together are sufficient to ensure that the operations
M
of α β : X × Y → FAC (X × Y ), restricted to the B -consistent pairs Pα,β , induce well-defined operations
M
Pα,β → FAC Pα,β on the pullback.
To do this, it is convenient to cast the properties (†L ), (†R ) in diagrammatic form, as shown in the left-hand
diagram below. (It also incorporates two vacuous assertions, (x , y).getL = (x , y).getL and similarly at R, which
we may safely ignore.) Then, we precompose this diagram with the equalizer eα,β as shown below-right, defining
M M
δ to be the resulting arrow Pα,β → FAB X given by the composition FAB π1 ◦ (α β) ◦ eα,β .
eα,β
X ×Y Pα,β / X ×Y
αβ αβ
M M
FAC (X × Y ) δ := FAC (X × Y )
M M
FAC π1 FAC π1
M M
FAC (α.getR ×β.getL ) FAC (α.getR ×β.getL )
v v
M / F M (B × B ) M / F M (B × B )
FAC X AC FAC X AC
M M
FAC hα.getR ,α.getR i FAC hα.getR ,α.getR i
M M
Under the assumption that M is wpp, so is FAC . Hence, the image under FAC of the ‘alternative’ pullback
characterisation of Pα,β (the right-hand diagram in Definition 4.4) is a weak pullback; it is shown below-left.
Now the above-right diagram contains a cone over the same span of arrows; hence (by definition) we obtain a
M
mediating morphism Pα,β → FAC (Pα,β ) (not a priori unique) as shown below-right. We take this to be the
coalgebra structure α • β of the composite bx.
M
FAC eα,β eα,β
M / F M (X × Y ) / X ×Y
FAC Pα,β AC Pα,β
α•β
αβ
% M
FAC eα,β
M M M / F M (X × Y )
FAC pα FAC (α.getR ×β.getL ) δ FAC Pα,β AC
M
FAC pα
M
FAC (α.getR ×β.getL )
y
M / F M (B × B )
FAC X AC
M
FAC X / F M (B × B )
AC
M
M
FAC hα.getR ,α.getR i FAC hα.getR ,α.getR i
Although this does not explicitly define the operations of the composition α • β, it does relate them to those
M
of α β via the monic arrow FAC eα,β (Remark 4.5) – allowing us to reason in terms of B -consistent pairs
(x , y) : X × Y , appealing to left-cancellability of monos. Moreover, in spite of only weak pullback preservation
M
of FAB , the coalgebra structure α • β is canonical: there can be at most one coalgebra structure α • β such that
eα,β is a coalgebra morphism from α • β to α β. This is a simple corollary of Lemma 4.11 below.
(iv) Proving the Composition is a Coalgebraic bx
Proposition 4.9. (CGetSet) (α • β) and (CSetGet) (α • β) hold at L and R.
Proof. We focus on the L case (the R case is symmetric). As described in (iii) above, we prove the laws post-
composed with the monos M eα,β and M (eα,β × id ) respectively; left-cancellation completes the proof. (The law
(CSetPL )(eα,β ) is given after Definition 3.1 below.) Here is (CGetSetL ) (α • β) postcomposed with M eα,β :
23
do {let a = z .getL ; z 0 ← z .setL a; return (eα,β (z 0 ))}
= [[ (CSetPL )(eα,β ) ]]
do {let a = z .getL ; let (x , y) = eα,β (z ); (x 0 , y 0 ) ← (x , y).setL a; return (x 0 , y 0 )}
= [[ swapping lets, and using (CGetPA )(eα,β ) ]]
do {let (x , y) = eα,β (z ); let a = (x , y).getL ; (x 0 , y 0 ) ← (x , y).setL a; return (x 0 , y 0 )}
= [[ definitions of (x , y).getL and (x , y).setL ]]
do {let (x , y) = eα,β (z ); let a = x .getL ; x 0 ← x .setL a; let b = x 0 .getR ; y 0 ← y.setL b; return (x 0 , y 0 )}
= [[ (CGetSetA ) for α ]]
do {let (x , y) = eα,β (z ); let b = x .getR ; y 0 ← y.setL b; return (x , y 0 )}
= [[ (x , y) = eα,β (z ) implies x .getL = y.getR by definition of eα,β ]]
do {let (x , y) = eα,β (z ); let b = y.getL ; y 0 ← y.setL b; return (x , y 0 )}
= [[ (CGetSetL ) for β ]]
do {let (x , y) = eα,β (z ); return (x , y)}
= [[ inline let; do-laws ]]
return eα,β (z )
(CSetGetL ) postcomposed with M (eα,β × id ):
do {z 0 ← z .setL (a); return (eα,β (z 0 ), z 0 .getL )}
= [[ inlining let; definition of z 0 .getL ]]
do {z 0 ← z .setL (a); let (x 0 , y 0 ) = eα,β (z 0 ); return ((x 0 , y 0 ), x 0 .getL )}
= [[ (CSetPL )(eα,β ) ]]
do {let (x , y) = eα,β (z ); (x 0 , y 0 ) ← (x , y).setL a; return ((x 0 , y 0 ), x 0 .getL )}
= [[ definition of (x , y).setL ]]
do {let (x , y) = eα,β (z ); x 0 ← x .setL a; let b = x 0 .getR ; y 0 ← y.setL b; return ((x 0 , y 0 ), x 0 .getL )}
= [[ (CSetGetL ) for α ]]
do {let (x , y) = eα,β (z ); x 0 ← x .setL a; let b = x 0 .getR ; y 0 ← y.setL b; return ((x 0 , y 0 ), a)}
= [[ definition of (x , y).setL ]]
do {let (x , y) = eα,β (z ); (x 0 , y 0 ) ← (x , y).setL a; return ((x 0 , y 0 ), a)}
= [[ (CSetPL )(eα,β ); inline let ]]
do {z 0 ← z .setL a; return (eα,β (z 0 ), a)}
4.1 Well-behavedness of cbx Composition
Having defined a notion of composition for cbx, we must check that it has the properties one would expect, in
particular that it is associative and has left and right identities. However, as noted in the Introduction, we cannot
expect these properties to hold ‘on the nose’, but rather only up to some notion of behavioural equivalence. We
will now prove that cbx composition is well-behaved up to the equivalence ≡ introduced in Section 3 (Definition
3.5). Recall also the identity cbx ι (a) : A − A introduced in Example 2.7.
−
Theorem 4.10. Coalgebraic bx composition satisfies the following properties (where α, α0 :A − B , β, β 0 :B −
− C,
−
0 D, and all compositions are assumed well-defined):
and γ, γ : C −−
identities: ι(α .getL ) • α ≡ α and α • ι(α .getR ) ≡ α
congruence: if α ≡ α0 and β ≡ β 0 then α • β ≡ α0 • β 0
associativity: (α • β) • γ ≡ α • (β • γ)
To prove this, we typically need to exhibit a coalgebra morphism from some coalgebra α to a composition
β = ψ • ϕ. As the latter is defined implicitly by the equalizer eψ,ϕ – which is a monic coalgebra morphism from
β to γ = ψ ϕ – it is usually easier to reason by instead exhibiting a coalgebra morphism from α into γ = ψ ϕ,
and then appealing to the following simple lemma:
Lemma 4.11. Let F be wpp, and a : α → γ ← β : b a cospan of pointed F -coalgebra morphisms with b monic.
Then any m : α → β with b ◦ m = a is also a pointed F -coalgebra morphism. If a is monic, than so is m; and
for any q with (a, q) jointly monic, so is (m, q).
Proof. One may show that Fb ◦ (β ◦ m) = Fb ◦ (Fm ◦ α) by a routine diagram-chase. Then using the fact that
F preserves the mono b, we may left-cancel Fb on both sides. Moreover, if m ◦ f = m ◦ f 0 , then post-composing
with b (and applying b ◦ m = a) we obtain a ◦ f = a ◦ f 0 ; the result then follows.
24
Remark 4.12. In the following proof, we will often apply Lemma 4.11 in the situation where b is given by
an equalizer (such as eψ,ϕ , after Definition 3.5) which is also a coalgebra morphism, and where the coalgebra
morphism a also equalizes the relevant parallel pairs. Then we obtain the arrow m by universality, and the
Lemma ensures it is also a coalgebra morphism.
We also use this simple fact in the first part of the proof (identities for composition):
Remark 4.13. A monic pointed coalgebra morphism h from α to α0 trivially yields a bisimulation by taking
(ζ, p, q) = (α, id , h), and hence α ≡ α0 ; but not all bisimulations arise in such a way.
We are now ready for the proof of Theorem 4.10.
Proof. The general strategy is to prove that two compositions γ = δ • ϑ and γ 0 = δ 0 • ϑ0 are ≡-equivalent, by
providing a jointly monic pair of pointed coalgebra morphisms p, q from some ζ into δ ϑ and δ 0 ϑ0 respectively,
which equalize the relevant parallel pairs. Lemma 4.11 and Remark 4.12 then imply the existence of a jointly
monic pair of pointed coalgebra morphisms m, m 0 into δ • ϑ and δ 0 • ϑ0 , giving the required bisimulation. We
indicate the key steps (i), (ii), etc. in each proof below.
identities: We sketch the strategy for showing ι(α .getL ) • α ≡ α, as the other identity is symmetric. We exhibit
the equivalence by taking α itself to be the coalgebra defining a bisimulation between α and ι(α .getL ) • α.
To do this, one shows that (i) h = hα.getL , id i : X → A × X is a pointed coalgebra morphism from α to
the composition ι(α .getL ) α defined on pairs, and (ii) h also equalizes the parallel pair ι(α .getL ).getR ◦ π1
and α.getL ◦ π2 (characterising the equalizer and coalgebra morphism from ι(α .getL ) • α to ι(α .getL ) α
– see Remark 4.12). Moreover, h is easily shown to be monic. Hence by Lemma 4.11, h induces a pointed
coalgebra morphism from α to ι(α .getL )•α which is also monic (in C), and hence by Remark 4.13 we obtain
the required bisimulation.
As for pointedness, the initial state of ι(α .getL ) α is (α .getL , α ), and this is indeed h (α ) as required.
congruence: We show how to prove that right-composition (− • β) is a congruence: i.e. that α ≡ α0 implies
(α•β) ≡ (α0 •β). By symmetry, the same argument will show left-composition (α0 •−) is a congruence. Then
one may use the standard fact that ‘bisimulations compose (for wpp functors)’: given pointed bisimulations
between γ and δ, and δ and ε, one may obtain a pointed bisimulation between γ and ε – provided the
M
behaviour functor FAC is wpp, which follows from our assumption that M is wpp. This allows us to deduce
that composition is a congruence in both arguments simultaneously, as required.
So, suppose given a pointed bisimulation between α and α0 : an FAB M
-coalgebra (R, r ) with a jointly monic
pair p, p 0 of pointed coalgebra morphisms from r to α, α0 respectively. One exhibits a bisimulation between
α • β and α0 • β as follows, by first constructing a suitable coalgebra (S , s), together with a jointly monic
pair (q, q 0 ) of coalgebra morphisms from s to the compositions α • β, α0 • β. To construct s, let ζ be the
equalizer of the following parallel pair – or equivalently, the pullback of r .getR and β.getL .
r .getR ◦π1
ζ /
S / R×Y /B
β.getL ◦π2
One may then follow the steps (i)-(iii) in Section 4, where ζ and r play the role of the equalizer eα,β and β
respectively, to construct s, such that ζ is a coalgebra morphism from s to r β. Even though r is not a
coalgebraic bx, it satisfies the following weaker form of (CSetGetL ) (and its R-version), sufficient for Lemma
4.7 to hold. (Here, we take j : R and a : A; there is a continuation version as in Lemma 4.3.)
(CSetGet− 0 0 0
L )(r ) : do {j ← j .setL a; return j .getL } = {j ← j .setL a; return a }
To construct q : S → Pα,β , it is enough to show (i) the composition of the upper and right edges in the
following diagram equalizes the given parallel pair:
ζ
S / R×Y
q p×id
eα,β α.getR ◦π1
/ X ×Y /
Pα,β /B
β.getL ◦π2
25
By also showing that (ii) p × id is in fact a coalgebra morphism, we can then appeal to Lemma 4.11 to show
that q itself defines a coalgebra morphism from s into the composition α • β. One obtains the coalgebra
morphism q 0 from s to α0 • β in an analogous way. Finally, from p, p 0 being jointly monic, and the fact that
eα,β is an equalizer, we obtain a proof that q, q 0 are jointly monic.
associativity: We follow the same strategy as we did for proving the identity laws: we may prove this law by
providing a pointed coalgebra morphism p from the LHS composition to the RHS, which is moreover monic.
We will do this in two stages: first, we show how to obtain an arrow p0 : P(α•β),γ → X × Pβ,γ making the
square in the following diagram commute; then, by applying Lemma 4.11 and Remark 4.12, we will show it
is a pointed coalgebra morphism from (α • β) • γ to α (β • γ), which is also monic.
e(α•β),γ
P(α•β),γ / Pα,β × Z (1)
p0 f
id×eβ,γ id×(β.getR ◦π1 )
/
X × Pβ,γ / X × (Y × Z ) / X ×C
id×(γ.getL ◦π2 )
In this diagram, the arrow f is defined by f (u, z ) = do {let (x , y) = eα,β (u); return (x , (y, z ))}, but it
may also be expressed as f = assoc ◦ (eα,β × id ), where we write assoc for the associativity isomorphism
on products; the isomorphism, and the pairing with id , make it apparent that f is monic. Note that the
functor X × (−), being a right adjoint, preserves equalizers, and hence (id × eβ,γ ) is the equalizer of the
given parallel pair (and moreover monic).
Following the proof strategy outlined above, to obtain p0 one must show that: (i) f ◦ e(α•β),γ equalizes the
parallel pair in the above diagram, ensuring existence of an arrow p0 making the square commute; (ii) the
equalizer id × eβ,γ is a pointed coalgebra morphism from α (β • γ) to α (β γ); and (iii) f is a pointed
coalgebra morphism from (α • β) γ to α (β γ). The facts (ii), (iii) allow us to apply Lemma 4.11 and
Remark 4.12, to deduce that p0 is a pointed coalgebra morphism, and moreover monic (using the fact that
f and e(α•β),γ are, and hence their composition too).
The final stage of constructing the required arrow p : P(α•β),γ → Pα,(β•γ) is to show that: (iv) p0 equalizes
the parallel pair defining Pα,(β•γ) as shown below. Thus we obtain p as the mediating morphism into the
equalizer Pα,(β•γ) ; by Remark 4.12 it is a coalgebra morphism, and it is monic because p0 is monic.
P(α•β),γ
p0
p
eα,(β•γ) ) α.getR ◦π1
/ X × Pβ,γ /
Pα,(β•γ) /B
(β•γ).getL ◦π2
This well-behavedness of composition allows us to define a category of cbx:
Corollary 4.14. There is a category Cbx• of pointed cbx, whose objects are pointed sets (A, a : A) – sets with
distinguished, “initial” values a – and whose arrows (A, a) → (B , b) are ≡-equivalence classes [α] of coalgebraic
bx α : A − B satisfying α .getL = a and α .getR = b.
−
We now describe how this category is related (by taking C = Set and M = Id ) to the category of symmetric
lenses defined in [16]. The point of departure is that cbx encapsulate additional data, namely initial values
α .getL , α .getR for A and B . The difference may be reconciled if one is prepared to extend SLs with such data
(and consider distinct initial-values to give distinct SLs, cf. the comments beginning Section 2.2):
Corollary 4.15. Taking C = Set and M = Id , Cbx• is isomorphic to a subcategory of SL, the category of
SL-equivalence-classes of symmetric lenses; and there is an isomorphism of categories Cbx• ∼ = SL• where SL• is
the category of (SL-equivalence-classes) of SLs additionally equipped with initial left- and right-values.
5 Relating Coalgebraic and Monadic bx
Here, we consider the relationship between our coalgebraic notion of bx and our previous monadic account [1].
The latter characterised bx in terms of monadic get and set operations, where the monad was not assumed a
priori to refer to any notion of state – such as the monad StateT X M , abbreviated to TXM throughout this
paper. The monad was only restricted to this stateful form for defining bx composition; such monadic bx were
26
called StateTBX . By contrast, our coalgebraic bx are explicitly stateful from the outset. Therefore, to compare
cbx and mbx in a meaningful way, throughout this Section we restrict mbx to StateTBX , i.e. with respect to
the monad TXM (as in most of our leading examples of monadic bx). Moreover, as was necessary for defining
composition for such mbx, we also assume them to be transparent: the get operations neither change the state
nor introduce M -effects, i.e. getL = λx .return (f x , x ) for some f :: X → A (likewise getR ).
Finally, we also assume monadic bx A ⇐⇒ B have explicit initial states, rather than the more intricate process
of initialising by supplying an initial A- or B -value as in [1].
5.1 Translating a Coalgebraic bx into a Monadic bx
M
Given a cbx α : X → FAB X , we can define its realisation, or “monadic interpretation”, [[α]] as a transparent
StateTBX with the following operations. (Following conventional Haskell notation, we overload the symbol ()
to mean the unit type, as well as its unique value.)
def
[[α]].getL : TXM A = do {x ← get; return (x .getL )}
def
[[α]].getR : TXM B = do {x ← get; return (x .getR )}
def
[[α]].setL : A → TX () = λa → do {x ← get; x 0 ← lift (x .setL a); set x 0 }
M
def
[[α]].setR : B → TXM () = λb → do {x ← get; x 0 ← lift (x .setR b); set x 0 }
Here, the standard polymorphic functions associated with TXM , namely get : ∀α . TαM α, set : ∀α . α → TαM (),
and the monad morphism lift : ∀α . M α → TXM α (the curried form of the strength of M ) are given by:
get = λa → return (a, a) set = λa 0 a → return ((), a 0 )
lift = λma x → do {a ← ma; return (a, x )}
Proposition 5.1. [[α]] indeed defines a transparent StateTBX over TXM .
Lemma 5.2. The translation [[·]] – from cbx for monad M with carrier X , to transparent StateTBX with an
initial state – is surjective; it is also injective, using our initial assumption that return is monic.
This fully identifies the subset of monadic bx which correspond to coalgebraic bx. Note that the translation [[·]]
is defined on an individual coalgebraic bx, not an equivalence class; we will say a little more about the respective
categories at the end of the next section.
5.2 Composing Stateful Monadic bxs
We will review the method given in [1] for composing StateTBX , using monad morphisms induced by lenses on
the state-spaces. We show that this essentially simplifies to step (ii) of our definition in Section 4 above; thus,
our definition may be seen as a more categorical treatment of the set-based monadic bx definition.
Definition 5.3. An asymmetric lens from source A to view B , written l : A ⇒ B , is given by a pair of maps
l = (v , u), where v : A → B (the view or get mapping) and u : A × B → A (the update or put mapping). It is
well-behaved if it satisfies the first two laws (VU), (UV) below, and very well-behaved if it also satisfies (UU).
(VU) u (a, (v a)) = a (UV) v (u (a, b 0 )) = b 0 (UU) u (u (a, b 0 ), b 00 ) = u (a, b 00 )
Lenses have a very well-developed literature [6, 8, 16, 18, among others], which we do not attempt to recap
here. For more discussion of lenses, see Section 2.5 of [1].
We will apply a mild adaptation of a result in Shkaravska’s early work [28].
Proposition 5.4. Let l = (v , u) : Z ⇒ X be a lens, and define ϑ l to be the following natural transformation:
ϑ l :: ∀α . (Z ⇒ X ) → TXM α → TZM α
def
ϑ ma = do {z ← get; (a 0 , x 0 ) ← lift (ma (v z )); z 0 ← lift (u (z , x 0 )); set z 0 ; return a 0 }
If l is very well-behaved, then ϑ l is a monad morphism.
27
We apply Prop. 5.4 to the following two lenses, allowing views and updates of the projections from X × Y :
l1 = (v1 , u1 ) : (X × Y ) ⇒ X l2 = (v2 , u2 ) : (X × Y ) ⇒ Y
v1 (x , y) =x v2 (x , y) =y
u1 ((x , y), x 0 ) = (x 0 , y) u2 ((x , y), y 0 ) = (x , y 0 )
. .
This gives us a cospan of monad morphisms left = ϑ (l1 ) : TXM → T(X
M M
×Y ) ← TY : ϑ (l2 ) = right, allowing us to
embed computations involving state-space X or Y into computations on the combined state-space X × Y .
Now suppose we are given two StateTBX t1 : A ⇐⇒TXM B , t2 : B ⇐⇒TYM C with
t1 .getL :: TXM A t1 .getR :: TXM B t2 .getL :: TYM B t2 .getR :: TYM C
t1 .setL :: A → TXM () t1 .setR :: B → TXM () t2 .setL :: B → TYM () t2 .setR :: C → TYM ()
In [1], we used left, right to define t1 # t2 , a composite StateTBX with state-space X × Y , as follows:
(t1 # t2 ).get L = left (t1 .get L ) (t1 # t2 ).get R = right (t2 .get R )
(t1 # t2 ).set L a = do {left (t1 .set L a); b ← left (t1 .get R ); right (t2 .set L b)}
(t1 # t2 ).set R c = do {right (t2 .set R c); b ← right (t2 .get L ); left (t1 .set R b)}
We then defined the subset, X o n Y , of X × Y given by B -consistent pairs, and argued that t1 # t2 preserved
B -consistency – hence its state-space could be restricted from X × Y to X o n Y . We will use the notation t1 • t2
for the resulting composite StateTBX .
In the context of coalgebraic bx, we made this part of the argument categorical by defining X o n Y to be a
pullback, and formalising the move from the pairwise definition α β to the full composition α • β by step (iii) of
Section 4. Given the 1-1 correspondence between transparent StateTBX and cbx given by Lemma 5.2, this may
be considered to be the formalisation of the monadic move from the composite t1 # t2 on the product state-space
to the composite t1 • t2 on the pullback.
This allows us to state our second principal result, namely that the two notions of composition – coalgebraic
bx (as in Definition 4.4) and StateTBX – may be reconciled by showing the pairwise definitions coherent:
Theorem 5.5. Coherence of composition: The definitions of StateTBX and coalgebraic bx composition on
product state-spaces are coherent: [[α]] # [[β]] = [[α β]]. Hence, the full definitions (on B -consistent pairs) are also
coherent: [[α]] • [[β]] = [[α • β]].
Proof. The operations of the monadic bx [[α]] at the beginning of Section 5.1, and the computation ϑ (v , u) ma,
may be re-written in do notation for the monad M rather than in StateT X M , as follows:
[[α]].getL : TXM A [[α]].setL : A → TXM () ϑ (v , u) ma : ∀α . TZM α
[[α]].getL = λx → return (x .getL ) [[α]].setL a = λx → do {x 0 ← x .setL a; return ((), x 0 )}
ϑ (v , u) ma = λz → do {(a 0 , s 0 ) ← ma (v z ); let z 0 = u (z , x 0 ); return (a 0 , z 0 )}
Applying ϑ to the lenses l1 and l2 gives the monad morphisms left and right as follows:
left = ϑ (l1 ) : ∀α . TXM α → T(XM
×Y ) α right = ϑ (l2 ) : ∀α . TYM α → T(X
M
×Y ) α
0 0 0 0
left = λmxa (x , y) → do { (a , x ) ← mxa x ; return (a , (x , y))}
right = λmya (x , y) → do {(a 0 , y 0 ) ← mya y; return (a 0 , (x , y 0 ))}
This allows us to unpack the operations of the composite [[α]] # [[β]] to show they are the same as [[α β]].
Again, this result concerns individual cbx, and not the ≡-equivalence classes used to define Cbx• . We now
comment on how one may embed the latter into a category of transparent StateTBX . In [1] (Theorem 26),
we defined an equivalence on StateTBX (∼, say) given by operation-respecting state-space isomorphisms, and
showed that •-composition is associative up to ∼. In line with Corollary 4.14, one obtains a category Mbx• of
∼-equivalence-classes of transparent StateTBX , and initial states as at the start of Section 5).
Translating this into our setting (by reversing [[·]] from Lemma 5.2), one finds that two transparent StateTBX
are ∼-equivalent iff there is an isomorphism of pointed coalgebra morphisms between their carriers – which is
generally finer than ≡. Therefore, we cannot hope for an equivalence-respecting embedding from Cbx• to Mbx• .
However, we may restrict ≡ to make such an embedding possible:
Corollary 5.6. Let ≡! be the equivalence relation on coalgebraic bx given by restricting ≡ to bisimulations whose
pointed coalgebra morphisms are isomorphisms; and let Cbx!• be the category of equivalence-classes of cbx up to
≡! . Then there is an isomorphism Cbx!• ∼ = Mbx• .
28
6 Conclusions and Further Work
In our search for unifying foundations of the field of bidirectional transformations (bx), we have investigated a
number of approaches, including monadic bx, building on those of (symmetric) lenses and relational bx.
We have given a coalgebraic account of bx in terms of intuitively simple building blocks: two data sources
A and B ; a state space X ; operations on X to observe (getL , getR ) and update (setL , setR ) each data source;
an ambient monad M of additional computational effects; and a collection of laws, entirely analogous to those
in existing bx formalisms. Moreover, these structures, being defined categorically, may be interpreted in a wide
variety of settings under very modest assumptions about the underlying category C.
Initial states were handled by introducing pointed coalgebras and bisimulations. A more elegant approach
would be to work in the category I / C of pointed objects from the outset – i.e. pairs (A, a : I → A) of an
object of C and an initial value a. Coalgebra morphisms and bisimulations are then automatically pointed,
and the assumption of initial B -consistency used in Section 4 ((i)) is enforced at a type level. However, lifting
exponentials (and strong monads) from C into I / C is rather delicate; we leave the details for future work.
Our definition allows a conceptually more direct, if technically slightly subtle, treatment of composition – in
which the state space, defined by a pullback, captures the idea of communication across a shared data source,
via the idea of B -consistent pairs. Our proof techniques involved reasoning about composition by considering
operations defined on such pairs. We defined an equivalence on cbx based on coalgebraic bisimulation, and
showed that composition does indeed define a category, up to equivalence. The notion of bisimulation improves
on existing, more ad-hoc definitions, such as that of symmetric lens equivalence, and we take this as further
evidence for the suitability of our framework and definitions.
We described several concrete instantiations of the general definition of bisimulation, given by varying the effect
monad M . Coarser equivalences may be suitable for modelling non-deterministic bx, and could be introduced
via alternative methods such as [14]; but we do not have space to explore this further here.
It is also worth investigating the relationship between our coalgebraic formulation of bx, and the spans of
lenses considered by Johnson and Rosebrugh [20]. A coalgebraic bx may be seen as a generalisation to a span of
‘monadic lenses’ or ‘M -lenses’, allowing effectful updates. However, in defining equivalence for spans of lenses,
Johnson and Rosebrugh consider an additional condition, namely that the mediating arrow between two spans,
witnessing equivalence, is a lens in which the get arrow is a split epi. It is unclear to us the relationship between
this condition, and pointed coalgebraic bisimulation. We leave such investigations to future work.
Another area to explore is combinatory structure for building larger cbx out of smaller pieces, in the style of
existing work in the lens community. Some examples were given in [1] – of which bx composition was by far the
most challenging to formulate – and we expect the other combinators to apply routinely for cbx as well, along
the same lines as [4]. One would expect coalgebraic bisimulation to be a congruence for these combinators; it
would be interesting to investigate whether the work of Turi and Plotkin [33] can help here.
We set great store by the fact that our definitions are interpretable in categories other than Set; we hope
thereby to incorporate richer, more intensional structures, such as delta lenses [7], edit lenses [17] and ordered
updates [15] in our framework, and not merely the state-based extensional bx we have considered so far. We also
hope to explore the connections between our work and existing coalgebraic notions of software components [4],
and techniques for composing coalgebras [13].
Acknowledgements An extended, unpublished abstract [2] of some of the results here was presented
at CMCS 2014; we thank the participants there for useful feedback. Our work is supported by the UK
EPSRC-funded project A Theory of Least Change for Bidirectional Transformations [32] (EP/K020218/1,
EP/K020919/1); we are grateful to our colleagues for their support, encouragement and feedback during the
writing of the present paper.
References
[1] F. Abou-Saleh, J. Cheney, J. Gibbons, J. McKinna, and P. Stevens. Notions of bidirectional computation
and entangled state monads. In MPC, June 2015. To appear. Extended version available at http://groups.
inf.ed.ac.uk/bx/bx-effects-tr.pdf.
[2] F. Abou-Saleh and J. McKinna. A coalgebraic approach to bidirectional transformations. In CMCS. ETAPS,
2014. Talk abstract.
[3] J. Adámek, S. Milius, L. S. Moss, and L. Sousa. Well-pointed coalgebras. Logical Methods in Computer
Science, 9(3), 2013.
29
[4] L. S. Barbosa. Towards a calculus of state-based software components. J. UCS, 9(8):891–909, 2003.
[5] J. Cheney, J. McKinna, P. Stevens, J. Gibbons, and F. Abou-Saleh. Entangled state monads (extended
abstract). In Terwilliger and Hidaka [31].
[6] K. Czarnecki, J. N. Foster, Z. Hu, R. Lämmel, A. Schürr, and J. F. Terwilliger. Bidirectional transformations:
A cross-discipline perspective. In ICMT, volume 5563 of LNCS, pages 260–283. Springer, 2009.
[7] Z. Diskin, Y. Xiong, and K. Czarnecki. From state- to delta-based bidirectional model transformations: the
asymmetric case. JOT, 10:6: 1–25, 2011.
[8] J. N. Foster, M. B. Greenwald, J. T. Moore, B. C. Pierce, and A. Schmitt. Combinators for bidirectional
tree transformations: A linguistic approach to the view-update problem. ACM TOPLAS, 29(3):17, 2007.
[9] J. Gibbons and R. Hinze. Just do it: Simple monadic equational reasoning. In ICFP, pages 2–14, 2011.
[10] J. Gibbons and M. Johnson. Relating algebraic and coalgebraic descriptions of lenses. ECEASST, 49, 2012.
[11] H. P. Gumm. Functors for coalgebras. Algebra Universalis, 45(2-3):135–147, 2001.
[12] H. P. Gumm. Copower functors. TCS, 410(12):1129–1142, 2009.
[13] I. Hasuo. The microcosm principle and compositionality of GSOS-based component calculi. In Algebra and
Coalgebra in Computer Science, pages 222–236. Springer, 2011.
[14] I. Hasuo, B. Jacobs, and A. Sokolova. Generic trace semantics via coinduction. CoRR, abs/0710.2505, 2007.
[15] S. J. Hegner. An order-based theory of updates for closed database views. Ann. Math. Art. Int., 40:63–125,
2004.
[16] M. Hofmann, B. C. Pierce, and D. Wagner. Symmetric lenses. In POPL, pages 371–384. ACM, 2011.
[17] M. Hofmann, B. C. Pierce, and D. Wagner. Edit lenses. In POPL, pages 495–508. ACM, 2012.
[18] Z. Hu, A. Schurr, P. Stevens, and J. F. Terwilliger. Dagstuhl seminar 11031: Bidirectional transformations
(BX). SIGMOD Record, 40(1):35–39, 2011. DOI: 10.4230/DagRep.1.1.42.
[19] B. Jacobs and J. Rutten. A tutorial on (co)algebras and (co)induction. Bulletin EATCS, 62:222–259, 1997.
[20] M. Johnson and R. Rosebrugh. Spans of lenses. In Terwilliger and Hidaka [31].
[21] E. Moggi. Computational lambda-calculus and monads. In LICS, pages 14–23. IEEE Computer Society,
1989.
[22] E. Moggi. Notions of computation and monads. Inf. Comput., 93(1):55–92, 1991.
[23] G. D. Plotkin and J. Power. Notions of computation determine monads. In FOSSACS, volume 2303 of
LNCS, pages 342–356. Springer, 2002.
[24] J. Power and O. Shkaravska. From comodels to coalgebras: State and arrays. ENTCS, 106, 2004.
[25] J. Power and H. Watanabe. An axiomatics for categories of coalgebras. ENTCS, 11:158–175, 1998.
[26] J. Rutten. Universal coalgebra: a theory of systems. Theor. Comput. Sci., 249(1):3–80, 2000.
[27] A. Schürr and F. Klar. 15 years of triple graph grammars. In ICGT, volume 5214 of LNCS, pages 411–425.
Springer, 2008.
[28] O. Shkaravska. Side-effect monad, its equational theory and applications. Seminar slides available at:
http://www.ioc.ee/~tarmo/tsem05/shkaravska1512-slides.pdf, 2005.
[29] A. Sokolova. Probabilistic systems coalgebraically: A survey. TCS, 412(38):5095–5110, 2011.
[30] P. Stevens. Bidirectional model transformations in QVT: Semantic issues and open questions. SoSyM,
9(1):7–20, 2010.
[31] J. Terwilliger and S. Hidaka, editors. BX Workshop. http://ceur-ws.org/Vol-1133/#bx, 2014.
[32] TLCBX Project. A theory of least change for bidirectional transformations. http://www.cs.ox.ac.uk/
projects/tlcbx/, http://groups.inf.ed.ac.uk/bx/, 2013–2016.
[33] D. Turi and G. Plotkin. Towards a mathematical operational semantics. In LICS, pages 280–291. IEEE,
Computer Society Press, 1997.
30