There are many di erent 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 sending sets to codiscrete categories; that symmetric set-based lenses can similarly be seen as symmetric delta-based lenses; that symmetric editbased 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 uni cation with concrete inter-conversions developed among the three main approaches to lenses in both their symmetric and asymmetric forms.
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 speci c types of lenses from each of the three classes, so we have tried to present the development of the relationships in a su ciently 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 di erent 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 speci c instance that we are working with, which in this case is called an e-lens and is de ned 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 setbased 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 de ned there are some delicacies and edit lenses do not merely form a subcategory of (fully de ned) 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 de ne 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 de nition 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 ner points of the choices made. We hope that this synthesis of di erent classes of lenses will go some way towards systematising the wide body of Bx theory that uses lenses. 2
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 di erent 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 rst 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 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.
Proof. Given a function f : X / Y , we de ne a functor f : X / Y as follows. On objects f is de ned by f . If x and x0 are elements of X and : x / x0 is the unique arrow of X from x to x0 then f ( ) is the unique arrow from f (x) to f (x0). 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 e ect on objects de nes a function f : X / Y .
We leave to the reader the straightforward veri cation 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 de nition 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 rst 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.
Y / X (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
(iii) (PutPut) composing Puts does not depend on the rst 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; y0 in Y : (i) g(p(x; y)) = y (ii) p(x; g(x)) = x (iii) p(p(x; y); y0) = p(x; y0)
We remind the reader of the de nition of (asymmetric) d-lens from, for example, [JR15] and [DXC11]. Write as usual jCj for the set of objects of a category C and jX2j = 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.
X /Y is a functor (the \Get") and P : jG=Yj /jX2j is a function (the \Put") and the data for : G(X) /Y and : G(X0) / Y 0 satisfy: (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 X0 is the codomain of P (X; ), and hence G(X0) = Y , then P (X; ) = P (X0; )P (X; )
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 corresponding to g. We need to de ne p. The domain of p is the set of objects jg=Yj. 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 . De ne 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 . De ne 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 veri cation 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 de nitions 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 de ned 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:
Proof. The proof is conceptually straightforward, so we need not rehearse all the details of the de nitions of the equivalences from earlier papers. It su ces 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 / S0 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 su ces 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
Ho man, 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 [HPW11] and symmetric delta-lenses (which we also call fb-lenses) [JR15]. There is an extensive discussion of the di erences between edit lenses and symmetric (set-based) lenses in the excellent thesis of Wagner [Wag14].
We rst review the de nitions. For consistency with our presentation of asymmetric set and d-lenses, we write the actions of modules (or partial M -sets) on the right.
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 de ned then the other side is also de ned and of course the resulting values on both sides are the same. In particular, the rst point implies that the action of the identity monoid element on any element of X is always de ned.
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 de nition is not present in [HPW12], but it provides the obvious way to compare modules.
is a function and : MX / MY is a monoid homomorphism, and for all x in X and m in MX they satisfy: /Y or, equivalently, the following diagram commutes: f (x m) = f (x)
(m) X f Y
MX MY / X / Y f
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) = f(x; m) j x m = x0g 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 de ned by (x0; m0)(x; m) = (x; mm0).
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 ) de nes 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-de ned 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 de ned, 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 ).
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:
Note immediately that this de nition di ers from the de nition in [HPW12] where stateful homomorphisms are required to be total functions. Nevertheless, our de nitions of edit lenses require that the stateful homomorphisms involved must be de ned whenever needed. Thus despite this variation there is a perfect correspondence between our edit lenses and those of [HPW12].
The rst 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: 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 de nition 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 homomorphism 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 e ect of the action starting from a consistent triple arrives at a consistent triple (see the diagram following the de nition). Formally: De nition 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) 2 K and xm de ned implies p(m; c) = (n; c0) (say) de ned, yn de ned and (xm; c0; yn) 2 K (2) (x; c; y) 2 K and yn de ned implies q(n; c) = (m; c0) (say) de ned, xm de ned and (xm; c0; yn) 2 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: 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) m m0 n n0 m x x0 c c0 y y0
n provides an edit n which necessarily acts on y giving y0 say, and a witness c0 to the synchronization of x0 = xm and y0 = yn. Similarly if the edit n is applied to y giving y0 then q(n; c) provides an edit m and a witness c0 to the synchronization of yn and xm. 4
We begin by de ning 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 C0 is called total on both sides when for any c 2 C there is some c0 2 C0 with c c0, and conversely for any c0 2 C0 there is some c 2 C with c c0.
De nition 11 Let = (C; p; q; K) and 0 = (C0; p0; q0; K0) be e-lenses from (X; MX ) to (Y; MY ). We say e 0 if there is a total on both sides relation C C0 satisfying whenever c c0: (i) (x; c; y) in K if and only if (x; c0; y) in K0 (ii) if p(m; c) = (n; d) and p0(m; c0) = (n0; d0) are both de ned then n = n0 and d d0 (iii) if q(n; c) = (m; d) and q0(n; c0) = (m0; d0) are both de ned then m = m0 and d d0 Proposition 12 The relation
e is an equivalence relation.
Proof. Re exivity of
e is clear. Conditions (i), (ii) and (iii) are also clearly symmetric and transitive.
Next we de ne a composite of e-lenses.
De nition 13 Let = (C; p; q; K) and = (C0; p0; q0; K0) be e-lenses from (X; MX ) to (Y; MY ) and (Y; MY ) to (Z; MZ ) respectively. We de ne = (D; r; s; M ) as follows: (i) D = C C0 (ii) r(m; (c; c0)) = (`; (c1; c01)) where p(m; c) = (n; c1) and p0(n; c0) = (`; c01). The function s is de ned similarly, but using q and q0. (iii) M = f(x; (c; c0); z) j 9y 2 Y with (x; c; y) 2 K and (y; c0; z) 2 K0g 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 C0) 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 De nition 10.
We show rst 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: 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 rst that (x; (c; c0); z) 2 M and r(m; (c; c0)) = (`; (c1; c01) implies (xm; (c1; c01); z`) 2 M . Consideration of the diagram m m0 c c1 c2 m x x0 c c1 n n0 c0 z z0 ` shows why this is the case. Similar considerations apply to s.
e. In other words, e is a congruence.
Proof.
Suppose that = (C; p; q; K) and 0 = (C0; p0; q0; K0) are e-lenses from (X; MX ) to (Y; MY ), that e 0 via
C C0, and that = (C00; p00; q00; K00) is an e-lens from (Y; MY ) to (Z; MZ ). We will show that e 0.
Now with the notation above = (C C00; r; s; M ) and 0 = (C0 C00; r0; s0; M 0). We need to de ne 0 (C C00) (C0 C00). We set
0 = f((c; c00); (c0; c00)) j (c; c0) 2 g We demonstrate that 0 witnesses e 0.
First, 0 is total on both sides since is: for any c 2 C there is a c0 2 C0 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 satis es conditions (i){(iii) in De nition 11. Throughout we suppose that (c; c00) 0(c0; c00) and hence that c c0.
Now (x; (c; c00); z) 2 M if and only if there is a y with (x; c; y) 2 K and (y; c00; z) 2 K00. Since c c0, this is exactly the same as (x; c0; y) 2 K0 and (y; c00; z) 2 K00 (using condition (i) for ) and this in turn is equivalent to (x; (c0; c00); z) 2 M 0. So, condition (i) is satis ed 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 de ned. We are required to show that ` = `0 and (d; d00) 0(d0; d000). Now referring to the formulas for r and r0 from De nition 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 2 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 q0.
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.
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 de nition of symmetric delta lens, often called an fb-lens (named after its basic operations which are known as \forwards" and \backwards"). We revisit the de nition from [JR15], which in turn is based on [DX+11]. De nition 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).
X : jXj o
RXY / jYj : 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) b : Arr(Y) jXj RXY jYj RXY / Arr(Y) / Arr(X) jYj RXY jXj RXY where the pullbacks (also known as bered 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) and and f(x; r) = (y; r0) and f(x0; r0) = (y0; r00) imply f(x0x; r) = (y0y; r00) b(y; r) = (x; r0) and b(y0; r0) = (x0; r00) imply b(y0y; r) = (x0x; 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 de ne a span of sets X : jXj o K / jYj : Y.
We need to de ne the forward and backward propagations for L . Suppose xm = x0 and (x; c; y) in K. De ne f((x; m); (x; c; y)) = ((y; n); (x0; c0; y0)) where p(m; c) = (n; c0) and yn = y0. Note that since is an e-lens, the conditions for on p and K guarantee that (x0; c0; y0) in K. The de nition of backward propagation is similar: b((y; n); (x; c; y)) = ((x; m); (x0; c0; y0)) 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:
We also review the equivalence of fb-lenses from [JR15].
De nition 19 Let L = ( X; Y; f; b) and L0 = ( X0; Y0; f0; b0) be two fb-lenses from X to Y with corrs RXY and RX0Y respectively. We say L fb L0 if and only if there is a relation from RXY to RX0Y with the following properties:
is compatible with the 's, i.e. r r0 implies Xr = X0r0 and Yr = Y0r0 is total in both directions, i.e. for all r in RXY, there is an r0 in RX0Y with r r0 and conversely.
equal and the second components are related, i.e. 0f(x; r) = 0f0(x; r0) and 1f(x; r) 1f0(x; r0).
0b(y; r) = 0b0(y; r0) and 1b(y; r) 1b0(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 = (C0; p0; q0; K0) are equivalent e-lenses from (X; MX ) to (Y; MY ) via
C C0. We want to show that L fb L 0 . For compactness, we will write consistent triples as strings without parentheses or commas.
Let = f(xcy; xc0y) j c c0 and xcy 2 Kg. Note that (xcy; xc0y) 2 implies xc0y 2 K0, so K K0 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 K0 and the s are projections, condition 1 in De nition 19 is immediately satis ed: (xcy) (x0c0y0) implies x = x0 and y = y0 so X(xcy) = X0(x0c0y0) and Y(xcy) = Y0(x0c0y0).
Condition 2 follows immediately from being total on both sides.
For conditions 3 and 4, suppose that (xcy) (xc0y) and xm is an arrow of XM with p(m; c) = (n; d) and p0(m; c0) = (n; d0). The rst component of both f(xm; xcy) and f0(xm; xc0y) is yn, and their second components are the -related x0dy0 and x0d0y0 demonstrating that condition 3 is satis ed. Condition 4 follows similarly.
Since
fb classes are arrows of the category sdLens (as we proved in [JR15]) we get a functor:
/ 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.
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 di erent 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 rst 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 e ciently 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 rst (respectively the second) injection.
De nition 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 De nition 9, composition and identity) satisfying: i) (f; ) is a morphism of modules (that is for k in K, ` in MK , if k ` is de ned, then f (k) and is equal to f (k `)) (`) is de ned ii) (PutGet) If f (k) m is de ned then { P (m; k) is de ned { 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 rst 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^ ) de ned 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 de ned by de ning 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 de ned if and only if 1. x0 = x m is de ned, whence p(m; c) is de ned 2. p(m; c) = (n; c0) (notice the n comes from the generator and it follows that y n = y0, say, is de ned) and then we de ne k (m; n)0 = (x0; c0; y0), which is an element of K^ .
Similarly for a generator (m; n)1 in MK^ , the action k (m; n)1 is de ned if and only if q(n; c) = (m; c00) for some c00 and y0 = y n is de ned (and hence x0 = x m is de ned), whence we de ne k (m; n)1 = (x0; c00; y0).
Now we de ne 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 nite of course), and, if x m is de ned, whence p(m; c) is de ned and equal say to (n; c0),
P (m; (x; c; y)) = ((m; n)0; (x m; c0; y n)) If x m is not de ned, then P (m; (x; c; y)) is not de ned.
The ae-lens just de ned 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 de ned similarly with g(x; c; y) = y, ((m; n)0(m0; n0)1 : : :) = nn0 : : : and, if y n is de ned, whence q(n; c) is de ned and equal say to (m; c00),
Q(n; (x; c; y)) = ((m; n)1; (x m; c00; y n))
Proof. We show that the ae-lens conditions are satis ed for the rst proposed ae-lens (the left leg).
First, since the action is de ned on generators it is equivariant and so (K^ ; MK^ ) is a module. As constructed, f is a function, and , being de ned 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 De nition 22. i) (f; ) is a module morphism since for k = (x; c; y) if k (m; n) is de ned (whether (m; n), a generator of the monoid MK^ , is from the rst or the second summand) then f (k) (m; n) = f (k) m = x m (note that x m being de ned is one of the preconditions for the action of (m; n) on k to be de ned). Furthermore, continuing with the assumption that k (m; n) is de ned, we know that its rst component is x m so f (k (m; n)) = x m = f (k) m. ii) Suppose f (k) m is de ned then 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) is de ned by construction
(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 de ne an e-lens : (X; MX ) $ (Y; MY ) with = (K; p; q; R) as follows.
Let R = f(f (k); k; g(k))jk 2 Kg. Let p(m; k) = ( (P (m; k)0); P (m; k)1) 2 MY K which is dened when P (m; k) is de ned and it in turn is de ned when f (k) m is de ned. Similarly let q(n; k) = ( (Q(n; k)0); Q(n; k)1) 2 MX K, which is de ned when g(k) n is de ned.
Proof. We show rst 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 de ned p(m; k) = ( (P (m; k)0); P (m; k)1) = (n; k0) say. When f (k0) m0 is de ned p(m0; k0) = ( (P (m0; k0)0); P (m0; k0)1) = (n0; k00) say. If and only if both those de nedness requirements are satis ed, f (k) mm0 is de ned. In that case p(mm0; k) = ( (P (mm0; k)0); P (mm0; k)1) = ( (P (m; k)0P (m0; k0)0); k00) = ( (P (m; k)0) (P (m0; k0)0); k00) = (nn0; k00).
Similarly q is a stateful monoid homomorphism.
Finally, we show that (K; p; q; R) satis es the two requirements of De nition 10 and so is an e-lens.
Suppose that r = (f (k); k; g(k)) 2 R and that f (k) m is de ned, then p(m; k) = ( (P (m; k)0); P (m; k)1) = (n; k0) is de ned. Notice that f (k) m = f (k0) and g(k) n = g(k) (P (m; k)0) = g(k P (m; k)0) = g(k0), so (f (k) m; k0; g(k) n) = (f (k0); k0; g(k0)) 2 R as required. Furthermore, the corresponding argument works for q when g(k) n is de ned, and this completes the proof. 6
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 de nition of a type asymmetric lens, and explicit constructions that interlink aspects of formal de nitions to provide interconversions.
The explicit illustration of various techniques is intended to give the reader con dence 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 e ort 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 de nitions 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 retro tted 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, wlenses (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 de ned, and when de ned 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 su er no such coherency restriction). The former, unde nedness, comes up in a number of guises. In particular, because of unde nedness there are many di erent 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 de nition of e-lens equivalence presented in De nition 11.
In De nition 11 note particularly conditions (ii) and (iii). The two propagations p(m; c) and p0(m; c0) will both be de ned together when it matters (that is when xm is de ned). But the conditions only apply when both are de ned. This is intended to allow one of, for example p or p0 to be de ned when the other is unde ned without putting any extra burden on the equivalence, and so the equivalence makes o cially di erent lenses with the same behaviour where it matters (that di er only in the de nedness of their partial stateful monoid homomorphisms) equivalent.
Also in De nition 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 De nition 11, and more general questions about the relationship between complements and consistency relations.
The de nition 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 satis ed by those constructions and the potential further applications of asymmetric edit lenses. 7
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. [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.