Taking Updates Seriously∗ Danel Ahman Laboratory for Foundations of Computer Science, University of Edinburgh 10 Crichton Street, Edinburgh EH8 9LE, United Kingdom d.ahman@ed.ac.uk Tarmo Uustalu Dept. of Software Science, Tallinn University of Technology Akadeemia tee 21B, 12168 Tallinn, Estonia tarmo@cs.ioc.ee Abstract 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 charac- terized 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. 1 Introduction In this paper, we discuss two types of asymmetric lens, update lenses of Ahman and Uustalu [AU14a] and update- update lenses (a new proposal of this paper). We show how state-based lenses, update lenses and update-update lenses arise systematically from the same paradigm: an asymmetric lens is about simulating changes in the view database by changes in the source database in a consistency-restoring manner; cf. McKinna’s [McK16] slogan that symmetric lenses are bisimulations. Each subsequent notion of lens takes the idea of first-class changes (in our terminology, updates) more seriously than the previous one. In each case, a lens is essentially the same as a coalgebra of a comonad of an appropriate type or a morphism between two comonads of an appropriate type. We briefly compare update lenses and update-update lenses to the delta lenses of Diskin et al. [DXC11] and the category lenses of Johnson et al. [JRW12]. This paper is organized as follows. First, in Section 2, we recapitulate state-based lenses. In particular, we recall that state-based lenses are the same as coalgebras of costate comonads, which also happen to be the same as morphisms between costate comonads. Then, in Section 3, we introduce simply-typed update lenses as an improvement where changes to view states, or updates, are taken seriously, and show that they are the same as coalgebras of what could be called coupdate comonads. To allow every view state to have its own set of enabled updates, also applicable to the relevant source states, we introduce, in Section 4, the concept of a directed containers as the appropriate notion of transition system, and point out that every directed container determines ∗The material of this paper was first presented in a talk at the NII Shonan Meeting on Bidirectional Transformations in Sept. 2016. Copyright c by the paper’s authors. Copying permitted for private and academic purposes. In: R. Eramo, M. Johnson (eds.): Proceedings of the Sixth International Workshop on Bidirectional Transformations (Bx 2017), Uppsala, Sweden, April 29, 2017, published at http://ceur-ws.org 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 first 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 briefly describe the related work, to conclude in Section 8. Some additional material appears in appendices. In Appendix A, we briefly 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. Finally, in Appendix C, we define and compare cofunctors and opfibrations. 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 definitions in Appendix A for reference. We assume no knowledge about containers or directed containers, introducing them in Section 4, where they are first needed. We provide no proofs in the main part of the paper, but prove the central proposition in Appendix B. 2 State-Based Lenses We will consider three types of asymmetric lens in this paper: state-based lenses, update lenses, and update- update 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 different 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 Foster et al. [F+07]. 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. The official definition of state-based lenses is as follows. 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 × S → S0 such that 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 (defines 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 (defines 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. get s0 &. s put  v~  s00 s0 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 fixed 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 Shkar- avska [PS04] and O’Connor [OCo11]. The costate comonad for a set S (of states) is the comonad defined 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 first 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 Simply-Typed Update Lenses We proceed to update lenses, as defined by Ahman and Uustalu [AU14a]. We first 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 effect as applying first the first 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. Update lenses are mathematically defined as follows. We recall that a monoid is a set P with an element o : P and a map ⊕ : P × P → P such that p⊕o=p o⊕p=p (p ⊕ p ) ⊕ p00 = p ⊕ (p0 ⊕ p00 ) 0 Recall also that a right action of a monoid (P, o, ⊕) on a set S is a map ↓ : S × P → S satisfying s↓o=s s ↓ (p ⊕ p0 ) = (s ↓ p) ↓ p0 Now, let S0 be a set (of source states). Moreover, let S be another set (of view states), (P, o, ⊕) be a monoid (of view updates), and ↓ a right action of (P, o, ⊕) on S (application of a view update to a view state). A (simply- typed) update lens between S0 and (S, P, ↓, o, ⊕) is given by two maps get : S0 → S and pput : S0 × P → S0 such that get (pput (s0 , p)) = get s0 ↓ p s0 = pput (s0 , o) pput (pput (s0 , p), p0 ) = pput (s0 , p ⊕ p0 ) The map pput describes how applying a view update to the current view state is simulated on the current source state. Consistency and simulation in an update lens are illustrated by the following diagram. get !) s0 s p ↓ pput  {   s00 s0 Differently from the case of a state-based lens, in this picture, the new view state s0 is not arbitrarily cho- sen; instead, it is obtained by applying an arbitrarily chosen view update p to the current view state s (i.e., s0 =df s ↓ p). The move from s to s0 is simulated by a move from s0 to s00 where s00 is defined 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. We can modify the bookshop example to obtain an update lens. Let S0 =df book ⇒ N × N and S =df book ⇒ N as in the previous section. As the monoid of view updates we use the free monoid on the set book × Z, i.e., P =df (book × Z)∗ o =df [] ⊕ =df ++ so a view update is a sequence of price changes to books. The get operation is defined as before. Application of view updates to view states and to source states is defined as follows. s ↓ [] =df v s ↓ ((b, c) :: p) =df (λb0 . if b0 = b then max (0, s b0 + c) else s b0 ) ↓ p pput (s0 , []) =df v pput (s0 , (b, c) :: p) =df 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 definition 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 significance 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), define 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 first 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 difference 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 defined by D0 X =df S × X ε0X (s, x) =df x 0 δX (s, x) =df (s, (s, x)) Given a monoid (P, o, ⊕), we have the cowriter comonad defined by D1 X =df P ⇒ X ε1X v =df v o 1 δX 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 Dependently-Typed Update Lenses 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 fixes 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), 1 We 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) satisfying s ↓ os = s s ↓ (p ⊕s p0 ) = (s ↓ p) ↓ p0 p ⊕s os↓p = p os ⊕s p = p (p ⊕s p ) ⊕s p00 = p ⊕s (p0 ⊕s↓p p00 ) 0 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 ) defines 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 defined 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 defined 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 defined 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. We are ready to define dependently-typed update lenses. 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 get (pput (s0 , p)) = get s0 ↓ p s0 = pput (s0 , oget s0 ) pput (pput (s0 , p), p0 ) = pput (s0 , p ⊕get s0 p0 ) Again the only difference from the simply-typed concept of the previous section is the presence of minor arguments and dependent typing. But exactly this difference makes the idea of updates enabled in a state work. Consider again the picture from the previous section. It is still valid. get !) s0 s p ↓ pput  {   s00 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 1st equation asserts that it does so. We can modify the bookshop example from the previous section as follows to obtain a dependently-typed update lens. We define P as an inductive family by the rules sb + c ≥ 0 p : P (λb0 . if b0 = b then s b0 + c else s b0 ) [] : P s (b, c) :: p : P s The operations o and ⊕ remain defined essentially as before. Also ↓ and pput can be defined 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 . Let us now compare state-based and update lenses. Any set S can be canonically extended into a directed container S ∗ =df (S, P, ↓, o, ⊕) by choosing 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 different 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 Update-Update Lenses In update lenses, we have first-class view updates, but no dedicated source updates. Instead, view updates double as source updates. This restriction can be lifted. We now proceed to the third type of lens of this paper, that we call update-update lenses. In an update-update lens, we have both view updates and source updates. Simulation means finding, 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 defining 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 o0s0 = qs0 ot s0 qs0 p ⊕0s0 qs0 ↓0 qs0 p p0 = qs0 (p ⊕t s0 p0 ) A morphism (t, q) between containers (S0 , P0 ) and (S, P ) defines a natural transformation Jt, qKc =df τ between their interpretations JS0 , P0 Kc =df D0 and JS, P Kc =df D (the interpretation of (t, q)) by τX (s0 , v) =df (t s0 , λp. v (qs0 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 , ⊕0 Kdc =df (D0 , ε0 , δ0 ) and JS, P, ↓, o, ⊕Kdc =df (D, ε, δ); we define 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 mor- phisms 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 different. They turn out to map to what Aguiar [Agu97] termed cofunctors, but with the source and target categories switched. We give the definition. A cofunctor between small categories (S, P̄ , src, tgt, id, ;) and (S0 , P̄0 , 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) → P̄0 (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 differences 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 defined 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 fixed 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 first case, we consider small categories and cofunctors, in the second case, small categories and functors.) We are all set to define update-update lenses. 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 o0s0 = pbwds0 oget s0 pbwds0 p ⊕0s0 pbwds0 ↓0 pbwds p p0 = pbwds0 (p ⊕get s0 p0 ) 0 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. get !) s0 s rz pbwd ↓0 p0 p ↓     s00 s0 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 source state s00 =df s0 ↓0 p0 and this is stipulated by the 1st equation. There are a many ways to modify the bookshop example to yield an update-update lens. Recall that in the previous sections we had S0 =df book ⇒ N × N and S =df book ⇒ N, with a source state associating to every book a price and quantity, and a view state only a price. Here are some possibilities. (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 [] =df λb0 . (0, 0) pbwd ((b, c) :: p) =df λ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 × Z<0 )∗ , so a view update is a sequence of book and negative price change pairs. pbwd remains essentially as in (i). Directed container theory tells us that update-update lenses between (S0 , P0 , ↓0 , o0 , ⊕0 ) and (S, P, ↓, o, ⊕) are in a bijection with the comonad morphisms between the corresponding two coupdate comonads. There no characterization of update-update lenses with comonad coalgebras similar to those of state-based lenses or update lenses, because the first comonad is a coupdate comonad and not a costate comonad. 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 S0∗ and (S, P, ↓, o, ⊕). In this way, update lenses are a special case of update-update lenses. 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 We then have the update-update lens (get, pbwd) where pbwds0 p =df p. This construction substantiates the intuition that, in an update lens, view updates double as source updates. 6 Comparison to Delta Lenses and Category Lenses Let us compare very briefly 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 difference 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 definitions 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 ↓0 p0 p00 = pfwds0 (p0 ⊕0s0 p00 ) get (s0 ↓0 pbwds0 p) = get s0 ↓ p o0s0 = pbwds0 oget s0 pbwds0 p ⊕0s0 pbwds0 ↓0 pbwds p p0 = pbwds0 (p ⊕get s0 p0 ) 0 pfwds0 (pbwds0 p) = p (The 2nd and 4th equation here are in fact derivable from the others.) It is immediate from this definition, 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 fill : Π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 pbwds0 p ⊕0s0 fills0 ,p (p0 , p0 ) = p0 pfwds0 ↓0 pbwds p (fills0 ,p (p0 , p0 )) = p0 0 fills0 ,p (pbwds0 p, oget s0 ↓p ) = o0s0 ↓0 pbwds p 0 fills0 ,p (p0 ⊕0s0 p00 , p0 ⊕get s0 ↓p pfwds0 ↓p0 p00 ) = fills0 ,p (p0 , p0 ) ⊕0s0 ↓0 pbwds p p00 0 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 fills0 ,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 update- update 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 , s00 , we have s0 ↓0 s00 = s00 , we must also have get s0 ↓ pfwds0 s00 = get s00 . But there may well exist 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 charac- terizations as comonad morphisms. We do not know whether something similar is also achievable for delta or category lenses. 7 Related Work 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 different strands of study developed and cross-fertilized. State-based lenses were introduced by Foster et al. [F+07]. Two finer concepts of lens relying on first-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 different types of asymmetric lens to Hofmann et al.’s [HPW12] on (symmetric) edit lenses, Johnson and Rosebrugh [JR16] introduced a yet different variation, asymmetric edit lenses. Power and Shkaravska [PS04] and O’Connor [OCo11] were probably the first 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 Conclusion We hope to have demonstrated in this paper that both update lenses and update-update lenses are natural concepts. Both are fit 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 difference 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 differences, and argued that update-update lenses have both practical and theoretical advantages. Acknowledgements Tarmo Uustalu is grateful to Michael Johnson and Paul-André Melliès for discussions. This research was supported by the Estonian Ministry of Education and Research institutional research grant No. IUT33-13. References [AAG05] M. Abbott, T. Altenkirch, N. Ghani. Containers: constructing strictly positive types. Theor. Comput. Sci., v. 342, n. 1, pp. 3–27, 2005. doi: 10.1016/j.tcs.2005.06.002 [Agu97] M. Aguiar. Internal Categories and Quantum Groups. Cornell University, 1997. http://www.math. cornell.edu/~maguiar/thesis2.pdf [ACU14] D. Ahman, J. Chapman, T. Uustalu. When is a container a comonad? Log. Methods in Comput. Sci., v. 10, n. 3, article 14, 2014. doi: 10.2168/lmcs-10(3:14)2014 [AU14a] D. Ahman, T. Uustalu. Coalgebraic update lenses. In B. Jacobs, A. Silva, S. Staton, eds., Proc. of 30th Conf. on Mathematical Foundations of Programming Semantics, MFPS XXX (Ithaca, NY, June 2014), v. 308 of Electron. Notes in Theor. Comput. Sci., pp. 25–48. Elsevier, 2014. doi: 10.1016/j.entcs.2014.10.003 [AU14b] D. Ahman, T. Uustalu. Update monads: cointerpreting directed containers. In R. Matthes, A. Schubert, eds., Proc. of 19th Conf. on Types for Proofs and Programs, TYPES 2013 (Toulouse, Apr. 2013), v. 26 of Leibniz Int. Proc. in Inform., pp. 1–23. Dagstuhl Publishing, 2014. doi: 10.4230/lipics.types.2013.1 [AU16] D. Ahman, T. Uustalu. Directed containers as categories. In R. Atkey, N. Krishnaswami, eds., Proc. of 6th Wksh. on Mathematically Structured Functional Programming, MSFP 2016 (Eindhoven, April 2016), v. 207 of Electron. Proc. in Theor. Comput. Sci., pp. 89–98. Open Publishing Assoc., 2016. doi: 10.4204/eptcs.207.5 [DXC11] Z. Diskin, Y. Xiong, K. Czarnecki. From state- to delta-based bidirectional model transformations: the asymmetric ase. J. of Object Technol., v. 10, article 6, 2011. doi: 10.5381/jot.2011.10.1.a6 [F+07] J. N. Foster, M. B. Greenwald, J. T. Moore, B. C. Pierce, A. Schmitt. Combinators for bidirectional tree transformations: a linguistic approach to the view-update problem. ACM Trans. on Program. Lang. and Syst., v. 29, n. 3, article 17, 2007. doi: 10.1145/1232420.1232424 [GJ12] J. Gibbons, M. Johnson. Relating algebraic and coalgebraic descriptions of lenses. In F. Hermann, J. Voigtländer, eds., Proc. of 1st Int. Wksh. on Bidirectional Transformations, BX 2012 (Tallinn, March 2012), v. 49 of Electron. Commun. of EASST, 16 pp. 2012. doi: 10.14279/tuj.eceasst.49.726 [HPW12] M. Hofmann, B. C. Pierce, D. Wagner. Edit lenses. In Proc. of 39th ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, POPL ’12 (Philadelphia, PA, Jan. 2012), pp. 495–508. ACM, 2012. doi: 10.1145/2103621.2103715 [JR13] M. Johnson, R. Rosebrugh. Delta lenses and opfibrations. 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 [JR16] M. Johnson, R. Rosebrugh. Unifying set-based, delta-based and edit-based lenses. In A. Anjorin, J. Gib- bons, 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 [JRW10] M. Johnson, R. Rosebrugh, R. J. Wood. Algebras and update strategies. J. of Univ. Comput. Sci., v. 16, n. 5, pp. 729–748. doi: 10.3217/jucs-016-05-0729 [JRW12] M. Johnson, R. Rosebrugh, R. J. Wood. Lenses, fibrations and universal translation. Math. Struct. in Comput. Sci., v. 22, n. 1, pp. 25–42, 2012. doi: 10.1017/s0960129511000442 [McK16] J. McKinna. Bidirectional transformations are proof-relevant bisimulations. Extended abstract pre- sented at 2016 ACM SIGPLAN Wksh. on Type-Driven Development, TyDe ’16 (Nara, Japan 2016). [OCo11] R. O’Connor. Functor is to lens as applicative is to biplate: introducing multiplate. arXiv preprint 1103.2841, 2011. (Paper presented at 2011 ACM SIGPLAN Wksh. on Generic Programming, WGP ’11, Tokyo, Sept. 2011.) https://arxiv.org/abs/1103.2841 [PS04] J. Power, O. Shkaravska. From comodels to coalgebras: state and arrays. In J. Adámek, S. Milius, eds., Proc. of 7th Int. Wksh. on Coalgebraic Methods in Computer Science, CMCS ’04 (Barcelona, March 2004), v. 106 of Electron. Notes in Theor. Comput. Sci., pp. 297–314. Elsevier, 2004. doi: 10.1016/j.entcs.2004.02.041 A Comonads, coalgebras of comonads, comonad morphisms For reference only, we recapitulate the definitions 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 D FFF / D · D / D·D δ δ D FFF D FFFF FFFF FFFF FFFF δ FFFF FFFF ε·D δ δ·D  FFF FFF    D·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 C DDD / D C / DC γ γ C DDDD DDDD DDDD εC γ δC D    C DC Dγ / D (D C) 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 D τ / D0 D τ / D0 ε ε0 δ δ0     Id Id D·D / D0 · D0 τ ·τ commute. B Coalgebras of a comonad vs morphisms from costate comonads 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 define a family of maps γ with components γ X : DS0 X → D X by γ X (s0 , v) =df D v (γ s0 ) γ is natural: for f : X → Y , we have 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 γ satisfies the laws of a comonad coalgebra structure: εX (γ X (s0 , v)) = εX (D v (γ s0 )) = v (εS0 (γ s0 )) = v s0 = εSX0 (s0 , v) δX (γ X (s0 , v)) = δX (D v (γ s0 )) = D (D v) (δS0 (γ s0 )) = D (D v) (D γ (γ s0 )) = D (D v ◦ γ) (γ s0 ) = D (λs00 . γ X (s00 , v)) (γ s0 )) = D γ X (D (λs00 . (s00 , v)) (γ s0 )) = D γ X (γ DS0 X (s0 , λs00 . (s00 , v)) S0 = D γ X (γ DS0 X (δX (s0 , v))) Given a comonad morphism τ , we define a map τ : S0 → D S0 by τ s0 =df τS0 (s0 , idS0 ) τ is a comonad coalgebra structure, because τ satisfies the comonad morphism laws: εS0 (τ s0 ) = εS0 (τS0 (s0 , idS0 )) = εSS00 (s0 , idS0 ) = s0 δ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. (γ) s0 = γ S0 (s0 , idS0 ) = D idS0 (γ s0 ) = γ s0 (τ )X (s0 , v) = D v (τ s0 ) = D v (τS0 (s0 , idS0 )) = τX (DS0 v (s0 , idS0 )) = τX (s0 , v)  C Cofunctors and opfibrations We recapitulate the definitions of a cofunctor in the sense of Aguiar [Agu97] and an opfibration (to be precise, an opfibration 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 : |C| → |D|, 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 k 0 : X → Y 0 of C and any map g : F Y → F Y 0 of D such that F k 0 = g ◦ F k, there exists a unique map ` : Y → Y 0 such that k 0 = ` ◦ 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 definition of a cofunctor, F is just an object mapping. In the definition of an opcleavage, F is a functor. Notice also that lifts in an opcleavage are required to be opCartesian.