We show how \taking updates seriously" leads from state-based lenses to update lenses and further; we witness a little hierarchy of types of lens that arises in a systematic way. Lenses of each type are characterized either as coalgebras of certain types of comonads or morphisms between certain types of comonads. In each case, a lens is simulation between two transition systems for suitable notions of transition system and simulation.
a dependently-typed coupdate comonad. We introduce dependently-typed update lenses as coalgebras of such comonads. In Section 5, we introduce a further generalization, called update-update lenses, where source states have their own enabled updates, and applying a view update to a source state goes via rst translating it into a source update and then applying that. We show that update-update lenses are morphisms between coupdate comonads. In Section 6, we compare update-update lenses to delta lenses and categorical lenses. Finally, in Section 7, we brie y describe the related work, to conclude in Section 8.
Some additional material appears in appendices. In Appendix A, we brie y review comonads, comonad coalgebras and comonad morphisms. In Appendix B, we prove the bijection between coalgebras of a given comonad and morphisms from costate comonads to this comonad.
compare cofunctors and op brations.
In the main part of the paper, we assume the reader to know basic category theory. While this includes the basics of comonads, we still give the main de nitions in Appendix A for reference. We assume no knowledge about containers or directed containers, introducing them in Section 4, where they are rst needed. We provide no proofs in the main part of the paper, but prove the central proposition in Appendix B. 2
We will consider three types of asymmetric lens in this paper: state-based lenses, update lenses, and updateupdate lenses (the latter being an original contribution of this paper). They have a lot in common.
Any type of asymmetric lens is about two evolving databases, the source database and view (target) database. At any moment, both databases are in some state and the two states must be consistent, i.e., be in a certain relation. If the view state is changed, it must be possible to change also the source state in such a way that consistency is re-established. Reasonably, this notion of simulation of the view database by the source database should be compositional in the sense that i) no view change should induce no source change and ii) the composition of two view changes should induce the composition of the two induced source changes. In the types of lens that we consider, the two databases operate generally on two di erent sets of states, and the consistency relation is functional, in other words, the graph of a function extracting a view state from a source state.
The simplest type of lens we consider is state-based lenses in the sense of the very well-behaved lenses of
The distinctive feature of state-based lenses is that the view state can be changed to any other view state and, moreover, the only thing identifying a view change (besides the current view state) is the new view state: view changes are unconstrained and, we might say, extensional. The same is true about source changes|they are likewise unconstrained and extensional|but of course a source change simulating a view change must re-establish consistency.
Let S0 and S be two sets (of source resp. view states). A (very well-behaved) state-based lens from S0 to S is given by two maps get : S0 ! S and put : S0
get (put (s0; s0)) = s0 s0 = put (s0; get s0) put (put (s0; s0); s00) = put (s0; s00) The map get is there to determine the view state corresponding to the current source state (de nes the consistency relation between source and view states). The map put takes the current source state, the next view state and returns the next source state (de nes simulation of view changes). The 1st equation asserts that consistency is restored in simulation. The 2nd and 3rd equations establish that simulation is compositional.
Pictorially, consistency and simulation are illustrated by the following diagram.
s0 get put .& s Simulation means that, given a source state s0 and a view state s that are consistent (get s0 = s), any change of the view state, i.e., a new view state s0, induces a change of the source state, i.e., a new source state s00 =df put (s0; s0), so that consistency is re-established (we have get s00 = get (put (s0; s0)) = s0).
As an example, consider two versions of a simple bookshop database. The sets of source and view states are S0 =df book ) N
N
S =df book ) N The idea is that a source state is an association to every book (from some xed list) of a price and a quantity (stock level); and a view state is an association to every book of just a price. The get operation corresponds to discarding the quantity of each book; the put operation changes the prices of all books leaving the quantities unchanged: get s0 =df b: fst (s0 b)
put (s0; s) =df b: (s b; snd (s0 b))
State-based lenses can be characterized in two ways in terms of costate comonads (a.k.a. array comonads), using comonad coalgebras or comonad morphisms. The coalgebraic characterization is due to Power and Shkaravska [PS04] and O'Connor [OCo11].
The costate comonad for a set S (of states) is the comonad de ned by
DX =df S (S ) X) "X (s; v) =df v s
X (s; v) =df (s; s0: (s0; s00: v s00))
First, there is a bijection between state-based lenses between S0 and S, and coalgebras of the costate monad for S with S0 as the carrier, i.e., a maps : S0 ! S (S ) S0) satisfying some equations.
On the level of data, this bijection is only about straightforward packing of the data of a lens into one datum with currying and pairing. Given a coalgebra structure , we obtain the lens data by taking get s0 =df fst ( s0)
put (s0; s0) =df snd ( s0) s0 Conversely, given a state-based lens (get; put), the coalgebra structure datum is
s0 =df (get s0; s0: put (s0; s0)) But the lens equations also imply the coalgebra equations and vice versa.
Second, there is also a bijection between state-based lenses between S0 and S, and comonad morphisms between the costate comonads for S0 and S, i.e., natural transformations with components X : S0 (S0 ) X) ! S (S ) X) satisfying some equations.
The second characterization follows from the rst thanks to a general fact that we also use later. For any comonad D, there is a bijection between coalgebras of the comonad D with set S0 as the carrier, and comonad morphisms between the costate comonad for S0 and the comonad D. Given a coalgebra structure : S0 ! D S0, the corresponding comonad morphism is given by X (s0; v) =df D v ( s0). Given a comonad morphism , the corresponding coalgebra structure is s0 =df S0 (s0; idS0 ). We provide a full proof of this proposition in Appendix B. 3
We proceed to update lenses, as de ned by Ahman and Uustalu [AU14a]. We rst consider a simpler special case of the concept and then, in the next section, the fully general version.
As we saw, in a state-based lens, a view change is a just a move to a freely chosen next state. In an update lens, we are in a richer situation. There is a dedicated set of view updates; any view update is applicable to the current view state and gives the next view state. There is a distinguished trivial view update (which incurs no update on the current view state) and any two view updates can be composed into a single view update (so that applying the composite view update to the current state has the same e ect as applying rst the rst view update to the current state and then the second view update to the next state). Not every view state needs to be accessible from the current one by applying a view update and some view states may be accessed by several view updates. In other words, in contrast to state-based lenses, changes of view states are generally constrained and intensional. A move to a new view state must be simulatable by a move to a new source state so that consistency is restored. However, there is no separate set of source updates; one could say that view updates also double as source updates.
that state.
Recall also that a right action of a monoid (P; o; ) on a set S is a map # : S
Now, let S0 be a set (of source states). Moreover, let S be another set (of view states), (P; o; ) be a monoid typed) update lens between S0 and (S; P; #; o; ) is given by two maps get : S0 ! S and pput : S0 (of view updates), and # a right action of (P; o; ) on S (application of a view update to a view state). A (simplyP ! S0 such p o o = p p = p (p p0) p00 = p (p0
p00) s # o = s s0 =df s # p). The move from s to s0 is simulated by a move from s0 to s00 where s00 is de ned by the map pput (i.e., s00 =df pput (s0; p)). Again the role of the 1st equation is to assert that consistency is restored in simulation, and the 2nd and 3rd equations stipulate compositionality of simulation. as in the previous section. As the monoid of view updates we use the free monoid on the set book We can modify the bookshop example to obtain an update lens. Let S0 =df book ) N N and S =df book ) N
Z, i.e., P =df (book
Z) o =df [] =df ++ so a view update is a sequence of price changes to books. de ned as follows.
The get operation is de ned as before. Application of view updates to view states and to source states is s # [] s # ((b; c) :: p) pput (s0; []) pput (s0; (b; c) :: p) =df =df =df v v =df ( b0: if b0 = b then max (0; s b0 + c) else s b0) # p
pput ( b0: if b0 = b then (max (0; fst (s0 b0) + c); snd (s0 b0)) else s0 b0; p)
One might complain that the concept of update lens is a bit of an exaggeration, since, by the de nition we have given, an update lens for (S; P; #; o; ) is nothing but a (P; o; )-set (S0; pput) (i.e., a set S0 and a right action pput of (P; o; ) on S0; this is stated by the 2nd and 3rd equations) together with a (P; o; )-set morphism get between (S0; pput) and (S; #) (stated by the 1st equation). Yet, we claim that update lenses make enough practical sense and have enough theoretical signi cance to deserve attention, both in the special form we are discussing here as well as in the general form that we will consider in the next section.
One argument in defense of update lenses for theory is that, similarly to state-based lenses, update lenses are characterizable as comonad coalgebras and as comonad morphisms. The coalgebraic characterization is due to Ahman and Uustalu [AU14a].
Both characterizations use coupdate comonads. Any set S (of states), monoid (P; o; ) (of updates) and right action # of (P; o; ) on S (application of an update to a state), de ne a comonad, which we call the coupdate comonad for (S; P; #; o; ), by
D X =df S (P ) X) "X (s; v) =df v o
X (s; v) =df (s; p: (s # p; p0: v (p p0)))
We have: First, update lenses between S0 and (S; P; #; o; ) are in a bijection with coalgebras of the update comonad for (S; P; #; o; ) with S0 as the carrier.
Second, they are also in a bijection with comonad morphisms between the costate comonad for S0 and the coupdate comonad for (S; P; #; o; ). This an immediate consequence of the rst characterization thanks to the same bijection between coalgebras of a given comonad and morphisms from costate comonads to this comonad that we exploited in the previous section.
A big di erence of coupdate comonads from costate comonads is that coupdate comonads are compatible compositions of simpler comonads. Costate comonads admit no similar decomposition.
Given a set S, we have the coreader comonad de ned by
D0 X =df S
X "0X (s; x) =df x
X0 (s; x) =df (s; (s; x)) Given a monoid (P; o; ), we have the cowriter comonad de ned by
D1 X =df P ) X "1X v =df v o
X1 v =df p: p0: v (p p0) Right actions of (P; o; ) on S are in a bijective correspondence with distributive laws of the comonad D0 over the comonad D1. As a consequence, coupdate comonads for (S; P; #; o; ) are in a bijection with compatible compositions of the comonads D0 and D1.
This composite nature of coupdate comonads leads to a number of further characterizations of update lenses, e.g., as pairs of comonad coalgebras, comonad-monad bialgebras (pairs of a comonad coalgebra and a monad algebra) etc. Those are beyond the scope of this paper; we refer the interested reader to [AU14a] for a detailed account of them. 4
In the type of update lenses that we considered in the previous section, view updates were always applicable and always composable. This may be unrealistic and is an unnecessary restriction. A generalization of update lenses from the previous section xes this issue. Instead of a set, monoid and right action, we need to describe the view database in terms of a directed container.
Containers were introduced by Abbott et al. [AAG05] as a representation for a wide class of set functors (datatypes) in terms of sets and positions. Directed containers [ACU14] are containers with additional structure. They characterize those containers whose interpretation as a set functor carries a comonad structure.
A container is a set S (of shapes / or, in our application, states) and, for any s : S, a set P s (of positions in the shape s / updates applicable to the state s)1. A directed container is a container (S; P ) equipped with maps # : ( s : S: P s) ! S (the subshape corresponding to a position in a shape / application of an update to a state), 1We originally adopted the letters S and P as mnemonics for shapes and positions, but coincidentally they also work perfectly for states and 'pdates.
o : s:S : P s (the root position / the trivial update), and
: s:S : ( p : P s: P (s # p)) ! P s (translation of a position in a position's subshape / composition of two updates) We notice that the data and equations of a directed container are like those of a set, monoid and a right action, modulo the presence of the \minor" (subscripted) arguments and the dependent typing. In particular, if P s, os, and p s p0 do not actually depend on s, then we indeed have a set, monoid and right action.
A container (S; P ) de nes a set functor JS; P Kc =df D, called its interpretation, by
D X =df s : S: P s ) X Given a directed container structure (#; o; ) on the container, this functor obtains a comonad structure de ned by "X (s; v) =df v os
X (s; v) =df (s; p: (s # p; p0: v (p s p0))) We call the comonad JS; P; #; o; Kdc =df (D; "; ) the interpretation of (S; P; #; o; ). We could also call it the (dependently-typed) coupdate comonad for (S; P; #; o; ). Not unexpectedly, the dependently-typed concept is de ned in exactly the same way as its simply-typed counterpart from the previous section, modulo the presence of the minor arguments and dependent typing.
Any comonad structure ("; ) on a set functor D that is the interpretation of some container (S; P ) (i.e., D X = s : S: P s ) X) arises from a directed container structure (#; o; ) on (S; P ). In fact, directed container structures on (S; P ) and comonad structures on D are in a bijection. Given a comonad structure ("; ), the corresponding directed container structure is de ned by os =df "P s (s; id) s # p =df fst (snd ( P s (s; id)) p) p s p0 =df snd (snd ( P s (s; id)) p) p0
Directed containers are in a bijection up to isomorphism with small categories. Given a directed container (S; P; #; o; ), the corresponding small category is obtained as follows. The set of objects is S. The set of maps with domain s : S is P s, which means that the total set of maps is P =df s : S: P s and the domain of a map (s; p) : P is src p =df s. The codomain of a map (s; p) : P is tgt p =df s # p. The identity map on an object s is ids =df (s; os) and the 1st directed container equation ensures that its codomain is s, as required. A map (s; p) can only be composed with a map (s0; p0), if s # p = s0, in which case the composition is (s; p); (s0; p0) =df (s; p s p0). By the 2nd directed container equation the codomain of this map is (s # p) # p0 = s0 # p0, as required. The 3rd to the 5th equations ensure that composition is unital and associative.
Let S0 be a set (of source states). Let (S; P; #; o; ) be a directed container (of view states and view updates, together with view update application). A (dependently-typed) update lens between S0 and (S; P; #; o; ) is given by two maps get : S0 ! S and pput : ( s0 : S0: P (get s0)) ! S0 satisfying
s0 = pput (s0; oget s0 ) pput (pput (s0; p); p0) = pput (s0; p Again the only di erence from the simply-typed concept of the previous section is the presence of minor arguments and dependent typing.
But exactly this di erence makes the idea of updates enabled in a state work. Consider again the picture from the previous section. It is still valid.
s0
Given a consistent pair of a current source state s0 and view state s (i.e., s = get s0), view updates applicable to s come from the set P s = P (get s0). The operation pput, which is supplied the current source state s0 and an applicable view update p, must pick the next source state s00 consistently with the next view state s0 # p. The
We can modify the bookshop example from the previous section as follows to obtain a dependently-typed update lens. We de ne P as an inductive family by the rules
remain de ned essentially as before. Also # and pput can be de ned like before, but comparison with 0 is no longer necessary. A view update is only applicable to a view state, if the aggregate price change to each book is not too negative.
Not surprisingly, it remains true in the dependently-typed case that update lenses between S0 and (S; P; #; o; ) are in a bijection with coalgebras of the coupdate comonad for (S; P; #; o; ) with S0 as the carrier. And likewise they are in a bijection with comonad morphisms between the costate comonad for S0 and the coupdate comonad for (S; P; #; o; ) with S0. container S =df (S; P; #; o; ) by choosing
Let us now compare state-based and update lenses. Any set S can be canonically extended into a directed P s =df S s # s0 =df s0 os =df s s0 s s00 =df s00 In the directed container S , updates are just states and applying an update (state) to the current state means moving to that state. Viewed as small category, S
is the codiscrete category with S as the set of objects, i.e., the category with exactly one map (s; s0) between any two objects s and s0. In the next section, we shall see that S
has a simple universal property.
It is easy to verify that the costate comonad for S is equal to the coupdate comonad for S .
As a result, coalgebras for the two comonads are on the nose the same thing, which in turn means that state-based lenses between S0 and S, and update lenses between S0 and S are essentially the same thing.
In other words, costate comonads are a special case of (dependently typed) coupdate comonads and state-based lenses are a special case of (dependently-typed) update lenses.
We note that this is not achievable with simply-typed coupdate comonads: there is no way to see the costate comonad for S as a simply-typed coupdate comonad, unless the set of view states S is a singleton. If S has multiple elements, we would need a di erent os = s for every s : S, and we are not allowed this in the simply-typed format.
But in one respect, we should point out, simply-typed coupdate comonads are more well-behaved than dependently-typed coupdate comonads: the former are compatible compositions of simpler comonads, but the latter are generally not. A decomposition is possible in terms of two relative comonads though. 5
Simulation means nding, given a view update applicable to the current view state, a source update applicable to the current source state so that the next source state will be consistent with the next view state.
We will see that an update-update lens is exactly a morphism between directed containers. We therefore begin by de ning morphisms of containers and morphisms of directed containers.
A container morphism between two containers (S0; P0) and (S; P ) is given by maps t : S0 ! S (the shape map) and q : s0:S0 : P (t s0) ! P0 s0 (the position map). A directed container morphism between two directed containers (S0; P0; #0; o0; 0) and (S; P; #; o; ) is a morphism (t; q) between the underlying containers satisfying t (s0 #0 qs0 p)) = t s0 # p If (t; q) is a morphism between directed containers (S0; P0; #0; o0; 0) and (S; P; #; o; ), then is a comonad morphism between JS0; P0; #0; o0; 0Kdc =df (D0; "0; 0) and JS; P; #; o; Kdc =df (D; "; ); we de ne Jt; qKdc =df .
Any natural transformation between the interpretations D0 and D of two containers (S0; P0) and (S; P ) is an interpretation of a unique container morphism, namely (t; q) where t s0 =df fst ( P s0 (s0; p0: p0)) qs0 p =df snd ( P s0 (s0; p0: p0)) p If is a comonad morphism between the interpretations (D0; "0; 0) and (D; "; ) of two directed containers (S0; P0; #0; o0; 0) and (S; P; #; o; ), then (t; q) is a directed container morphism interpreting to .
Containers and containers morphisms form a monoidal category Cont, interpretation of containers is a fully faithful monoidal functor from Cont to [Set; Set]. Directed containers and directed container morphisms form a category DCont, interpretation of directed containers is fully faithful functor from DCont to Comonad(Set). In fact, DCont is isomorphic to the category Comonoid(Cont) and is the pullback in CAT of U : Comonad(Set) ! [Set; Set] along J Kc : Cont ! [Set; Set].
While directed containers are in a bijection up to isomorphism with small categories, the category of directed containers is not equivalent to the category of small categories. Directed container morphism are not at all like functors between small categories, they are quite di erent. They turn out to map to what Aguiar [Agu97] termed cofunctors, but with the source and target categories switched. We give the de nition.
A cofunctor between small categories (S; P ; src; tgt; id; ;) and (S0; P0; src0; tgt0; id0; ;0) is given by two maps t : S0 ! S (the object map) and q : ( s0 : S0: p : P : t s0 = src p) ! P0 (the morphism map) satisfying src0 (q (s0; p)) = s0 and t (tgt0 (q (s0; p))) = tgt p
id0s0 = q (s0; idt s0 ) q (s0; p) ;0 q (tgt0 (q (s0; p)); p0) = q (s0; p ; p0) While a functor maps objects and maps of the source category to those in the target category, a cofunctor's object map is from the target category to the source category, but the morphism map is still from the source to the target category. A cofunctor looks a bit like an opcleavage, but it is not one. We will comment on the exact di erences in the next section.
The category DCont of directed containers is equivalent to the opposite category of the category Cat of small categories and cofunctors. Given a directed container morphism (t; q), the corresponding cofunctor is (t; q) where q is de ned by q (s0; (t s0; p)) =df (s0; qs0 p).
In the previous section, we discussed the construction of the directed container S0 from a set S0. The corresponding small category was the codiscrete category on S0. Now that we have xed what we want to consider as morphisms between directed containers, we can say that this directed container is the free directed container on S0, or, as a small category, the free object in (Cat)op on S0. It is also at the same time the cofree small category (in the sense of being the cofree object in Cat) on S0. (Note that in the rst case, we consider small categories and cofunctors, in the second case, small categories and functors.)
An update-update lens between two directed containers (S0; P0; #0; o0; 0) and (S; P; #; o; ) (for source states, updates and update application resp. view states, updates and update application) is given by two maps get : S0 ! S and pbwd : s0:S0 : P (get s0) ! P0 s0 such that get (s0 #0 pbwds0 p)) = get s0 # p In other words, an update-update lens is just a directed container morphism, we only renamed t to get and q to pbwd. Or, we could also say, it is a cofunctor.
Consistency and simulation in an update-update lens are illustrated in this picture.
s0 p0 rz source state s00 =df s0 #0 p0 and this is stipulated by the 1st equation.
If the current source and view state are s0 and s =df get s0, then a view update p applicable to s is simulated by an update p0 =df pbwds0 p applicable to s0. The next view state s0 =df s # p must be consistent with the next
There are a many ways to modify the bookshop example to yield an update-update lens. Recall that in the book a price and quantity, and a view state only a price. Here are some possibilities. previous sections we had S0 =df book ) N
N and S =df book ) N, with a source state associating to every (i) Take P s =df (book
Z) with the intent that a view update is an (unsafe) sequence of book and price change pairs, and take P0 s0 =df (book (Z + Z))
with the intent that a source update is an association of an (unsafe) price or quantity change for every book. The function pbwd would be the obvious embedding of P (get s0) in P0 s0.
pbwd []
=df [] pbwd ((b; c) :: p)
=df ((b; inl c) :: pbwd p (ii) Let P remain as in (i), but take P0 s0 =df book ) Z
Z, with the idea that a source update is an association of a price change and quantity change to every book. The function pbwd should then aggregate the price changes for every book by summing them up; the quantity change of every book should be 0.
pbwd [] pbwd ((b; c) :: p) =df =df b0: (0; 0) b0: (if b0 = b then fst (pbwd p b0) + c else fst (pbwd p b0); 0) (iii) Let P0 remain as in (i), but take P s =df (book
negative price change pairs. pbwd remains essentially as in (i). are in a bijection with the comonad morphisms between the corresponding two coupdate comonads.
Directed container theory tells us that update-update lenses between (S0; P0; #0; o0; 0) and (S; P; #; o; )
(S; P; #; o;
). In this way, update lenses are a special case of update-update lenses.
Because the costate comonad for a set S0 equals the coupdate comonad for the free directed container S0 , update lenses between S0 and (S; P; #; o; ) are the same thing as update-update lenses between S 0 and
Update lenses can be seen as a special case of update-update lenses also in another way. Given an update lens (get; pput) between S0 and (S; P; #; o; ), we can equip S0 with a directed container structure by P s0 =df P (get s0) s0 #0 p0 =df pput (s0; p0) o0s0 =df oget s0 p0 0s0 p00 =df p0 get s0 p0o intuition that, in an update lens, view updates double as source updates.
We then have the update-update lens (get; pbwd) where pbwds0 p =df p. This construction substantiates the
Let us compare very brie y the update-update lenses introduced in the previous section to Diskin et al.'s delta lenses [DXC11] and Johnson et al.'s category lenses [JRW12].
Common to all three is that there are not only view updates, but also source updates. A big di erence is that update-update lenses have only backward-pushing of updates (view updates are mapped to source updates, depending on the current source state). In delta and category lenses, updates can also be pushed forward; there is a map sending source updates to view updates.
For the sake of comparison, we present the de nitions of delta and category lenses in terms of directed containers.
Given two directed containers (S0; P0; #0; o0; 0) and (S; P; #; o; ) (for source states, updates and update application, resp. view states, updates and update application). A delta lens is given by maps get : S0 ! S, pfwd : s0:S0 : P0 s0 ! P (get s0), and pbwd : s0:S0 : P (get s0) ! P0 s0 satisfying get s0 # pfwds0 p0 = get (s0 #0 p0)
oget s0 = pfwds0 o0s0 pfwds0 p0 get s0 pfwds0#0p0 p00 = pfwds0 (p0 0s0 p00) get (s0 #0 pbwds0 p) = get s0 # p
o0s0 = pbwds0 oget s0 (The 2nd and 4th equation here are in fact derivable from the others.) It is immediate from this de nition, that a delta lens is an update-update lens with additional structure. pfwd simulates a source update by a view update. The 7th equation says that simulation of a view update p by a source update p0 by pbwd must be \correct" in the sense that pfwd must simulate p0 by the same view update p.
In terms of small categories, we do not only have a cofunctor (get; pbwd) from the target category to the source category in a delta lens, but also a functor (get; pfwd) from the source category to the target category, with the same object mapping get. Composition of pfwd after pbwd must be identity. A structure like this could be called a splitting pre-opcleavage (where we say `pre-' to express that have waived the standard opCartesianness requirement on the lifts pbwds0 p).
A category lens is a delta lens with an additional map ll : s0:S0 : p:P (get s0): ( p0 : P0 s0: p0 : P (get s0 # p): pfwds0 p0 = p get s0 p0) ! P0 (s0 #0 pbwds0 p) satisfying Intuitively, in a category lens, simulation of a view update by a source update causes least change to the source state. Suppose we are simulating a view update p : P (get s0) consistent with some source state s0 : S0. The simulating source update is pbwds0 p : P0 s0. Suppose we have some other source update p0 : P0 s0 for the same source state s0 whose view simulation pfwds0 p0 : P (get s0) factors through p, i.e., pfwds0 p0 = p p0 for some p0. Then, on the source side, p0 factors through pbwds0 p, as we have pbwds0 p 0 lls0;p (p0; p0) = p0, moreover this is the unique such factoring of p0.
In terms of small categories, a category lens is a splitting opcleavage. The additional data and equations assure that the lifts pbwds0 p are opCartesian.
We would like to argue that although pfwd can serve as a kind of quality yardstick of pbwd, it can often be unnatural from the applications viewpoint to require the map pfwd. It is easy to construct meaningful updateupdate lenses that are not delta lenses. The presence of an operation pfwd forces that all source updates, even those not in the range of pbwd, must be simulable as view updates, which makes it impossible to accommodate example (iii) from the previous section: the equation get s0 # pfwds0 p0 = get (s0 #0 p0) cannot be met. The equation pfwds0 (pbwds0 p) = p can only hold when pbwd is injective, which rules out example (ii) from the previous section.
But any update lens can be considered as a delta lens, by using its view updates also as source updates (i.e., P0 s0 =df P (get s0), pbwds0 p =df p, and s0 #0 p =df pput (s0; p)). It is then also a category lens.
In contrast, when we consider the source states of an update lens as its source updates (i.e., P0 s0 =df S0, pbwds0 p =df pput (s0; p), and s0 #0 s00 =df s00), then the update lens is generally not a delta lens. Indeed, since, for any s0, s0 , we have s0 #0 s00 = s0 , we must also have get s0 # pfwds0 s00 = get s00. But there may well exist 0 0 source states s0, s00 for which there is no view update p : P (get s0) satisfying get s0 # p = get s00.
On the theoretical side, state-based lenses, update lenses, and update-update lenses admit concise characterizations as comonad morphisms. We do not know whether something similar is also achievable for delta or category lenses. 7
The literature on lenses has grown quite large. As this paper is on notions of asymmetric lens, where one distinguishes between a source database and a view (target) database, we only discuss works on those, to explain how the di erent strands of study developed and cross-fertilized.
State-based lenses were introduced by Foster et al. [F+07]. Two ner concepts of lens relying on rst-class state changes or deltas, namely, delta lenses and categorical lenses, were introduced independently by Diskin et al. [DXC11] and Johnson et al. [JRW12]. Johnson and Rosebrugh [JR13] worked out the interrelationship of these two concepts. To be able to compare the di erent types of asymmetric lens to Hofmann et al.'s [HPW12] on (symmetric) edit lenses, Johnson and Rosebrugh [JR16] introduced a yet di erent variation, asymmetric edit lenses.
Power and Shkaravska [PS04] and O'Connor [OCo11] were probably the rst to notice that state-based lenses are the same as coalgebras of costate comonads. Johnson et al. [JRW10] at the same time promoted an algebraic characterization of state-based lenses. Gibbons and Johnson [GJ12] explained why both are possible by showing that they are directly interderivable.
Containers as a useful \syntax" for a wide class of set functors were introduced by Abbott et al. [AAG05]. Directed containers as characterization of those containers whose endofunctor interpretation carries a comonad structure were introduced by Ahman et al. [ACU14]. In a later work [AU16], they noticed that directed containers are the same as categories whereas morphisms between them are not functors, but particular \relative splitting pre- opcleavages". Now they know that this concept of map between two categories is 20 years old and was introduced under the name of cofunctor by Aguiar [Agu97]. Ahman and Uustalu [AU14b] noticed that, in addition to the interpretation as comonads, directed containers can also be interpreted (\cointerpreted") as monads of a particular type, which they called update monads, generalizing state monads. Only subsequently [AU14a], they noticed that coalgebras of coupdate comonads (comonads denoted by a directed container) make a useful notion of lens, which they termed update lenses. They also showed that, similarly to state-based lenses, update lenses admit multiple characterizations, among them characterizations as algebras. 8
We hope to have demonstrated in this paper that both update lenses and update-update lenses are natural concepts. Both are t for their application purpose and well-motivated theoretically, which is witnessed in particular by the fact that they can be characterized in several canonical ways. The leading intuition should in both cases be that a lens is a simulation between two transition systems, the di erence being between whether the simulating system must use the same alphabet of transition labels as the simulated system or can have its own. Update lenses are the same as coalgebras of a comonad whose underlying endofunctor is the interpretation of a container, update-update lenses are morphisms between two such comonads.
We compared update-update lenses to delta and categorical lenses, singled out the di erences, and argued that update-update lenses have both practical and theoretical advantages.
Acknowledgements Tarmo Uustalu is grateful to Michael Johnson and Paul-Andre Mellies for discussions.
This research was supported by the Estonian Ministry of Education and Research institutional research grant No. IUT33-13. [JR13]
M. Johnson, R. Rosebrugh. Delta lenses and op brations. In P. Stevens, J. F. Terwilliger, eds., Proc. of 2nd Int. Wksh. on Bidirectional Transformations, BX 2013 (Rome, March 2013), v. 57 of Electron. Commun. of EASST, 18 pp., 2013. doi: 10.14279/tuj.eceasst.57.875 M. Johnson, R. Rosebrugh. Unifying set-based, delta-based and edit-based lenses. In A. Anjorin, J. Gibbons, eds., Proc. of 5th Int. Wksh. on Bidirectional Transformations, BX 2016 (Eindhoven, April 2016), v. 1571 of CEUR Wksh. Proc., pp. 1{13, 2016. http://ceur-ws.org/Vol-1571/paper_13.pdf
D D
D F
FFFF
FFFF FFFF
FFFF
F / D D "
D F
FFFF
FFFF FFFF
FFFF
F / D D
" D D / D D
D / D D D commute.
A coalgebra of a comonad (D; "; ) is a an object C together with a map : C ! D C such that the diagrams commute.
A morphism between two comonads (D; "; ) and (D0; "0; 0) on the same category C is a natural transformation : D ! D0 such that the diagrams A
For reference only, we recapitulate the de nitions of comonads, coalgebras of comonads, comonad morphisms.
A comonad on a category C is given by a functor D : C ! C together with natural transformations " : D ! Id and : D ! C C such that the diagrams
is natural: for f : X ! Y , we have commute. by B
We prove the following proposition for Set, but in fact this proof scales to any monoidal closed category. Proposition 1 Given a comonad D, for any set S0, there is a bijection between coalgebras of D with S0 as the carrier and morphisms from the costate comonad DS0 to the comonad D.
Proof. Given a comonad coalgebra structure : S0 ! D S0, we de ne a family of maps with components
C D C
D D D
D D D
D
C / D C D / D (D C) / D0
0 / D0 D0 C D
DDDD
DD DD DD DDDD
D / D C
"C
C D " Id / D0
"0 Id
X : DS0 X ! D X
X (s0; v) =df D v ( s0) D f ( X (s0; v)) = = = =
D f (D v ( s0)) D (f v) ( s0)
Y (s0; f v)
Y (DS0 f (s0; v)) is a comonad morphism, because satis es the laws of a comonad coalgebra structure:
is a comonad coalgebra structure, because satis es the comonad morphism laws: S0 ( s0) = S0 ( S0 (s0; idS0 )) = D S0 ( DS0 S0 ( SS00 (s0; idS0 ))) = D S0 ( DS0 S0 (s0; s00: (s00; idS0 ))) = D S0 ( DS0 S0 (DS0 ( s00: (s00 idS0 )) (s0; idS0 ))) = D S0 (D ( s00: (s00 idS0 )) ( S0 (s0; idS0 ))) = D ( s00: S0 (s00; idS0 )) ( S0 (s0; idS0 )) = D ( S0 (s0; idS0 )) = D ( s0) ( ) is a bijection, as demonstrated by the following calculations.
We recapitulate the de nitions of a cofunctor in the sense of Aguiar [Agu97] and an op bration (to be precise, an op bration with chosen lifts, also called an opcleavage) and compare.
A cofunctor from a category D to a category C is given by an object mapping F : jCj ! jDj, and an operation taking any object X of C and any map f : F X ! W of D into a map fX : X ! Y of C (the lift of f ) such that F Y = W . It is required that (idF X )X = idX and gY fX = (g f )X .
Given a functor F : C ! D, a map k : X ! Y of C is said to be opCartesian wrt. F , if, for any map k0 : X ! Y 0 of C and any map g : F Y ! F Y 0 of D such that F k0 = g F k, there exists a unique map ` : Y ! Y 0 such that k0 = ` k and F ` = g.
An opcleavage of a category C over a category D is given by a functor F : C ! D, and an operation taking any object X of C and any map f : F X ! W of D into an opCartesian map fX : X ! Y of C (the lift of f ) such that F fX = f (so also F Y = W ). An opcleavage is said to be splitting, if additionally (idF X )X = idX and gY fX = (g f )X .
Notice that in the de nition of a cofunctor, F is just an object mapping. In the de nition of an opcleavage, F is a functor. Notice also that lifts in an opcleavage are required to be opCartesian.