Principles and Practice of Bidirectional Programming in BiGUL

Abstract

Putback-based bidirectional programming allows the programmer to write only one backward transformation, from which the unique corresponding forward transformation is derived for free. A key distinguishing feature of putback-based bidirectional programming is full control over the bidirectional behavior, which is important for specifying intended bidirectional transformations without any ambiguity. In this chapter, we will introduce BiGUL, a simple yet powerful putback-based bidirectional programming language, explaining the underlying principles and showing how various kinds of bidirectional application can be developed in BiGUL.

1 Putback-Based Bidirectional Programming

In this chapter, the kind of bidirectional transformations (BXs) we discuss is aymmetric lenses [8], which basically consist of a pair of transformations¹: a forward transformation producing a view from a source, and a backward, or putback, transformation which takes a source and a possibly modified view, and reflects the modifications on the view to the source, producing an updated source. These two transformations should be well-behaved in the sense that they satisfy the following round-tripping laws:

The GetPut property requires that no change to the view should be reflected as no change to the source, while the PutGet property requires that all changes in the view should be completely reflected to the source so that the changed view can be successfully recovered by applying the forward transformation to the updated source.

The purpose of bidirectional programming is to develop well-behaved bidirectional transformations to solve various synchronization problems. A straightforward approach to bidirectional programming is to write two unidirectional transformations. Although this ad hoc solution provides full control over both get and putback transformations, and can be realized using standard programming languages, the programmer needs to show that the two transformations satisfy the well-behavedness laws, and a modification to one of the transformations requires a redefinition of the other transformation as well as a new well-behavedness proof. To ease and enable maintainable bidirectional programming, it is preferable to write just a single program that can denote both transformations.

Lots of work [2, 3, 8, 9, 12, 15, 16] has been devoted to the get-based approach, allowing the programmer to write, mainly, the forward transformation , and deriving a suitable putback transformation. While the get-based approach is friendly, a function will typically not be injective, so there may exist many possible functions that can be combined with it to form a valid BX. This ambiguity of is what makes bidirectional programming challenging and unpredictable in practice. For specific domains where declarative approaches suffice, the get-based approach works fine, but when it comes to problems for which it is essential to precisely control behavior, the get-based approach is inherently awkward: while most get-based languages/systems offer some features for programming behavior, the programmer ends up having to break the -based abstraction and figure out the semantics of their programs in excruciating detail to be able to reliably use these features, largely defeating the purpose of these languages/systems.

The main topic of this chapter is the putback-based approach to bidirectional programming. In contrast to the get-based approach, it allows the programmer to write a backward transformation and derives a suitable that can be paired with this to form a bidirectional transformation. Interestingly, while usually loses information when mapping from a source to a view, must preserve information when putting back from the view to the source, according to the PutGet property.

Before explaining how to program in practice, let us briefly review the foundations [5,6,7], showing that “putback” is the essence of bidirectional programming. We start by defining validity of as follows:

Definition 1

(Validity of ). We say that a function is valid if there exists a function such that both GetPut and PutGet are satisfied.

The first interesting fact is that, for a valid , there exists exactly one that can form a BX with it. This is in sharp contrast to get-based bidirectional programming, where many s may be paired with a to form a BX.

Lemma 1

(Uniqueness of ). Given a function, there exists at most one function that forms a well-behaved BX.

The second interesting fact is that it is possible to check the validity of without mentioning . The following are two important properties of .

• The first, which we call view determination, says that the equivalence of updated sources produced by a implies equivalence of views that are put back.

  $$\begin{aligned} \forall ~s, s', v, v'.~put~s~v~=~put~s'~v'~\Rightarrow ~v~=~v'&\qquad {\textsc {ViewDetermination}} \end{aligned}$$

  Note that view determination implies that is injective (with ).

• The second, which we call source stability, denotes a slightly stronger notion of surjectivity for every source:

  $$\begin{aligned} \forall ~s.~\exists ~v.~put~s~v~=~s&\qquad \qquad \qquad \qquad \qquad \qquad \qquad \text {S}{\textsc {ource}}\text {S}{\textsc {tability}} \end{aligned}$$

These two properties together provide an equivalent characterization of the validity of [5].

Theorem 1

A function is valid if and only if it satisfies ViewDetermination and SourceStability.

Practically, there are few languages supporting putback-based bidirectional programming. This is not without reason: as argued by Foster [7], it is more difficult to construct a framework that can directly support putback-based bidirectional programming.

In the rest of this chapter, we will introduce BiGUL [11] (pronounced “beagle”), a simple yet powerful putback-based bidirectional language, which grew out of some prior putback-based languages [13, 14]. BiGUL is implemented as an embedded language in Haskell, and we will assume that the reader is reasonably familiar with Haskell. After briefly explaining how to install BiGUL in Sect. 2, we will introduce basic BiGUL programming in Sect. 3, and see a few more examples about lists in Sect. 4. We will then move on to the underlying principles in Sect. 5, explaining the design and implementation of BiGUL in detail. Those readers who are more interested in practical applications or want to see more examples first may safely skip Sect. 5 (which is rather long) and proceed to the last three sections, which will show how various bidirectional applications can be developed, including list alignment in Sect. 6, relational database updating in Sect. 7, and parsing and “reflective” printing in Sect. 8.

2 Preparation: Installing BiGUL

BiGUL is implemented as an embedded domain-specific language in Haskell, and this chapter assumes that the readers have some Haskell background. (If not, see https://wiki.haskell.org/Learning_Haskell for a list of resources for learning Haskell; for the Haskell environment, it is recommended to install Haskell Platform at https://www.haskell.org/platform/.) BiGUL has been released to Hackage, and the latest version (1.0.1 at the time of writing) can be installed using Cabal in the usual way, by executing the following in the command line:

If you want to ensure compatibility with this chapter, you can instead install BiGUL-1.0.1 specifically by executing:

Now you can easily check whether BiGUL is correctly installed. First, create a simple file called Test.hs with the following content for importing BiGUL modules.

Then load it using GHCi.

If you see the above message, congratulations on your successful installation.

To make it more convenient to play with the BiGUL code in this chapter, the Haskell source files for Sect. 3 (Basic.hs), Sect. 4 (List.hs), Sect. 6 (Alignment.hs), Sect. 7 (Brul.hs), and Sect. 8 (BiYacc.hs) are provided at:

https://bitbucket.org/prl_tokyo/bigul/src/master/SSBX16/

They are also available as electronic supplementary material to the online version of this chapter on SpringerLink. There are some dependencies among the files: List.hs imports Basic.hs, and Brul.hs imports Alignment.hs. The imported files should be present in the same directory as the files being loaded.

3 A Quick Tour of BiGUL

Intuitively, we can think of a bidirectional BiGUL program

as describing how to manipulate a state consisting of a source component of type  and a view component of type ; the goal is to embed all information in the view to proper places in the source. For each , we can run it forwards by calling and backwards by calling :

Here, is a function mapping a source to a view, which can possibly fail: it either returns a successfully computed view wrapped in the constructor of , or signifies failure by producing the constructor. On the other hand, accepts an original source and uses a view to update it to get an updated source (and might fail as well).

In BiGUL, it suffices for the programmer to write the behavior (i.e., how to use a view to update the original source to a new source), and the (unique) behavior is obtained for free. The core of BiGUL consists of a small number of primitives and combinators for constructing well-behaved bidirectional transformations, which we introduce below.

3.1 Skip

The first primitive for writing is

The put behavior of keeps the source unchanged, provided that the view is computable from the source by  (while in the get direction, the view is fully computed by applying function to the source). Consider a simple defined by where

We can test its put behavior as follows:

It first checks if the view $\mathrm {100}$ is the square of the source $\mathrm {10}$. If that is the case, the original source is returned. But if the view is changed, say to $\mathrm {250}$, it should produce :

To see why produces , we may use instead of to get more information:

Each putback transformation in BiGUL is equipped with a unique for doing forward transformation. We can test the behavior as follows:

In prose: doing the forward transformation of on the source $\mathrm {5}$ gives the view $\mathrm {25}$. If fails, we can also use to see more information about the failure, analogous to .

As a simple exercise, can you see what the following does?

3.2 Replace

The second primitive is

which completely replaces the source with the view. For instance,

uses the view $\mathrm {100}$ to replace the source $\mathrm {1}$ and gets a new source $\mathrm {100}$.

3.3 Product

If we want to use a view pair to update a source pair , we can write or , a product of two putback transformations and , to use to update with and to with .

For instance, we can use to combine and to put a view pair into a source pair.

Generally, we can use nested s to describe a complicated structural mapping:

3.4 Source/View Rearrangement

So far, the source and view have been of the same structure. What if we wish to put a view into a source of a different structure, say , to replace by and by ? To do that, we need to rearrange the source and view into the same structure, and BiGUL provides a way of rearranging either the source or view through a “simple” $\lambda$-expression :

The “simple” $\lambda$-expression e should be wrapped inside Template Haskell quasi-quotes (written as in plain text Haskell); it is then processed and expanded by or to “core” BiGUL code, which is spliced (pasted) into the invocation site by Template Haskell, as instructed by ${^\$}(\ldots )$. By “simple” we mean that there should be no wildcards ‘’ in the argument pattern, and that the body can only contain the argument variables and constructors, and must mention all the argument variables. We will discuss the details later in Sect. 5.6. Returning to the problem of putting a pair into a triple, we may define the following putback transformation

by first rearranging the view to a triple with the same structure as the source, and then using to put the arranged view into the source . The type context above is required by BiGUL for printing debugging messages. And note that the two ‘$’ signs in the definition off have different meanings: the first one marks the beginning of a Template Haskell splice, while the second one is the low-precedence application operator.

The mechanism of source/view rearrangement enables us to process algebraic data structures such as lists and trees, by mapping an algebraic structure to the (nested) pair structure. The following example uses the view to replace the first element of a nonempty source list:

It rearranges the source (a nonempty list) to a pair with its head element and its tail , and the view to a pair , so that we can use  to replace  and $()$ to keep .

What if we wish to define a general putback transformation that uses the view to replace the th element of the source list? We can define it recursively as follows:

If is $\mathrm {0}$, we simply use to update the head element of the source with the view. Otherwise, we do the same arrangements on the view and the source as we did for , but then keep the head element unchanged and replace the th element of the tail of the source by the view.

As we know, any putback function in BiGUL is equipped with a function. For , we can test its behavior as follows; its corresponding function is actually the familiar index function $(\mathbin {!!})$.

Both and contain the programming pattern in which both the source and view are rearranged into a product and then further updates are performed on corresponding components. This is a ubiquitous pattern in BiGUL, for which we provide a more compact syntax:

The source and view are respectively decomposed using and inside the pattern quasi-quotes (written as in plain text Haskell), and corresponding elements are updated using the programs provided in the declaration quasi-quote ( in plain text Haskell). For example, we may describe by

In this concrete example, the three elements of the tuple (in both the source and view) are bound to the variables , , and , and they are sent to the three combinators as arguments in the part. Note that since does nothing on its source but checks if its view is $()$, we can just match that source element with a wildcard ‘’ in the source pattern and avoid writing in .

3.5 Case

The combinator is for case analysis, and the general structure is as follows:

It contains a sequence of cases, each of which is either or . We try the conditions of these cases in order and decide which branch we go into.

• For a normal case, takes two predicates, which we call the main condition and the exit condition. The predicate for the main condition is very general, and we can use any function of type to examine the source and view. The predicate for the exit condition checks the source only. If the main and the exit conditions are satisfied, then the BiGUL program after the arrow ‘$\Longrightarrow$’ (written in plain text Haskell and defined in the module Generics.BiGUL.Lib) is executed. The exit conditions in different branches are expected to be disjoint for efficient execution of the forward transformation.

• For an adaptive case, if the main condition is satisfied, a function of type is used to produce an adapted source from the current source and view before the whole is rerun, with the expectation that one of the normal cases will be applicable this time. Note that if adaptation does not lead to a normal case, an error will be reported at runtime. This is to ensure that BiGUL does not stuck in adaptation and fail to terminate.

As a simple example, consider using the view to replace each element in the source list. To do so, we use to describe a case analysis.

It consists of two normal cases and one adaptive case. The first normal case says that if the source is of length $\mathrm {1}$ (containing a single element), we rearrange the source list by extracting the single element, and replace this element with the view. The second normal case says that if the source has more than $\mathrm {1}$ element, we rearrange the source list to a pair of its head element and its tail, rearrange the view by duplicating it to a pair, and use one copy of the view to replace the head element, and the other copy to recursively replace each element in the tail of the source. The last adaptive case says that if the source is empty, we adapt the source to a singleton list with the don’t-care element $\bot$ (‘undefined’ in plain text Haskell), and rerun the whole executing the first normal case.

Note that in the first running example, the source $[]$ is first adapted to $[\bot ]$, and the don’t care element $\bot$ is replaced by $\mathrm {100}$ at the rerun of the whole .

As another interesting example, we define , which can safely embed any pair of well-behaved and into BiGUL. It is defined as follows:

where, given a pair of well-behaved and functions, if the view is the same as that produced by applying to the source, we make no change on the source with (hinting that the view can be produced using g), otherwise we adapt the source using to reflect the change on the view to the source. Note that if and form a well-behaved bidirectional transformation, in the rerun of the whole after the adaptation, the first normal case will always be applicable. To see a use of , we may define the following putback function to update a pair with its sum.

While we allow a general function to describe the main condition or the exit condition, it is usually more concise to use patterns to describe these conditions. For instance, we may replace the condition by

Here, the meaning of a boolean-valued pattern-matching lambda-expression is redefined as a total function which computes to when an input does not match the pattern; this meaning is different from that of a general pattern-matching lambda-expression, which fails to compute (and throws an exception) when the pattern is not matched. For example, in general the lambda-expression will fail to compute if the first input is not a singleton list; when used in branch construction, however, the lambda-expression will compute to upon encountering an empty list. A unary condition like where only the pattern part matters can be abbreviated to

to further reduce syntactic noise. Finally, to also allow this kind of abbreviation in main conditions, BiGUL provides a special form for the case where the main condition is specified as the conjunction of two unary predicates on the source and view respectively:

and a special form for the case where the main condition is specified as the conjunction of two unary predicates on the source and view respectively:

3.6 View Dependency

Sometimes, a view may contain derived values that are computed from other parts of the view, and the view should be consistently changed. For instance, for the view , the second component is an indicator showing whether or not the first component is an even number. To capture this, BiGUL provides

to describe this intention. We may, for example, define

to replace all elements of the source by the first component of the view, while checking whether the second component is consistent with the first component.

As seen in the last running of , it reports an error because the view is inconsistent: $\mathrm {100}$ is an even number, so the second component should be .

3.7 Composition

BiGUL programs can be composed sequentially:

This combinator is straightforward in the direction: (where and ) simply applies to its input of type  to compute an intermediate value of type , which is then processed by to produce the final result of type . Its direction is more complex: starts with a source and a view , and the aim is to produce an updated source of type . The only way to proceed is to use to put  into some intermediate source  of type , and to produce this  we are forced to use on . We can then update  with  to  using , and update  with  using . In general, programs involving are significantly harder to think about since we have to think in both and directions to figure out precisely what is going on.

As a simple example, consider that we wish to use the view to update the head element of the head element of a list of lists. We can define such a putback function as the following by composing with .

The following is an example to demonstrate this:

4 Bidirectional Programming on Lists

To give some more involved examples, in this section we demonstrate that many list functions can be bidirectionalized using BiGUL. The putback behaviors of these functions are in fact non-trivial, and the reader might want to skip to later sections in which more examples are developed, starting from Sect. 6.

To show the correspondence with the original list functions, we prefix the original forward function names with lens. Note that in our context, the original forward functions can be automatically derived from the new putback transformations by calling .

We shall focus on bidirectionalizing , an important higher-order function on lists:

Many interesting functions can be defined in terms of :

where sums up all the elements in a list, and applies to every element in a list.

We start by developing a putback function for in BiGUL:

where we hope to define a putback program of type that is to use the view to update the source, a list together with a value, by recursively applying a simpler putback function of type (until a condition is satisfied or all the list elements have been visited). The program is somewhat tricky, and is probably not easy to understand since is involved.

The program accepts a putback function and a view condition , and performs a case analysis to put the view to the source . If the view satisfies but the list in the source is not empty, then it adapts the list to be empty. If the list in the source is empty, we do nothing but use the view to replace the second component of the source. Otherwise, we rearrange the source from the form of to that of , and apply recursively with a composition with . One may understand the composition through the following picture (where ).

$$\begin{aligned} (x,(xs,e)) \overset{r}{\leftrightarrow } (x,e') \overset{bx}{\leftrightarrow } v \end{aligned}$$

With , we can redefine many list functions from the putback point of view. As the first example, consider :

We can define its putback function as follows.

Here has the type of and is defined on that has the type of .

Note that, for testing, we embed into our framework the bijective functions for increasing and decreasing a number by $\mathrm {1}$.

For a second example, consider the function , which is to sum up all elements of the list starting from the seed . If the sum is changed, there are many ways to reflect this change to the input . The following describes one way in BiGUL:

which will reflect the change difference on the view to the head element of if is not empty, or to the seed otherwise. We may choose other ways, say to reflect the change difference on the view only to the seed by defining

Note that although , their putback behaviors are different:

It is worth noting that our definition of is just one putback function for , and there are many others. This reflects the fact that one can have many s, each describing one updating strategy.

5 BiGUL’s Bidirectionality

We have been writing programs, usually having a corresponding in mind but not explicitly describing it, and yet BiGUL is capable of finding the right behaviour as if it could read our mind. How? We will see that, when writing a BiGUL program, we are always simultaneously describing both a function and a function, which are guaranteed to be a well-behaved pair. And the “mind-reading” ability is far from magic: It is the consequence of the fact that well-behavedness directly implies that is uniquely determined by , which is the main motivation for taking a putback-based approach. In this section, we will first review the theory, this time explicitly taking partiality into account, and then we will dive into BiGUL’s internals to get a taste of putback-based design.

This is a fairly long section, but it is not a prerequisite for subsequent sections; readers who wish to see more examples first or are more interested in practical BiGUL applications can safely skip this section and proceed to Sect. 6.

5.1 Lenses, Well-Behavedness, and the Fundamental Theorem

Formally, we call a well-behaved pair of and a lens:

Definition 2

(lens). A lens between a source type s and a view type v consists of two functions:

satisfying two well-behavedness laws:

In the original formulation [8], a lens refers to just a pair of functions having the right types, and one needs to explicitly say “well-behaved lens” to mean a well-behaved pair; we will, however, discuss well-behaved lenses only, so we build well-behavedness into our definition of lenses by default. Note that this definition models partial transformations explicitly as -valued functions: and are total functions that can nevertheless produce to indicate failure. From now on, this definition replaces the one in Sect. 1, where only total lenses were discussed. Also note that these well-behavedness laws are actually easy to satisfy vacuously, by making the transformations produce all (or most of) the time. One important task of the BiGUL programmer is thus to meet certain side conditions for guaranteeing the totality of their BiGUL programs. These side conditions will be introduced below along with the relevant BiGUL constructs.

From this revised definition of well-behavedness, we can immediately prove a reformulation of Lemma 1:

Theorem 2

(uniqueness of get). Given two lenses whose components are equal, their components are also equal.

Proof

Let l and r be two lenses; denote their components as / and / respectively, and assume that . Then for any s and v,

(This also entails that if and only if .)    $\square$

This might be called the “fundamental theorem” of putback-based bidirectional programming, as the theorem guarantees that the BiGUL programmer is in full control of the bidirectional behaviour—programming the behavior is sufficient to determine the behaviour. Also, to the language designer, the theorem gives a kind of reassurance that, once the behaviour of a construct is determined, there is no need to worry about which behaviour should be adopted—there is at most one possibility. This is in contrast to -based design, in which there are usually more than one viable semantics that can be assigned to a -based construct, and the designer needs to justify the choice or provide several versions.

For the rest of this section, we will look at several constructs of BiGUL in detail to get a taste of putback-based design. Each BiGUL construct is conceived, at the design stage, as a lens (like and ) or a lens combinator (like ), which constructs a more complex lens from simpler ones. The and components of these lenses usually have to be developed together, but for each lens we will employ a more “-oriented” design process: We start from an intended behaviour, and then add restrictions so that we can find a corresponding . This does not guarantee that the lenses we arrive at will have a “strong flavour”—that is, some of the lenses will be as (or even more) suitable for -based programming as for putback-based programming. But we will also see that some other lenses are more naturally understood in terms of their behaviour.

5.2 Replacement

The simplest lens is probably , which replaces the entire source with the view:

Is there a semantics that can be paired with this ? Yes, quite obviously—in fact, PutGet directly gives us the definition of :

We still need to verify GetPut, which can be easily checked to be true.

5.3 Skipping

Coming up next is , whose natural behaviour is

Considering PutGet, though, we immediately see that this behaviour is too liberal: If the view is simply thrown away, how can possibly recover it? One way out is to require that the view is trivial enough such that it can be thrown away and still be recovered, by setting the view type of to the unit type $()$. Then it is easy for to recover the view, for which there is only one choice:

This is the approach adopted prior to BiGUL 1.0.

More generally, we can establish well-behavedness as long as has only one view choice for each source, regardless of what the view type is. The existence of this “unique choice” is witnessed by a function , which we add as an additional argument to . The direction is then

From the direction, we may think of this function  as specifying a consistency relation, saying that the view information is completely included in the source (since you can compute the view from the source) and can be safely discarded. can be used if and only if the source and view are consistent in that sense, and this is the side condition about that the BiGUL programmers need to be aware of if they want their programs using to be total. We thus arrive at:

This pair of and can be verified to be well-behaved. , which features in BiGUL 1.0, is one lens which turns out to be more easily understood from the direction—it bidirectionalizes any $get$ function whose codomain has decidable equality, albeit trivially. We recover the first version of as a special case by setting  to .

5.4 Product

For a simplest example of a lens combinator, we look at . Both the source and view types should be pairs; accepts two lenses, say  and , and applies them respectively to the left and right components:

The direction is unsurprising:

Having constructed and from  and , we also expect that their well-behavedness is a consequence of the well-behavedness of  and . While this may look obvious, we take this opportunity to show how a well-behavedness proof for a lens combinator can be carried out formally and in detail. To prove PutGet, for example, we should prove that the assumption

(1)

implies the conclusion

(2)

Both equations say that a somewhat complicated monadic -program computes successfully to some value. It may seem that we need some messy case analysis, but what we know about -programs tells us that such a program computes successfully if and only if every step of the program does, and this helps us to split both (1) and (2) into simpler equations. Formally, we have this lemma:

Lemma 2

Let and . Then, for all ,

if and only if

Proof

Case analysis on .    $\square$

This lemma can be nicely applied to -programs written in the $\mathbf {do}$-notation, transforming such programs into predicates saying that a program computes to some given value. To do it more formally: Define a translation $\mathcal {S}$ from $\mathbf {do}$-blocks of type to predicates on  by

Then we can extend Lemma 2 to the following:

Lemma 3

The proposition

is true if and only if

Proof

By induction on the list structure of , using Lemma 2 repeatedly.    $\square$

For example, applying $\mathcal S$ to yields

where the last equation is equivalent to (since for the . Applying Lemma 3 and doing some simplification, (1) is equivalent to

Similarly, (2) can be shown to be equivalent to

The entailment is then just PutGet for  and .

5.5 Case Analysis

This is a representative combinator in BiGUL, and arguably the most complex one. For simplicity, let us consider a two-branch variant of . A branch is a condition and a body; since in we manipulate both a source and a view, the conditions in general can be binary predicates on both the source and view. We thus define the type of branches as:

and consider the following variant of :

The straightforward behaviour is

That is, depending on which condition is satisfied (with having higher priority), we execute either or , or fail the computation if neither of the conditions is satisfied. Now, again, we ask the question: Can we find a behaviour to pair with this ?

Ruling out branch switching for PutGet. An important working assumption here is that we want lens combinators to be compositional: When we looked at , for example, we defined its and in terms of those of the smaller lenses, and derived the overall well-behavedness from that of the smaller lenses. For , this implies that, when establishing well-behavedness, we want a following a (or a following a ) to use the same branch taken by the (or the ), so we can make use of PutGet (or GetPut) of the branch. The current behaviour of does not leave any clue in the updated source about which branch is used to produce it, though, so it is impossible for to always choose the correct branch.

One solution, which does not require changing the syntax of , is to check that the ranges of the branches are disjoint. In general, for a lens, the range of a can be shown to coincide with the domain of the corresponding . So the behaviour of can simply try to execute both branches on the input source, and there will be at most one branch that computes successfully. We can put (expensive) disjointness checks into such that if succeeds, the subsequent will have at most one branch to choose:

The function is from Haskell’s prelude and has type depending on whether the third, -typed, argument is or a -value, the result is either the first argument or the second argument applied to the value wrapped inside . In the first branch of the code above, if successfully produces an updated source $s^\prime$, we will ensure that does not succeed: If is as we want, we will ; otherwise we emit .

If favours the first branch, meaning that it declares success as soon as the first branch succeeds (without requiring that the second branch fails),

then we can also omit the check in ’s first branch:

Ruling out branch switching for GetPut. The GetPut direction, on the other hand, still does not avoid branch switching—the outcome of does not say anything about which of and will be satisfied in the subsequent . So we add some checks to such that ’s success will tell us which branch will be chosen by :

The definition of should also be revised to use for the disjointness check. This fixes GetPut, but breaks PutGet! Since does not guarantee that the updated (not the original) source and the view satisfy the condition of the branch executed, even though will be able to choose the correct branch, the subsequent, newly added check is not guaranteed to succeed. We thus also need to add similar checks to :

Now this pair of and can be verified to be well-behaved.

Improving the Efficiency of get. The efficiency of the current does not look very good, especially when, in general, more than two branches are allowed, and has to try to execute each branch, possibly with a high cost, until it reaches a successful one; also, inefficient affects the efficiency of , since this calls to check range disjointness. An idea is to ask the programmer to make a rough “prediction” of the range of each branch: We enrich with a third component, which is a source predicate:

This new predicate is supposed to be satisfied by the updated source; we again add checks to to ensure this:

Let us call and the main conditions, and and the exit conditions. The exit condition, in general, over-approximates the range of a branch. Well-behavedness tells us that the range of $put$ is exactly the domain of the corresponding $get$. Thus, in the direction, every source in the domain of a branch satisfies the exit condition. Contrapositively, if a source does not satisfy the exit condition, then for that branch will necessarily fail, and we do not need to try to execute the branch at all. This leads to the following revised definition of :

If we do not care about efficiency, we can simply use as exit conditions, and the behaviour will be exactly the same as the previous version. But if we supply disjoint exit conditions, then will try at most one branch. Incidentally (but actually no less importantly), making exit conditions explicit also encourages the programmer to think about range disjointness, which is essential to guaranteeing the totality of .

Adaptation. We have seen that, to make total, one thing we need to ensure is that the main condition of a branch should be satisfied again after the update. In practice, the main condition is usually closely related to the consistency relation, and we will only be able to deal with sources and views that are already more or less consistent; this is a rather severe restriction. As we have seen in Sect. 3.5, the solution is to introduce a different kind of branch called adaptive branches, which can deal with sources and views that are too inconsistent by adapting the source to establish enough consistency such that a normal branch becomes applicable. Again, for simplicity, we consider only a variant of which has just one adaptive branch at the end:

The execution structure of becomes slightly more complicated, as the whole thing has to be run again after adaptation; to ensure termination, we require that the second run does not match an adaptive branch again. This is realized in BiGUL in continuation-passing style:

Major work is now moved into a separate function , which takes an extra argument of type . This extra argument is a continuation that takes over after the body of an adaptive branch is executed, and is invoked with the adapted source. The requirement of not doing adaptation twice is met by setting itself as a continuation, and this inner takes the continuation that always fails.

What about ? It turns out that can simply ignore the adaptive branch! If you have doubt about this “choice”, just invoke the fundamental theorem (Theorem 2): The behaviour is exactly what we want, and we can verify that the pair of and is well-behaved, so we are reassured that our “choice” is “correct”, simply because there is no other choice of .

To sum up, we have arrived at a simpler variant of which nevertheless has all the features of the multi-branch in BiGUL. We have inserted various dynamic checks into the semantics, and the BiGUL programmer needs to be aware of these constraints to make execution of succeed: For each normal branch, (i) the main condition should be satisfied after the update, (ii) the main conditions of the branches before this one should not be satisfied after the update, and (iii) the exit condition should be satisfied by the updated source. Also the ranges of all the normal branches should be disjoint; the programmer is encouraged to write disjoint exit conditions, which imply disjointness of the ranges, and improve the efficiency of . Finally, for each adaptive branch, the adapted source and the view should match the main condition of a normal branch.

5.6 Rearrangement

Source and view rearrangements are also among the more complex constructs of BiGUL. Their complexity lies in the strongly and generically typed treatment of pattern matching, though, rather than their bidirectional behavior. (We are referring to “pattern matching” in functional programming, where a pattern matching checks whether a value has a specific shape and decomposes it into components. For example, matching a list with a pattern checks whether the list has two or more elements, and then binds  to the first element,  to the second one, and  to the rest of the list.) The two kinds of rearrangement are similar, and we will discuss view rearrangement only. We will start by formalizing pattern matching as a bidirectional operation—in fact an isomorphism. Based on pattern matching, evaluation and inverse evaluation of rearranging $\lambda$-expressions can be defined, again forming an isomorphism. The semantics of a view rearrangement is then the composition of this latter isomorphism with the lens obtained by interpreting the inner BiGUL program.

Strongly typed pattern matching, bidirectionally. Pattern matching is inherently a bidirectional operation: In one direction, we break something into a collection of its components at the variable positions of a pattern. This collection can be considered as indexed by the variable positions, and acting like an environment for expression evaluation. Indeed, conversely, if we have a pattern and a corresponding environment, we can treat the pattern as an expression and evaluate it in the environment. These two directions are inverse to each other, i.e., they form a (partial) isomorphism. For the language designer, it may be slightly tedious to establish such isomorphisms, but for the programmer, pattern matching and evaluation are arguably the most natural way to decompose and rearrange things. Previous bidirectional languages usually provide theoretically simpler combinators for decomposition and rearrangement, but they are hard to use in practice. BiGUL’s native support of pattern matching, on the other hand, turns out to be one important contributing factor in its usability.

BiGUL’s patterns are strongly typed: The programmer has to declare a target type for a pattern, and the pattern is guaranteed, through typechecking, to make sense for that target type. This can be achieved by defining the datatype of patterns as a generalised algebraic datatype:

A pattern can be a (nameless) variable, a constant, a product, a or injection (for the type), or a generic constructor, and its target type is given as the index in its type. For example, the pattern has type , and can only be used to match those values of type (and matching succeeds only for the value ). The typeclass contains the types that are isomorphic to (and therefore interconvertible with) a sum-of-products representation. The isomorphism is witnessed by

which will be used to define pattern matching and evaluation. For example, is an instance of , and , an isomorphic sum-of-products representation of , is . The two functions witnessing the isomorphism for lists are defined by

How do we define pattern matching? As we mentioned above, the result of matching a value against a pattern is an environment indexed by the variable positions of the pattern. For example, matching a list against the cons pattern

(3)

should produce an environment containing its head and tail. Here we want a safe (but not necessarily efficient) representation of the environment type, in the sense that the indices into the environment should be exactly the variable positions of the pattern, and we want that to be enforced statically by typechecking. In other words, this environment type depends on the pattern, and a way to compute this type is to encode it as a second index of the datatype:

Notice that an environment type is just a product of types—for example, the environment type computed for the cons pattern (3) is

(4)

We will discuss later, which is simply defined by

Now we can define the (strongly typed) pattern matching operation:

and its inverse (which is total):

Precisely speaking, we have

for all , , and , establishing a (half-) partial isomorphism between and .

$\varvec{\lambda }$-expressions for rearrangement and their evaluation. Now consider view rearrangement, which evaluates a “simple” pattern-matching $\lambda$-expression on the view and continues execution with the transformed view. The body of the $\lambda$-expression refers to the variables appearing in the pattern. How do we represent such references? We have seen that an environment type is a product, i.e., a binary tree; to refer to a component in an environment, we can use a path that goes from the root to a sub-tree. In BiGUL, these paths are called directions:

The type of a direction is indexed by the environment type it points into and the component type it points to. Note that the type of is specified to work with only environment types marked with ; this is for ensuring that a direction goes all the way down to an actual component at a variable position of the pattern, rather than stopping half-way and pointing to a sub-tree which include more than one component. For example, for the environment type (4) for the cons pattern, only two directions are valid, namely and , whereas alone would point to the entire environment instead of one of the variable positions, and is ruled out by typechecking (in the sense that it is impossible for to have type for any ). It is easy to extract a component from an environment following a direction:

Now we can define expressions, which are similar to patterns but include directions rather than variables, to represent the body of rearranging $\lambda$-expressions:

For example, the rearranging $\lambda$-expression

(5)

is represented by the cons pattern (3) and the pair expression

(6)

Evaluating an expression under an environment is similar to inverse pattern matching:

The type of is then:

Note that in the type of , the types of the pattern and expression share the same environment type index, ensuring that the directions in the expression can only refer to the variable positions in the pattern. And the behaviour of is simply:

Inverse evaluation of rearranging $\varvec{\lambda }$-expressions. For the direction, after executing the inner BiGUL program to obtain an intermediate view, we should reverse the roles of the pattern and body in the rearranging $\lambda$-expression , using  as a (possibly non-linear) pattern to match the intermediate view, and computing the final view by evaluating . For example, the direction of view rearrangement with the $\lambda$-expression (5) turns a view list into a pair, on which the inner program operates; in the direction, the inner program will extract from the source an intermediate view pair, which should be converted back to a list by the inverse $\lambda$-expression . In more detail, given an intermediate view pair , we match it with the pair expression (6), and see that x is associated with the direction and with . From such associations we can reconstruct an environment of type (4) with and in the right places, and then we can evaluate the cons pattern (3) in this reconstructed environment, arriving at the final view .

In general, the intermediate view will be decomposed according to the body expression, and eventually each of its components will be paired with a direction indicating which variable position the component should go into in the reconstructed environment. To do the reconstruction, we can prepare a “container” which is similar to an environment except that the variable positions are initially empty. For each pair of a component and a direction, we try to put that component into the place in the container pointed to by the direction; if two components are put into the same position (indicating that the $\lambda$-expression uses a variable more than once), then they must be equal. In the end, we check that all places in the container are filled, and then use it as an environment to evaluate the pattern. Again, to compute the type of containers from a pattern, we add a third index to :

A container type is just like an environment type except that the variable positions give rise to instead of . For the cons example, the computed container type is

(7)

The first step—matching a value with an expression—can then be implemented as:

This function initially takes an empty container, which is generated by:

And then we can try to convert a container to an environment, checking whether the container is full in the process:

We can let out a sigh of relief once we successfully get hold of an environment, since the last step—inverse pattern matching—is total. To sum up:

To be concrete, let us go through the steps of inverse rearranging in the cons example. Starting with an intermediate view and an empty container of type (7), will invoke twice, the first time updating the container to and the second time to . The resulting container is full, and thus will successfully turn it into an environment of type (4), in which we evaluate the cons pattern (3) and obtain .

Conceptually, this is just reversing pattern matching and expression evaluation. To actually prove the well-behavedness, though, we need to reason about stateful computation (which is what essentially is), which involves coming up with suitable invariants and proving that they are maintained throughout the computation.

It is interesting to mention that there would be a catch if we designed this combinator from the direction: It is tempting to think that, since a rearranging $\lambda$-expression gives rise to a partial isomorphism, which can be lifted to a lens, we can simply compose the lens lifted from the isomorphism with the inner lens to give a lens semantics to . This would result in a redundant computation of an intermediate source which is immediately discarded, and now the success of the whole computation would unnecessarily depend on that of the intermediate source. To eliminate the redundant computation, we would need to use a special composition which composes a lens directly with an isomorphism on the right. Such a need would be hard to notice since the behaviour of the two compositions are the same; that is, we really have to think in terms of to see that the special composition is needed.

5.7 Summary

In one (long) section, we have examined the internals of BiGUL. After seeing the definition of (well-behaved) lenses that takes partiality explicitly into account, we have gone through the development of most of BiGUL’s constructs and justified their well-behavedness—in the case of , we have even seen a more formal and detailed well-behavedness proof. The construct is the most interesting one in terms of its design for achieving bidirectionality, while the rearrangement operations showcase more advanced datatype-generic programming techniques in Haskell for guaranteeing type safety. We will now shift our focus back to BiGUL programming, this time looking at some larger examples.

6 Position-, Key-, and Delta-Based List Alignment

In the next three sections, we will talk about some applications in BiGUL, starting with the list alignment problem. List alignment is one of the tasks that frequently show up when developing bidirectional applications. When the source and view are both lists, and the direction (i.e., the consistency relation) is a , how do we put an updated view—the updates on which might involve insertions, deletions, in-place modifications, and reordering—into the source? This topic has be treated by Barbosa et al.’s matching lenses [1], which are special-purpose lenses into which several fixed alignment strategies are hard-coded. Below we will see how a number of alignment strategies can be programmed with BiGUL’s general-purpose constructs, instead of having to extend the language with special-purpose alignment constructs.

Throughout the section, we use a concrete example to introduce three variations of list alignment. Suppose that we represent a payroll database as a list. (This is a slightly inadequate setting for explaining list alignment, because entries in a database are usually unordered. But let us assume that order matters.) Each entry is a triple—more precisely, a pair whose second component is again a pair—consisting of an identification number (“id” henceforth), a name, and a salary number:

For example, here is a sample payroll database:

Suppose that the human resource department is in charge of hiring or sacking employees but does not handle salary numbers, so the entries of the database are presented to them only as pairs of ids and names:

For example, is presented to them as

on which they can make modifications. It is easy to write a BiGUL program to synchronize the source and view elements:

The problem is then how the correspondences between sources and views in the two lists can be determined, so that can be applied to the right pairs.

6.1 Position-Based Alignment

As a first exercise, we consider the simplest strategy, which matches source and view elements by their positions in the lists. If the source list has more elements than the view list, the extra elements at the tail are simply dropped; if the source list has fewer elements, then new source elements have to be created, which we can specify as a function:

The salary is set to zero, which could be taken care of by, say, the accounting department later. We will use and as the element synchronizer and creator respectively for our payroll database throughout this section, but our alignment programs will not be restricted to the payroll database setting—we will develop our alignment programs generically, setting the source and view types as polymorphic type parameters ( and  below) and also the element synchronizer and element creator as parameters ( and  below), so the alignment programs can be widely applicable. Here is how we implement position-based alignment, which is fairly standard:

The normal branches deal with the situations where both lists are empty or non-empty, and the adaptive branches remove or create elements when the lengths of the two lists differ.

The direction of does exactly what we want it to do:

It should be quite obvious, though, that the direction is not so useful for our purpose. If we sack Josh:

then the database will be updated to:

where Jeremy inadvertently gets Josh’s original salary. Even if we do not remove any employee, we may still want to reorder them:

and now everyone gets the wrong salary:

This first exercise shows that the alignment problem is inherently one that should be solved from the direction. It is easy to implement the direction correctly, but what matters is the behavior.

6.2 Key-Based Alignment

A more reasonable strategy is to match source and view elements by some key value. In our example, we can use the id as the key. Key-based alignment might seem much more complex than position-based alignment, but, in fact, we can just revise to get a BiGUL program for key-based alignment!

First of all, we need to somehow obtain the keys. In our example, on both the source and view we can use to extract the key value. In general, we can further parametrize the alignment program with key extraction functions and for some type  of key values:

The first normal branch of still works perfectly. As for the second normal branch, we should revise the main condition to also require that the head elements of the two lists have the same key value:

The first adaptive branch, again, works well. The second adaptive branch, on the other hand, is no longer applicable: since the main condition of the second normal branch has been tightened, it is no longer the case that this adaptive branch will receive only empty source lists. In fact, whether the source list is empty or not is irrelevant here—what matters now is whether the key of the first view is in the source list. If it is, then we bring the (first) source element with the same key value to the head position, and the second normal branch can take over; otherwise, we create a new source element. This gives us key-based alignment:

Note that the program does not assume that keys are unique—if there are n view elements having the same key, then the first n source elements with that key will be retained and synchronised with those view elements in order. This strategy is a somewhat arbitrary choice, but can be changed by, for example, using a different . (On the other hand, in practice it is probably wiser to enforce uniqueness of keys, so that we can be sure which source element will be used to match a view element, and do not need to rely on the choices made by the implementation.)

Back to our payroll database example. The direction behaves the same:

Unlike position-based alignment, view element deletion can now be reflected correctly:

And reordering as well:

So it seems that key-based alignment is just what we need. Indeed, key-based alignment usually works well, but there is an important assumption: the key values should not be changed. If, for example, we decide to assign a different id to Josh:

Then the effect is the same as sacking Josh and then hiring him again, and his salary is thus reset:

The problem is that we cannot distinguish modification from deletion and insertion pairs. To be able to have such distinction, we need the notion of deltas [4], which allows us to explicitly represent and keep track of the correspondences between source and view elements.

6.3 Delta-Based Alignment

A (horizontal) delta between a source list and a view list is a list of pairs of corresponding positions:

For example, the delta we have in mind between the source list and the view list is $[(\mathrm {0},\mathrm {0}),(\mathrm {1},\mathrm {1}),(\mathrm {2},\mathrm {2})]$, which, in particular, associates the source and view entries for Josh since $(\mathrm {1},\mathrm {1})$ is included, instead of $[(\mathrm {0},\mathrm {0}),(\mathrm {2},\mathrm {2})]$, which indicates that Josh’s source entry does not correspond to any view entry and should be deleted, and that Josh’s view entry does not correspond to any source entry and is thus new. Deltas can easily represent reordering as well. For example, we would supply the delta between and as $[(\mathrm {0},\mathrm {1}),(\mathrm {1},\mathrm {2}),(\mathrm {2},\mathrm {0})]$, associating the 0th element in the source—namely the one for Zhenjiang—with the 1st element in the view, and so on. Comparing this treatment with the key-based one, we might say that keys are “poor man’s correspondences”, which are not as explicit and unambiguous as . A between source and view lists directly describes the accurate correspondences between them, whereas with keys the correspondences can only be inferred, sometimes inaccurately.

So the input now includes not only source and view lists but also a delta between them. Recall key-based alignment: what it does overall is to bring the first matching source element to the front for each view element, so the source list is updated throughout execution, with the links between the source and view elements gradually and implicitly restored. If we are doing something similar with delta-based alignment, then when the source list is updated, the delta should also be updated to reflect the restored consistency. This suggests that the delta should be paired with the source list, so that it can be updated. The type we use for the delta-based alignment program is thus:

Here we take a simpler approach to implementing , analyzing the problem into just two cases: The delta can tell us either that the source and view elements are all in correspondence, in which case a simple position-based alignment suffices, or that we need to do some rearrangement of the source elements, which can be done by adaptation. In BiGUL:

The source and view lists are in full correspondence if and only if they have the same length and the delta associates all their elements positionally. This full positional delta can be computed by . When this is the case, it suffices to call to carry out element-wise synchronization, since no rearrangement is required. Otherwise, we enter the adaptive branch, which constructs a new source list in full correspondence with the view list, drawing elements from the original source list or creating new ones as the delta dictates. The new source list is in full correspondence with the view list, so the delta we pair with it is the one computed by .

Only when performing does a delta make sense. When performing , however, we still need to supply a delta since it is part of the source; but there is a natural choice, namely . So we define:

It is easy to prove that, given the same  and , these two functions do form a lens. The key observation is that the delta produced by is necessarily the one computed by , so, for example, in PutGet, throwing away the delta in the direction is fine because it can be recomputed by , and the direction can resume from exactly the same source pair.

Back to our example. We can now update Josh’s id without resetting his salary by providing a full delta indicating that there are only in-place updates:

Besides obvious modifications like reordering, we can also do some fairly subtle modifications now: If we actually sack Josh and replace him with a new Josh (inheriting the original Josh’s id) whose salary should be reset (to be re-considered by the accounting department), we can say so by providing a partial delta:

One alignment to rule them all. Where do deltas come from? In general, we may provide a special view editor which monitors how the view is modified and produces a suitable delta. But in more specialized scenarios, deltas can simply be computed by, for example, comparing the source and view. We can formalize this delta computation as:

and further parametrize :

Position-based and key-based alignment can then be seen as special cases of delta-based alignment using specific delta-computing strategies. For position-based alignment, we simply compute the identity delta:

And for key-based alignment, we compute a delta associating source and view elements with the same key:

We can check that these strategies indeed give us position-based and key-based alignment:

7 Bidirectionalizing Relational Queries with BiGUL

In work on relational databases, the view-update problem is about how to translate update operations on the view table to corresponding update operations on the source table properly². Relational lenses [3] try to solve this problem by providing a list of combinators that let the user write get functions (queries) with specified updated policies for put functions (updates); however this can only provide limited control of update policies. To resolve this problem, we define a new library Brul [17], where two putback-based combinators (operators) are designed to specify update policies, from which forward queries (selection, projection, join) can be automatically derived.

• is to update a source list with a view list by aligning part of source elements filtered by a predicate with view elements according to a matching criteria between source element and view element;

• is to decompose a join view to update two sources.

In this section, we will focus on . As will be seen in Sect. 7.3, it can describe more flexible update strategies (related to selection/projection queries) than relational lenses, while the well-behavedness is guaranteed for free.

7.1 Relational Database Representation

A relational table () is denoted by a list of records (where the order does not really matter), and each record () is denoted by a list of attributes of type , which could be an integer, a string, a floating point number, or a double-precision floating point number.

To allow pattern matching on the newly defined algebraic data type in BiGUL, we need to add the following declaration.

Consider the table in Fig. 1 that stores five music track records, and each record contains its Track name, release Date, Rating, Album, and the Quantity of this Album. We can represent it as follows, where all the records have the same structure.

Fig. 1.

Source table

7.2 Relation Alignment

The alignment of two relational tables, which is related by a selection/projection query, is similar to the key-based list alignment in Sect. 6. The difference is that we need to consider filtering on (i.e., selection of) the source records based on a condition.

Let us see how to extend (in Sect. 6) to implement the new align that can deal with filtering of source elements. We extend with two new arguments; one is the predicate for filtering source elements, and the other is the function for hiding/concealing source elements if their corresponding elements are removed from the view. As seen below, has a similar case structure as that of , except that we refine the third case of into two cases (the third and the fourth cases of ): the third case says that if the view is empty but the first record in the source satisfies , we should hide this record using , and the fourth case says that if the first record of the source does not satisfy , we simply ignore it and continue with the remaining records.

To test, recall the example in Sect. 6. Consider the following use of , denoting that the view is selected from those records from the source whose salary is greater than $\mathrm {1000}$, and that if a view record is removed, the corresponding record in the source will be removed (and thus hidden).

We have:

7.3 Describing Update Policies in Selection/Projection

With , we can describe various update policies for the selection/projection queries. To be concrete, consider the following selection/projection query:

which extracts the track, rating, album and quality information from those music tracks in the source whose quantity is greater than $\mathrm {2}$. Let us see how to write a single BiGUL program so that its does the above query and its describes a specific update policy.

The first BiGUL program is below.

It tries to match the source records whose is greater than $\mathrm {2}$ with the view records by the key (). There are three cases:

• A source record is matched with a view record: we first use a rearrangement function to rearrange the view from a four-element list to a five-element list with the second element matched against a widecard. This rearrangement function reshapes the view to match the shape of the source. Then, the element in the source is d by the corresponding element in the view.

• A view record that has no matching source record: a new source record is created with a default value d filled into the Date.

• A source record that has no matching view record: we simply delete this record by returning .

Now if we wish to hide the source record by setting its to $\mathrm {0}$ rather than deleting it if it has no matching view record, we could simply change the last line of and get as follows.

To test, let us see some concrete running examples of using . Recall defined in Sect. 7.1. We can confirm that performs the query given at the start of this subsection.

Now suppose that we change the above result (view) to the following by raising the rating of from $\mathrm {3}$ to $\mathrm {4}$, raising the quality of from $\mathrm {4}$ to $\mathrm {7}$, and deleting :

We can reflect these changes to the source by performing with .

In the updated source, the changes of rating and quality are correctly reflected, and the music track is removed. Note that we may reflect the changes to the source by performing with , another update strategy, and we will keep the music track while setting its quality to be $\mathrm {0}$.

8 Parsing and Reflective Printing

When we mention the front-end of a compiler, we usually think of a parser that turns concrete syntax, which is designed to be programmer-friendly and provides convenient syntactic sugar, into abstract syntax, which is concise, structured, and easily manipulable by the compiler back-end. There is another direction, though, in which a printer turns abstract syntax back into concrete syntax. This is useful, for example, for reporting the result of compiler optimizations done on abstract syntax to the programmer, who knows only concrete syntax. In this case, though, we would want to print the optimized program in a form that is as close to the original program as possible, so the programmer can spot what has changed—and not changed—correctly and more easily. This is where the notion of reflective printing comes in: By taking both the original concrete program and the optimized abstract program as input, we can try to retain the look of the original program as much as possible. Below we will use a simplified arithmetic expression language to explain how reflective printing can be implemented in BiGUL.

8.1 Well-Behavedness

It is probably obvious that the idea of reflective printing comes from transformations; parsing, then, is the direction. Before we proceed to implement parsing and reflective printing in BiGUL, a natural question to ask is: is well-behavedness meaningful in the context of parsing of reflective printing? The answer is yes, especially for PutGet: An abstract syntax tree (AST) may be thought of as a concise and canonical representation of a concrete program, so it would be strange if a concrete program printed from an AST could not be parsed back to the same AST. GetPut, on the other hand, is in fact not strong enough for our purpose, as it only says that, when an AST is unmodified, printing it reflectively to the original program does not change anything, whereas we would have liked to also say that “small” changes to the AST lead to only “small” changes to the concrete program. That is, we would like reflective printing to conform to some sort of least-change principle, a topic which is still unsettled and actively investigated by the BX community. It is at least a good start to have GetPut, though. We thus conclude that BiGUL is indeed a suitable language for implementing reflective printers and corresponding parsers.

8.2 Additive Expressions

Here we use a minimal example which is simple and yet can demonstrate what reflective printing is capable of. Consider the following abstract syntax of arithmetic expressions consisting of integer constants, addition, and subtraction:

This is a nice representation for the compiler, but we cannot expect the programmer to write something like “”, and should provide a concrete syntax so that they can write “$1 - (2+3)$”. Such a concrete syntax is usually defined in terms of a BNF grammar:

The two-level structure of and ensures that plus and minus associate to the left by default; to change association, we should use parentheses. And, to spice up the problem a little, we allow minus to be used also as a negative sign, as specified by the second production rule for . BiGUL deals with structured data only, so we should represent a string generated using this grammar as a concrete syntax tree of the following type:

Again, we need to provide one statement for each of the above datatypes to allow BiGUL to operate on them:

Apart from the constructors, which are inserted to represent incomplete trees that can occur during reflective printing, these two datatypes are in direct correspondence with the grammar, so it is easy to recover the string from a concrete syntax tree:

Conversely, using modern parser technologies like Haskell’s parsec parser combinator library, we can easily implement a “concrete parser” that turns a string into a concrete syntax tree:

The rest of the job is then to write a BiGUL program between and .

8.3 Reflective Printing in BiGUL

The program is basically a case analysis: For example, when the concrete side is a plus and the abstract side is an addition, they match, and we can go into their sub-trees recursively. For the concrete side, the right sub-tree is of type instead of , so in fact we will write two (mutually recursive) programs:

The branch for plus and addition can then be written as:

Following the same line of thought, we can fill in other branches to relate all abstract constructors with concrete production rules:

This covers only “normal” cases though, namely when the source and view are “the same” except for parentheses and literals. What about the cases where the source and view have mismatched shapes? For these cases, we need adaptation. Corresponding to each branch we have already written, we add an adaptive branch which looks at the shape of the view only, throws away a mismatched source, and creates an incomplete one whose shape matches that of the view; the source will be completely created through recursive processing. For example, corresponding to the plus/addition branch, we write:

The full programs are:

8.4 Reflecting Optimizations and Evaluation Sequences

The BiGUL programs, being bidirectional, can be executed in the direction as a reflective printer, or in the direction as a parser. Let us look at parsing first. For example:

Note that a unary minus is regarded as syntactic sugar, and is desugared into a subtraction whose left operand is zero. Also note that parentheses are turned into correct structure of the abstract syntax tree, and nothing more—excessive parentheses are cleanly discarded.

For reflective printing, as we mentioned, one application is reporting what compiler optimizations do. We can optimize the sub-expression $3+0$ by getting rid of the superfluous ${+}0$, for example, and the reflective printer will be able to retain the excessive parentheses:

Notice also that the unary minus is preserved. If the original concrete expression uses a binary minus instead, it will be preserved as well:

In the above example, the pair of parentheses around 3 is also preserved. This is more a coincidence, though—if we change to , for example, the pair of parentheses will not be preserved:

This behavior is indeed what we described with our BiGUL program: the concrete binary minus does not match the abstract , so the whole concrete expression 0-(3+0) inside the outermost pair of parentheses is discarded, and a new concrete expression 0+3 is generated by adaptation. This behavior does not give us “least change”, however: the pair of parentheses around 3 could have been kept. This is one example showing that, while GetPut (no view change implies no source change) is guaranteed by BiGUL, least-change behavior (small view change implies small source change) is another matter completely, and requires extra care and effort to achieve.

Another thing we can do is reflecting the steps in an evaluation sequence of an abstract syntax tree to concrete syntax. For example, starting from:

it takes two steps to evaluate this expression:

This means that if we have an evaluator on the abstract syntax, we will automatically get an evaluator on the concrete syntax!

A reflective printer can also be used as an ordinary printer by setting the original source to an empty one. For example:

Note that the subtraction is reflected as a binary minus instead of a unary one, despite that the left operand is zero. This behavior is easily customizable: By adding an adaptive branch before the one dealing generically with in :

the above abstract syntax tree can be printed as:

8.5 A Domain-Specific Language

As a final remark, the above programs may look long, but at the core of them are merely the correspondences between concrete production rules and abstract constructors. We can design a domain-specific language (DSL) that expresses such correspondences concisely, and then expand programs in this DSL into BiGUL. In fact, we have already done so, and the DSL is called BiYacc. For example, all the programs we have written can be generated from the following eight-line BiYacc program:

See our SLE 2016 paper [18] for more interesting experiments about reflective printing, done on a more realistic imperative language.

9 Conclusion

We have given an introduction to BiGUL programming, explained the underlying design of its putback-based language constructs, and presented a number of applications. BiGUL in its current form is merely one step toward a versatile bidirectional programming language, though. We conclude this chapter by laying out some future directions.

While BiGUL is designed to ensure that programmers can freely describe whatever consistency restoration strategies they have in mind and guarantees that the described strategies are well-behaved, well-behavedness guarantees may be trivial if a described strategy is not actually well-behaved and consequently fails some dynamic checks at runtime. Working with the current BiGUL can thus involve a lot of tedious testing to see if those dynamic checks can go through; also, since we must keep the dynamic checks in place to ensure well-behavedness, at runtime they can incur serious performance overheads. We need ways to precisely characterize the behavior of the dynamic checks, so that it is possible to know that they are redundant and can be safely skipped during execution.

Also we have observed that, as consistency relations or consistency restoration strategies become more complex, BiGUL programs can quickly become awkward to write and hard to read. It is also not that easy to develop reusable libraries because BiGUL programs are not easily composable. (The only general composition operator, namely the classical lens composition, behaves obscurely in the putback direction and is difficult to understand in practice. A discussion of this problem is offered by, e.g., Diskin et al. [4, Sect. 2.2].) We need to design new language constructs that improve composability of BiGUL programs, discover programming patterns and architectures, and eventually build reusable libraries to facilitate program development.

Apart from language-specific issues, there are also challenges faced by the functional programming approach to BXs in general. For one, graphs have always been a kind of data structure that is hard to deal with in functional programming, but the application domains of other BX sub-communities usually require the ability to work with graphs; this is an area where BiGUL and other functional programming–based languages/tools need to catch up. More fundamentally, while programmable from one single direction, asymmetric lenses are a less expressive BX formalism, and we probably should not restrict the future version of BiGUL and new bidirectional languages to the framework of asymmetric lenses. We should recognize that the essence of BiGUL is its full programmability of bidirectional behavior, not the framework of asymmetric lenses which it currently supports, and we should strive to bring this programmability into other existing BX formalisms, or, if that is difficult, come up with new formalisms that are designed with such programmability in mind.