Abstract
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.
Original language | English |
---|---|
Pages (from-to) | 31-42 |
Number of pages | 12 |
Journal | CEUR Workshop Proceedings |
Volume | 1396 |
Publication status | Published - 2015 |
Event | International Workshop on Bidirectional Transformations (4th : 2015) - L'Aquila, Italy Duration: 24 Jul 2015 → 24 Jul 2015 |