=Paper=
{{Paper
|id=Vol-1827/paper11
|storemode=property
|title=Taking Updates Seriously
|pdfUrl=https://ceur-ws.org/Vol-1827/paper11.pdf
|volume=Vol-1827
|authors=Danel Ahman,Tarmo Uustalu
|dblpUrl=https://dblp.org/rec/conf/etaps/AhmanU17
}}
==Taking Updates Seriously==
https://ceur-ws.org/Vol-1827/paper11.pdf
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.