=Paper=
{{Paper
|id=Vol-2999/bxpaper2
|storemode=property
|title=Delta Lenses as Coalgebras for a Comonad
|pdfUrl=https://ceur-ws.org/Vol-2999/bxpaper2.pdf
|volume=Vol-2999
|authors=Bryce Clarke
|dblpUrl=https://dblp.org/rec/conf/staf/Clarke21
}}
==Delta Lenses as Coalgebras for a Comonad==
https://ceur-ws.org/Vol-2999/bxpaper2.pdf
Delta lenses as coalgebras for a comonad
Bryce Clarke
Centre of Australian Category Theory, Macquarie University, Sydney, Australia
Abstract
Delta lenses are a kind of morphism between categories which are used to model bidirectional trans-
formations between systems. Classical state-based lenses, also known as very well-behaved lenses, are
both algebras for a monad and coalgebras for a comonad. Delta lenses generalise state-based lenses, and
while delta lenses have been characterised as certain algebras for a semi-monad, it is natural to ask if
they also arise as coalgebras.
This short paper establishes that delta lenses are coalgebras for a comonad, through showing that
the forgetful functor from the category of delta lenses over a base, to the category of cofunctors over
a base, is comonadic. The proof utilises a diagrammatic approach to delta lenses, and clarifies several
results in the literature concerning the relationship between delta lenses and cofunctors. Interestingly,
while this work does not generalise the corresponding result for state-based lenses, it does provide new
avenues for exploring lenses as coalgebras.
Keywords
delta lens, cofunctor, coalgebra, bidirectional transformation
1. Introduction
The goal of understanding various kinds of lenses as mathematical structures has been an
ongoing program in the study of bidirectional transformations. For example, very well-behaved
lenses [1], also known as state-based lenses [2], have been understood as both algebras for a
monad [3] and coalgebras for a comonad [4, 5]. A generalisation of state-based lenses called
category lenses [6] were also introduced as algebras for a monad, based on classical work in
2-category theory on split opfibrations [7]. Another kind of lens between categories called a
delta lens [8] was shown to be a certain algebra for a semi-monad [9], however it remained
open as to whether delta lenses could also be characterised as (co)algebras for a (co)monad.
The purpose of this short paper is to characterise delta lenses as coalgebras for a comonad
(Theorem 9). The proof of this simple result builds upon and clarifies several recent advances in
the theory of delta lenses.
In 2017, Ahman and Uustalu introduced update-update lenses [2] as morphisms of directed
containers [10], which are equivalent to certain morphisms called cofunctors between categories
[11]. In the same paper, they show explicitly how, using the notation of directed containers,
delta lenses may be understood as cofunctors with additional structure.
In earlier work [12] from 2016, Ahman and Uustalu also provide a construction on morphisms
of directed containers which yields a split pre-opcleavage for a functor; in other words, they
Bx 2021: 9th International Workshop on Bidirectional Transformations, part of STAF, June 21, 2021
" bryce.clarke1@hdr.mq.edu.au (B. Clarke)
0000-0003-0579-2804 (B. Clarke)
Β© 2021 Copyright for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0).
CEUR
Workshop
Proceedings
http://ceur-ws.org
ISSN 1613-0073
CEUR Workshop Proceedings (CEUR-WS.org)
show how cofunctors may be turned into delta lenses. We show that this construction is actually
a right adjoint to the forgetful functor from delta lenses to cofunctors (Lemma 8), and that the
coalgebras for the comonad generated from this adjunction are delta lenses (Theorem 9).
In 2020, a diagrammatic characterisation of delta lenses was introduced by the current author
[13], building upon an earlier characterisation of cofunctors as spans [14]. This diagrammatic
approach is utilised throughout this paper, and leads to another simple characterisation of delta
lenses (Proposition 6).
Overview of the paper and related work
This section provides an informal overview of the paper, together with further commentary
on the background, and references to related work. The goal is to provide a conceptual under-
standing of the results; later sections will be dedicated to the formal mathematics.
Section 2 contains the mathematical background required for the main results, which are
presented in Section 3. Consequences of the main result and concluding remarks are in Section 4.
Throughout the paper we make the assumption that a system, whatever that may be, can be
understood as a category. The objects of this category are the states of the system, while the
morphisms are the transitions (or deltas) between system states.
Delta lenses were introduced in [8, Definition 4] to model bidirectional transformations
between systems when they are understood as categories. The Get of a delta lens is a functor
π : π΄ β π΅ from the source category π΄ to the view category π΅, while the Put is a certain kind
of function (that this paper calls a lifting operation) satisfying axioms analogous to the classical
lens laws. A slightly modified definition of delta lens appeared in [9, Definition 1], however this
definition still seemed to be ad hoc, and made it difficult to prove deep results without checking
many details.
The definition of delta lens (Definition 4) given in this paper is based on a diagrammatic
characterisation which first appeared in [13, Corollary 20], by representing the Put in terms
of bijective-on-objects functors (Definition 1) and discrete opfibrations (Definition 2). This
diagrammatic approach provides a natural framework for studying delta lenses using category
theory, and has the benefit of allowing for very simple (albeit more abstract) proofs. This
approach will be utilised throughout this paper, although in many places we will also include
explicit descriptions of constructions using the traditional definition of a delta lens.
A key idea presented in [2, 13] is that the Get and Put of a delta lens can be separated into
functors and cofunctors (Definition 3), respectively. Intuitively, a cofunctor can be understood
as a delta lens without any information on how the Get acts on morphisms; it is the minimum
amount of structure needed to specify a Put operation between categories. It was shown in the
paper [2] that delta lenses are cofunctors with additional structure. In this paper, we aim to
show that said structure arises coalgebraically via a comonad.
Both delta lenses and cofunctors are predominantly understood and studied as morphisms
between categories, however to prove that delta lenses are cofunctors equipped with coalgebraic
structure, it is necessary for them to be understood as objects. Therefore this paper introduces a
new category Cof(π΅), whose objects are cofunctors into a fixed category π΅ (Definition 5). The
category Lens(π΅), whose objects are delta lenses into a fixed category π΅, was previously studied
in [15, 16]. Surprisingly, we show that the category Lens(π΅) can be defined (Definition 7) as
the slice category Cof(π΅)/1π΅ . Not only does this provide a new characterisation of delta lenses
in term of cofunctors (Proposition 6), but also provides the insight that the canonical forgetful
functor πΏ : Lens(π΅) β Cof(π΅), which takes a delta lens to its underlying Put cofunctor, is a
projection from a slice category.
Finally, proving that delta lenses are coalgebras for a comonad on Cof(π΅) amounts to showing
that the forgetful functor πΏ : Lens(π΅) β Cof(π΅) is comonadic (Theorem 9). A necessary
condition is that πΏ has a right adjoint π
(Lemma 8), which constructs the cofree delta lens
from each cofunctor in Cof(π΅). This construction first appeared explicitly in [12, Section 3.2],
however it was not obviously a right adjoint β or even a functor β and it was disconnected from
the context of cofunctors and delta lenses. Both Lemma 8 and Theorem 9 admit straightforward
proofs, with the benefit of the diagrammatic approach to cofunctors and delta lenses.
Notation and conventions
This section outlines some of the notation and conventions used in the paper. Given a category π΄,
its underlying set (or discrete category) of objects is denoted π΄0 . Given a functor π : π΄ β π΅,
its underlying object assignment is denoted π0 : π΄0 β π΅0 . Similarly, a cofunctor π : π΄ β π΅
will have an underlying object assignment π0 : π΄0 β π΅0 . Thus the orientation of a cofunctor
agrees with the orientation of its underlying object assignment (this convention is chosen to
agree with the orientation of delta lenses, however this choice is not uniform in the literature
on cofunctors). The operation cod sends each morphism to its codomain or target object.
2. Prerequisites for the main result
We first recall two special classes of functors, which we will use as the building blocks for
defining cofunctors and delta lenses. New contributions in this section include the category
Cof(π΅) whose objects are cofunctors (Definition 5), and the characterisation of delta lenses as
certain morphisms therein (Proposition 6).
Definition 1. A functor π : π΄ β π΅ is bijective-on-objects if its underlying object assignment
π0 : π΄0 β π΅0 is a bijection.
Definition 2. A functor π : π΄ β π΅ is a discrete opfibration if for all pairs,
(π β π΄, π’ : π π β π β π΅)
there exists a unique morphism π€ : π β πβ² in π΄ such that π π€ = π’.
Definition 3. A cofunctor π : π΄ β π΅ between categories is a span of functors,
π
π π
(1)
π΄ π΅
where π is a bijective-on-objects functor and π is a discrete opfibration.
Alternatively, a cofunctor π : π΄ β π΅ consists of a function π0 : π΄0 β π΅0 , together with
a lifting operation π, which assigns each pair (π β π΄, π’ : π0 π β π β π΅) to a morphism
π(π, π’) : π β πβ² in π΄, such that the following axioms are satisfied:
(οΈ )οΈ
(1) π0 cod π(π, π’) = cod(π’);
(2) π(π, 1π0 π ) = 1π ;
(3) π(π, π£ β π’) = π(πβ² , π£) β π(π, π’), where πβ² = cod π(π, π’) .
(οΈ )οΈ
Definition 4. A delta lens (π, π) : π΄ β π΅ between categories is a commutative diagram of
functors,
π
π π
(2)
π΄ π
π΅
where π is a bijective-on-objects functor and π is a discrete opfibration.
We can also describe a delta lens (π, π) : π΄ β π΅ as consisting of a functor π : π΄ β π΅
together with a lifting operation π, which assigns each pair (π β π΄, π’ : π π β π β π΅) to a
morphism π(π, π’) : π β πβ² in π΄, such that the following axioms are satisfied:
(1) π π(π, π’) = π’;
(2) π(π, 1π π ) = 1π ;
(3) π(π, π£ β π’) = π(πβ² , π£) β π(π, π’), where πβ² = cod π(π, π’) .
(οΈ )οΈ
Every delta lens (π, π) : π΄ β π΅ has an underlying functor π : π΄ β π΅ and an underlying
cofunctor π : π΄ β π΅, and their corresponding underlying object assignments are equal; that is,
π0 = π0 .
Definition 5. For each category π΅, there is a category Cof(π΅) of cofunctors over the base π΅
whose objects are cofunctors with codomain π΅, and whose morphisms are given by commutative
diagrams of functors of the form:
β
π΄ πΆ
π πΎ
β (3)
π π
π πΎ
π΅
Equivalently, a morphism in Cof(π΅) from a cofunctor π : π΄ β π΅ to a cofunctor πΎ : πΆ β π΅
consists of a functor β : π΄ β πΆ such that πΎ0 βπ = π0 π for all π β π΄, and βπ(π, π’) = πΎ(βπ, π’)
for all pairs (π β π΄, π’ : π0 π β π β π΅). The functor β : π β π is then uniquely induced from
this data. Intuitively, if π΄ and πΆ are understood as source categories with a fixed view category
π΅, then the morphisms in Cof(π΅) are functors between the source categories which preserve
the chosen lifts, given by the corresponding cofunctors, from the view category.
Proposition 6. Every delta lens (π, π) : π΄ β π΅ is equivalent to a morphism in Cof(π΅) whose
codomain is the trivial cofunctor on π΅.
Proof. Consider the morphism in Cof(π΅) given by the commutative diagram of functors:
π
π΄ π΅
π 1π΅
π (4)
π π΅
π 1π΅
π΅
The upper commutative square describes a delta lens as given in Definition 4. Conversely, every
delta lens may be depicted as a morphism in Cof(π΅) in this way.
We can unpack (4) using the explicit characterisation of morphisms in Cof(π΅) to obtain the
precise difference between cofunctors and delta lenses, in terms of objects and morphisms.
Namely, the diagram (4) states that a delta lens corresponds to a cofunctor π : π΄ β π΅ together
with a functor π : π΄ β π΅ such that π π = π0 π for all π β π΄, and π π(π, π’) = π’ for all pairs
(π β π΄, π’ : π π β π β π΅).
Definition 7. For each category π΅, we define the category of delta lenses over the base π΅ to be
the slice category Lens(π΅) := Cof(π΅) / 1π΅ , where 1π΅ is the trivial cofunctor on π΅.
By Proposition 6, the objects of Lens(π΅) are delta lenses with codomain π΅, represented as a
morphism into the trivial cofunctor as shown in (4). The morphisms in Lens(π΅) are given by
morphisms (3) in Cof(π΅) such that the following pasting condition holds:
β π π
π΄ πΆ π΅ π΄ π΅
π πΎ 1π΅ π 1π΅
β πΎ = π (5)
π π π΅ π π΅
πΎ
π 1π΅ π 1π΅
π΅ π΅
In other words, the only additional requirement on a morphism β : π΄ β πΆ between delta lenses
over π΅, compared to a morphism between cofunctors over π΅, is that π β β = π . This is opposed
to just requiring πΎ0 βπ = π0 π on objects (where recall for delta lenses, the underlying object
assignments for the functor and cofunctor are equal, that is, π0 = πΎ0 and π0 = π0 ).
There is a canonical forgetful functor,
πΏ : Lens(π΅) ββ Cof(π΅)
which assigns every delta lens to its underlying cofunctor. This forgetful functor is the focus of
the main result in the following section.
3. Main result
While not every cofunctor may be given the structure of a delta lens, Ahman and Uustalu [12]
developed a method which constructs a delta lens from any cofunctor. To understand their
construction, first recall that the underlying objects functor (β)0 : Cat β Set has a right adjoint
(β)
ΜοΈ : Set β Cat which takes each set π to the codiscrete category π. ΜοΈ
Given a cofunctor π : π΄ β π΅ with underlying object assignment π0 : π΄0 β π΅0 , we may
construct the following pullback in Cat:
π
ππ΄ ππ΅
β
π΄ π΅ (6)
ΜοΈ0 β ππ΄
π ππ΅
π΅
ΜοΈ0
Here ππ΅ : π΅ β π΅ ΜοΈ0 is the component of the unit for the adjunction at π΅, and π ΜοΈ0 β ππ΄ the
component of the unit at π΄ followed by image of π0 under the right adjoint. Using the universal
property of the pullback, we have the following:
π
π β¨π,πβ© π
π
ππ΄ ππ΅ (7)
β
π΄ π΅
ΜοΈ0 β ππ΄
π ππ΅
π΅
ΜοΈ0
Since ππ΅ is bijective-on-objects, the projection functor ππ΄ is also bijective-on-objects which,
together with the functor π, implies that β¨π, πβ© : π β π is bijective-on-objects, due to the
properties of bijections at the level of objects. Thus, the upper right triangle in (7) defines a
delta lens π β π΅.
The category π has the same objects as π΄, but morphisms π β πβ² in π are given by pairs
of the form (π€ : π β πβ² β π΄, π’ : π0 π β π0 πβ² β π΅). The functor ππ΅ : π β π΅ projects to
the second arrow in this pair. The lifting operation which makes this functor into a delta lens
is induced by the lifting operation of the original )οΈ π β π and a
cofunctor; it takes an object
morphism π’ : π0 π β π β π΅ to the morphism π(π, π’) : π β πβ² , π’ : π0 π β π in π .
(οΈ
We now show that this construction due to Ahman and Uustalu is universal, in the sense
that it provides a right adjoint to the functor taking a delta lens to its underlying cofunctor.
Lemma 8. The forgetful functor πΏ : Lens(π΅) β Cof(π΅) has a right adjoint.
Proof. Using the construction in (7), define the functor π
: Cof(π΅) β Lens(π΅) by the assign-
ment:
π π
π π β¨π,πβ© π
β¦ββ (8)
π΄ π΅ π ππ΅ π΅
We describe the components of the unit and counit for the adjunction πΏ β£ π
and omit the
detailed checks that the triangle identities hold.
Given a cofunctor π : π΄ β π΅ the component of the counit is given by:
ππ΄
π π΄
β¨π,πβ© π
π π (9)
π π
π΅
Given a delta lens (π, π) : π΄ β π΅ the component of the unit is given by:
β¨1π΄ ,π β© ππ΅ π
π΄ π π΅ π΄ π΅
π β¨π,πβ© 1π΅ π 1π΅
π = π (10)
π π π΅ π π΅
π
π 1π΅ π 1π΅
π΅ π΅
The above diagrams show that the pasting condition required in (5) is satisfied.
Theorem 9. The forgetful functor πΏ : Lens(π΅) β Cof(π΅) is comonadic.
Proof. By Lemma 8, the functor πΏ has a right adjoint π
. To prove that πΏ is comonadic, it remains
to show that the category of coalgebras for the induced comonad πΏπ
on Cof(π΅) is equivalent
to Lens(π΅).
Given a cofunctor π : π΄ β π΅, a coalgebra structure map is given by a morphism in Cof(π΅)
of the form:
β
π΄ π
π β¨π,πβ©
β (11)
π π
π π
π΅
However compatibility with the counit forces β = 1π and β = β¨1π΄ , π β©, where π : π΄ β π΅ is a
functor such that π β π = π. Compatibility with the comultiplication doesnβt add any further
conditions. Therefore, a coalgebra for the comonad πΏπ
on Cof(π΅) is equivalent to a delta lens
(π, π) : π΄ β π΅.
This theorem establishes the result stated in the title of the paper, that delta lenses (2) are
coalgebras (11) for a comonad.
4. Concluding remarks
In this paper, the category Lens(π΅) of delta lenses over the base π΅ was characterised as the
category of coalgebras for a comonad on the category Cof(π΅) of cofunctors over the base π΅. This
brings together recent results in the study of delta lenses and cofunctors. In particular, we have
shown that the extra structure on cofunctors given in Ahman and Uustaluβs [2] characterisation
of delta lenses is coalgebraic, and that their construction of a delta lens from cofunctor in the
paper [12] is precisely the cofree delta lens on a cofunctor. Throughout we have also shown
how the abstract diagrammatic approach to delta lenses, first introduced in [13], has led to
concise proofs of these results, and offers a clear perspective on the relationship between these
ideas.
Aside from clarification and development of theory, the results presented in this paper have
several other mathematical consequences. For example, the functor πΏ : Lens(π΅) β Cof(π΅)
creates all colimits which exist in Cof(π΅). Thus we can take the coproduct of a pair of cofunctors
in Cof(π΅), and automatically know how to construct the coproduct of the corresponding delta
lenses in Lens(π΅).
Another consequence from the unit (10) of the adjunction between Cof(π΅) and Lens(π΅) is
that every delta lens factorises into a bijective-on-objects functor followed by a cofree lens.
Intuitively, this allows us to first pair every transition in the source category π΄ with a transition
in the view category π΅ via the functor part π : π΄ β π΅ of the delta lens,
π€ : π β πβ² β π΄ β¦ββ (π€ : π β πβ² β π΄, π π€ : π π β π πβ² β π΅)
then consider the update propagation determined by the cofunctor part π : π΄ β π΅ of the
delta lens. The cofree delta lens on a cofunctor behaves much like an analogue of constant
complement state-based lenses, except that the complement is with respect to morphisms rather
than objects.
While the main contributions of this paper are mathematical, it is hoped that these results
also prompt new ways of understanding delta lenses. For example, previously state-based lenses
have been considered from a βPut-basedβ perspective [17, 18], however this approach could
also be adapted to the setting of delta lenses. Rather than starting with a Get functor between
systems and then asking how we might construct a delta lens, we might instead start with a
Put cofunctor and then ask for ways in which this can be given the structure of a delta lens.
This shift of focus is subtle but important, especially in the context of the ideas in [2], as it
is arguably the Put structure (rather than the Get structure) which is central to the study of
bidirectional transformations and lenses.
On an separate note, it is worth remarking on the similarity between the main result of
this paper and the classical result stating that very well-behaved lenses are coalgebras for a
comonad [4, 5]. Despite the clear analogy between them, and the inspiration that this paper
derives from the classical result, it seems that they are unrelated at a mathematical level. The
classical result relies on Set being a cartesian closed category, and arises from the adjunction
(β) Γ π΅ β£ [π΅, β], whereas the results in this paper arise from a different adjunction, and donβt
require any aspect of cartesian closure.
There are many questions to be explored in future work. For instance, it is natural to ask if
Lens(π΅) is comonadic over other categories (such as Cat as was suggested by an anonymous
reviewer), or if split opfibrations (also known as c-lenses [6]) are also comonadic over Cof(π΅).
In recent work by the current author, it has been demonstrated that delta lenses arise as algebras
for a monad on Cat/π΅, providing a dual to the main result of this paper and strengthening the
previous work of Johnson and Rosebrugh [9]. Finally, given the importance of the category
Lens(π΅) in the study of symmetric lenses [15, 16], it is also hoped that the coalgebraic perspective
provides new insights into this area, and this will be the subject of further investigation.
Acknowledgments
The author would like to thank Michael Johnson for his feedback on this work, the anonymous
reviewers of this paper for their helpful comments, and the audience of the Bx2021 workshop
for their insightful questions. The author also thanks Eli Hazel and Giacomo Tendas for their
suggestions which improved the final version of this paper. The author is grateful for the
support of the Australian Government Research Training Program Scholarship.
References
[1] 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 Transactions on Programming Languages and Systems 29 (2007) 1β65. doi:10.1145/
1232420.1232424.
[2] D. Ahman, T. Uustalu, Taking updates seriously, in: Proceedings of the 6th International
Workshop on Bidirectional Transformations, volume 1827 of CEUR Workshop Proceedings,
2017, pp. 59β73. URL: http://ceur-ws.org/Vol-1827/paper11.pdf.
[3] M. Johnson, R. Rosebrugh, R. Wood, Algebras and update strategies, Journal of Universal
Computer Science 16 (2010) 729β748. doi:10.3217/jucs-016-05-0729.
[4] R. OβConnor, Functor is to lens as applicative is to biplate: Introducing multiplate, 2011.
arXiv:1103.2841.
[5] J. Gibbons, M. Johnson, Relating algebraic and coalgebraic descriptions of lenses, in: Pro-
ceedings of the First International Workshop on Bidirectional Transformations, volume 49
of Electronic Communications of the EASST, 2012, pp. 1β16. doi:10.14279/tuj.eceasst.
49.726.
[6] M. Johnson, R. Rosebrugh, R. Wood, Lenses, fibrations and universal transla-
tions, Mathematical Structures in Computer Science 22 (2012) 25β42. doi:10.1017/
S0960129511000442.
[7] R. Street, Fibrations and Yonedaβs lemma in a 2-category, in: Category Seminar, volume
420 of Lecture Notes in Mathematics, 1974, pp. 104β133. doi:10.1007/BFb0063102.
[8] Z. Diskin, Y. Xiong, K. Czarnecki, From state- to delta-based bidirectional model
transformations: the asymmetric case, Journal of Object Technology 10 (2011) 1β25.
doi:10.5381/jot.2011.10.1.a6.
[9] M. Johnson, R. Rosebrugh, Delta lenses and opfibrations, Electronic Communications of
the EASST 57 (2013) 1β18. doi:10.14279/tuj.eceasst.57.875.
[10] D. Ahman, J. Chapman, T. Uustalu, When is a container a comonad?, Logical Methods in
Computer Science 10 (2014) 1β48. doi:10.2168/LMCS-10(3:14)2014.
[11] M. Aguiar, Internal Categories and Quantum Groups, Ph.D. thesis, Cornell University,
1997.
[12] D. Ahman, T. Uustalu, Directed containers as categories, in: Proceedings 6th Workshop on
Mathematically Structured Functional Programming, volume 207 of Electronic Proceedings
in Theoretical Computer Science, 2016, pp. 89β98. doi:10.4204/EPTCS.207.5.
[13] B. Clarke, Internal lenses as functors and cofunctors, in: Applied Category Theory 2019,
volume 323 of Electronic Proceedings in Theoretical Computer Science, 2020, pp. 183β195.
doi:10.4204/EPTCS.323.13.
[14] P. J. Higgins, K. C. H. Mackenzie, Duality for base-changing morphisms of vector bundles,
modules, Lie algebroids and Poisson structures, Mathematical Proceedings of the Cam-
bridge Philosophical Society 114 (1993) 471β488. doi:10.1017/S0305004100071760.
[15] M. Johnson, R. Rosebrugh, Universal updates for symmetric lenses, in: Proceedings of
the 6th International Workshop on Bidirectional Transformations, volume 1827 of CEUR
Workshop Proceedings, 2017, pp. 39β53. URL: http://ceur-ws.org/Vol-1827/paper8.pdf.
[16] B. Clarke, A diagrammatic approach to symmetric lenses, in: Applied Category Theory
Conference 2020, volume 333 of Electronic Proceedings in Theoretical Computer Science,
2021, pp. 79β91. doi:10.4204/EPTCS.333.6.
[17] H. Pacheco, Z. Hu, S. Fischer, Monadic combinators for putback style bidirectional pro-
gramming, in: Proceedings of the ACM SIGPLAN 2014 Workshop on Partial Evaluation and
Program Manipulation, volume 333 of PEPM β14, 2014, pp. 39β50. doi:10.1145/2543728.
2543737.
[18] S. Fischer, Z. Hu, H. Pacheco, The essence of bidirectional programming, Science China
Information Sciences 58 (2015) 1β21. doi:10.1007/s11432-015-5316-8.