Unifying Set-Based, Delta-Based and Edit-Based Lenses Michael Johnson CoACT, Departments of Mathematics and Computing Macquarie University Robert Rosebrugh Department of Mathematics and Computer Science Mount Allison University Abstract There are many different types of lenses, but largely they fall into the three classes of the title: set-based, delta-based and edit-based lenses. This paper develops some of the general relationships between those classes. The main results are that a category of set-based lenses is a full subcategory of a category of delta-based lenses determined by send- ing sets to codiscrete categories; that symmetric set-based lenses can similarly be seen as symmetric delta-based lenses; that symmetric edit- based lenses are able to be represented as symmetric delta-based lenses, although not as a subcategory; and that symmetric edit-based lenses can also be seen as spans of a new notion of asymmetric edit-based lenses. The importance of the paper is that it provides a substantial unification with concrete inter-conversions developed among the three main approaches to lenses in both their symmetric and asymmetric forms. 1 Introduction In a developing field like Bidirectional Transformations (Bx), many different formalisms are introduced as different application needs are recognised. Some of the main functions of a mathematical foundation are to determine when different formalisms are the same, when they are special cases of one another, and when they can be interconverted in some way. Most important of all, any relationships established between different formalisms need to be presented via precise mathematical translations. Once this is done, workers seeking to use the formalisms for new applications can know when a different choice of formalism makes a real difference, or can choose the formalism that suits their thinking best, knowing that it can be interconverted automatically with formalisms that others might prefer. There are many different types of lenses. Indeed, it sometimes seems that every paper with “lens” in its title defines at least one new type of lens. There are lenses, well-behaved lenses, very well-behaved lenses, symmetric lenses, delta lenses, symmetric delta lenses, category lenses (which are asymmetric), edit lenses (which are symmetric), and there are monadic lenses (both symmetric and asymmetric), product lenses, quotient lenses, relational lenses and resourceful lenses. The list goes on. Synthesis and comparison is important. A review of these and other lens proposals shows that they (mostly) fall into three main classes: lenses among sets with functions as their main update operations, lenses among categories with functors (and sometimes functions) as their main update operations, and lenses among modules (M -sets with partial action of a monoid M of “edits”) Copyright c by the paper’s authors. Copying permitted for private and academic purposes. In: A. Anjorin, J. Gibbons (eds.): Proceedings of the Fifth International Workshop on Bidirectional Transformations (Bx 2016), Eindhoven, The Netherlands, April 8, 2016, published at http://ceur-ws.org 1 with (stateful) monoid homomorphisms as their main update operations. These three classes are the set-based, delta-based and edit-based classes of the title of this paper. (As mathematicians we were tempted to focus on the mathematical content and describe them as set-based, category-based and monoid-based, but the latter two classes seem to be better known in the Bx community as delta lenses and edit lenses.) This paper establishes precise mathematical relationships between these three main classes of lenses. Of course, to establish precise mathematical relationships we need to work with specific types of lenses from each of the three classes, so we have tried to present the development of the relationships in a sufficiently general way that it should be clear how other instances from a particular class of lenses might be similarly treated. And we have chosen to illustrate a number of different useful approaches to establishing the relationships. In addition, we try to be clear about when we are talking about a class, the edit lenses for example, and when we are talking about the specific instance that we are working with, which in this case is called an e-lens and is defined explicitly in the appropriate section of this paper. An outline of the plan of the paper is as follows. We begin by discussing codiscrete categories to show how asymmetric set-based lenses can be viewed as special cases of asymmetric delta lenses, and we establish precise interconversions. The codiscrete categories model the notion that, in set-based lenses, typically, any state can be updated to any other state, and no information about the nature of the update process is recorded apart from which state the update began in, and which state it ended in. We could have proceeded by following a similar approach to develop a relationship between symmetric set- based lenses and symmetric delta lenses, but instead we illustrate a general approach to symmetric lenses (of various kinds) which uses spans of asymmetric lenses (of corresponding kinds). Since we already have established the interconversions among asymmetric set-based lenses and asymmetric delta lenses, they can be used to interconvert spans of such, and that leads directly to the interconversions between symmetric set-based lenses and symmetric delta lenses. We then turn to edit lenses. To date, these have only appeared in a symmetric form, and the core of the paper is devoted to analysing edit lenses and relating them too to delta lenses, this time using a category of elements construction. Because the action of an edit in an edit lens is not necessarily fully defined there are some delicacies and edit lenses do not merely form a subcategory of (fully defined) delta lenses, but we do obtain a functor concretely realising each edit lens as a symmetric delta lens. After this detailed treatment of edit lenses, we are well-placed to introduce the new notion of asymmetric edit lens. (After all, every paper with “lens” in its title should define at least one new type of lens!) Doing so presents an instance of the authors’ approach to deducing asymmetric lenses from symmetric ones. Of course, one test of the success of the definition of asymmetric edit lenses is how spans of them relate to symmetric edit lenses, so we proceed to carefully develop two constructions to show how to interconvert between spans of the new asymmetric edit lenses and the extant (symmetric) edit lenses. Finally, in the concluding section we draw together some of the more categorical aspects of the correspondences developed in the body of the paper and clarify some of the finer points of the choices made. We hope that this synthesis of different classes of lenses will go some way towards systematising the wide body of Bx theory that uses lenses. 2 Sets, codiscrete categories and lenses A category X is called codiscrete if there is exactly one arrow between each pair of objects, including between an object and itself. This property is in a sense dual to the property of a discrete category where there is no arrow between different objects and exactly one endo-arrow, the identity, on each object. For each set X there is both a unique discrete category whose objects are X, and a unique codiscrete category with objects X. (In fact, the functors constructing discrete and codiscrete categories on sets are the two adjoints to the forgetful functor sending each category to its set of objects.) We are going to show that codiscrete categories provide a good context for considering lenses in the category set (often called “set-based lenses” and including, among many others, the work in [PS03] and [HPW11]) using the idea that each state can be updated to every other state. Note first that for any two sets X and Y there is a bijective correspondence between functions from X to Y and functors between the codiscrete categories with objects X and Y . In fact, the functor sending each set to its corresponding codiscrete category is full and faithful (like the functor sending each set to its corresponding 2 discrete category) and so gives another way that the category set of sets and functions can be seen as a full subcategory of the category cat of categories. Proposition 1 Let X and Y be sets and X and Y the corresponding codiscrete categories. There is a bijective correspondence between functions from X to Y and functors from X to Y. Proof. Given a function f : X / Y , we define a functor f : X / Y as follows. On objects f is defined by f . If 0 x and x are elements of X and α : x / x is the unique arrow of X from x to x0 then f (α) is the unique arrow 0 0 from f (x) to f (x ). It is easy to see that f is a functor. In the other direction, if f : X / Y is a functor, restricting it to its effect on objects defines a function f :X / Y. We leave to the reader the straightforward verification that these constructions are mutually inverse. We are going to use this correspondence to realise asymmetric lenses in set as delta lenses (d-lenses). First, recall the definition of an asymmetric lens in a category C with products, for example from [JRW10]. Note that we have reversed the order of X and Y in the domain of the Put for consistency with other Puts below. We write as usual π0 and π1 for the two projections from a binary product. We use multiple subscripts, for example π02 for the projection onto the corresponding factors (in this case the first and the third factor) of a product with more than two factors. And we write hf, gi for the unique arrow into a binary product determined by two arrows with common domain (also called a span of arrows) f and g. Definition 2 For objects X and Y in C, an asymmetric lens in C from X to Y , denoted L : X / Y is a quadruple (X, Y, g, p) of sets and functions where g : X / Y is called the “Get” morphism and p : X × Y /X is called the “Put” morphism. A lens is called well-behaved if it satisfies: (i) (PutGet) the Get of a Put is the projection: gp = π1 (ii) (GetPut) the Put for a trivially updated state is trivial: ph1X , gi = 1X A well-behaved lens is called very well-behaved if it satisfies: (iii) (PutPut) composing Puts does not depend on the first view update: p(p × 1Y ) = pπ0,2 : X × Y × Y /X When C is the category set of sets, the equations can be written as follows for x in X and y, y 0 in Y : (i) g(p(x, y)) = y (ii) p(x, g(x)) = x (iii) p(p(x, y), y 0 ) = p(x, y 0 ) We remind the reader of the definition of (asymmetric) d-lens from, for example, [JR15] and [DXC11]. Write as usual |C| for the set of objects of a category C and |X2 | = Arr(X) for the set of arrows of the category X. For a functor G : X / Y the comma category G/Y has as objects pairs (X, α) where X is an object of X and α : G(X) / Y is an arrow of Y with arbitrary codomain. Definition 3 A (very well-behaved) asymmetric delta lens (d-lens) from X to Y is a pair (G, P ) where G : X / Y is a functor (the “Get”) and P : |G/Y| / |X2 | is a function (the “Put”) and the data for α : G(X) /Y and β : G(X ) 0 / Y satisfy: 0 (i) d-PutInc: the domain of P (X, α) is X (ii) d-PutId: P (X, idG(X) ) = idX (iii) d-PutGet: G(P (X, α)) = α (iv) d-PutPut: if X 0 is the codomain of P (X, α), and hence G(X 0 ) = Y , then P (X, βα) = P (X 0 , β)P (X, α) 3 From a (very) well-behaved asymmetric set lens L = (X, Y, g, p) in set we can construct a corresponding asymmetric d-lens (g, p) between codiscrete categories. The construction follows. The categories X and Y are the codiscrete categories corresponding to X and Y and g is the functor corre- sponding to g. We need to define p. The domain of p is the set of objects |g/Y|. These objects are pairs (x, α) for an object x of X and an arrow α : g(x) / y in Y. Since α is unique, such an object is the same thing as a pair (x, y) in X × Y . Define p(x, α) to be the unique arrow of X from x to p(x, y). Conversely, suppose that (G, P ) is a very well-behaved d-lens between codiscrete categories X and Y. Let X and Y be the sets of objects of X and Y and let g : X / Y be the object function of the functor G. Once again, when Y is codiscrete the objects of G/Y are in bijective correspondence with the elements of X × Y . Define p : X ×Y / X by letting p(x, y) be the codomain of P (x, α), where α is the unique arrow from Gx to y. Then L = (X, Y, g, p) is a very well-behaved asymmetric lens in set. Proposition 4 There is a bijective correspondence between asymmetric lenses L = (X, Y, g, p) and asymmetric d-lenses (g, p) from X to Y between the corresponding codiscrete categories. Proof. The correspondence is based on the constructions above. The verification of the correspondence is straightforward. We turn now to developing a similar correspondence between set-based symmetric lenses (see [HPW11]) and symmetric delta lenses (see [DX+11]) between codiscrete categories. We could approach this directly, as we have done above for asymmetric lenses and as we will do below for symmetric edit lenses, by reviewing the relevant definitions and building a correspondence. Instead, since we see that approach below when studying edit lenses, we will illustrate the usefulness of the span approach to symmetric lenses of various kinds ([JR14, JR15]). We will see how the correspondence we have just laid out for the asymmetric case can be carried across to the symmetric case. Recall from [JR14] and [JR15], and from the remarks in [HPW11], that symmetric lenses of various kinds can be defined via equivalence classes of spans of asymmetric lenses of the corresponding kinds. In particular, a set-based symmetric lens can be presented as a span of asymmetric set-based lenses. By Proposition 4, the span of asymmetric lenses corresponds to a span of d-lenses between codiscrete categories. We need to show that this correspondence is independent of the choice of representative, that is: Proposition 5 Suppose that X o S / Y and X o S0 / Y are equivalent spans of very well behaved asymmetric lenses in set. Then the corresponding spans of d-lenses between codiscrete categories X o S /Y and X o S 0 / Y are equivalent symmetric d-lenses. Proof. The proof is conceptually straightforward, so we need not rehearse all the details of the definitions of the equivalences from earlier papers. It suffices to prove the result for generators of the equivalence relation in spans of lenses in set, and that equivalence is generated by non-empty asymmetric lenses between the peaks of the spans that commute, as lenses, with the spans [JR14]. But a non-empty asymmetric lens in set is well known to have a surjective Get function, and under the correspondence (Proposition 4) such a lens K : S / S0 corresponds to a surjective on objects d-lens K : S / 0 S between codiscrete categories. It is easy to see that if the lens K commutes with the spans X o S / Y and X o S0 / Y then the lens K commutes with the spans X o S / Y and X o S0 / Y. Finally, in [JR15] it was shown that such a surjective on objects d-lens K suffices to show that the two spans of d-lenses X o S / Y and X o S0 / Y are equivalent as symmetric d-lenses. 3 Edit Lenses Hoffman, Pierce and Wagner [HPW12, Wag14] have introduced a symmetric lens notion that includes “deltas” but requires them to be chosen from a monoid (a set with an associative binary operation having a unit element) whose elements are called “edits”. The idea is that some members of a common set of edits can be applied to some states, and that the action of the edits is unitary and composes according to the monoid multiplication (properties that are also called “equivariance”). This goes part way towards reconciling the gap between symmetric lenses 4 [HPW11] and symmetric delta-lenses (which we also call fb-lenses) [JR15]. There is an extensive discussion of the differences between edit lenses and symmetric (set-based) lenses in the excellent thesis of Wagner [Wag14]. We first review the definitions. For consistency with our presentation of asymmetric set and d-lenses, we write the actions of modules (or partial M -sets) on the right. Definition 6 Let X be a set and MX a monoid. A module (X, MX ) is a (partial) monoid action of MX on X. That is, there is a partial function denoted · : X × MX / X. The multiplication in MX (and sometimes the action) will be denoted by juxtaposition. They satisfy the following: (M1) for all x in X, x · 1 = x (M2) for all x in X and m, m0 in MX , (x · m) · m0 = x · (mm0 ). We stress that the action is partial. This means that the (standard) meaning of the equations is that whenever either side of an equation involving the action is defined then the other side is also defined and of course the resulting values on both sides are the same. In particular, the first point implies that the action of the identity monoid element on any element of X is always defined. For now we ignore the requirement in [HPW12] for a distinguished (initial) element of the set X in a module. Although it is essential for the behavioural equivalence among edit lenses in [HPW12], the distinguished element plays no role in our equivalence among edit lenses. The following definition is not present in [HPW12], but it provides the obvious way to compare modules. Definition 7 A module homomorphism between modules (X, MX ) and (Y, MY ) is a pair (f, φ) where f : X /Y is a function and φ : MX / MY is a monoid homomorphism, and for all x in X and m in MX they satisfy: f (x · m) = f (x) · φ(m) or, equivalently, the following diagram commutes: X × MX · /X f ×φ f   Y × MY · /Y Again, since the actions are partial, the equation means that if x · m is defined, then so is f (x) · φ(m), and conversely. It should be clear that there is an associative composition of module homomorphisms, and we denote the category whose objects are modules and whose morphisms are module homomorphisms by mod. There is also a category which is very naturally determined by a module. Indeed, let (X, MX ) be a module. We construct the category XM as follows. The set of objects of XM is X. Next, let XM (x, x0 ) = {(x, m) | x · m = x0 } Thus the set of arrows from x to x0 is just the set of pairs (x, m) such that x · m = x0 . If (x, m) is an arrow with codomain x0 , so x · m = x0 , and (x0 , m0 ) is an arrow with codomain x00 , so x0 · m0 = x00 , their composite is defined by (x0 , m0 )(x, m) = (x, mm0 ). Proposition 8 For any module (X, MX ), XM is a category. Moreover, the construction (X, MX ) 7→ XM is the object function of a functor mod / cat. Proof. It is easy to see that XM is a category. The identity arrow on x is (x, 1) and composition is associative because it is so in MX . A module homomorphism (f, φ) : (X, MX ) / (Y, MY ) defines a functor from XM to YM . It is just the function f on objects and the property of module homomorphisms guarantees that the functor is well-defined on arrows. Functoriality follows from equivariance. We are going to use this construction below when we associate an edit lens to an fb lens. It is perhaps worth noting that, when the monoid action is fully defined, the category XM is just the well known category of elements: a monoid action on a set X is just a functor F from the monoid, viewed as a category with one object, to the category of sets, with the one object sent to the set X, and then XM = el(F ). 5 Definition 9 Let MX and MY be monoids and C a set (the complements or better the consistencies). A stateful monoid homomorphism from MX to MY is a partial function p : MX ×C / MY ×C and. letting p(m, c) = (n, c0 ) and p(m0 , c0 ) = (n0 , c00 ), we have: p(1, c) = (1, c) and p(mm0 , c) = (nn0 , c00 ). Note immediately that this definition differs from the definition in [HPW12] where stateful homomorphisms are required to be total functions. Nevertheless, our definitions of edit lenses require that the stateful homomorphisms involved must be defined whenever needed. Thus despite this variation there is a perfect correspondence between our edit lenses and those of [HPW12]. The first equation says that p respects the identity while preserving the complement. In terms of squares where the vertical arrows are elements of the monoids M and N and the horizontal bars are elements of C, the second considers: c m n   c0 m0 n0   c00 The intention is that the application of p to the top and left elements results in the bottom and right elements. The second equation in the definition says that the squares “paste” together respecting the multiplications of M and N . An edit lens consists of modules (X, MX ) and (Y, MY ), a common set of complements C, a stateful homo- morphism p from MX to MY with complements C, and another q from MY to MX also with complements C along with a set K ⊆ X × C × Y of “consistent triples” which express synchronization of elements of X and Y , thought of as states. The module actions are required to interact with the stateful homomorphisms so that on both sides the effect of the action starting from a consistent triple arrives at a consistent triple (see the diagram following the definition). Formally: Definition 10 Let (X, MX ) and (Y, MY ) be modules. An edit-lens (e-lens) λ : (X, MX ) ↔ (Y, MY ) from (X, MX ) to (Y, MY ) is given by λ = (C, p, q, K) where C is a set whose elements are called complements, p : MX × C / MY × C and q : MY × C / MX × C are stateful monoid homomorphisms (with the same complements C) and K is a non-empty relation K ⊆ X × C × Y called the consistency relation. The data are required to satisfy: (1) (x, c, y) ∈ K and xm defined implies p(m, c) = (n, c0 ) (say) defined, yn defined and (xm, c0 , yn) ∈ K (2) (x, c, y) ∈ K and yn defined implies q(n, c) = (m, c0 ) (say) defined, xm defined and (xm, c0 , yn) ∈ K. Again, we do not include the requirement in [HPW12] for a distinguished (initial) element in the set of complements of an edit lens. Thus we do not have the corresponding requirement that it be consistent with the initial elements of the participating modules. It has been suggested that for consistency of notation we should call the edit lenses discussed here “se-lenses” since they are a symmetric form of edit lens. In deference to the originators of edit lenses, who chose to call them simply “edit lenses” rather than emphasising their symmetric nature, we have chosen here to use “e-lens” and to instead emphasise the asymmetric nature of the “ae-lenses” that will be described later in this paper. Diagrammatically, in terms of squares similar to those above, but with the vertical arrows now indicating monoid action and the horizontal bars consistent triples from K, we have that in: c x y m n   x0 y0 c0 if the top row is in K, and the bottom row and one side arise from an application of p or q to the top row and the other side, then the bottom row is also in K. The idea is as follows. Suppose that the consistency or synchronization of x and y is witnessed by c. When the edit m is applied to x giving x0 then the image of p(m, c) 6 provides an edit n which necessarily acts on y giving y 0 say, and a witness c0 to the synchronization of x0 = xm and y 0 = yn. Similarly if the edit n is applied to y giving y 0 then q(n, c) provides an edit m and a witness c0 to the synchronization of yn and xm. 4 Edit lenses as symmetric delta lenses We begin by defining an equivalence relation on e-lenses with common domain and codomain. Modulo this equivalence relation, e-lenses will compose associatively and we will then have a category of e-lenses that can be compared with the known category sdLens of symmetric delta lenses, also called fb-lenses [JR15]. A relation σ between C and C 0 is called total on both sides when for any c ∈ C there is some c0 ∈ C 0 with cσc0 , and conversely for any c0 ∈ C 0 there is some c ∈ C with cσc0 . Definition 11 Let λ = (C, p, q, K) and λ0 = (C 0 , p0 , q 0 , K 0 ) be e-lenses from (X, MX ) to (Y, MY ). We say λ ≡e λ0 if there is a total on both sides relation σ ⊆ C × C 0 satisfying whenever cσc0 : (i) (x, c, y) in K if and only if (x, c0 , y) in K 0 (ii) if p(m, c) = (n, d) and p0 (m, c0 ) = (n0 , d0 ) are both defined then n = n0 and dσd0 (iii) if q(n, c) = (m, d) and q 0 (n, c0 ) = (m0 , d0 ) are both defined then m = m0 and dσd0 Proposition 12 The relation ≡e is an equivalence relation. Proof. Reflexivity of ≡e is clear. Conditions (i), (ii) and (iii) are also clearly symmetric and transitive. Next we define a composite of e-lenses. Definition 13 Let λ = (C, p, q, K) and µ = (C 0 , p0 , q 0 , K 0 ) be e-lenses from (X, MX ) to (Y, MY ) and (Y, MY ) to (Z, MZ ) respectively. We define µλ = (D, r, s, M ) as follows: (i) D = C × C 0 (ii) r(m, (c, c0 )) = (`, (c1 , c01 )) where p(m, c) = (n, c1 ) and p0 (n, c0 ) = (`, c01 ). The function s is defined similarly, but using q and q 0 . (iii) M = {(x, (c, c0 ), z) | ∃y ∈ Y with (x, c, y) ∈ K and (y, c0 , z) ∈ K 0 } Proposition 14 µλ is an e-lens. Proof. The data for D and M for µλ are of compatible types since M may be considered to be contained in X × (C × C 0 ) × Z. We need to verify that r and s are stateful monoid homomorphisms and that they satisfy the two conditions involving the consistency relation in Definition 10. We show first that r is a stateful monoid homomorphism. The preservation of the identity by both p and p0 guarantees the same for r. For the preservation of multiplication for r consider the diagram: c c0 m n `    c1 c01 0 0 m n `0    c2 c02 which should convince the reader that for the composite we can “paste” squares arising from p and p0 horizontally, as well as vertically from the monoid compositions. Similarly s is a stateful monoid homomorphism. Next consider the conditions involving the consistency relation M . We need to show first that (x, (c, c0 ), z) ∈ M and r(m, (c, c0 )) = (`, (c1 , c01 ) implies (xm, (c1 , c01 ), z`) ∈ M . Consideration of the diagram c c0 x y z m n `    x0 c1 y0 z0 c01 7 shows why this is the case. Similar considerations apply to s. Proposition 15 The composite of e-lenses respects the relation ≡e . In other words, ≡e is a congruence. Proof. Suppose that λ = (C, p, q, K) and λ0 = (C 0 , p0 , q 0 , K 0 ) are e-lenses from (X, MX ) to (Y, MY ), that λ ≡e λ0 via σ ⊆ C × C 0 , and that µ = (C 00 , p00 , q 00 , K 00 ) is an e-lens from (Y, MY ) to (Z, MZ ). We will show that µλ ≡e µλ0 . Now with the notation above µλ = (C × C 00 , r, s, M ) and µλ0 = (C 0 × C 00 , r0 , s0 , M 0 ). We need to define σ ⊆ (C × C 00 ) × (C 0 × C 00 ). We set 0 σ 0 = {((c, c00 ), (c0 , c00 )) | (c, c0 ) ∈ σ} We demonstrate that σ 0 witnesses µλ ≡e µλ0 . First, σ 0 is total on both sides since σ is: for any c ∈ C there is a c0 ∈ C 0 with cσc0 , so for any (c, c00 ) there is a (c0 , c00 ) with (c, c00 )σ 0 (c0 , c00 ), and similarly for the other side. Next we show that σ 0 satisfies conditions (i)–(iii) in Definition 11. Throughout we suppose that (c, c00 )σ 0 (c0 , c00 ) and hence that cσc0 . Now (x, (c, c00 ), z) ∈ M if and only if there is a y with (x, c, y) ∈ K and (y, c00 , z) ∈ K 00 . Since cσc0 , this is exactly the same as (x, c0 , y) ∈ K 0 and (y, c00 , z) ∈ K 00 (using condition (i) for σ) and this in turn is equivalent to (x, (c0 , c00 ), z) ∈ M 0 . So, condition (i) is satisfied for σ 0 . For condition (ii) we assume that both r(m, (c, c00 )) = (`, (d, d00 )), say, and r0 (m, (c0 , c00 )) = (`0 , (d0 , d000 )), say, are defined. We are required to show that ` = `0 and (d, d00 )σ 0 (d0 , d000 ). Now referring to the formulas for r and r0 from Definition 13 we see that d and d0 arise from p(m, c) and p(m, c0 ) and so dσd0 (by condition (ii) for σ). Furthermore, p(m, c) and p(m, c0 ) also provide elements of the monoid MY , and by condition (ii) for σ they are both equal, say to n ∈ MY . Finally, (`, d00 ) and (`0 , d000 ) are both p(n, c00 ), so ` = `0 and d00 = d000 , and hence (d, d00 )σ 0 (d0 , d000 ). Condition (iii) involving s and s0 follows from the same argument applied to q and q 0 . For composition on the other side, suppose ν is an e-lens from (W, MW ) to (X, MX ). An essentially symmetric argument shows that λν ≡e λ0 ν, completing the proof. Corollary 16 The ≡e equivalence classes are the arrows of a category eLens with modules as objects. The composition in eLens is by e-lens composite on equivalence classes. Our next goal is to construct a symmetric delta lens from an edit lens. First we need the definition of symmetric delta lens, often called an fb-lens (named after its basic operations which are known as “forwards” and “backwards”). We revisit the definition from [JR15], which in turn is based on [DX+11]. Definition 17 Let X and Y be categories. An fb-lens from X to Y is given by a 4-tuple M = (δX , δY , f, b). The data δX , δY are functions with common domain denoted RXY forming a span of sets denoted δX : |X| o RXY / |Y| : δY An element r of RXY is called a corr. For r in RXY , if δX (r) = X and δY (r) = Y the corr is denoted r : X ↔ Y . The data f and b are operations called forward and backward propagation: f : Arr(X) ×|X| RXY / Arr(Y) ×|Y| RXY b : Arr(Y) ×|Y| RXY / Arr(X) ×|X| RXY where the pullbacks (also known as fibered products) ensure that when f(x, r) = (y, r0 ), we have d0 (x) = δX (r) and d1 (y) = δY (r0 ). We also require that d0 (y) = δY (r) and δX (r0 ) = d1 (x). Likewise for b: when b(y, r) = (x, r0 ), we have d0 (y) = δY (r) and d1 (x) = δX (r0 ) along with d0 (x) = δX (r) and δY (r0 ) = d1 (y). Furthermore, we require that both propagations respect both the identities and composition in X and Y, so that we have: r : X ↔ Y implies f(idX , r) = (idY , r) and b(idY , r) = (idX , r) 8 and f(x, r) = (y, r0 ) and f(x0 , r0 ) = (y 0 , r00 ) imply f(x0 x, r) = (y 0 y, r00 ) and b(y, r) = (x, r0 ) and b(y 0 , r0 ) = (x0 , r00 ) imply b(y 0 y, r) = (x0 x, r00 ) Construction 0: An fb-lens from an e-lens. Let (X, MX ) and (Y, MY ) be modules and let λ = (C, p, q, K) be an e-lens from (X, MX ) to (Y, MY ). We construct from λ an fb-lens Lλ = (δX , δY , f, b). Let XM and YM be the categories constructed from (X, MX ) and (Y, MY ) according to Proposition 8. We let the set of corrs of Lλ be K and the projections from K define a span of sets δX : |X| o K / |Y| : δY . We need to define the forward and backward propagations for Lλ . Suppose xm = x0 and (x, c, y) in K. Define f((x, m), (x, c, y)) = ((y, n), (x0 , c0 , y 0 )) where p(m, c) = (n, c0 ) and yn = y 0 . Note that since λ is an e-lens, the conditions for λ on p and K guarantee that (x0 , c0 , y 0 ) in K. The definition of backward propagation is similar: b((y, n), (x, c, y)) = ((x, m), (x0 , c0 , y 0 )) for q(n, c) = (m, c0 ) and xm = x0 . When we note that compatibility of f and b with identities and composition follows immediately from the corresponding requirements for the stateful homomorphisms p and q of λ, we have shown: Proposition 18 For any e-lens λ, Lλ is an fb lens. We also review the equivalence of fb-lenses from [JR15]. Definition 19 Let L = (δX , δY , f, b) and L0 = (δX 0 0 , δY , f 0 , b0 ) be two fb-lenses from X to Y with corrs RXY and 0 0 0 RXY respectively. We say L ≡fb L if and only if there is a relation σ from RXY to RXY with the following properties: 1. σ is compatible with the δ’s, i.e. rσr0 implies δX r = δX 0 0 0 0 r and δY r = δY r 2. σ is total in both directions, i.e. for all r in RXY , there is an r0 in RXY 0 with rσr0 and conversely. 3. for x an arrow of X, if rσr0 and δX r is the domain of x then the first components of f(x, r) and f 0 (x, r0 ) are equal and the second components are σ related, i.e. π0 f(x, r) = π0 f 0 (x, r0 ) and π1 f(x, r)σπ1 f 0 (x, r0 ). 4. the corresponding condition for b, i.e. for y an arrow of Y, if rσr0 and δY r is the domain of y then π0 b(y, r) = π0 b0 (y, r0 ) and π1 b(y, r)σπ1 b0 (y, r0 ). The construction of fb-lenses from e-lenses preserves equivalences: Proposition 20 λ ≡e λ0 implies Lλ ≡fb Lλ0 . Proof. Suppose λ = (C, p, q, K) and λ0 = (C 0 , p0 , q 0 , K 0 ) are equivalent e-lenses from (X, MX ) to (Y, MY ) via σ ⊆ C × C 0 . We want to show that Lλ ≡fb Lλ0 . For compactness, we will write consistent triples as strings without parentheses or commas. Let τ = {(xcy, xc0 y) | cσc0 and xcy ∈ K}. Note that (xcy, xc0 y) ∈ τ implies xc0 y ∈ K 0 , so τ ⊆ K × K 0 is, as required, a relation between the corrs of Lλ and the corrs of Lλ0 . Since the corrs for Lλ and Lλ0 are K and K 0 and the δs are projections, condition 1 in Definition 19 is immediately satisfied: (xcy)τ (x0 c0 y 0 ) implies x = x0 and y = y 0 so δX (xcy) = δX 0 (x0 c0 y 0 ) and δY (xcy) = δY 0 (x0 c0 y 0 ). Condition 2 follows immediately from σ being total on both sides. For conditions 3 and 4, suppose that (xcy)τ (xc0 y) and xm is an arrow of XM with p(m, c) = (n, d) and p (m, c0 ) = (n, d0 ). The first component of both f(xm, xcy) and f 0 (xm, xc0 y) is yn, and their second components 0 are the τ -related x0 dy 0 and x0 d0 y 0 demonstrating that condition 3 is satisfied. Condition 4 follows similarly. Since ≡fb classes are arrows of the category sdLens (as we proved in [JR15]) we get a functor: Corollary 21 The assignment λ 7→ Lλ is the arrow part of a functor eLens / sdLens. Thus we have a functor realising each e-lens as an fb-lens and sending the composition of e-lenses to the composition of the corresponding fb-lenses. This functor will be discussed further in Section 6. 9 5 Asymmetric edit lenses We now return to the question of whether every e-lens arises as a span of some kind of asymmetric e-lens. To provide edit lens analogues of results in [JR15], we need to introduce a notion of asymmetric edit lens. The fundamental idea is that the Get should be a module homomorphism (K, MK ) to (X, MX ) and the Put should be a stateful homomorphism MX to MK with complements the elements of K. We begin with some notation. In what follows we will use subscript 0 and subscript 1 in two distinct ways (the context will make clear which is intended, but beware — sometimes the same subscript will be used in the two different senses inside one equation). First, a stateful monoid homomorphism is a partial function of two variables which returns two values — we will write for example P (m, k)0 for the first component of the result and P (m, k)1 for the second. We often use this notation to “hide” the projections from a product and efficiently talk about one component or the other. But also, in Construction 1 below we need to work with the co-product of two monoids. Like all binary coproducts it comes with two inj ections, and a subscript 0 (or subscript 1) is used to indicate whether a particular generator of the coproduct arises from using the first (respectively the second) injection. Definition 22 Let (X, MX ) and (K, MK ) be modules. An asymmetric edit-lens (ae-lens) from (K, MK ) to (X, MX ), often written κ : (K, MK ) / (X, MX ), is a triple κ = (f, φ, P ) where f : K / X is a function, φ : MK / MX is a monoid homomorphism and P is a stateful monoid homomorphism from MX to MK with complement K (that is is a partial function MX × K / MK × K respecting, as in Definition 9, composition and identity) satisfying: i) (f, φ) is a morphism of modules (that is for k in K, ` in MK , if k · ` is defined, then f (k) · φ(`) is defined and is equal to f (k · `)) ii) (PutGet) If f (k) · m is defined then – P (m, k) is defined – k · P (m, k)0 = P (m, k)1 – φ(P (m, k)0 ) = m (and notice that these imply f (k) · m = f (P (m, k)1 )). Construction 1: A span of ae-lenses from an e-lens. In this construction we will use the coproduct A∗B of two monoids, A and B. It is the monoid freely generated by the non-identity elements of A and of B subject to the relations inside each of A and B. More concretely, it can be represented as strings of non-identity elements alternately from A and B with multiplication given by concatenation and, as necessary, reduction of adjacent elements by multiplication inside A and B. As it happens in our construction below A and B will both be the same monoid, so we need to carefully use subscripts to distinguish whether a generator is from the first copy (A) or from the second (B). Suppose that λ = (C, p, q, K) : (X, MX ) ↔ (Y, MY ) is an e-lens from (X, MX ) to (Y, MY ). We construct a span of ae-lenses as follows. The head of the span is the module (K̂, MK̂ ) defined by: i) The set K̂ = K ii) The monoid MK̂ is the coproduct of the monoid MX ×MY with itself, that is MK̂ = (MX ×MY )∗(MX ×MY ) iii) The action on K is defined by defining it on generators: for a k in K̂ with form (x, c, y), and a generator (m, n)0 in MK̂ , the action k · (m, n)0 is defined if and only if 1. x0 = x · m is defined, whence p(m, c) is defined 2. p(m, c) = (n, c0 ) (notice the n comes from the generator and it follows that y · n = y 0 , say, is defined) and then we define k · (m, n)0 = (x0 , c0 , y 0 ), which is an element of K̂. Similarly for a generator (m, n)1 in MK̂ , the action k · (m, n)1 is defined if and only if q(n, c) = (m, c00 ) for some c00 and y 0 = y · n is defined (and hence x0 = x · m is defined), whence we define k · (m, n)1 = (x0 , c00 , y 0 ). 10 Now we define an ae-lens κ̂ : (K̂, MK̂ ) / (X, MX ), denoted κ̂ = (f, φ, P ), by f (x, c, y) = x, φ((m, n)0 (m0 , n0 )1 . . .) = mm0 . . . (where the string is finite of course), and, if x · m is defined, whence p(m, c) is defined and equal say to (n, c0 ), P (m, (x, c, y)) = ((m, n)0 , (x · m, c0 , y · n)) If x · m is not defined, then P (m, (x, c, y)) is not defined. The ae-lens just defined will be left leg of the span of ae-lenses. The data for the right leg ae-lens κ̂0 : (K̂, MK̂ ) / (Y, MY ), denoted (g, ψ, Q), is defined similarly with g(x, c, y) = y, ψ((m, n)0 (m0 , n0 )1 . . .) = nn0 . . . and, if y · n is defined, whence q(n, c) is defined and equal say to (m, c00 ), Q(n, (x, c, y)) = ((m, n)1 , (x · m, c00 , y · n)) Proposition 23 The data just described amount to a span of ae-lenses. Proof. We show that the ae-lens conditions are satisfied for the first proposed ae-lens (the left leg). First, since the action is defined on generators it is equivariant and so (K̂, MK̂ ) is a module. As constructed, f is a function, and φ, being defined on generators is a monoid homomorphism. Also, P is a partial stateful monoid homomorphism — this follows since p is a partial stateful monoid homomorphism. Now we check in turn each of the remaining conditions in Definition 22. i) (f, φ) is a module morphism since for k = (x, c, y) if k · (m, n) is defined (whether (m, n), a generator of the monoid MK̂ , is from the first or the second summand) then f (k)·φ(m, n) = f (k)·m = x·m (note that x·m being defined is one of the preconditions for the action of (m, n) on k to be defined). Furthermore, continuing with the assumption that k · (m, n) is defined, we know that its first component is x · m so f (k · (m, n)) = x · m = f (k) · m. ii) Suppose f (k) · m is defined then • P (m, k) is defined by construction • k · P (m, k)0 = k · (m, n)0 = (x, c, y) · (m, n)0 = (x · m, c0 , y · n) = P (m, k)1 (where c’ comes from p(m, c)) • φ(P (m, k)0 ) = φ((m, n)0 ) = m. Similar arguments apply for the other ae-lens involving g, ψ and Q. Construction 2: An e-lens from a span of ae-lenses. Suppose that κ = (f, φ, P ) : (K, MK ) / (X, MX ) and κ0 = (g, ψ, Q) : (K, MK ) / (Y, MY ) are ae-lenses from (K, MK ) to (X, MX ) and from (K, MK ) to (Y, MY ) respectively. We define an e-lens λ : (X, MX ) ↔ (Y, MY ) with λ = (K, p, q, R) as follows. Let R = {(f (k), k, g(k))|k ∈ K}. Let p(m, k) = (ψ(P (m, k)0 ), P (m, k)1 ) ∈ MY × K which is de- fined when P (m, k) is defined and it in turn is defined when f (k) · m is defined. Similarly let q(n, k) = (φ(Q(n, k)0 ), Q(n, k)1 ) ∈ MX × K, which is defined when g(k) · n is defined. Proposition 24 The data just described form an e-lens. Proof. We show first that p is a stateful monoid homomorphism. This follows since p respects the identity, that is p(1, k) = (ψ(P (1, k)0 ), P (1, k)1 ) = (ψ(1), k) = (1, k), and, as the following argument shows, p respects the multiplication ofMX . When f (k) · m is defined p(m, k) = (ψ(P (m, k)0 ), P (m, k)1 ) = (n, k 0 ) say. When f (k 0 )·m0 is defined p(m0 , k 0 ) = (ψ(P (m0 , k 0 )0 ), P (m0 , k 0 )1 ) = (n0 , k 00 ) say. If and only if both those definedness requirements are satisfied, f (k)·mm0 is defined. In that case p(mm0 , k) = (ψ(P (mm0 , k)0 ), P (mm0 , k)1 ) = (ψ(P (m, k)0 P (m0 , k 0 )0 ), k 00 ) = (ψ(P (m, k)0 )ψ(P (m0 , k 0 )0 ), k 00 ) = (nn0 , k 00 ). Similarly q is a stateful monoid homomorphism. Finally, we show that (K, p, q, R) satisfies the two requirements of Definition 10 and so is an e-lens. Suppose that r = (f (k), k, g(k)) ∈ R and that f (k) · m is defined, then p(m, k) = (ψ(P (m, k)0 ), P (m, k)1 ) = (n, k 0 ) is defined. Notice that f (k) · m = f (k 0 ) and g(k) · n = g(k) · ψ(P (m, k)0 ) = g(k · P (m, k)0 ) = g(k 0 ), so (f (k) · m, k 0 , g(k) · n) = (f (k 0 ), k 0 , g(k 0 )) ∈ R 11 as required. Furthermore, the corresponding argument works for q when g(k) · n is defined, and this completes the proof. 6 Conclusion We have developed precise inter-relationships between e-lenses, ae-lenses, d-lenses, sd-lenses (symmetric d-lenses), v-lenses (very well behaved set-based lenses) and sv-lenses (symmetric very well behaved set-based lenses). Along the way we have illustrated some uses of codiscrete categories and categories of elements, and we have demonstrated techniques using equivalence classes of spans of asymmetric lenses to obtain symmetric lenses, the analysis of partly trivial symmetric lenses to obtain a new definition of a type asymmetric lens, and explicit constructions that interlink aspects of formal definitions to provide interconversions. The explicit illustration of various techniques is intended to give the reader confidence that similar approaches to other variants of set-based, delta-based and edit-based lenses can be used to systematically inter-relate them. The work here seems applicable to systematising a very wide range of lenses. Although the status of monadic lenses [AC+16] seems beyond the current framework (and they may form a fourth class), a large proportion of lenses currently in use have been dealt with here. In our effort to illustrate techniques appropriate for Bx work we have restrained ourselves from presenting mathematics beyond that immediately required. Nevertheless, a few remarks here in the concluding section are in order. In the following paragraphs, each category of lenses has appropriate objects (sets, categories or modules) and has lenses between those objects as morphisms using lens composition to compose morphisms. The categories are named after their morphisms (the type of lenses that they contain). The relationship between v-lenses and d-lenses is very strong. Although we didn’t take the time in Section 2 to repeat the definitions of composition for each of v-lenses and d-lenses we have nevertheless constructed a functor vLens / dLens which uses the codiscrete category construction on objects and acts fully and faithfully on v-lenses. Since the codiscrete category construction is injective we see that vLens is simply a full subcategory of dLens. Of course, there are d-lenses which are not v-lenses, but every d-lens between codiscrete categories is a v-lens and vice versa (every v-lens is a d-lens between codiscrete categories). The most elegant category theoretic approach to relating sv-lenses and sd-lenses involves showing that the functor vLens / dLens not only preserves spans (as all functors do), but also preserves “pullbacks” (the inverted commas are used to remind us that the lenses constructed on the pullback of the gets [JR14] are not usually in fact pullbacks in the category of lenses, in this case in vLens). When “pullbacks” are preserved so is composition of spans and so we have a functor span(vLens) / span(dLens). Then the argument in the body of the paper that shows that equivalence is preserved by the functor tells us that we have an induced functor svLens / sdLens. As it happens this functor is full but not faithful: the interesting example at the end of [JR15] motivated a coarser equivalence relation among spans of d-lenses than the one used among spans of v-lenses in [JR14]. We now believe that the coarser equivalence relation is preferable in both cases, and it can be retrofitted to span(vLens) to obtain a category with fewer distinct sv-lenses called say svLens0 , and the functor svLens0 / sdLens is indeed full and faithful. Once again the object function is injective, and so once again we see that svLens0 is simply a full subcategory of sdLens. In summary, v-lenses, whether symmetric or asymmetric, are precisely d-lenses between codiscrete categories. Incidentally, this, like many of the results in this paper, carries across to a range of variants. For example, w- lenses (those that don’t necessarily satisfy the Put-Put law) can be related to a variant of d-lenses that themselves don’t necessarily satisfy the Put-Put law. However, the well-behavedness is necessary in the argument about the preservation of equivalences, so we are not making claims about non-well-behaved set-based lenses. The correspondence between e-lenses and sd-lenses is a little more delicate because the actions in an e-lens module need not be defined, and when defined the propagations have to act coherently for a given monoid element m and complement c. The latter means that we shouldn’t presume that the functor eLens / sdLens of Corollary 21 is full (since sd-lenses suffer no such coherency restriction). The former, undefinedness, comes up in a number of guises. In particular, because of undefinedness there are many different modules that correspond to the same category of elements, so the functor eLens / sdLens is not a subcategory inclusion. But perhaps most importantly we should say a few words about the definition of e-lens equivalence presented in Definition 11. In Definition 11 note particularly conditions (ii) and (iii). The two propagations p(m, c) and p0 (m, c0 ) will both be defined together when it matters (that is when xm is defined). But the conditions only apply when both are defined. This is intended to allow one of, for example p or p0 to be defined when the other is undefined 12 without putting any extra burden on the equivalence, and so the equivalence makes officially different lenses with the same behaviour where it matters (that differ only in the definedness of their partial stateful monoid homomorphisms) equivalent. Also in Definition 11 the totality on both sides requirement, along with condition (i), implies that an e-lens in which every complement occurs as part of some triple in K and an e-lens which is identical except for having one or more complements which take part in no consistent triples in K are inequivalent. Thus the functor eLens / sdLens of Corollary 21 is not faithful. In on-going work we are exploring variations on Definition 11, and more general questions about the relationship between complements and consistency relations. The definition of asymmetric edit lenses, and the constructions of spans of asymmetric edit lenses from edit lenses and vice versa, are our most recent developments. In on-going work we are exploring the detailed properties satisfied by those constructions and the potential further applications of asymmetric edit lenses. 7 Acknowledgements The authors are grateful for the support of the Australian Research Council, the Canadian National Science and Engineering Research Council and the Centre of Australian Category Theory. References [AC+16] Abou-Saleh, F., Cheney, J., Gibbons, J., McKinna, J. and Stevens, P. (2016) Reflections on monadic lenses. WadlerFest festschrift, to appear. [DXC11] Zinovy Diskin, Yingfei Xiong, Krzysztof Czarnecki (2011), From State- to Delta-Based Bidirectional Model Transformations: the Asymmetric Case. Journal of Object Technology 10, 6:1–25, [DX+11] Zinovy Diskin, Yingfei Xiong, Krzysztof Czarnecki, Hartmut Ehrig, Frank Hermann and Francesco Orejas (2011), From State- to Delta-Based Bidirectional Model Transformations: the Symmetric Case. ACM/IEEE 14th International Conference on Model Driven Engineering Languages and Systems, Springer. [HPW11] Hofmann, M., Pierce, B., and Wagner, D. (2011) Symmetric Lenses. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Austin, Texas. [HPW12] Hofmann, M., Pierce, B., and Wagner, D. (2012) Edit Lenses. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 495–508. [JR14] Johnson, M. and Rosebrugh, R. (2014) Spans of lenses. CEUR Proceedings, vol 1133, 112–118. [JR15] Johnson, M. and Rosebrugh, R. (2015) Spans of delta lenses. CEUR Proceedings, vol 1396, 1–15. [JRW10] Johnson, M., Rosebrugh, R. and Wood, R. J. (2010) Algebras and Update Strategies. J.UCS 16, 729–748. [PS03] Pierce, B. and Schmitt, A. (2003) Lenses and view update translation. Preprint. [Wag14] Wagner, D. (2014) Edit Lenses. Ph.D Thesis, University of Pennsylvania. 13