We have previously (Bx, 2014; MPC, 2015) shown that several statebased bx formalisms can be captured using monadic functional programming, 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 simpler than, our previous mbx definition. Coalgebraic bisimulation yields a natural notion of behavioural equivalence on cbx, which respects composition, and essentially includes symmetric lens equivalence as a special case. Finally, we speculate on the applications of this coalgebraic perspective to other bx constructions and formalisms.
composition t1 # t2 for those mbx with transparent get operations – i.e. get s 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 [
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 statebased 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 [
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 [
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 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 [
P Y pX g / X / B f
Q cY ∃!h
P ! Y cX pX pY g / X / B
f dY
dX ∃k " M P M pY/ M" X ! M Y
M pX
Mg
Mf / M B
Remark 2.1. The wpp condition lets us consider (at least for C = Set) monads M of computational interest
such as (probabilistic) non-determinism [
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 [
Now we define the behaviour functors we use to describe bx coalgebraically; as anticipated above, we
incorporate 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 [
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.
Definition 2.3. For objects A and B , define the functor FAMB (−) = A × (M (−))A × B × (M (−))B .
For a given choice of objects A and B , we will use the corresponding functor FAMB to characterise the behaviour
of those bx between A and B , as FAMB -coalgebras. By taking projections, we can see the structure map α : X →
FAMB X of a pointed FAMB -coalgebra as supplying four pieces of data: a function X → A which observes the
A-value in a state X ; a function X → (MX )A which, uncurried into the form X × A → MX , gives us the
sideeffectful 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 [
To ensure that pointed FAMB -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. Definition 2.6. A coalgebraic bx is a pointed FAMB -coalgebra (X , α : X → FAMB X , α) for which the following laws hold at L (writing x .getL for α.getL x , etc. as per Convention 2.4): (CGetSetL) (α) : (CSetGetL) (α) : x .setL (x .getL)
= return x do {x 0 ← x .setL a; return (x 0, x 0.getL)} = do {x 0 ← x .setL a; return (x 0, a)} and the corresponding laws (CSetGetR) and (CGetSetR) hold at R.
These laws are the analogues of the (GS), (SG) laws [
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 a0 = return a0 = a.setR a0.
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
In this section, we introduce the notion of pointed coalgebraic bisimulation, which defines a behavioural equivalence ≡ 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 ◦ α = β .
Remark 3.2. In terms of do notation, h : X → Y being an FAMB -coalgebra morphism between α and β is equivalent to the following laws (where we again write x .setL for α.setL x , and so on): (CGetPL)(h) : (CSetPL)(h) : x .getL = (h x ).getL 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 [
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: Proposition 3.4. A pointed FAIdB -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. 3.1
In this subsection, we describe symmetric lenses (SL) [
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 set s 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.
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. [
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, m0) and n = out (o, n0) for some o : O and m0 ∼R n0; or • m = in (λi → m(i )) and n = in (λi → n(i )), where m(i ) ∼R n(i ) for all i : I .
One may now show that a pointed FAMB -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. 3.2.2 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 , • 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
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 fine-grainedness. A pointed FAMB -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 a0 changes it to either u or u0. Each state-change is only observable to the user through the values of getL and getR; so suppose u.getR = u0.getR = b. (Note that u.getL = u0.getL = a0 by (CGetSetL)). This means u and u0 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 a0 maps these respectively to u and u0 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 [
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 [
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].
Remark 4.2. The following technical observation will also be useful for reasoning about FAMB -coalgebras. As M is wpp (assumption 2 of Section 2.1), so too is FAMB , using the fact that A × (−) and (−)A preserve pullbacks, and hence are wpp. Then by Lemma 4.1, FAMB 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. (i)
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α,β
pα X
pβ α.getR / Y / B β.getL
Pα,β pα
X eα,β=hpα,pβi hα.getR,α.getRi
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. left-cancellable), and thus by Lemma 4.1, so too is its image under the wpp functors M and FAMB .
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)
β Definition 4.6. (X × Y , α
β) is an FAMC -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)
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)} do {(x 0, y 0) ← (x , y ).setL a; return (x 0.getR, x 0.getR)} (†L) 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)} 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 of α β : X × Y → FAMC (X × Y ), restricted to the B -consistent pairs Pα,β , induce well-defined operations Pα,β → FAMC 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 δ to be the resulting arrow Pα,β → FAMB X given by the composition FAMB π1 ◦ (α β) ◦ eα,β .
Although this does not explicitly define the operations of the composition α • β, it does relate them to those of α β via the monic arrow FAMC 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 of FAMB , 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)
Proof. We focus on the L case (the R case is symmetric). As described in (iii) above, we prove the laws postcomposed 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α,β :
Pα,β δ :=
v α•β FAMC pα / X × Y
α β FAMC (α.getR×β.getL) / FAMC (B × B ) FAMC π1
X × Y
α β
FAMC (X × Y ) FAMC (α.getR×β.getL)
eα,β FAMC π1 / X × Y
α β
FAMC (X × Y ) FAMC (α.getR×β.getL) FAMC X v
/ FAMC (B × B ) FAMC hα.getR,α.getRi
FAMC X
/ FAMC (B × B ) FAMC hα.getR,α.getRi Under the assumption that M is wpp, so is FAMC . Hence, the image under FAMC 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 mediating morphism Pα,β → FAMC (Pα,β ) (not a priori unique) as shown below-right. We take this to be the coalgebra structure α • β of the composite bx.
FAMC Pα,β
FAMC eα,β / FAMC (X × Y )
Pα,β
eα,β FAMC X
/ FAMC (B × B ) FAMC hα.getR,α.getRi
FAMC X y
FAMC hα.getR,α.getRi FAMC pα
FAMC (α.getR×β.getL) δ
% FAMC Pα,β
FAMC eα,β / FAMC (X × Y ) = = = = = = = 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, y0) ← (x , y).setL a; return (x 0, y0)}
[[ swapping lets, and using (CGetPA)(eα,β) ]] do {let (x , y) = eα,β (z ); let a = (x , y).getL; (x 0, y0) ← (x , y).setL a; return (x 0, y0)}
[[ 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; y0 ← y.setL b; return (x 0, y0)} [[ (CGetSetA) for α ]] do {let (x , y) = eα,β (z ); let b = x .getR; y0 ← y.setL b; return (x , y0)}
[[ (x , y) = eα,β (z ) implies x .getL = y.getR by definition of eα,β ]] do {let (x , y) = eα,β (z ); let b = y.getL; y0 ← y.setL b; return (x , y0)}
[[ (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, y0) = eα,β (z 0); return ((x 0, y0), x 0.getL)}
[[ (CSetPL)(eα,β) ]] do {let (x , y) = eα,β (z ); (x 0, y0) ← (x , y).setL a; return ((x 0, y0), x 0.getL)}
[[ definition of (x , y).setL ]] do {let (x , y) = eα,β (z ); x 0 ← x .setL a; let b = x 0.getR; y0 ← y.setL b; return ((x 0, y0), x 0.getL)} [[ (CSetGetL) for α ]] do {let (x , y) = eα,β (z ); x 0 ← x .setL a; let b = x 0.getR; y0 ← y.setL b; return ((x 0, y0), a)} [[ definition of (x , y).setL ]] do {let (x , y) = eα,β (z ); (x 0, y0) ← (x , y).setL a; return ((x 0, y0), a)}
[[ (CSetPL)(eα,β); inline let ]] do {z 0 ← z .setL a; return (eα,β (z 0), a)} 4.1
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 , and γ, γ0 : C −− D, and all compositions are assumed well-defined): 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. 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, m0 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 behaviour functor FAMC 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 FAMB -coalgebra (R, r ) with a jointly monic pair p, p0 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.
S ζ / R × Y r.getR◦π1 β.getL◦π2 // B 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.) (CSetGetL−)(r ) : do {j 0 ← j .setL a; return j 0.getL } = {j 0 ← 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 q Pα,β
ζ eα,β / R × Y
p×id β.getL◦π2 // B 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, p0 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.
P(α•β),γ
p0 X × Pβ,γ e(α•β),γ id×eβ,γ / Pα,β × Z
f / X × (Y × Z ) id×(β.getR◦π1) id×(γ.getL◦π2) // X × C 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. (1) P(α•β),γ
p Pα,(β•γ)
p0 eα,(β•γ) ) / X × Pβ,γ
α.getR◦π1 (β•γ).getL◦π2 // B
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 [
Here, we consider the relationship between our coalgebraic notion of bx and our previous monadic account [
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 [
Given a cbx α : X → FAMB 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.) d=ef do {x ← get ; return (x .getL)} d=ef do {x ← get ; return (x .getR)} [[α]].setL : A → TXM () d=ef λa → do {x ← get ; x 0 ← lift (x .setL a); set x 0 } [[α]].setR : B → TXM () d=ef λ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 = λa0 a → return ((), a0) 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
We will review the method given in [
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 [
We will apply a mild adaptation of a result in Shkaravska’s early work [
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 α ϑ ma d=ef do {z ← get ; (a0, x 0) ← lift (ma (v z )); z 0 ← lift (u (z , x 0)); set z 0; return a0 } If l is very well-behaved, then ϑ l is a monad morphism. l2 = (v2, u2) : (X × Y ) ⇒ Y v2 (x , y ) = y u2 ((x , y ), y 0) = (x , y 0) This gives us a cospan of monad morphisms left = ϑ (l1) : TXM →. T(MX ×Y ) ←. TYM : ϑ (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 [
In the context of coalgebraic bx, we made this part of the argument categorical by defining X on 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 {(a0, s0) ← ma (v z ); let z 0 = u (z , x 0); return (a0, z 0)} Applying ϑ to the lenses l1 and l2 gives the monad morphisms left and right as follows: left = ϑ (l1) : ∀α . TXM α → T(MX ×Y ) α left = λmxa (x , y ) → do { (a0, x 0) ← mxa x ; return (a0, (x 0, y )) } right = λmya (x , y ) → do {(a0, y 0) ← mya y ; return (a0, (x , y 0)) }
right = ϑ (l2) : ∀α . TYM α → T(MX ×Y ) α 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 [
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•.
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 [
It is also worth investigating the relationship between our coalgebraic formulation of bx, and the spans of
lenses considered by Johnson and Rosebrugh [
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 [
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 [
Acknowledgements An extended, unpublished abstract [