Asymmetric c-lenses are the special cases of asymmetric d-lenses (also called delta lenses) whose updates satisfy a universal property which in many applications ensures \least-change". There has therefore been hope that symmetric c-lenses might characterize those symmetric dlenses which satisfy a similar universal property. This paper begins an analysis of symmetric c-lenses and their relationship to symmetric dlenses and explains why the authors do not expect symmetric c-lenses, that is, equivalence classes of spans of c-lenses, to be central to developing universal properties for symmetric lenses. Instead, we consider cospans of c-lenses and show that they generate symmetric c-lenses with an appropriate universal property. That property is further analysed and used to motivate proposed generalisations to obtain universal, least-change, properties for symmetric d-lenses. In addition we explore how to characterise the symmetric d-lenses that arise from cospans of c-lenses among all symmetric d-lenses.
Introduction Bidirectional transformations maintain consistency between two di erent data sources.
Over the last several years there has been a signi cant exploration of bidirectional transformations and
possible least-change properties, see [
One proposal for least-change asymmetric lenses has been c-lenses [
Of course, many applications of bidirectional transformations depend upon using symmetric lenses [
Recall that in an asymmetric lens one data source, the slave data source, can be completely reconstructed from the other data source, the master data source. Thus the only interesting updates arise when a change is made to the slave data source and the master data source needs to be updated to restore consistency. That update is the one called the Put, and as we've noted, c-lenses provide a universal update | an update that satis es the universal condition outlined above and presented in more detail in Section 2.
In a symmetric lens, when a change is made to one of the data sources we seek a corresponding update to the other data source to restore consistency. In non-trivial symmetric cases, neither data source is derivable from the other, and a change in either data source requires an update of the other data source to restore consistency. Usually, there will be many possible choices for such updates. It is natural to ask what universal conditions we might put on these symmetric lens updates. How do we make a \best" choice?
The authors have carried out detailed studies on the relationships between various kinds of asymmetric lenses
and the corresponding kinds of symmetric lenses [
When asked, we've suspected that, and correspondingly reported in lectures our suspicion that, symmetric c-lenses do not in fact provide universal updates. The source of the di culty is that in a span of c-lenses the master data source for both c-lenses is the peak (also called the head) of the span. The reason symmetric lenses are equivalence classes of spans of corresponding asymmetric lenses is because the actual nature of the peak of the span is unimportant for the symmetric lens | the peak must be able to accommodate enough information that it can mediate the update in both directions, but peaks that could accommodate more information while formally di erent may, with appropriately similar asymmetric lenses, amount to the same symmetric lens. As long as the updates mediated through the peak are the same, the symmetric lenses are the same, even if the peaks are di erent.
Now the reader will see why we've suspected that c-lenses do not provide universal updates for symmetric lenses: because the universal properties occur in the peak of the span, and what happens in the peak of the span is unimportant except in as much as it must have the power to mediate the updates between the data sources, it seems likely that symmetric c-lenses are not particularly special among symmetric d-lenses.
In Section 3 we look in more detail at the relationship between c-lenses and d-lenses. We show that every d-lens has, as we would expect, a free presentation | it is a \quotient" of a \free" d-lens. But more, the \free" d-lenses are in fact c-lenses. We also see how we can, in some cases, use this to prove that a given span of d-lenses is equivalent to some span of c-lenses. We remain unsure as to whether there are spans of d-lenses that are not equivalent to any span of c-lenses.
Interestingly, cospans play a crucial role in the argument in Section 3. In Section 4 we give an explicit construction of a symmetric delta lens from a cospan of d-lenses. Former work has focused on spans rather than cospans. As Section 5 shows, taking the cospan approach has implications for universal updates: A cospan of c-lenses does, unlike the span case, generate a symmetric d-lens whose updates automatically satisfy a universal property. This addresses in part the title of this paper, and calls out for further generalisation.
So, what about more general symmetric delta lenses (those that don't arise from cospans of c-lenses)? What would it mean to ask for their updates to be universal, whether they corresponded to cospans of d-lenses that aren't c-lenses, or indeed were just an arbitrary symmetric delta lens? Motivated by the cospan of c-lenses case, we explore in Section 6 what extra structure might be required to talk about universality, and then in the following section we look at how that extra structure interacts with our attempt to characterize those symmetric lenses which do correspond to cospans of asymmetric lenses. Section 7 begins the analysis of symmetric lenses which arise from cospans, providing a necessary condition which suggests that symmetric lenses which can be represented by cospans are relatively uncommon.
We end this introduction with a quick remark about state spaces which will hopefully limit possible confusion. On one level of analysis, bidirectional transformations are frequently between systems whose state spaces have the property that every state can be updated in at least one way to every other state. In the authors' opinions, this kind of representation can obscure important information. Instead, we prefer, whenever possible, to have state spaces whose arrows have semantic relevance. For example, an arrow might indicate an increase in the information order (so in a database example, an arrow would indicate an insert | more information is provided by the state at the target of the arrow than was provided by the state at the source of the arrow). It will be easier for readers to think of state spaces like the information order state space just described when trying to understand least-change updates and proposed universal updates for symmetric lenses.
Of course, none of this denies that there are updates which take place along reductions in the information
order (deletions in the case of databases). These updates can be analysed in the op-state space, or equivalently,
using notation from Section 2, using the monad L rather than the monad R. And nally, again of course, there
are mixed updates. The machinery for dealing all at once with updates along a chosen order like the information
order, updates along the reversed order, and mixes of the two, was presented in [
Background and notation: d-lenses and c-lenses In this section we introduce notation and review some material from earlier work. Much of this section, and the next section, assumes some knowledge of relatively sophisticated category theory including monads and brations. Readers with less background in those areas might like to read the notational conventions presented in the next paragraph and then skip to Section 4. The remainder of the paper, beginning there, is intended to be comprehensible for readers with a background in lenses and basic category theory.
We assume the reader is familiar with basic notions of category theory as found, for example, in [
The following notion is standard but we review it to set our notation and remind the reader. For functors G / V o H S T with common codomain V, their \comma category" is denoted (G; H). Its objects are triples (S; T; a) where S and T are objects of S and T, and a : G(S) / H(T ) is a morphism of V. A morphism from (S; T; a) to (S0; T 0; a0) is two morphisms S / S0 and T / T 0 making the obvious square in V commute. The comma category has projection functors to S and T and a transformation denoted as follows: (G; H)
! Where possible we suppress subscripts on projections. Note that (S;T;a) is just a. When H = 1V the objects of (G; 1V) are formally pairs (S; ) with S an object of S and : GS / V an arrow of V (whose codomain is arbitrary). An arrow (S; ) / (S0; 0) where 0 : GS0 / V 0 is a pair ( ; ') where : S / S0; ' : V / V 0 and they satisfy ' = 0G( ).
We now recall the de nition of an asymmetric delta lens ([
The comma category (G; H) has a universal property that we use to establish some further notation needed below. Explicitly, given a triple consisting of two functors and a natural transformation (K : X / S; L : X / T; ' : GK / HL), there is a unique F : X / (G; H) (satisfying certain properties). When H = 1V we can de ne the functor G corresponding to the triple (1S; G; 1G). We can also iterate the comma category construction and its projections, as in the right hand diagram: 1S
S
G
G (G; 1V)
! (G; 1V) (RG; 1V) LRvlGl1lVll
!
Then we can de ne the functor corresponding to the triple (LG1V LRG1V; RRG; ( LRG1V)), and we denote it
G:
LG1VLRG1V
RRG (RG; 1V)
G (G; 1V)
!
The assignment G 7! RG de nes (on objects) the functor part of a monad R on cat=V. The G and G just de ned are the unit and multiplication of the monad at an object G. Similarly, H 7! LH = L1V H : (1V; H) /V de nes a monad L on cat=V.
The following is the original de nition of c-lens. It amounts to an algebra for the monad R. As such, it
connects to a large body of work on op brations. The formulation of a (split) op bration as an algebra for the
monad R was rst achieved by Street in [29]. Algebras for L are the split brations. The recognition that lenses
are algebras for monads (or in some cases for \semi-monads"), thus ultimately connecting back to Street's work,
appeared in [
G / V and (G; 1V)
P / S are functors i) c-PutGet: GP = RG ii) c-GetPut: P G = 1S iii) c-PutPut: P G = P (P; 1V) or equivalently but diagrammatically, the following commute:
G S GGGGGG 1S GGGGGG# S / (G; 1V)
GGG P
GGGRG
GGGGG#/ V G (RG; 1V)
G (G; 1V) (P;1V)
P / (G; 1V)
P / S
We recall from [
We now turn to spans of d-lenses. Such spans represent symmetric d-lenses, but, as noted in Section 1, di erent spans may represent the same symmetric d-lens. The equivalence that we need on spans of d-lenses is generated by functors satisfying the following conditions.
X jtVhhV((hVGGhV0LLhV;;hVPPhVLL0hV))hVhVhVhV SS0 hVhVhVhV((hVGGhVR0RhVh;V;PPhVRR0hV))hVVh4* Y the top and bottom spans are spans of d-lenses and is said to satisfy conditions (E) if: (1) GL = G0L and GR = G0R, (2)
is surjective on objects, and (3) whenever S0 = S, we have both
PL(S; GLS / X) =
P L0(S0; G0LS0 / X) and
PR(S; GRS / Y ) =
P R0(S0; G0RS0 / Y ):
by functors satisfying conditions (E). 3
Symmetric d-lenses and symmetric c-lenses We turn now to a further study of functors like and an initial exploration of when spans of d-lenses might be
Sp-equivalent to spans of c-lenses. We present some useful results, but further study will be required to fully answer the question, raised in the introduction, of just how special are symmetric c-lenses among symmetric d-lenses.
Let S G / V be a functor. We write (Gi; 1V) for the subcategory of (G; 1V) with the same objects as (G; 1V) but whose morphisms from say (S; : GS / V ) to (T; 0 : GT / V 0) require that S = T and are (rather than commutative squares as they are in the full comma category) commutative triangles of the form: V
GS77777770 / V 0 so that necessarily 0 = . Composition is by juxtaposition of triangles. In what follows, we will sometimes refer to morphisms of this form as the triangular morphisms. We remark that if we write Si for the (discrete) category with the same objects as S and only identity arrows, and Gi for the composite of G with the inclusion of Si in S, then (Gi; 1V) is actually the comma category which the notation suggests. We write RGi : (Gi; 1V) / V for the functor whose value on an object (S; : GS / V ) is the object V , and whose value on an arrow : (S; ) / (S; 0) as above is just : V / V 0. It is easy to see that, RGi is functorial. Once again, this notation is consistent with that of the previous section.
(G;P )
Suppose further that S / V is a d-lens. We next de ne a functor : (Gi; 1V) / S. On an object (S; : GS / V ) of (Gi; 1V) de ne (S; ) to be the codomain, d1P (S; ) = T say, of P (S; ) : S / T . Suppose (S; 0 : GS / T 0) is another object and : (S; ) / (S; 0) is an arrow in (Gi; 1V), so 0 = . Notice that, since GP (S; ) = , we have GT = V . Moreover, (S; 0 : GS / V 0) = d1P (S; 0) = T 0 say, so that GT 0 = V 0. We de ne on a morphism as above by ( : (S; ) / (S; 0)) = P (T; ). This is meaningful since (G; P ) is a d-lens so that P (S; 0) = P (S; ) = P (T; )P (S; ). Thus the domain of ( ) is the codomain of P (S; ) which is (S; ) while the codomain of ( ) is the codomain of P (S; 0) which is (S; 0). That is functorial now also follows from a similar argument.
There is a \one-sided" version of the conditions (E) of De nition 3: De nition 5 Suppose that in the diagram both (G; P ) and (G0; P 0) are d-lenses and is a functor. Then is said to satisfy conditions (E1) if: (1) G
= G0, (2)
SS0 gWgWgWgW((gGGWgW0;PgPWgW0))gWWg+3 V (GiS;1jVj)jjT(jTGjTR;jTPjGT)jTiTj*4 V
= RGi and RGi is a c-lens. Moreover satis es conditions (E1).
Proof. First, from the description of on an object : GS / V above, it is immediate that G (S; ) = V = RGi(S; ). Similarly, on an arrow , we have G ( ) = GP ( ) = = RGi( ).
Next we show that RGi is a c-lens, that is a split op- bration. Thus, for an object (S; : GS / V ) of (Gi; 1V) and an arrow : RGi(S; ) / V 0 of V, we need to provide an op-cartesian arrow in (Gi; 1V). But RGi(S; ) = V , so we have : V /V 0 in V. For the op-cartesian arrow in (Gi; 1V) we take : (S; ) /(S; ). For use below, the Put for the d-lens structure on RGi will be denoted P 0 and we have just de ned P 0((S; ); ) = : (S; ) / (S; ) To see that this de nition works, suppose further that : (S; ) / (S; 00 : GS / V 00) is an arrow of (Gi; 1V) such that = RGi( ) factors as = 0 in V (and refer to the diagram below). The required arrow of (Gi; 1V) from (S; ) / (S; 00) is 0, which is indeed an arrow since 00 = = 0( ). It is unique in making the upper triangle below commute since RGi( 0) = 0.
(Gi; 1V) RGi
V (S; )
RRRRRR( (S; ) lllll0l6
/ (S; 00)
Finally, we show that satis es conditions (E1). We already have that G = RGi. To see that is surjective on objects we note that for any object S in S, we have S = d11S = d1P (S; 1GS) = (S; 1GS). Next, suppose that for (S; ) in (Gi; 1V), we have (S; ) = T (= d1P (S; )). We need to show that P (T; : GT / V 0) =
P 0((S; ); : Gi(S; ) / V 0). Now as noted in the previous paragraph, P 0((S; ); : Gi(S; ) / V 0) is the arrow : (S; ) / (S; ) in (Gi; 1V), and of it was de ned to be P (T; ). This completes the proof.
It may be worth remarking that the conditions (E1) on are, as noted in [
In fact, in a sense that we won't explore in full here because of space limitations, may be seen as the free presentation of the algebra (G; P ).
In brief: recall that for any monad (T; m; ) the free algebra on A is mA : T T A / T A. Thus the free c-lens
on G is G : RRG / RG. It turns out that the image of G includes only triangular morphisms (in other words,
all the opcartesian morphisms for the free c-lens are triangular). So G restricts to iG : RiRiG / RiG, where
Ri is, as above, the semi-monad that takes G to RiG = RGi. Furthermore, the \free" d-lens (inverted commas
because we are now in the semi-monad case) might be de ned as iG : RiRiG / RiG. It is a d-lens since G,
and therefore iG, satisfy the extra \identity" condition from [
It is interesting to note that the \free" d-lens is in fact a c-lens. Furthermore, presents the d-lens as a surjective on objects homomorphic image of a free c-lens.
In unpublished work we have explored lens structures on because, referring to the diagram below in which the diamond is a pullback of functors, when the L and R are c-lenses, the pullback projections of L and R would be c-lenses, the composites of c-lenses are c-lenses, so the top would be a span of c-lenses, and since the pullbacks and composites of functors satisfying (E1) satisfy (E1), the middle diamond would show that the upper span of c-lenses is Sp-equivalent to the lower span of d-lenses. Of course need not have a c-lens, or indeed d-lens, structure because we can construct examples where is not surjective on arrows while it is surjective on objects. It remains important to explore when spans of d-lenses are Sp-equivalent to spans of c-lenses..
V ozttt
ztttt0Rtttttt T JJJJJJJ0LJJJ$ (GiL; 1) (GiR; 1) RGtiLtttttt JJJJJJJLJJJ$ S zttttRtttttt JJJJJRJJGJiJRJ$/ W (GL;PL)
As it happens, a weaker condition than c-lens structures on the cospan ( L; R) will su ce to nd an
Spequivalent span of c-lenses for a given span of d-lenses. The cospan might be a half-duplex interoperability
cospan [
In the remainder of this paper we turn to a detailed, but in category theoretic requirements more elementary, study of cospans of lenses and the implications that they have for universal updates for symmetric lenses. 4
Symmetric delta lenses and cospans of d-lenses In symmetric lenses the two data sources are in some sense peers. Neither can generally be used to reconstruct the other, and the two operations are no longer called Put and Get (with the implication that the Get operation is straightforward while the Put operation needs to deal with the complications of many possible choices), and so they are typically given more neutral names like Left and Right or Forwards and Backwards.
So far we have looked at symmetric lenses via equivalence classes of spans of asymmetric lenses. This has been appropriate because in the absence of a direct de nition of symmetric c-lenses, we can still study them via the \symmetrising" span construction applied to asymmetric c-lenses.
We turn now to a deeper study of symmetric d-lenses and revert to a more traditional de nition that highlights
the two operations. The symmetric lenses that we will use are called fb-lenses (the f and b standing for Forwards
and Backwards). They are based upon the symmetric delta lenses of Diskin et al [
De nition 7 [
X : jXj o
R / jYj : Y An element r of R is called a corr. For r in R, if X(r) = X; Y(r) = Y the corr is denoted r : X $ Y , or sometimes even just r : X Y . The data f and b are operations called forward and backward propagation: f : Arr(X) b : Arr(Y) jXj R jYj R / Arr(Y) / Arr(X) jYj R jXj R where the pullbacks ensure that if f(x; r) = (y; r0), we have d0(x) = X(r), d1(y) = Y(r0) and similarly for b. We also require that d0(y) = Y(r) and X(r0) = d1(x), and the similar equations for b.
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) 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) If f(x; r) = (y; r0) and b(y0; r) = (x0; r00), we display instances of the propagation operations as: The main purpose of this section is to present the following construction of an fb lens from a cospan of d-lenses.
De ne ( X; Y; f; b) : X
! Y by Let the set of corrs be f(X; Y ) j GLX = GRY = V g (in diagrams we will often label the corr (X; Y ) with the corresponding object V )
r f X x
PR(Y;GL( )) where Y 0 = d1PR(Y; GL( )) and since GR(PR(Y; GL( ))) = GL( ) we set V 0 = d1GL( ).
It is easy to see that the fb-lens just constructed is the one which, under the equivalence between fb-lenses
and spans of d-lenses [
Notice that, in Construction 8, because GL and GR de ne a cospan of object functions, there is at most one
corr for given X and Y . That corr, when it exists, is determined by the object V of V which both X and Y map
to. As before, in diagrams we will usually label a corr (X; Y ) by V = GLX = GRY . In a sense, V \witnesses"
the consistency relationship between X and Y [
A cospan similarly provides a relationship between the arrows of X and the arrows of Y, and that relationship on arrows is consistent with the corrs. We will see in the next section that that relationship, ignored until now, is an important ingredient in specifying universal updates for symmetric lenses. 5
Universality and cospans of c-lenses We begin with a de nition.
X (GL;PL)
(GR;PR) / V o
Y arrows of X and
of Y are called compatible if GL( ) = GR( ).
Next, if the lenses in the cospan, (GL; PL) and (GR; PR), are not just d-lenses but in fact c-lenses, then there is a universal property for the corresponding forward propagation f constructed in the previous section.
Suppose given : X / X0 and V representing the corr (X; Y ). Recall that f( ; (X; Y )) has two components, an arrow of Y and a corr relating X0 and the codomain of the arrow of Y so as to form the square shown (in which the new corr has been left unlabelled).
We distinguish the two components of f( ; (X; Y )) by subscripting with 0 for the rst component (as shown on the right hand side of the square above) and 1 for the second component. Recall that we write d0 and d1 for the operations which give the domain and codomain of an arrow (thus for example d0 = X).
Now we state the universal property satis ed by f( ; (X; Y )).
= 0f( ; (X; Y ))0 and GR( 0) = 1GLX0 .
V X0 G
GGGGG
Y Proof. The proof is a routine application of the universal property of the c-lens (GR; PR): Since GL( ) is an arrow of V with domain V = GRY we can use the c-lens Put to calculate PR(Y; GL( )). But by Construction 8 the value of that Put is precisely the rst component of f( ; (X; Y )) so the latter has the same universal property as the former, and the claimed universal property is satis ed by the former. of
In other words, among all those arrows with domain Y which are compatible with , the forward propagation and (X; Y ) constructed from the cospan of c-lenses (that is f( ; (X; Y ))0) is the least-change one. All other possible compatible updates factor through that one and do so via an arrow ( 0 in the picture) which is compatible with the identity on X0.
There is of course a corresponding universal property for the back propagation b which we leave to the reader to formulate.
Remark 11 The proposition is about cospans of c-lenses. Meanwhile, spans of c-lenses similarly determine relations that correspond to the usual corrs on the objects of X and Y and that could be called compatibility relations on the arrows of X and Y, but there does not seem to be a similar universal property using those relations, nor would we expect there to be one. There is an image in Y of the universal property that holds in the peak of the span, but since Y may have many more arrows than those that appear in that image, the result is not universal and cannot be expressed independently of reference to the peak of the span. Remark 12 In fact, there is a stronger version of Proposition 10. That proposition has not used the full power of the c-lens universal property for PR. We have not yet investigated the implications of the stronger result since Proposition 10 su ces for investigations of least-change updates. (For readers who are familiar with the description of these properties in terms of cartesian arrows, the condition in Proposition 10 corresponds to precartesianness, while the stronger condition that we have not yet investigated corresponds to full cartesianness.) 6
Universality and symmetric d-lenses Having revealed the universal property of a symmetric lens that arises from a cospan of c-lenses, we turn now to more general symmetric lenses X $ Y, not just those that arise from cospans of c-lenses, and ask when we might be able to describe an fb-lens as being \least change". We would need a universal property for each operation (f and b), and the preceding section suggests that the statement of such a universal property will depend not just on corrs relating objects of X and objects of Y, but also on a \compatibility" relation between the arrows of X and the arrows of Y.
We will proceed supposing that we want universal properties as close as possible to those discovered in Section 5.
We already have some examples of compatible arrows. In any forward or backward propagation square X x the arrows x and y need to be compatible | after all, the universal property will say something like, in the rst case, the arrow y is minimal among all the arrows of Y which are compatible with x, and similarly for the minimality of x among the arrows of X which are compatible with y in the second case.
So, we expect a compatibility relation to include both the relations determined by the f-squares and the b-squares.
Let's check our intuition here for a moment. A given arrow x of X will be compatible with an arrow y of Y which is obtained by forward propagating x along some corr r. Presumably this means that y, which makes changes in Y, (1) makes changes that include the changes that x makes in as much as there is shared data between X and Y, (2) makes no changes in Y which a ect data shared with X beyond those that are made by x, and (3) may make further changes in Y which a ect data only relevant to Y. The third of these is why we expect there to be in general other arrows y0 compatible with x and why we might seek a least-change choice from amongst them.
Of course, we could have two compatibility relations, one from arrows of X to arrows of Y, and one from arrows of Y to arrows of X. But if the relations are determined by a cospan as in Section 5, or indeed by a span as the corr relation is in symmetric lenses presented as spans of asymmetric lenses, then the two relations are essentially the same, each being merely the op-relation of the other. For simplicity for now we will study a single relation between the arrows of X and the arrows of Y, and read it in the appropriate direction as required.
All this motivates the following de nition: De nition 13 Let L = ( X; Y; f; b) be an fb-lens between X and Y with corrs R. A compatibility relation on
there is a corr r : d0( ) $ d0( ), and similarly for d1) and containing the relation on arrows given by the union of the f-squares and the b-squares. When a pair ( ; ) of arrows is in the compatibility relation, that is when
Now de ne a least-change fb-lens with compatibility relation to be one whose f and b satisfy the universal properties previously observed in cospans of c-lenses: De nition 14 An fb-lens L equipped with a compatibility relation C is called least-change if for any and corr r : X $ Y it is the case that f( ; r) satis es the following universal property: For any compatible with there is a unique 0 : Y 0 / Y 00 with = 0f( ; r)0 and 1X0 C 0 : : X : Y /X0 / Y 00 X X0
r GGGGGG
Y Y 0
0 Y 00 and similarly for the back propagation b.
It might be worth remarking that the corr in the diagram between X0 and Y 00 is not important, but it is guaranteed to exist because and are compatible, and the compatibility relation respects corrs (and indeed because 1X0 and 0 are compatible and the compatibility relation respects corrs).
Note that being least-change depends upon conditions that an fb-lens with compatibility might or might not
satisfy, rather than being a property derived from the c-lenses that make up a cospan as in Section 5 { a priori a
least-change fb-lens might not even be representable as cospans of even general d-lenses. Among the important
questions to be addressed in future work is the question of when are least-change fb-lenses representable as cospans
of lenses, and among them, when are the cospan lenses c-lenses. Also, since fb-lenses are always representable
as spans of d-lenses [
Cospan and span representations We have now seen various symmetric lenses presented as spans of asymmetric lenses (Section 3) and cospans of asymmetric lenses (Construction 8) and directly via forward and backward operations (De nition 7). Now we brie y look at the interactions between these.
We know from earlier work that the various kinds of symmetric lenses can be equivalently presented in fb-style,
or as equivalence classes of spans of corresponding asymmetric lenses (see [
What about cospans?
We know from [
Furthermore, the \pullback" operation (keeping the inverted commas to emphasise that it is as just described, and not the pullback in the category of lenses) respects Construction 8 so that the fb-behaviour of the resulting span of lenses is the same as the fb-behaviour of the cospan of lenses. And even more, the corr (Construction 8) and the compatibility relations (De nition 9) for the cospan are preserved, meaning that the resulting span determines a relation between the objects of X and the objects of Y and that relation is exactly the same as the corr relation for the cospan, and similarly that span of functors determines a relation between the arrows of X and the arrows of Y and that relation is exactly the same as the compatibility relation for the cospan).
We will say that a symmetric lens with compatibility relation is represented by a particular span or cospan of asymmetric lenses if the forwards and backwards propagations have the same e ects and the corr and compatibility relations are the same. We have just seen that a cospan of lenses (whether d-lenses or c-lenses) and its \pullback" both represent the same symmetric lens with compatibility relation. Equivalent spans of d-lenses often also give examples of representations, but note that we need to check that the compatibility relations agree: a functor : S / S0 can satisfy conditions (E) without being surjective on arrows and so the compatibility relation tabulated by S might be strictly contained in the compatibility relation tabulated by S0. It is important to note that equivalent spans of lenses may represent di erent symmetric lenses with compatibility relations.
Remember that the \pullback" operation shows us that every cospan of lenses can be represented by a span of lenses (the one obtained by \pulling back" the cospan).
We show now that the converse is not the case. Not every span of lenses can be represented by a cospan of lenses. We develop below a necessary condition for a span of d-lenses to be represented by a cospan of d-lenses. Furthermore, we will see that not all spans of d-lenses satisfy the necessary condition. Indeed, it is, relatively speaking, rare among spans of d-lenses.
We study brie y the compatibility relation on cospans of d-lenses. Recall, from De nition 9 that in a cospan of d-lenses the compatibility relation exists between an arrow of X and an arrow of Y exactly when they are both sent to the same arrow in, in the notation of the de nition, V. This tells us a lot about the structure of possible compatibility relations for cospans of d-lenses.
A relation R between two sets, A and B, is called complete if for every a 2 A and every b 2 B it is the case that a R b. This includes of course the case where one or both of A and B are empty, whence the empty relation is the only possible relation between A and B, and it is complete. In the cases where neither A nor B is empty, a complete relation is sometimes called \complete bipartite" because the graph of the relation, in which related elements are joined by an edge, is a complete bipartite graph with the parts being A and B.
Given relations R between two sets, A and B, and S between two sets C and D, the coproduct of R and S is the relation R + S between A + C and B + D | two elements of the two disjoint unions A + B and C + D are R + S-related precisely if they are either R-related or S-related. Naturally this can be extended to coproducts of arbitrarily many relations including, if needed, of in nitely many relations.
Proof. Suppose that the cospan of d-lenses is
X (GL;PL) / V o (GR;PR)
Y Let C be the compatibility relation between Arr(X) and Arr(Y). It su ces to show for x and x0 in Arr(X) and y and y0 in Arr(Y) that if x C y, x0 C y and x0 C y0 then x C y0. But this follows immediately since the rst three relationships imply that all four arrows have the same image (under GL or GR as appropriate) in V.
Thus we have a necessary condition for a least-change fb-lens to be represented by a cospan of d-lenses: The compatibility relation must be a coproduct of complete relations. This is quite a strong limitation.
We brie y turn now to a degenerate case.
Consider a set-based symmetric lens [
The comparison of this result with the \RLR = R" property presented in [
Future work In the rst part of this paper, up to and including Section 3, we present initial results in our studies of when spans of d-lenses are equivalent to spans of c-lenses. The fundamental question of whether there are spans of d-lenses which are not equivalent to any span of c-lenses remains open, and is an important topic for future work. If, as seems possible, every span of d-lenses is equivalent to a span of c-lenses, then spans of c-lenses can be of no use in identifying universal updates for symmetric lenses. The question of when and how symmetric d-lenses with extra structure might have universal updates is taken up in the second part of the paper.
The second part of this paper begins a new endeavour. There are many open questions about cospans of asymmetric lenses, about symmetric lenses satisfying universal properties, and about the relationships between the two. We record here just a few of the issues.
Firstly the stronger universal property: Least change symmetric lenses are required to satisfy the universal property speci ed in De nition 14. That property was chosen because it exactly matches informal descriptions of least-change. But spans of asymmetric c-lenses satisfy a stronger universal property:
X X0 0 r
Y Y 0 0 Given : X / X0 and r : X $ Y then for any -compatible : Y / Y 00, if there is a : X / X00 which is compatible with and which factors through via some arrow 0 : X0 / X00 (see diagram), then there is a unique 0 : Y 0 / Y 00 with = 0f( ; r)0 and 0 compatible with 0. The reader can check easily that the universal property we have discussed up until now is the special case of this one obtained by taking = and 0 = 1X0 .
We know from other applications that this universal property not only has the least-change property as a
special case, but is strictly stronger (see for example the discussion about precartesian arrows in [
Similarly we restricted ourselves here to considering a single compatibility relation including both the relation determined by the f-squares and the relation determined by the b-squares. Having two independent compatibility relations is an easy extension of the work above, but guarantees, unless each happens to be the op-relation of the other, that the compatibility relation cannot arise from a span or cospan. Among our rst questions is determining which least-change symmetric lenses arise from spans or cospans of asymmetric lenses, so in the rst instance we are interested in the single compatibility relation (or equivalently, two op-related compatibility relations) case. After that work is completed we should study the more general case of a pair of compatibility relations, one from arrows of X to arrows of Y and including the relation determined by the f-squares, and one from arrows or Y to arrows of X and including the relation determined by the b-squares.
It is clear both from the simplicity of the situation in Section 5, and from earlier work of Johnson and
Dampney [
We should also do further work on cospans of lenses including why they seem (1) to be rare among spans of asymmetric lenses, but (2) to su ce for many applications. One possible answer: Our prior work has mainly been in the database applications, and interoperating databases seem to naturally have compatibility relations which are unions of complete relations and that in turn implies that the relation meets the necessary conditions of the previous paragraph and can be captured by a cospan of functors. Furthermore our earlier work has usually included universal properties (so in the parlance of the present paper the symmetric lenses have been at least least-change lenses). In such situations we have proposals for how to enrich the cospan functors to possibly obtain a cospan of asymmetric lenses, and in some cases even of c-lenses. This could explain mathematically why in our earlier industrial work the rare situation of bidirectional transformations being represented by cospans of lenses did in fact obtain.
There are more basic open questions including the following: Can d-lenses with universality always be represented by cospans of c-lenses? And even more basically: What appropriate equivalence relations should be taken among cospans of lenses so that equivalent cospans generate the same symmetric lens?
There are many interesting opportunities for further work. 9
Conclusion
The results presented here open up new areas. The observation that cospans of c-lenses do satisfy universal
properties yields immediately a class of symmetric lenses with universal updates, and motivates further proposals
for more general \least-change" symmetric lenses. In addition, old work of Johnson and Dampney [
It is also worth noting that, as explained in Johnson's forthcoming Oxford Summer School lectures [
The remaining results presented here begin the detailed study of cospans of d-lenses, seeking to characterize them among symmetric delta lenses, and they lead to proposals for more generalised notions of symmetric delta lenses with universal updates. 10
Acknowledgements The authors are grateful for the support of the Australian Research Council and the Centre of Australian Category Theory. brations. Electronic Communications of the