日本ソフトウェア科学会第 30 回大会 (2013 年度) 講演論文集

A Type Class for Bidirectionalization
Or, a Light-Weight Approach to the View-Update Problem

Kazutaka Matsuda

Meng Wang

A bidirectional transformation is a pair of mappings between source and view data objects, one in each direction. When the view is modified, the source is updated accordingly with respect to some laws. Over theyears, a lot of eﬀort has been made to oﬀer better language support for programming such transformations.
In particular, a technique known as bidirectionalization is able to analyze and transform unidirectional
programs written in general purpose languages, and “bidirectionalize” them.
Among others, a technique termed as semantic bidirectionalization proposed by Voigtländer stands out
in term of user-friendliness. The unidirectional program can be written using arbitrary language constructs,
as long as the function is polymorphic and the language constructs respect parametricity. The free theorems
that follow from the polymorphic type of the program allow a kind of forensic examination of the transformation, determining its eﬀect without examining its implementation. This is convenient, in the sense thatthe programmer is not restricted to using a particular syntax; but it does require the transformation to bepolymorphic.
In this paper, we lift this polymorphism requirement to improve the applicability of semantic bidirectionalization. Concretely, we provide a type class PackM γ α µ, which intuitively reads “a concrete datatype γ
is abstracted to a type α, and the ‘observations’ made by a transformation on values of type γ are recorded
by a monad µ”. With PackM , we turn monomorphic transformations into polymorphic ones, that are readyto be bidirectionalized. We demonstrate our technique with a case study of standard XML queries, whichwere considered beyond semantic bidirectionalization because of their monomorphic nature.

1 Introduction
Bidirectionality is a fundamental aspect of computing: transforming data from one format to another, and requiring a transformation in the opposite direction that is in some sense an inverse.
The most well-known instance is the view-update
problem [1] [5] from database design: a “view” represents a database computed from a source by aquery, and the problem comes when translating an
update of the view back to a “corresponding” update on the source.
Let us consider a (simplified version of)
双方向化のための型クラス、あるいはビュー更新問題への軽量なアプローチ
松田 一孝, 東京大学, The University of Tokyo.

Meng Wang, チャルマーズ工科大学, Chalmers University of Technology.
The international-conference version of this paper willappear in PPDP 2013

XML example taken from http://www.w3.org/TR/
xquery-use-cases/: a source (in Figure 1) can betransformed by query Q1 (in Figure 2) to produce
a view (Figure 3). Here the query Q1 is the “forward transformation”, and a corresponding “backward” transformation maps an updated view backto the source. For example, one may change thetitle TCP/IP Illustrated to TCP/IP Illustrated(second edition) in the view and expect thesource to be updated accordingly. Things are moreinteresting with the year of a publication: this attribute’s value is observed by the query in producing the view, so whatever changes to it shall not alter the existing observations. For example, we canchange the year for the first book to 2000, but not
to any value that is less than 1992. The backward
transformation is required to correctly register theformer valid change, but to reject the latter invalidone.
By dint of hard eﬀort, one can construct separately the forward transformation from source to<bib><book year="1994"><title>TCP/IP Illustrated</title><author>Stevens W.</author><publisher>Addison-Wesley</publisher><price>65.95</price></book><book year="1992"><title>Advanced Programming in the Unix environment</title><author>Stevens W.</author><publisher>Addison-Wesley</publisher><price>65.95</price></book><book year="2000"><title>Data on the Web</title><author>Abiteboul Serge</author><author>Buneman Peter</author><author>Suciu Dan</author><publisher>Morgan Kaufmann Publishers</publisher><price>39.95</price></book></bib>
Fig. 1An XML Source<bib>{
for $b indoc("http://example.com/bib.xml")/bib/bookwhere $b/publisher = "Addison-Wesley"
and $b/@year > 1991
return<book year="{ $b/@year }">{ $b/title }</book>}</bib>
Fig. 2<bib><book year="1994"><title>TCP/IP Illustrated</title></book><book year="1992"><title>Advanced Programming in the Unix environment</title></book></bib>
Fig. 3view together with the corresponding backward
transformation. However, this is a significant duplication of work, because the two transformations
are closely related. Moreover, it is prone to error, because they do really have to correspond witheach other to be bidirectional. And, even worse,
it introduces a maintenance issue, because changes
to one transformation entail matching changes tothe other. Therefore, a lot of work has gone intoways to reduce this duplication and the problems
it causes; in particular, there has been a recent
rise in linguistic (mostly functional) approaches tostreamlining bidirectional transformations—this isvery much a current problem.
Using terminologies advocated by the lens framework [6] that traces back to database research: theforward function is commonly known as get having
type S → V , and the backward one as put having
type S → V → S . The idea is that put, in addition to an updated view, takes the original source
as an input, so that get does not have to be bijective to have a backward semantics. The correctnessof the pair of functions is governed by the following
definitional properties [3]:Consistency

get s′ = v

Acceptability

put s (get s) = s

if

put s v = s′Query Q1

Result of Applying Q1 to the Source inFigure 1

Here consistency (also known as the PutGet
law [6]) roughly corresponds to right-invertibility,
basically ensuring that all updates on a view are
captured by the updated source (the change of year
to values less that 1992 in the above example violates this law), and acceptability (also known as
the GetPut law [6]) roughly corresponds to leftinvertibility, prohibiting changes to the source if noupdate has been made on the view. Bidirectionaltransformations satisfying the above two laws are
sometimes called well-behaved [6]. In additions tothese definitional properties, some desirable laws
such as composability and undoability are also discussed in the literature [1] [11].
The paradigm of bidirectional programming isabout constructing get in a bidirectional language
and expect a corresponding put to be created automatically. Very often, such languages are defined
as a collection of combinators which can be readin two ways [13] [6] [7] [2]: forward, as ordinary functions from source to view, and backward, from original source and updated view to updated source. A
disadvantage of the combinator-based approach isthat transformations have to be encoded in a some-what inconvenient programming style.
Other than creating special purpose bidirectional
languages, an alternative is to mechanically transform existing unidirectional programs to obtain abackward counterpart, a technique known as bidirectionalization [17]. Diﬀerent flavors of bidirectionalization have been proposed: syntactic [17],semantic [22], and a combination of the two [24].
Syntactic bidirectionalization inspects a get definition written in a somehow restricted syntactic
representation and synthesizes a definition for the
backward version. Semantic, or extensional, bidirectionalization on the other hand treats polymorphic get as an opaque semantic object, applying
the function independently to a collection of unique
identifiers, and the free theorem [25] arising fromparametricity [21] states that whatever happens tothose identifiers happens in the same way to any
other inputs—this information is suﬃcient to construct the backward transformation. (We will give
more details of the technique in Section 2.) Thisis convenient, in the sense that the programmer is
not confined to a certain (sometime awkward) syntactic representation; but it does require that thetransformation is polymorphic.
This polymorphism requirement has prevented
the use of semantic bidirectionalization in many applications, for example XML transformations where
queries are predominantly monomorphic. Consider
query Q1 we have seen earlier on (Figure 2). The
attribute value of year and content of publisher
are compared to constant values, which instantiates their types to monomorphic ones, and the creation of new element book is also beyond the reachof the existing techniques of semantic bidirectionalization [22] [24] because the possibility of creating
values of polymorphic types complicates the use of
free theorems.
In this paper, we propose a novel bidirectionalization approach that circumvents the polymorphism
restriction, and allows us to program and bidirectionalize monomorphic transformations in a convenient manner. At the heart of the technique is a
type class PackM that uses run-time logging to reinstate the applicability of free theorems amid thecreation of polymorphic elements, which in turnprovides a solution to the problem of comparison
with constant values.

class (Pack γ α, Monad µ) ⇒ PackM γ α µ where
liftO :: Eq β ⇒ ([γ] → β) → ([α] → µ β)class Pack γ α | α → γ where
new :: γ → α
Intuitively, a type class PackM encapsulates thefact that a concrete datatype γ is abstracted to a
type α, and the “observations” made by a transformation on values of type γ are recorded by a monadµ so that the information can be used to check thevalidity of updates. For example, in our librarythe equality comparison found in query Q1 can be
expressed by the following code fragment (the complete code can be found in Figure 4 in Section 6)
liftO2 (==) (label p) (tx "Addison-Wesley")In the above the constant "Addison-Wesley" isturned into a polymorphic value through the application of the function new , which does not instantiate the type, and the lifting operator liftO2 ,which is a specialized version of liftO, enables runtime logging of the equality comparison == througha monad. As a result, the backward transformation is able to reject any changes to the publishers
in the view to satisfy the consistency law.
The rest of the paper is organized as follows. In
Section 2, we firstly review the concept of semantic
bidirectionalization [22], and in Section 3, we describe our proposal and the handling of monomorphic transformations. In Section 4, we prove thecorrectness (consistency and acceptability) of ourapproach, based on the free theorems concerning type classes [23]. In Section 5, we discuss adatatype-generic implementation of our approach.
In Section 6, we revisit the XML example mentioned in this section and show how it is handled
by our technique. In Section 7, we review additional issues of bidirectionalization. In Section 8,
we discuss related work, and conclude in Section 9.
A prototype implementation of our framework
is available from https://bitbucket.org/kztk/
cheap-b18n, which also contains more examples.

2 The Essence of Semantic Bidirectionalization

As a preparation, we firstly introduce the basic
idea of semantic bidirectionalization [22]. Consider
that we are given a polymorphic function of type
∀α. [α] → [α]. Parametricity [21] asserts that thefunction can only drop or reorganize its input list
elements, without inspecting them or constructing
new ones. In other words, an element in a viewmust come directly from an element in the source,
and this correspondence enables an updates to aview element to be translated into an update toits origin in the source, which forms the basis of a
backward transformation. In a sense, we can see semantic bidirectionalization as a functional way tocharacterize a “pointer-based” update-translation
mechanism satisfying the consistency law.
2. 1 Construction of Backward Transformation
We present a simple implementation of semantic bidirectionalization that captures the core idea
found in the original paper [22], which will be expanded in Section 3. We assume basic knowledge
of Haskell and its standard libraries, and may use
functions from Prelude without explanation. We
use rank-2 polymorphism; thus the language option Rank2Types is required to run the code in thissection.
Consider an arbitrary polymorphic function oftype ∀α. [α] → [α], for example tail . Its type tells
us that the function can only reorganize or drop
its input list elements, and an element in a viewmust have a unique corresponding element in thesource as its origin. However, it is not possible
to conclude the behaviour of the function by observing the source-view pair. For example, giving
a source "aab" and its view "ab", it is not clear
which "a"-element in the source corresponds to the"a"-element in the view.
A way to distinguish potentially equal elements
is to identify them with their unique location(pointer). We use the following datatype Loc torepresent location-aware data.
data Loc α = Loc {body :: α, location :: Int}For example, the source "aab" may have a locationaware version as [Loc ’a’ 1, Loc ’a’ 2, Loc ’b’ 3]. If
we apply the same polymorphic function to it, we
get [Loc ’a’ 2, Loc ’b’ 3], with a clear show of correspondence.
Now suppose that the view "ab" is updated

to "cd". Matching it to the location-aware view
[Loc ’a’ 2, Loc ’b’ 3], we can know that location-2
and location-3 are updated to ’c’ and ’d’ respectively. We represent such an update as a list ofpairs of location and the new value that is assigned
the location.
type Update α = [(Int, α)]For the above case, we obtain an update[(2, ’c’), (3, ’d’)]. Applying the update to thelocation-aware source and then extracting thebodys, gives us an updated source "acd".
The application of the update can be easily implemented in Haskell, as the following function
update.
update upd (Loc x i) =case lookup i upd of
Nothing → Loc x i
Just y → Loc y i
And the matching of the location-aware view andthe updated view that produces the update is defined as the following.
matchViewsSimple ::Eq γ ⇒ [Loc γ] → [γ] → Update γ
matchViewsSimple vx v =if length vx == length v thenminimize vx $ makeUpdSimple $ zip vx v
else
error "Shape Mismatch"
Here, makeUpdSimple is an auxiliary function defined as
makeUpdSimple = foldr f []where
f (Loc x i, y) u =case lookup i u ofNothing → (i, y) : u
Just y ′ →if y == y ′ thenuelse
error "Inconsitent Update"
A number of checks are performed by matchViewsSimple
to ensure that the updates to the view do not causeinconsistency: the updates to the view shall notchange the list length, and if a source element appears more than once in the view, the multiple occurrences of the same element need to be updated
consistently (that’s why the Eq context is needed).
Note that for simplicity we assume that the user-defined equality (==) actually implements semantic
equality (=) for elements. For example, consider aforward function f [x] = [x, x] of type ∀α.[α] → [α].
Suppose an initial source "a", and thus a view "aa".
Then, updating the view to "ab" will be rejectedby matchViewsSimple, whereas updating to "bb"will be accepted. Note that we also use a function minimize to remove duplicates from an update,
which is defined as the following.
minimize vx u = u \\ [(i, x) | Loc x i ← vx ]Here, (\\), imported from Data.List, computes thediﬀerence of two lists. It is worth remarking thatthe application of minimize is optional, as identical updates will not change the behaviour the backward transformation. But having this minimality
property of updates simplifies the proofs for correctness that will be discussed in Section 4.
With the ground prepared, the higher-order function that takes a forward function and produces abackward counter-part can be realized as the following.
bwd :: Eq γ ⇒ (∀α. [α] → [α]) → [γ] → [γ] → [γ]bwd h = λs v. let sx = zipWith Loc s [1..]vx = h sx
upd = matchViewsSimple vx v
in map (body ◦ update upd ) sx
This version of bwd is specific to list-to-list transformations, which is conveniently used to illustrate
the basic idea of semantic bidirectionalization. It
is shown that the technique generalizes to arbitrary
Traversable datatypes such as rose trees [22] [8].
2. 2 Extensions and Limitations
Things become more complicated if the forward
function is not fully polymorphic. For example,
consider function nub :: ∀α. Eq α ⇒ [α] → [α]that removes duplicates from a list based on a given
equality comparison operator. Now similar to thecase of query Q1 we have seen before, the forward
transformation is able to observe equality among elements, and the free theorems on fully polymorphic
functions are no longer applicable. In the original
paper [22], the problem is solved by a more sophisticated indexing scheme catered for each observer
function. In the case of nub, where equality is used,
we need to make sure that the indices fully reflect
the equality among elements: indices are equal if
and only if the elements are equal, and no update

is allowed to break this condition.
As we will see in the next section, this techniqueof creating specialized indexing system to mimic
the actual source is not enough to handle functions
that construct elements of the polymorphic type.
Nevertheless, semantic bidirectionalization remains
particularly attractive because it oﬀers the possibility of programming forward transformations in a
general-purpose language that is expressive enoughfor practical applications.

3 Our Bidirectionalization
In this section, we present our improved semantic bidirectionalization framework in Haskell. For
illustration, we use a toy example based on rosetrees:
data Tree α = Node α [Tree α]deriving (Eq, Functor )To run the codes in this section, the following language options must be turned on: DeriveFunctor,
FlexibleInstances, MultiParamTypeClasses andFunctionalDependencies in addition to Rank2Types.
Example 1 (Links). Query “Links”: Collect all
subtrees with "a" as root label, and arrange themunder a new root labeled "results".
For example, if we apply Links to the source
src links = Node "root" [Node "a" [Node "text" []],
Node "p" [Node "a" [Node "text2" []]]]
we get the following view.
view links = Node "results" [Node "a" [Node "text" []],
Node "a" [Node "text2" []]]
Although being very simple, query Links is representative in the sense that its execution involves
comparing source labels with constants, and theconstruction of new labels. A direct implementation of the query is as follows.
linksmono :: Tree String → Tree String
linksmono t = Node "results" (linkssmono t)linkssmono :: Tree String → [Tree String]linkssmono (Node n ts) =if n == "a" thenNode "a" ts
else
concatMap linkssmono ts

However, this function is monomorphic, which is
not subject to the existing bidirectionalization technique.
3. 1 Making Monomorphic Queries Polymorphic
The reasons for linksmono to be monomorphic
are the equality comparison of tree labels with theconstant "a" and the construction of the constant"results". So a technique to prevent this type instantiation is to avoid the direct use of constants,
and instead construct new labels from them. The
following type class PackTrial can be used for thispurpose.
class Eq γ ⇒ PackTrial γ α | α → γ where
new :: γ → α
eq :: α → α → Bool
Function new abstracts a constant to a polymorphic type, and function eq compares polymorphic
labels for equality. With them, we can implement
our query as a polymorphic function.
linkspoly :: PackTrial String α ⇒ Tree α → Tree α
linkspoly t = Node (new "results") (linksspoly t)
linksspoly :: PackTrial String α ⇒ Tree α → [Tree α]linksspoly (Node n ts) =if eq n (new "a") thenNode (new "a") ts
else
concatMap linksspoly ts
The functional dependency α → γ in the class definition has helped us to avoid a type annotation for
the expression eq n (new "a").
Problem solved? Not really. Due to the usesof new together with eq, which are able to construct new polymorphic values and compare themwith arbitrary labels, the free theorems of thetype ∀α. PackTrial γ α → Tree α → Tree α are nolonger strong enough to support bidirectionalization. Concretely, since the forward transformation
is able to construct new labels and use them in observer functions such as equality comparisons, it is
no longer possible, without inspecting the actual
implementation of the forward function, to predict what changes may aﬀect the observations, andtherefore need to be rejected. In such a case, accepting any update risks violating the consistency
law, which reduces semantic bidirectionalization to

a completely useless state.
3. 2 Tracking Observations Using MonadAs we have seen, with the existing bidirectionalization technique, it is necessary to reject all updates when label construction is used, because of
the fear that the update may aﬀect the control (or,computation path) of the forward function. On
the other hand, this requirement is certainly overconservative: for a given query such as Links, not
all the updates can aﬀect its control. For example, updating "a" to any other strings in view links
aﬀects the control, but updating "text" to otherstrings does not.
Our idea is to use a monad to keep track of whatobservations are performed in the execution of aforward transformation. Then, we can employ amore targeted update-checking strategy by rejecting only those that do aﬀect the observations.
Specially, we extend type class PackTrial to
PackM by including a monad parameter. We also
separate the construction of new labels into a different class Pack .
class (Pack γ α, Monad µ) ⇒ PackM γ α µ where
liftO :: Eq β ⇒ ([γ] → β) → ([α] → µ β)class Pack γ α | α → γ where
new :: γ → α
In this new design, we no longer deal with specific observer functions such as eq; instead function
liftO lifts any observer function Eq β ⇒ [γ] → β
on a concrete datatype γ to a monadic one Eq β ⇒[α] → µ β on an abstracted datatype α. The context Eq β is needed because we will compare theobservation results to check the validity of updates.
For convenience, we also introduce two specific instances of liftO that operates on unary and binary
observer functions respectively.
liftO1 p x = liftO (λ[x].p x) [x]liftO2 p x y = liftO (λ[x, y].p x y) [x, y]
As a result, forward functions in our setting havethe following type.
∀α.∀µ. PackM γ α µ ⇒ Tree α → µ (Tree α)
The type is polymorphic in α which is suitable
for semantic bidirectionalization. And importantly,
the type is polymorphic also in µ so that the monadcannot be manipulated directly in the definitionsof the forward functions, which guarantees the in-tegrity of the observation results recorded in themonad.
3. 3 Extended Semantic Bidirectionalization (An Overview)
We are now ready to bidirectionalize Links. In
our new setting, the query can be defined as thefollowing.
links :: PackM String α µ ⇒ Tree α → µ (Tree α)links t = do as ← linkss t
return $ Node (new "results") as
linkss :: PackM String α µ ⇒ Tree α → µ [Tree α]linkss (Node n ts) =do b ← liftO2 (==) n (new "a")if b thenreturn $ Node (new "a") ts
else
concatMapM linkss ts
where concatMapM h x = do y ← mapM h x
return (concat y)
As we can see, the above is a straightforward adaptation of the definition of linkspoly .
Similar to before we attach locations to polymorphic labels, with the following type.
data Loc α = Loc {body :: α, location :: Maybe Int}
Unlike what we saw in Section 2, the location partof the type is optional (represented by the Maybetype): a newly constructed label by new does nothave a corresponding source label, and is therefore not updatable. For brevity, we write x@i for
Loc x (Just i) and x@# for Loc x Nothing.
Let’s assume that a monadic infrastructure isprepared (we will see how it is done very soon in
Section 3. 5). Applying links to a location-aware
version srcx links of src links defined as
srcx links =Node ("root"@1) [Node ("a"@2) [Node ("text"@3) []],
Node ("p"@4) [Node ("a"@5)[Node ("text2"@6) []]]]
gives us a location-aware version viewx links ofview links
viewx links =Node ("results"@#) [Node ("a"@2) [Node ("text"@3) []],
Node ("a"@5) [Node ("text2"@6) []]]

together with the following observation history thatis recoded in the monad.
Observation
==
==
==
==

Arg-1
"root"@1
"a"@2
"p"@4
"a"@5

Arg-2
"a"@#
"a"@#
"a"@#
"a"@#

Result
False
True
False
True

Entries in the above table represent the observations that are made during the execution of links,
which contribute to the control of the computation
path. No update is allowed to alter the results.
For example, consider an update [(3, "changed")],which changes the label "text" in the view to"changed". Since the label aﬀected does not appear in the history, the update does not change thetable, and thus can be accepted. In contrast, an
update [(2, "b")] involves location 2 that appears
in the history. We then need to check whether thechange, from "a" to "b", alters the observation result.
Observation
==
==
==
==

Arg-1
"root"@1
"b"@2
"p"@4
"a"@5

Arg-2
"a"@#
"a"@#
"a"@#
"a"@#

Result
False
True
False
True

In this case, the comparison "b" == "a" returns
False, which is diﬀerent from the result in the history. As a result, the observation table becomesinconsistent, and the update needs to be rejected.
This consistency check of the history is key for theapplication of free theorems, and therefore the correctness of our proposal, which will be discussed
formally in Section 4.
In the rest of this section, we present a realizationof the above discussed idea.
3. 4 Forward Execution
To execute links, we need to instantiate themonad and provide instances of its type class context. For forward execution, which does not require
the recording of observations, the identity monad I
is used.†1†1 We do not use Identity in Haskell for brevity ofthe proofs.

newtype I α = I {runI :: α}instance Monad I wherereturn = I
I x >>= f = I (f x)

new do not have obvious origins in the source, andtherefore won’t have locations. This is reflected in
the instance declaration of Pack for backward execution.

And accordingly we prepare the following instancesof Pack and PackM .

instance Pack γ (Loc γ) where
new x = Loc x Nothing

instance Pack γ (I γ) where
new = I
instance PackM γ (I γ) I where
liftO p x = I (p $ map runI x)

Just like pointers, the mapping between values
and locations has to be injective: only one value
can be assigned to a particular location.
Definition 1 (Location Consistency). Let γ to bea label type. A tree t :: Tree (Loc γ) is location consistent if, for any labels x@i and y@j in t such thati ̸= # and j ̸= #,i=j⇒x=yholds.
We use the following function to assign locations
to all source labels.
assignIDs :: Tree γ → Tree (Loc γ)
And it must satisfy the following conditions.
Condition (assignIDs). assignIDs must satisfy:
For all s• assignIDs s is location consistent, and• fmap body (assignIDs s) = s.
This specification is rather loose and leave room for
diﬀerent implementations of assignIDs. In Example 2, we have chosen the following assignment withrunning integers.

In the above, I γ is used instead of γ to satisfy thefunctional dependency required by Pack .
Then, we can construct a function fwd for forward execution as below.
fwd :: (∀α.∀µ. PackM γ α µ ⇒ Tree α → µ (Tree α))→ Tree γ → Tree γ
fwd h = λs.let I v = h (fmap I s) in fmap runI v
Example 2 (linksF ). We can instantiate links forforward execution as follows.
linksF :: Tree String → Tree String
linksF = fwd links
We can apply linksF directly to sources as inlinksF src links = view links .
3. 5 Backward Execution
The construction of backward transformations isa bit more complicated than that of forward ones.
As explained in the previous section, updates arereflected in steps.
• Firstly, an observation history is constructedby applying the forward function, instantiatedwith an appropriate monad, to the locationaware source.
• Then, given an updated view, an update isconstructed and checked against the observation history obtained in the previous step.
• Finally, if the update passes the check, it isapplied to the source.
In the following, we explain these steps in detail.
For generality, we introduce helper functions primarily with their specifications, especially for theones that may have multiple diﬀerent correct implementations.
3. 5. 1 Locations
As mentioned in Section 3. 3, locations for labelsthat appear in a view are optional. In particular,
the labels that are newly constructed by function"root"@1, "a"@2, "text"@3, "p"@4, "a"@5, "text2"@6

Another implementation is to assign the same locations to “identical” labels as in the following.
"root"@1, "a"@2, "text"@3, "p"@4, "a"@2, "text2"@5This assignment still guarantees location consistency as "a" = "a". The diﬀerence is that now
the two "a"s are considered duplicates, instead of
separate labels with the same value.
In this paper, we mainly discuss the former strategy, and a datatype-generic implementation of it
can be found in Section 5. Nevertheless, we will
discuss the implication of the diﬀerent choices in
Section 7.
3. 5. 2 Observation History
The observation history is represented as the following datatype.
data Result α =∀β.Eq β ⇒ Result ([α] → β) [α] βRoughly speaking, a value Result p [x1 , . . . , xn ] rcorresponds to a line in the observation table shownin Section 3. 3, as below.

Observation
p

Arg-1
x1

...
...

Arg-n
xn

Resultraware view and an updated view with a function of
the following type.

The actual type of the observation outcome is existentially quantified, so that results of diﬀerent observers can be more easily kept together.
The consistency of a history entry can be easily
checked.

matchViews ::Eq γ ⇒ Tree (Loc γ) → Tree γ → Update γ

which allows us to define the following instance of
PackM for backward executions.

bwd :: Eq γ ⇒(∀α.∀µ.PackM γ α µ ⇒ Tree α → µ (Tree α))→ Tree γ → Tree γ → Tree γ
bwd h = λs v.
let sx= assignIDs s
W (vx , hist) = h sx
upd
= matchViews vx v
in if checkHist (update upd ) hist thenfmap (body ◦ update upd ) sx
else
error "Inconsistent History"

The definition of matchViews is similar to thatof matchViewsSimple in Section 2, except thatmatchViews needs to recognize labels without locations and reject any changes to them. We postpone
check :: Result α → Boolthe definition of matchViews to Section 5 where wecheck (Result p xs r) = p xs == rpresent a datatype-generic version of it. We require
And we can checks whether a history remains conmatchViews to satisfy the following conditions.
sistent after an update.
Condition (matchViews). matchViews must satcheckHist :: (α → α) → [Result α] → Bool
isfy:
checkHist u h = all (check ◦ u′ ) h• Correctness.
for any v ′ and locationwhere u′ (Result p xs r) = Result p (map u xs) r
consistent vx , let upd = matchViews vx v ′ ,A “Writer” monad W is responsible for gathering
fmap (body ◦ update upd ) vx = v ′ holds.
†
2
histories• Minimality.
for any v and locationconsistentvx
suchthat fmap body vx = v,
newtype W η β = W (β, [Result η])
matchViews vx v = [] holds.
instance Monad (W α) where
3. 5. 4 Putting Everything Together
return x = W (x, [])With all the ground prepared, we are now ready
W (x, h1 ) >>= f =to set up the backward execution.
let W (y, h2 ) = f x in W (y, h1 ++ h2 )instance PackM γ (Loc γ) (W (Loc γ)) where
liftO p x = W (p′ x, Result p′ x (p′ x))
where p′ = p ◦ map body
3. 5. 3 Updates
The application of updates remains straightforward. The only change from Section 2 is that we
now deal with optional locations.
update :: Update γ → (Loc γ) → (Loc γ)
update upd (Loc x Nothing) = Loc x Nothing
update upd (Loc x (Just i)) =case lookup i upd of
Nothing → Loc x (Just i)
Just y → Loc y (Just i)
The above definition satisfies the following conditions, which will be used in the proofs in Section 4.
Condition (update). update satisfies the following
conditions. For any x,• update [] x = x, and• update upd (new x) = new x.
Updates are extracted by comparing a location†2 We do not use Writer in Haskell instead of W for
brevity of the proofs.

Example 3 (links). We can instantiate links forbackward execution as follows.
linksB :: Tree String → Tree String → Tree String
linksB = bwd links
Suppose that view links is updated to the followingtree.
view ′ = Node "results" [Node "a" [Node "changed" []],
Node "a" [Node "text2" []]]
Then, linksB src links view ′ results in the following
updated source.

Node "root" [Node "a" [Node "changed" []],
Node "p" [Node "a" [Node "text2" []]]]On the other hand, an update to the view view ′′view ′′ = Node "results" [Node "b" [Node "text" []],
Node "a" [Node "text2" []]]
is rejected for the reason discussed in Section 3. 3.

4 Correctness of Our Bidirectionalization
In this section, we prove the correctness of our approach. That is, we prove that a forward transformation and the derived backward transformation
satisfy the consistency and acceptability mentioned
in Section 1.
We rewrite the laws in our setting. Let h be afunction of type ∀α.∀µ. PackM γ α µ ⇒ Tree α →µ (Tree α). We prove that the following laws holdfor any sources s and s′ , and view v.
Acceptability

bwd h s (fwd h s) = s

Consistency

fwd h s′ = v

if

bwd h s v = s′Following the original work [22], we make use of
free theorems [25] [23] in the proofs, and aim at being “morally correct” [4]; that is, our reasoning iscorrect in the absence of ⊥. In another words, weinterpret types as sets and functions as set-theoretic
functions. This totality assumption is reasonable inthe context of bidirectional transformation.
4. 1 Free Theorem
Roughly speaking, free theorems [25] [23] are theorems obtained for free as corollaries of relationalparametricity [21], which states that, for a term
f of type τ , (f, f ) belongs to a certain relational
interpretation of τ . A simple example of a freetheorem is that f of type ∀α.[a] → [a] satisfies
map g ◦ f = f ◦ map g for any function g of typeσ → τ . This theorem is key to the correctness ofthe original work [22].
We start by introducing some notations. We
write R :: σ1 ↔ σ2 if R is a relation on σ1 × σ2 .
For a base type B, we abuse the notation to write
B for the relation {(f, f ) | f :: B}. For relations
R :: σ1 ↔ σ2 and R′ :: τ1 ↔ τ2 , we write
R → R′ :: (σ1 → τ1 ) ↔ (σ2 → τ2 ) for the re-lation {(f, g) | ∀(x, y) ∈ R. (f x, g y) ∈ R′ }. For apolymorphic term f of type ∀α.τ and a type σ, wewrite fσ for the instantiation of f to σ that has
type τ [σ/α]. For simplicity, we sometimes omit thesubscript and simply write f for fσ if σ is clear fromthe context or irrelevant.
We introduce a relational interpretation Jτ Kρ oftypes, where ρ is a mapping from type variables torelations, as follows.
JαKρ
= ρ(α)JBKρ
=B
if B is a base typeJτ1 → τ2 Kρ = {Jτ1 Kρ → Jτ2 Kρ
}∀R : σ1 ↔ σ2 .
J∀α.τ Kρ= (u, v)(uσ1 , vσ2 ) ∈ Jτ Kρ[α7→R]
Here, ρ[α 7→ R] is an extension of ρ with α 7→ R.
If ρ = ∅, we sometimes write Jτ K instead of Jτ K∅ .
We abuse the notation to write J∀α.τ K as ∀R.F[R]where F [R] is the interpretation Jτ K{α7→R} . For example, we write ∀R.∀S. R → S for J∀α.∀β.α → βK.
The relational interpretation can be extended to
the list type [ · ] and the rose-tree type Tree, as
follows.
J[τ ]Kρ= [Jτ Kρ ]JTree τ Kρ = Tree Jτ Kρ
Here, we write [S] for the smallest relation satisfying([], []) ∈ [S],and(a1 : x2 , a1 : x2 ) ∈ [S] ⇔ (a1 , a2 ) ∈ S ∧ (x1 , x2 ) ∈ [S],and write Tree R for the smallest relation satisfying(Node x1 ts 1 , Node x2 ts 2 ) ∈ Tree R⇔ (x1 , x2 ) ∈ R, (ts 1 , ts 2 ) ∈ [Tree R].
Intuitively, [R] relates two lists with the samelength of which each pair of the elements in a same
position are related by R, and similarly Tree R relates two trees with the same shape of which eachpair of labels in the same position are related by R.
Then, parametricity states that, for a term f ofa closed type τ , (f, f ) is in Jτ K.
Free theorems are theorems obtained by instantiating parametricity. For example, for f :: ∀α.[α] →[α], we must have (f, f ) ∈ ∀R.[R] → [R]. Thus,
for any R : σ1 ↔ σ2 , (fσ1 , fσ2 ) ∈ [R] → [R], if wetake R = {(x, g x) | x :: σ1 } for some g :: σ1 → σ2 ,we obtain map g ◦ f = f ◦ map g.
Voigtländer [23] extends parametricity to a typesystem with type constructors. A key notation in
his result is relational action.
Definition 2 (Relational Action [23]). For type
constructor κ1 and κ2 , F is called a relational action between κ1 and κ2 , denoted by F : κ1 ↔ κ2 ,if F maps any relation R : τ1 ↔ τ2 for every closed
type τ1 and τ2 to F R : κ1 τ1 ↔ κ2 τ2 .
Accordingly, the relational interpretation is extended as:
JκKρ = ρ(κ)
Jτ1 τ2 K = Jτ
{ 1 K Jτ2 K
J∀κ.τ K =∀F : κ1 ↔ κ2 .
(u, v)(uκ1 , vκ2 ) ∈ Jτ Kρ[κ7→F ]}Parametricity holds also on the relational interpretation. Here, κ, κ1 and κ2 are type constructorsof kind ∗ → ∗, and thus the quantified F is a relational action.
Voigtländer [23] handles a function with typeclass constraints as a higher-order function thattakes the methods of the type classes as inputs.
For example, a function f :: Monad µ ⇒ τ canbe seen as a function f ′ :: (∀α. α → µ α) →(∀α.∀β. µ α → (α → µ β) → µ β) → τ withf ′ = λreturn.λ(>>=).f , and an instance fκ of f canbe seen as f ′ return κ (>>=)κ . As he packed the conditions posed by the above interpretation of Monadby Monad -action, we introduce a similar notion of
PackM -action for PackM .
Definition 3 (PackM -action). For relations L ::σ1 ↔ σ2 and U :: τ1 ↔ τ2 and a relational action
F :: κ1 ↔ κ2 , a triple (L, U , F ) is called a PackM action if all the following conditions hold.
• (σi , τi , κi ) is an instance of PackM for i = 1, 2,• (return κ1 , return κ2 ) ∈ ∀R. R → F R,
• ((>>=)κ1 , (>>=)κ2 ) ∈ ∀R.∀S. F R → ((R →F S) → F S),• (new σ1 ,τ1 , new σ2 ,τ2 ) ∈ L → U , and• (liftO σ1 ,τ1 ,µ1 ,β1 , liftO σ2 ,τ2 ,µ2 ,β2 ) ∈ ([L] →S) → [U] → F S for all S :: β1 ↔ β2 satisfying ((==)β1 , (==)β2 ) ∈ S → S → Bool .
Intuitively, a PackM -action is a property that is“preserved” under PackM -methods.
Now, we are ready to state a free theorem fora function h of the type ∀α.∀µ. PackM γ α µ ⇒Tree α → µ (Tree α).
Theorem 1 (A Free Theorem on h). Suppose h bea function of type ∀α.∀µ. PackM γ α µ ⇒ Tree α →µ (Tree α). Let γ be a type and L be a relation{(x, x) | x :: γ}. Let (τ1 , κ1 ) and (τ2 , κ2 ) are pairsof types and type constructors such that (γ, τ1 , κ1 )and (γ, τ2 , κ2 ) are instances of PackM . Then, forevery PackM -action (L :: γ ↔ γ, T :: τ1 ↔ τ2 , R ::
κ1 ↔ κ2 ), we have (hτ1 ,κ1 , hτ2 ,κ2 ) ∈ Tree U →F (Tree U).
4. 2 Preservation of Local Consistency
First of all, we prove that a tree vx constructedin bwd is location consistent. This is used to apply
the properties on matchViews.
Lemma 1 (Location-Consistency of vx ). Suppose
W (vx , ) = h (assignIDs s) for a tree s. Then, vx
is location consistent.
Proof. Let s be a source and E be the set of labelsin assignIDs s. Then, it is easy to show that vx islocation-consistent if all the labels e = x@i in vx
with i ̸= # are also in E.
The statement is proved by the free theorem onh, taking U and F as below.
U= {(x@i, x@i) | x@i ∈ E, i ̸= #}F R = {(W (x, ), W (y, )) | (x, y) ∈ R}
Note that Tree U is a diagonal relation, and v
such that (v, v) ∈ Tree U is location-consistent.
Then, assuming that (L, U, F) is a PackM -action,
we have (h, h) ∈ Tree U → F (Tree U ). Since(assignIDs s, assignIDs s) ∈ Tree U, we have(vx , vx ) ∈ Tree U . Thus, vx is location consistent.
Then, the remaining obligation is to check that
(L, U , F ) is a PackM -action as we have assumed
above. We omit the straightforward proof here.
4. 3 Proof of Acceptability
The overall structure of our (calculational-style)proof of acceptability is as follows.
bwd h s (fwd h s)
= { Unfolding bwd }if checkHist (update upd ) hist thenfmap (body ◦ update upd ) sx else . . .
= { (*) — see below }if True then fmap (body ◦ id ) sx else . . .
= { Reduction }fmap body sx= { Property of assignIDs }s
At (*), we use two properties: one is upd = [],and the other is checkHist (update []) hist = True.

To show them, it suﬃces to use the following lemma
together with the properties on matchViews (withLemma 1) and update.
Lemma 2. Let sx be assignIDs s. Suppose wehave W (vx , hist) = h sx and I v = h (fmap I s).
Then, we have fmap body vx = fmap runI v andcheckHist id hist = True.
Proof. Let U :: I γ ↔ (Loc γ) and F :: I ↔
W (Loc γ) be a relation and a relational action defined by:U= {(x,{ y) | runI x = body y}

FR=(x, y) ∈ R(I x, W (y, w))∧ checkHist id w}

Assume that the triple (L, U , F ) is a PackM action. Then, we can obtain (h, h) ∈ Tree U →F (Tree U) from the free theorem on h; thatis, for any x and y satisfying fmap runI x =fmap body y, we have fmap runI v = fmap body vx
and checkHist id hist = True where I v = h x andW (vx , hist) = h y. Taking x = fmap I s andy = assignIDs s, we obtain the lemma.
Then, the remaining obligation is to prove that
(L, U , F ) is a PackM -action. We omit the straightforward proof.
4. 4 Proof of Consistency
The proof of consistency is a bit more complicated but has a similar structure. The overall structure of our proof is as follows.
fwd h (bwd h s v) (where bwd h s v succeeds)= { Unfolding bwd , and bwd succeeded }fwd h (fmap (body ◦ update upd ) sx )= { (*) — see below }fmap (body ◦ (update upd )) vx= { Property of matchViews and Lemma 1}v
At (*), we used the following lemma.
Lemma 3. Let sx be assignIDs s, and s′ befmap (body ◦ update upd ) sx . Let v ′ be what obtained from I v ′ = h (fmap I s′ ), and vx and hist be
those obtained from W (vx , hist) = h sx . Suppose
we have checkHist (update upd ) = True. Then we
have fmap runI v ′ = fmap (body ◦ update upd ) vx .
Proof. Let U :: I γ ↔ Loc γ and F :: I ↔
W (Loc γ) be a relation and a relational action de-fined by:U
= {(x, y) | runI x = body (update upd y)}F{R=}(I x, W (y, w))

checkHist (update upd ) w⇒ (x, y) ∈ R

Then, assuming that (L, U, F) is a PackM -action,
we can prove the lemma straightforwardly from thefree theorem on h.
Then, the remaining obligation is to prove that
(L, U , F ) is a PackM -action. We omit the straightforward proof.

5 Going Generic
So far, we have demonstrated our idea for a specific datatype, namely Tree. In this section, we
extend the solution to be datatype-generic.
As a matter of fact, this generalization has already been done in the previous work [22] [8], andwe borrow the ideas and adapt them for our new
setup. More concretely, we use the following
datatype-generic functions from Data.Traversable
and Data.Foldable to define assignIDs andmatchViews, and change the type declarations of
fwd and bwd accordingly.
traverse :: (Traversable κ, Applicative θ) ⇒(α → θ β) → κ α → θ (κ β)toList :: (Foldable κ) ⇒ κ α → [α]We redefine assignIDs as a function of typeassignIDs :: Traversable κ ⇒ κ γ → κ (Loc γ)with definition
assignIDs t = evalState (traverse f t) 0
where f x =do i ← Control .Monad .State.getControl .Monad .State.put (i + 1)
return $ Loc x (Just i)
Here, we qualified the state monad operations get
and put with Control .Monad .State to distinguishthem from the get and put as bidirectional transformations. The conditions we mentioned in Section 3. 5 hold for typical instances of Traversable,
especially for those that are systematically obtained [18].
We also redefine matchViews.

matchViews :: (Foldable κ, Eq (κ ())) ⇒κ (Loc γ) → κ γ → Update γ
What matchViews does is to perform element-wisecomparison after shape-equality check.
matchViews vx v =if fmap ignore vx == fmap ignore v thenlet lx = toList vx
l = toList v
in minimize lx $ makeUpd $ zip lx lelse
error "Shape Mismatch"
Here, ignore is a function defined by ignore x = (),which ignores its input but leaves a place-holder.
Function makeUpd , which is defined below, constructs an update from two views, making sure thatelements without locations are not changed, and location consistency is not violated.
makeUpd = foldr f []where
f (Loc x Nothing, y) u =if x == y thenuelse
error "Update of Constant"f (Loc x (Just i), y) u =case lookup i u ofNothing → (i, y) : u
Just y ′ →if y == y ′ thenuelse
error "Inconsistent Update"
The conditions we posed on matchViews hold for
typical instances of Foldable, with which toList extracts all the elements of a container.
Accordingly, the types of fwd and bwd are updated.
fwd :: (Traversable κ1 , Foldable κ2 ,
Eq (κ2 ()), Eq γ) ⇒(∀α µ.PackM γ α µ ⇒ κ1 α → µ (κ2 α))→ κ1 γ → κ2 γ
bwd :: (Traversable κ1 , Foldable κ2 ,
Eq (κ2 ()), Eq γ) ⇒(∀α µ.PackM γ α µ ⇒ κ1 α → µ (κ2 α))→ κ1 γ → κ2 γ → κ1 γ
No change is required in the definitions of fwd andbwd .
It is worth noting that the GHC extensions-XDeriveFoldables and -XDeriveTraversables
allow Foldable and Traversable instances to be
automatically derived, which comes handy forbidirectionalizing transformations on user-defined
datatypes.

6 XML Query Example
In this section, we revisit our motivating example
of XML querying, and show how we can bidirectionalize the query Q1 shown in Figure 2. Recall
that, if we apply Q1 to the XML source shown in
Figure 1 we get the XML view shown in Figure 3.
6. 1 A Datatype for XML
Firstly, we define a datatype to describe XML
documents, using the rose-tree datatype defined in
Section 3 with the following label type.
data L = A String | E String | T String deriving Eq
Here, A, E and T stand for “attribute”, “element”(in terms of XML) and “text” (attribute values andcharacter data). We omit other features of XML
that are not expressed by this datatype, such as
namespaces.
For example, an XML fragment<book year="1994"><title>Text</title></book>is represented as
Node (E "book") [Node (A "year") [Node (T "1994")],
Node (E "title") [Node (T "Text")]]
The following function label is handy when we
write programs that manipulate the rose trees.
label (Node l ) = l
6. 2 Programming the Forward Transformation
Then, we implement Q1 as a function of type∀α.∀µ. PackM L α µ ⇒ Tree α → µ (Tree α) that issuitable for bidirectionalization. We will use a few
auxiliary “filters” [26] that performs various content processings. In [26], the filters (if we simplify
and customize them to our rose trees) are of type

Tree L → [Tree L], which will be made polymorphic
in our setting as
PackM L α µ ⇒ Tree α → ListT µ (Tree α).
where we use a monad transformer ListT inControl.Monad.List, defined by:newtype ListT µ α = ListT {runListT :: µ [α]}which has an implementation for the method
lift :: µ α → ListT µ α in Control.Monad.Trans.
In addition, we will make use of the factthat ListT µ is an instance of MonadPlus inControl.Monad.
Specifically, we use function
mzero :: MonadPlus κ ⇒ κ α to represent computation failure.
A simple example of a filter is children that returns the children of a node, defined as follows.
children :: PackM L α µ ⇒Tree α → ListT µ (Tree α)
children (Node ts) = ListT (return ts)
Another example is ofL l that returns its argument
as is if the node has label l, and fails otherwise.
ofL :: PackM L α µ ⇒α → Tree α → ListT µ (Tree α)
ofL l t = do guardM $ lift $ liftO2 (==) (label t) lreturn t
Here, guardM is a function that is similar to guardin Control.Monad except that guardM takes amonadic argument. It fails if its argument is Trueand do nothing otherwise.
guardM :: MonadPlus κ ⇒ κ Bool → κ ()guardM x =x >>= (λb.if b then return () else mzero)
Filters are composable [26]. For example, we
can compose children and ofL to obtain a filter
childrenOfL that extracts the children of a givenlabel, as follows.
childrenOfL l x = do {c ← children x; ofL l c}
Or by using the Kleisli-composition operator (>=>)
in Control.Monad, we can write
childrenOfL l = children >=> ofL l
Now we are ready to implement Q1. The code
can be found in Figure 4 and is self-explanatory.

6. 3 Permitted Updates
Given that q1 has the right type, we can easily
bidirectionalize it with fwd and bwd . It is not difficult to see that fwd q1 implements Q1, although
there is a subtle diﬀerence that Q1 reads an input
XML documents from a certain URL while q1 takes
the input as a parameter.
Let us discuss what kind of updates will be permitted by bwd q1 . Consider the view in Figure 3.
There are the following kinds of in-place updates:• Changing bib-tags to other tags.
• Changing book-tags to other tags.
• Changing year to other attributes.
• Changing the values of year-attributes.
• Changing title-tags to other tags.
• Changing title-texts under titles.
The first three updates should be rejected because these elements and attributes are those introduced by the query q1 instead of coming fromthe original source.
As expected, bwd q1 rejects the three updates; more precisely, an error"Update of Constant" is raised by matchViews.
The fourth update, which is the most interestingcase among the six, is conditionally accepted by
bwd q1 ; more precisely, we can change the value toany (string representation of) numbers as long as
the number is greater than 1991. This behavior isquite natural because if we change the year to one
that is no greater than 1991, say 1990, then thebook will disappear from the view, which violates
the consistency law.
The fifth-update is rejected for a similar reason. Note that the query extracted titles bychildrenOfL (el "title") b.
Thus, if we allowchanging title-tags to other tags, the consistency
law will be violated.
The last update is unconditionally accepted by
bwd q1 because q1 does not inspect titles.

7 Discussion
In this section, we discuss design issues that arecommon to bidirectional frameworks.
7. 1 The Interpretation of Duplication
It is rather natural to expect that in any reasonable system, duplicates shall be updated at thesame time to the same values. In theory, there islittle controversy about this statement; yet in prac-q1 :: PackM L α µ ⇒ Tree α → µ (Tree α)
q1 t = pick $ do bs ← gather $ childrenOfL (el "book") t >>= hreturn $ Node (el "bib") bs
where
hb=
do y ← childrenOfL (at "year") b >>= childrents ← gather $ childrenOfL (el "title") bp ← childrenOfL (el "publisher") b >>= children
guardM $ lift $ liftO2 gtInt (label y) (tx "1991")
guardM $ lift $liftO2 (==) (label p) (tx "Addison-Wesley")return $ Node (el "book")(Node (at "year") [y] : ts)
gtInt l1 l2 = (read l1 :: Int) > (read l2 :: Int)tx s = new (T s)
el s = new (E s)
at s = new (A s)gather :: Monad µ ⇒ ListT µ α → ListT µ [α]gather (ListT m) = ListT $ do {x ← m; return [x]}pick :: Monad µ ⇒ ListT µ α → µ α
pick (ListT x) = do a ← x
return $ head a
Fig. 4

Query Q1 in Our Framework

tice, it is less obvious whether two values are actual
duplicates, or merely being incidentally equal.
As mentioned in Section 3. 5. 1, in this paper
we take a conservative approach by considering all
source elements as independent data regardless of
their values. This decision makes a lot of sense.
For example, consider our example Q1 in Figure 2.
Suppose that there are books published in the same
year in the source, we don’t want to have all of themchanged just because one is changed.
On the other hand, it is also obvious that our
choice is not the only correct one. In the original
work on semantic bidirectionalization [22], when
the system is extended to non-fully polymorphic
forward functions such as∀α. Eq α ⇒ [α] → [α]they use a strategy of considering elements as duplicates, as along as they are equal. The idea tohandle the above function is to provide a specialized version of assignIDs that assigns locations thatreflect the uses of Eq (i.e., equal elements get thesame location so that for every two elements x@i
and y@j (i ̸= # and j ̸= #) the condition thatx = y if and only if i = j holds). Any updates
that violate this condition are rejected. As an ex-

ample, consider function nub in Data.List that removes duplicated elements from a list. The backward function named as nubB has the following behavior.
> nub "abba"ab> nubB "abba" "cb"cbbc
In the above, the two ’a’s are considered duplicates, and the changing of one changes the other.
If we use our system on a variant of nub of thesuitable type nub ′ :: Eq γ ⇒ ∀α µ.PackM γ α µ ⇒[α] → µ [α], the result is diﬀerent due to the different interpretation of duplication. Our systemassigns locations as [’a’@1, ’b’@2, ’b’@3, ’a’@4],and applying nub ′ returns the view [’a’@1, ’b’@2]
and possibly (depending on the implementation)
the following history.
Observation
==
==
==

Arg-1
’a’@1
’a’@1
’b’@2

Arg-2
’b’@2
’a’@4
’b’@3

Result
False
True
True

The same update [(1, ’c’)] that turns ’a’ into ’c’
is rejected when checking the history.
It is however easy to switch between the above
two interpretations in our system: only assignIDs

needs to be changed.
7. 2 Bidirectional Properties
We have discussed in this paper the definitional
properties of bidirectional transformations, namely
the acceptability and consistency laws. There areother laws that are mentioned in the literature,
which are very often considered optional but desirable. Two of them are undoability and composability [17] [1] [10] [11], which are variants of PutPut [6]†3Composability put s v = s′ ∧ put s′ v ′ = s′′ ⇒put s v ′ = s′′Undoability

put s v = s′ ⇒ put s′ (get s) = s

Intuitively composability says that subsequent updates can be combined, and undoability says thatan update can be undone through the view. Theselaws are useful properties especially when updates
on the view and source sides are conducted by different systems [9] [10]: for example, composability
allows us to schedule updates on the view separated from those on the source [9]. Without proofs,
we state that our derived bidirectional transformations satisfy both the composability and undoability laws. The justification of this claim comes fromthe fact that semantic bidirectionalization can beseen as a form of constant-complement bidirectionalization [1] [8], in which the four laws, i.e., acceptability, consistency, composability and undoability,
hold. Specifically, the shape of the source and theobservation history serve as the constant complement in our framework.
The desirable laws are sometimes considered too
restrictive [16] [6] because a framework that supports shape changes (insertion and deletion of elements) of views is unlikely to be able to satisfy
them (for example, consider a forward transformation map fst and source [("A", 2)], and consider
what happens if we change a view from ["A"] to []and then insert "A" again). In [24], where semantic
bidirectionalization is combined with another bidirectionalization technique [17] aiming at shape updates, the composability and undoability laws are
sacrificed. Further studies on the desirable laws
in the presence of insertions and deletions can be†3 If put is total, both of the composability and undoability coincide with PutPut [6].

found in [9] [11] [15].
There is another law discussed by Hegner [10] [11]that, with the four laws, ensures information not inthe view cannot be accessed.
Uniformity

put s(v = s′⇒∀s′′ .get s′′ = get s⇒ ∃s′′′ . put s′′ v = s′′′)Intuitively, uniformity says that whether an updateon the view is accepted or not does not depend on
the source. Our framework does not satisfy thislaw. For example, for f defined by
f [x, y] = liftO2 (==) x y >>= λ .[x]whether an update is accepted depends on theequality between x and y.

8 Related Work
Another way of bidirectionalizing programsis through syntactically transforming forwardfunction definitions [17], a technique termed as syntactic bidirectionalization in [22], in contrast to thesemantic approach that does not inspect the program definitions. The advantages of the syntactic
approach is that it can derive more eﬃcient andeﬀective (in the sense of allowing certain shape updates) backward transformations. For example, thetechnique in [17] can derive a backward transformation for function zip that accepts arbitrary updates
on the view, including insertion and deletion of elements. On the downside, since syntactic bidirectionalization inspects the definition of a program,the resulting backward transformation depends on
the syntactic structure of the forward transformation, which is fragile and less predictable. Moreover, the ability of permitting more updates comespartly at the cost of the expressiveness of the forward transformation. It is usually much harderto develop programs that are suitable for syntactic
bidirectionalization than that for semantic bidirectionalization.
Instead of trying to bidirectionalize unidirectional programs, one can try to program directly
in a “bidirectional” language, in which the resulting programs are bidirectional by construction.
Such bidirectional languages are usually combinator based [6] [13] [19] [2] [20] [27], and the programmer
constructs a bidirectional transformation by com-bining smaller ones with special combinators. Some
combinator languages can be implemented as libraries [13] [19], which is rather light-weight, whilesome languages [6] [2] [27] need richer type systems,
which are not available in most general-purpose
languages, to be eﬀective. It is usually easy to extend the languages by adding or removing combinators for specific domains [20] [27] [2], and typicallyusers of the bidirectional languages have better control of the behaviors of the programs by not relying
on a black-box bidirectionalization system; but theusers do have to program in an unusual style andis limited by the expressiveness of the languages.
The use of run-time recording of the forward
execution path for the backward execution is not
new [6] [17]. The lens framework [6] provides a combinator ccond that performs conditional branchingin the forward execution, and in the backward direction, the recorded history prohibits updates that
may cause the execution to take a diﬀerent branch.
This treatment of branching is more explicit in [17],where branching information is recorded in a complement, which is kept constant to guarantee thebidirectional laws.
Both ours and the original work on semantic
bidirectionalization [22] focus on in-place updates,
which is a non-trivial problem when the forward
transformations are complex [12], It is shown that
this limitation of updates can be relaxed to someextent by combining semantic bidirectionalization
with other techniques that are good at shape updates [24]. We expect that a similar extension is
also applicable to our proposal, which will be aninteresting direction for future work.

9 Conclusion
In this paper, we extend semantic bidirectionalization to handle monomorphic transformations, by
programming them in a polymorphic way througha type class PackM .
Specifically, we replacemonomorphic values in the definition of a transformation with polymorphic elements that are newly
constructed from those values. A history of the
program execution is recorded at run-time, which
can be checked to reinstate the applicability of freetheorems in the presence of newly constructed polymorphic elements. We prove that the transformations produced by our bidirectionalization system

satisfy the bidirectional properties, i.e., the acceptability and consistency laws. The practicality of
our system is demonstrated by a case study of XML
transformations.
At the moment, our system is general purpose,
which is expressive, but lacking in conveniency. As
future work, we plan to design new or adapt existing domain-specific languages to use our system
as a backend, so that bidirectionality can be moreeasily achieved.
References[ 1 ] Bancilhon, F. and Spyratos, N.: Update Semantics of Relational Views, ACM Trans. Database
Syst., Vol. 6, No. 4(1981), pp. 557–575.
[ 2 ] Bohannon, A., Foster, J. N., Pierce, B. C.,
Pilkiewicz, A., and Schmitt, A.: Boomerang: resourceful lenses for string data, POPL, Necula,
G. C. and Wadler, P.(eds.), ACM, 2008, pp. 407–
419.
[ 3 ] Czarnecki, K., Foster, J. N., Hu, Z., Lämmel,
R., Schürr, A., and Terwilliger, J. F.: Bidirectional
Transformations: A Cross-Discipline Perspective,
Berlin, Heidelberg, Springer-Verlag, 2009, pp. 260–
283.
[ 4 ] Danielsson, N. A., Hughes, J., Jansson, P., andGibbons, J.: Fast and loose reasoning is morally
correct, POPL, Morrisett, J. G. and Jones, S.
L. P.(eds.), ACM, 2006, pp. 206–217.
[ 5 ] Dayal, U. and Bernstein, P. A.: On the Correct Translation of Update Operations on Relational Views, ACM Trans. Database Syst., Vol. 7,
No. 3(1982), pp. 381–416.
[ 6 ] Foster, J. N., Greenwald, M. B., Moore, J. T.,
Pierce, B. C., and Schmitt, A.: Combinators forbidirectional tree transformations: A linguistic approach to the view-update problem, ACM Trans.
Program. Lang. Syst., Vol. 29, No. 3(2007).
[ 7 ] Foster, J. N., Pilkiewicz, A., and Pierce, B. C.:
Quotient lenses, ICFP, Hook, J. and Thiemann,P.(eds.), ACM, 2008, pp. 383–396.
[ 8 ] Foster, N., Matsuda, K., and Voigtländer, J.:
Three Complementary Approaches to Bidirectional
Programming, Generic and Indexed Programming,
Gibbons, J.(ed.), Lecture Notes in Computer Science, Vol. 7470, Springer Berlin Heidelberg, 2012,
pp. 1–46.
[ 9 ] Gottlob, G., Paolini, P., and Zicari, R.: Properties and Update Semantics of Consistent Views,
ACM Trans. Database Syst., Vol. 13, No. 4(1988),
pp. 486–524.
[10] Hegner, S. J.: Foundations of Canonical Update Support for Closed Database Views, ICDT,
Abiteboul, S. and Kanellakis, P. C.(eds.), Lecture
Notes in Computer Science, Vol. 470, Springer,
1990, pp. 422–436.

[11] Hegner, S. J.: An Order-Based Theory of Updates for Closed Database Views, Ann. Math. Artif.
Intell., Vol. 40, No. 1-2(2004), pp. 63–125.
[12] Hidaka, S., Hu, Z., Inaba, K., Kato, H.,
Matsuda, K., and Nakano, K.: Bidirectionalizing
graph transformations, In Hudak and Weirich [14],pp. 205–216.
[13] Hu, Z., Mu, S.-C., and Takeichi, M.: A programmable editor for developing structured documents based on bidirectional transformations,
PEPM, Heintze, N. and Sestoft, P.(eds.), ACM,
2004, pp. 178–189.
[14] Hudak, P. and Weirich, S.(eds.): Proceedingof the 15th ACM SIGPLAN international conference on Functional programming, ICFP 2010, Baltimore, Maryland, USA, September 27-29, 2010,
ACM, 2010.
[15] Johnson, M. and Rosebrugh, R. D.: Lens
put-put laws: monotonic and mixed, ECEASST,
Vol. 49(2012).
[16] Keller, A. M.:
Comments on Bancilhon
and Spyratos’ “Update Semantics and Relational
Views”, ACM Trans. Database Syst., Vol. 12,
No. 3(1987), pp. 521–523.
[17] Matsuda, K., Hu, Z., Nakano, K., Hamana, M.,
and Takeichi, M.: Bidirectionalization transformation based on automatic derivation of view complement functions, ICFP, Hinze, R. and Ramsey,N.(eds.), ACM, 2007, pp. 47–58.
[18] McBride, C. and Paterson, R.: Applicative programming with eﬀects, J. Funct. Program., Vol. 18,
No. 1(2008), pp. 1–13.
[19] Mu, S.-C., Hu, Z., and Takeichi, M.: An

Algebraic Approach to Bi-directional Updating,
APLAS, Chin, W.-N.(ed.), Lecture Notes in Computer Science, Vol. 3302, Springer, 2004, pp. 2–20.
[20] Rajkumar, R., Lindley, S., Foster, N., and Cheney, J.: Lenses for Web Data, In Preliminary Proceedings of Second International Workshop on Bidirectional Transformations (BX 2013), 2013.
[21] Reynolds, J. C.: Types, Abstraction and Parametric Polymorphism, Information Processing, Mason, R.(ed.), Elservier Science Publishers B.V.
(North-Holland), 1983, pp. 513–523.
[22] Voigtländer, J.: Bidirectionalization for free!
(Pearl), POPL, Shao, Z. and Pierce, B. C.(eds.),
ACM, 2009, pp. 165–176.
[23] Voigtländer, J.: Free theorems involving type
constructor classes: functional pearl, ICFP, Hutton,
G. and Tolmach, A. P.(eds.), ACM, 2009, pp. 173–
184.
[24] Voigtländer, J., Hu, Z., Matsuda, K., and Wang,
M.: Combining syntactic and semantic bidirectionalization, In Hudak and Weirich [14], pp. 181–192.
[25] Wadler, P.: Theorems for Free!, FPCA, 1989,
pp. 347–359.
[26] Wallace, M. and Runciman, C.: Haskell andXML: Generic Combinators or Type-Based Translation?, ICFP, Rémi, D. and Lee, P.(eds.), ACM,
1999, pp. 148–159.
[27] Wang, M., Gibbons, J., Matsuda, K., and Hu,Z.: Gradual Refinement: Blending Pattern Matching with Data Abstraction, MPC, Bolduc, C., Desharnais, J., and Ktari, B.(eds.), Lecture Notes
in Computer Science, Vol. 6120, Springer, 2010,
pp. 397–425.