Spans are pairs of arrows with a common domain. Despite their symmetry, spans are frequently viewed as oriented transitions from one of the codomains to the other codomain. The transition along an oriented span might be thought of as transitioning backwards along the first arrow (sometimes called 'leftwards') and then, having reached the common domain, forwards along the second arrow (sometimes called 'rightwards'). Rightwards transitions and their compositions are wellunderstood. Similarly, leftwards transitions and their compositions can be studied in detail. And then, with a little hand-waving, a span is 'just' the composite of two well-understood transitions - the first leftwards, and the second rightwards. In this paper we note that careful treatment of the sources, targets and compositions of leftwards transitions can be usefully captured as a monad L built using a comma category construction. Similarly the sources, targets and compositions of rightwards transitions form a monad R, also built using a comma category construction. Our main result is the development of a distributive law, in the sense of Beck [3] but only up to isomorphism, distributing L over R. Such a distributive law makes RL a monad, the monad of anchored spans, thus removing the hand-waving referred to above, and establishing a precise calculus for span-based transitions. As an illustration of the applicability of this analysis we use the new monad RL to recast and strengthen a result in the study of databases and the use of lenses for view updates.
1.1
There is an important distinction among extant bidirectional transformations between those that are “set-based” and those that are “category-based” (the latter are sometimes also called “delta-based”). This paper analyses the origins of that distinction and lays the mathematical foundations for a calculus integrating both points of view along with an often implicit point of view in which deltas sometimes have a “preferred” direction.
So, what are these set-based and category-based transformations, and how did the distinction arise?
To quote from the Call for Papers: “Bidirectional transformations (Bx) are a mechanism for maintaining the consistency of at least two related sources of information. Such sources can be relational databases, software models and code, or any other document following standard or ad-hoc formats.”
A fundamental question in bidirectional transformations is: What are the state spaces of the sources among which consistency needs to be maintained? After all, consistency only needs to be worked on when one source changes state, so a careful analysis of permissible state changes is important.
This analysis will be important whatever the nature of the sources, but for ease of explication we will focus at first on an example. Let us consider relational databases. Recall that state spaces of systems are most often represented by graphs whose nodes are states and whose arrows represent transitions among the states.
Consider the state space of a relational database. Nodes in the state space, states, are just snapshots of the database at a moment in time — all of the data, stored in the database, in its structured form, at that moment.
Typically, with a database, one can transition (update the database) from any snapshot to any other. So, the state space could be all possible snapshots with an arrow between every pair of snapshots. (This kind of state space is sometimes called a “chaotic” or “co-discrete” category. A co-discrete category is a category with exactly one arrow between each ordered pair of objects.)
This kind of state-space, a co-discrete state-space, is a perfectly reasonable analysis of database updating. It comes naturally from focusing on the states, and from noticing that there is always an update that will lead from any state S to any other state S0. After all, when one can transition between any two states, why keep track of arrows that tell you that you can do that? All that one needs to know is what the new state S0 is. And, no matter what the current state S might be, the database can transition to that new state S0.
So, it is natural to do away with the arrows, consider simply the set of states, and plan one’s Bx assuming that any state S might be changed to any other state S0.
This is the foundation of set-based bidirectional transformations.
Important, pioneering work on set-based bidirectional transformations was carried out in this community by Hoffmann, Pierce et al, and by Stevens et al, among others. 1.2
Other workers chose to analyse the state spaces differently.
Pioneering work by Diskin [
For example, S0 might be obtainable from S by inserting a single row in a single table. Let’s call that transition α. But there are many other ways to transition from S to S0. To take an extreme example, let’s call it β, one might in a single update delete all of the contents of the database state S, and then insert into the resultant empty database all of the contents of the database state S0. Both α and β are transitions from S to S0, so if one wishes to distinguish them, then a set-based, or indeed a co-discrete category based, description of the state space will not suffice. While the states themselves remain pre-eminently important, the transitions need to be tracked in detail, along with their compositions (one transition followed by another) and the state space becomes a category (we assume that the reader is familiar not just with set theory, but also with category theory).
Incidentally, much of the former controversy surrounding put-put laws arises from the different analyses of set-based and category-based bidirectional transformations. If a state space does not distinguish α from β then the result of maintaining consistency with α (a single row insert) has to be the same as the result of maintaining consistency with β and the latter could, on breaking down the update result in synchronising with the empty database state, and then synchronising with the update from that state to S0. On that analysis the put-put law (which says that an update can be synchronized only at the end, or at any intermediate step and then resynchronized at the end, with the same outcome in either case) is a very strong, probably unreasonably strong, requirement. Alternatively, if α and β are different updates then the put-put law says nothing a priori about their synchronizations and is a much less stringent requirement. 1.3
There is yet another way in which one might analyse the state space of a relational database.
A basic transition might be inserting one or more new rows in some table(s). So we might consider a statespace with the same snapshots as before, but with an arrow S / S0 just when S0 is obtained from S by inserting rows. This is in fact the “information order” — the arrow S / S0 can be thought of as the inclusion of the snapshot S in the bigger (more information stored) snapshot S0.
Notice that this state space has arrows corresponding to inserts, and we will below call the inserts “rightwards” transitions. But those very same arrows correspond to deletes if we transition them “leftwards”, backwards, along the arrow (one can move from S0 to S by deleting the relevant rows).
The information order provides yet another potential state space for a relational database, and is wellunderstood by database theorists. It has the added complication that arrows can be transitioned in both directions. But it has the advantage of separating out two distinct kinds of transition, the rightwards, insert, transitions, and leftwards, delete, transitions, and these can be analysed separately.
It is of great convenience that transitions of the same kind — all leftwards or all rightwards — have very good properties: For example, an insert followed by another insert is definitely just an insert, and the corresponding “monotonic” (rightwards) put-put law for a Bx using multiple inserts has never been controversial. Similarly for multiple leftwards transitions.
Of course an arbitrary update can involve some mixture of leftwards and rightwards transitions, and the main technical content of this paper is the development of a detailed calculus for mixed transitions. 1.4
We have seen that there are (at least) three fundamental approaches to state spaces for relational databases. These approaches apply more generally to various sources for bidirectional transformations. 1. In many systems we can concentrate on the states, assume that we can transition from any state S to any other state S0, and view the state space either as a set over which we might build a set-based Bx (for example a well-behaved lens), or equivalently as a co-discrete category (which explicitly says that there is a single arrow S / S0 for any two states S and S0). 2. Alternatively, we can attempt to distinguish among different ways of updating S / S0, different “deltas”, and view the state space as a category over which we might build a category-based Bx (for example, a delta-lens). 3. And very often among the categories of state spaces there is a “preferred direction” for arrows that can be identified in which case the state space as a category can be simplified by showing only the preferred direction, with arbitrary transitions recovered as composites of rightwards (normal direction along an arrow) and leftwards (backwards along an arrow) transitions.
Naturally, if a particular application lends itself well to set-based analysis then a set-based Bx will suffice.
Frequently however, knowledge of the deltas, when available, is sufficiently advantageous for us to want to build a category-based Bx. One advantage of the co-discrete representation of set-based bidirectional transformations is that set-based results can be derived from category-based results since co-discrete categories are merely a special case of categories.
Furthermore, if the application presents a natural “preferred” order of transition then the third approach might be used. Such information order and related situations are so common that this approach has been used implicitly for some time. The main goal of this paper is to develop the machinery that mathematically underlies this approach, and to show how it incorporates the other two approaches so that ordinary category-based, or indeed, via co-discrete categories, ordinary set-based bidirectional transformations, can be recovered as special cases. 1.5
In earlier work [
The monads involved are all in some sense state space dependent.
For asymmetric lenses we will call the state spaces of the two systems S and V, and suppose given a Get function or functor G : S / V.
In the set-based case the monad, ΔΣ, captures completely the notion that all that is needed for a Put operation is a given state S ∈ S and a new state V 0 ∈ V with no necessary relationship between GS and V 0.
In the category-based case the monad (−, 1V ) (which we will rename here as R because it will be used to model the rightwards transitions), captures completely the notion that a Put operation depends on a given state S ∈ S and an arrow of the state space V of the form GS / V 0.
In this paper we will show how to construct analogously a monad L which models the leftwards transitions, and which has as algebras lenses for the backwards (in database terms, delete) updates. A Put operation for leftwards transitions depends on a given state S ∈ S and an arrow of the state space V of the form V 0 / GS. (Notice that the update from GS to V 0 transitions leftwards along the arrow to reach V 0.)
Most importantly in this paper we exhibit a distributive law, in the sense of Beck [
Algebras for the new monad RL are lenses that synchronise with arbitrary strings of leftwards and rightwards transitions in V. 1.6
The paper shows that the category theoretic structure of arrows rightwards from GS can be captured as a
monad R. Similarly, the category theoretic structure of arrows leftwards from GS can be captured as a monad
L. There are some important new technical advantages in this, and some important new implications for the
lens community, but the basic ideas of these two monads are not new (first appearing in the paper of Street [
Database theorists often work with the information order. But an arbitrary database transition involves inserts and deletes — a mixing of L and R transitions in the information order. Until now this has been done with handwaving — the R monad tells us all about inserts, the L monad tells us all about deletes, so we mix transitions together doing say a delete followed by an insert as a general transition which could be drawn as a “span” S o S0 / S00 (get from S to S00 by deleting some rows from S to get to S0, and then inserting some rows into S0 to get to S00). And of course we want to distinguish this from other ways of getting from S to S00, perhaps S o T / S00 where T may be very different from S0. But we’ve moved from the monads that tell us everything we need to know about rightwards transitions and their interactions, and leftwards transitions and their interactions, to a vague idea of mixing such transitions together.
The main point of the paper is the discovery of a previously unobserved distributive law between L and R which, like all distributive laws, gives a new monad RL, and this composite monad precisely captures the calculus of these spans (“calculus” meaning we can calculate with it using routine procedures (various versions of μ and η below) determining algorithmically how all possible mixings, zigzags, etc, interact, which ones are equivalent to one another, and so on).
It should perhaps be noted here that the spans in this paper are mathematically the same as, but largely
semantically otherwise unrelated to, the authors’ use of equivalence classes of spans to describe symmetric lenses
of various kinds in [
The plan of this paper is fairly straightforward. In Section 2 we introduce in detail the two monads R and L. In Section 3 we develop the distributive law, slightly generalising the work of Beck as it is in fact a pseudodistributive-law. (Recall that in category theory, when an axiom is weakened by requiring only a coherent isomorphism rather than an equality, the resulting notion is given the prefix “pseudo-”. The coherency of the isomorphisms involved can be daunting, but in this paper the isomorphisms arise from universal properties and thus coherency is automatic and we will say no more about it.) In addition in Section 3 we display explicitly the basic operations of the new monad RL. In Section 4 we study the algebras for such monads, noting that these algebras are (generalised) lenses. And how useful might all this be? Well, Proposition 3 in Section 4 is an example of a strong new result that couldn’t even be stated without the new monad RL.
We hope that having these things in mind might be some help in seeing through the technical details in the mathematics that follows. 1.7
State spaces with reversible transitions have been the source of a number of confusions. The fact that every state is accessible from every other state in the same connected component, has sometimes led to researchers ignoring transitions (the set-based state spaces referred to above). Conversely, if instead of ignoring transitions all the transitions are explicitly included in the state space, then in many applications we are failing to distinguish two different types of transition, the “rightwards” and the “leftwards”. The resulting plethora of transitions of mixed types can seriously complicate any analysis.
With the two monads L and R, state spaces with reversible transitions can be managed effectively. Rather than constructing state spaces in which transitions come in pairs S / S0 and S0 / S, we include only one of each pair (there is usually a “preferred” direction which can be the one included). Then the monad R is used for analyses and constructions using the categorical structure of the preferred transitions. Similarly the monad L can be used for analyses and constructions using the reverse transitions. And arbitrary composites of transitions can be broken down into “zig-zags” of L and R transitions, and in many cases into spans, L transitions followed by R transitions.
However, at this point we have come to the “hand-waving”. What does it really mean mathematically to deal with zig-zags of L and R transitions? What does it mean to deal with an L transition followed by an R transition? And what is the calculus of mixed L and R transitions?
The main point of this paper is to show how under a modest hypothesis (the existence of pullbacks in the state
space category V) there is, up to isomorphism, a distributive law [
For basic category theoretic notions readers are referred to any of the standard texts, including for example [
G /Vo H
Given two functors with common codomain V, say S T, the comma category (G, H) was introduced in the thesis of F.W. Lawvere. It has as objects triples (s, t, a) where s is an object of S, t is an object of T, and a : Gs / Ht is an arrow of V. The arrows of the comma category are, as one would expect, given by an arrow p : s / s0 of S and an arrow q : t / t0 of T which make the corresponding square in V commute (so for an arrow (p, q) from (s, t, a) to (s0, t0, a0) we have (Hq)a = a0(Gp) in V) .
The comma category has evident projections to S and T shown in the figure below.
We denote the comma category and its projections as follows:
S w
LGH
G (G, H)
γ −→ ' V w
RHG H ' T
Where possible we will suppress the subscripts on projections. This is especially desirable if the subscript is itself an identity functor, and this situation arises frequently since the comma categories we will consider below will usually have the identity functor on V for one of either G or H.
The central arrow, γ in the figure, is included because the comma category has not just projections LH and RG, but also a natural transformation γ : G(LH) / H(RG) (because each object (s, t, a) of (G, H) is in natural correspondence with an appropriate arrow, a itself, of V). Indeed, the comma category is a kind of 2-categorical limit — it is universal among spans from S to T with an inscribed natural transformation.
Explicitly, the universality of the comma category is given by the following. Each functor F : X / (G, H) corresponds bijectively with a triple (K, L, ϕ) where K : X / S, L : X / T and ϕ : GK / HL (with the correspondence given by composing each of LH, RG and γ with F ).
Using this universal propertly we establish some further notation. Write ηG for the functor corresponding to the triple (1V, G, 1G) : S
/ (G, 1V) as in
between these two monads and consequently, the composite RL is a monad. LR λ / RL
If G : S / V then the domain of the functor RG is the comma category (G, 1V) and so has as objects arrows from V indexed by objects of S of the form Gs a / v. The important projection RG (important because it is the one which shows us the effect on G of the monad functor R) gives RG(Gs a / v) = v. The projection RG is also important because when we apply L to RG, L will build on the projected value v. Thus applying the functor L to RG gives a functor LRG : (1V, RG) / V whose domain has objects of the form Gs that is cospans (a, b) from Gs to v0. Moreover LR(G)(a, b) = v0. a / v o b
v0, / V has objects of the form w / V whose domain has c / Gs in V and
On the other hand, the domain of the functor LG : (1V, G) LG(w
c / Gs) = w. Applying the functor R to LG gives a functor RL(G) : (LG, 1V) objects of the form Gs o c w d / w0, that is spans (c, d) from Gs to w0, and RL(G)(c, d) = w0.
Now we can define the G’th component of λ. It is the (pseudo-)functor (over V) λG : (1V, RG) a / v o b defined at an object Gs v0 of the domain of LRG by taking the pullback in V (and on arrows using the induced maps). Thus λG(a, b) is a span in V from Gs to v0. The value of the functor LR(G) at (a, b) is v0 and the value of RL(G) at the pullback of the cospan (a, b) is also v0. Thus, RL(G)(λG(a, b)) = LR(G)(a, b) on the nose.
To see that λ is natural, suppose that G0 : S0 / V and the functor F : S / S0 defines an arrow from G to G0 in cat/V, that is G0F = G. We need to show that λG0 LR(F ) = RL(F )λG. Thus the following square of functors must commute (over V): / (LG, 1V) (1V, RG) LR(F ) (1V, RG0) / (LG, 1V) / (LG0, 1V)
RL(F ) λG λG0 L λ R λ where LR(F ) is the functor (1V, R(F )) which defines a morphism LRG / LRG0. The square does commute, up to isomorphism, since the effect of LR(F ) on a cospan Gs a / v o b v0 (an object of (1V, RG)) is actually the same cospan G0F s = Gs
a / v o b v0 and λG0 computes a pullback span, G0F s o c w d / v0. On the other hand RL(F )λG applied to the (same) cospan (a, b) computes a pullback span, Gs o c0 applies RL(F ) which likewise leaves the span unchanged, and so isomorphic to (c, d).
Next we consider the distributive law equations [
a / Gs o 1 v o 1 v a / Gs. On the other hand ηRL applied to v
The other unit equation is:
Gs. Application of λG gives a pullback span which we can choose to be a / Gs is exactly the same span v o 1 v a / Gs.
At a functor G, the left hand side of the triangle LηR applies to an object v a / Gs of the domain of LG and At a functor G, the left hand side ηLR applies to an object Gs b / v of the domain of RG and the result is the cospan Gs b / v o 1 v. Application of λG gives a pullback span which we choose to be Gs o 1 Gs b / v. Again, this is the same as the effect of RηL on Gs b / v.
LηR
ηRL ηLR
RηL LR w LR w '/ RL /' RL is:
We consider only one of the equations involving multiplications; the other is similar. The equation we consider
LRR LμR
LR λR / RLR
Rλ λ / RRL / RL μRL Again, we look at the equation in the domain and at an object G. A typical object of the domain of LRR(G) is an extended cospan of the form Gs a / v a0 / v0 o b w. Since μR(a, a0) is simply the composite Gs a0a / v0, we see that λG(LμR(G))(a, a0, b) is a pullback span Gs o c u d / w of b along a0a. On the other hand, λGR(G) applied to (a, a0, b) computes a pullback span of b along a0 with result Gs computes a pullback of c0 along a with result Gs o c00 u00 d00 / u0 giving the span Gs o c00 u00 d00d0 / w which is isomorphic to Gs o c
The preceding considerations give: u d / w.
Proposition 1 The transformation LR λ / RL is a (pseudo-)distributive law.
a / v o c0
u0 d0 / w. Applying RGλG d0 / w. Applying μRGLG composes d00 and d0
Using this proposition, and with minor modifications of the work of Beck [
It is convenient for later work to introduce some notation and use it to describe the unit and multiplication for the composed monad RL.
As noted above, for G : S / V, the domain of RLG is a comma category whose objects are certain spans in V. Let us denote them
a GCs v b
v0 Gs c w0
C w d a GCs b c Cv0 v v00 d
v000 The effect of the multiplication for RL on the zig-zag is to first form the span: 1 GCs Gs 1
Gs where w is a pullback of b and c, and then to compose each of the legs using the multiplication μL for the top leg (which is an instance of LLG), and the multiplication μR for the bottom leg (which is by then an instance of RRLG).
The unit for RL simply forms spans of identity arrows, so each object s of S yields a span 4
To illustrate the benefits of the distributive law and the resultant monad RL we present here a significantly
stronger version, made possible by the use of RL, of a result from [
We first describe a condition that is essentially the Beck-Chevalley condition for our purposes. (It does not matter if the reader is not familiar with other instances of the Beck-Chevalley condition.)
G / V and that RG r / G and LG l / G are R- and L-algebra structures. If Gs k / w is an object of (G, 1V), we denote its image under r by r(s, k). Similarly if v i / Gs is an object of (1V, G), we denote its image under l by l(i, s). Since r and l are arrows in cat/V, G(r(s, k)) = w and G(l(i, s)) = v. We say that condition (*) is satisfied if for any object s in S and any pullback (in V) it is the case that r(l(i, s), j) ∼= l(m, r(s, k)).
v i j k
? w m G?s v0 / G (on objects) by ξ(Gs o i v j / v0) = r(l(i, s), j). Then ξ ξ Proposition 3 If RLG
/ G is an RL-algebra, then r = ξRηLG and l = ξηRLG define R- and L-algebras, respectively, that satisfy condition (*). Conversely, suppose RG r / G and LG l / G are R- and L-algebra structures satisfying (*). Define ξ : RLG determines an RL-algebra structure on G.
ξ Proof. Suppose RLG
/G is an RL-algebra, r and l are defined as in the statement, and the square in condition (*) is a pullback in V. The definitions of r and l amount, on objects, to r(Gs and l(v a / Gs) = ξ(Gs o a
v 1 / v). For clarity we will sometimes suppress the objects of V, (v, Gs, etc), in what follows. Then, using the notation from the pullback square and noting that G(ξ( o 1 k / )) = w, a / v) = ξ(Gs o 1
Gs a / v) l(m, r(s, k)) = = = = = = = = l(m, ξ( o 1 ξ(G(ξ( o 1 ξ · RL(ξ)( o 1 ξμG( o 1 o i
j ξ( o 1 ξ( o i r(ξ( o i r(l(i, s), j) k / o m j
/ / ) 1 / ), j) k / )) k / )) o m k / o m 1 / )
1 / ) 1 / ) 1 / ) (where the fourth equality uses the associative law for the RL-algebra ξ) which proves condition (*).
To check that r and l satisfy the algebra axioms for R and L respectively is routine.
Conversely, suppose that r and l are R- and L-algebras respectively, and that they satisfy condition (*). Suppose that ξ is defined on objects as in the statement. Notice that it is straightforward to extend the definition of ξ to arrows of (the domain of) RLG.
For the RL-algebra associative law we need to verify that for a “zig-zag” W = Gs o x y starting from Gs, say, that ξRLξ(W ) = ξμG(W ). Now RL(ξ) applies ξ to o x / (while carrying along z and w) giving an object G-over the codomain of z, and ξ applies to this result along with z and w. So using the definition of ξ above, and writing o a b / for the pullback of y / o z , w / y / o z ξRL(ξ)(W )
w / ) = = = = = = = ξ(G(r(l(x, s), y)) o z r(l(z, r(l(x, s), y)), w) r(r(l(a, l(x, s)), b), w) r(r(l(xa, s), b), w) r(l(xa, s), wb) ξ( o xa ξ(μG(W )) wb / ) in which the third equation is an application of property (*) and the fourth and fifth equations use the associative laws of the L-algebra and the R-algebra respectively.
The RL-algebra identity law for ξ is straightforward noting the definition of ηRL in terms of ηR and ηL. 5
In the development of a 2-categorical treatment of the Yoneda Lemma, Ross Street [
In the realm of database state spaces it seems that most authors have taken the set-based state space approach.
We have argued elsewhere [
Spans have a wide variety of applications, and so have long been studied category theoretically. Given a category C with pullbacks there is a bicategory spanC with the same objects as C, with spans of arrows from C as arrows, and with composition given by pullback, and most treatments take this point of view. Such spans are oriented, despite their symmetry, by definition, since they are arrows of a bicategory. To the authors’ knowledge, the monad of anchored spans presented here, including its relationship to the comma category monads L and R, is entirely new. In addition it has noteworthy and desirable differences from earlier treatments because the orientation of spans comes from the fibering over V, and because, in the manner of comma categories, spans appear as objects rather than as arrows.
Meanwhile spans have also had a wide range of applications among researches into bidirectional
transformations. In particular the graph transformation community has used spans for many years and the recent paper
of Orejas et al [
The main findings from this paper are 1. By explicitly working on cat/V the two comma categories (G, 1V) and (1V, G) can be fibred over V and so sources and targets can be tracked, resulting in monads R and L respectively. Those monads capture the category theoretic structure of arrows out of images of G and into images of G respectively, and, being built from those comma categories, they lift arrows of V to objects of RG and LG (fibred over V). 2. There is a pseudo-distributive law between R and L, and so RL is itself a monad, the monad of anchored spans. Furthermore the tracking of sources and targets, provided by the fibring, orients the spans as spans from images of G (the “anchoring”). The monad RL captures the category theoretic structure of spans from images of G, and, being built from iterated comma categories, lifts spans in V from images of G to objects of RLG (fibred over V). 3. Having an RL-algebra is equivalent to having a pair of algebras (one R and one L) satisfying condition (*).
The first finding shows that we have found the right context in which to work with comma categories for a variety of state space based applications. The second finding solves the long standing problem of making mathematically precise the composition of preferred and reversed transitions (eliminating the “hand-waving”). The third finding neatly illustrates the extra power available when spans of transitions can be dealt with as single objects. 7
The authors are grateful for the support of the Australian Research Council and NSERC Canada, and for insightful suggestions from anonymous referees.