1 Introduction

A bidirectional transformation (BX) is a pair of mutually related mappings between source and target data objects. A well-known example solves the view-update problem [2] from relational database design. A view is a derived database table, computed from concrete source tables by a query. The problem is to map an update of the view back to a corresponding update on the source tables. This is captured by a bidirectional transformation. The bidirectional pattern is found in a broad range of applications, including parsing [17, 30], refactoring [31], code generation [21, 27], and model transformation [32] and XML transformation [25].

When programming a bidirectional transformation, one can separately construct the forwards and backwards functions. However, this approach duplicates effort, is prone to error, and causes subsequent maintenance issues. These problems can be avoided by using specialised programming languages that generate both directions from a single definition [13, 16, 33], a discipline known as bidirectional programming.

The most well-known language family for BX programming is lenses [13]. A lens captures transformations between sources S and views V via a pair of functions \(: S \rightarrow V\) and \(: V \rightarrow S \rightarrow S\). The function extracts a view from a source and takes an updated view and a source as inputs to produce an updated source. The asymmetrical nature of and makes it possible for to recover some of the source data that is not present in the view. In other words, does not have to be injective to have a corresponding  .

Bidirectional transformations typically respect round-tripping laws, capturing the extent to which the transformations preserve information between the two data representations. For example, well-behaved lenses [5, 13] should satisfy:

$$\begin{aligned} \textsf {put} \; (\textsf {get} \; s)\; s = s \quad \quad \quad \quad \textsf {get} \; (\textsf {put} \; v \; s) = v \end{aligned}$$

Lens languages are typically designed to enforce these properties. This focus on unconditional correctness inevitably leads to reduced practicality in programming: lens combinators are often stylised and disconnected from established programming idioms. In this paper, we instead focus on expressing bidirectional programs directly, using monads as an interface for sequential composition.

Monads are a popular pattern [35] (especially in Haskell) which combinator libraries in other domains routinely exploit. Introducing monadic composition to BX programming significantly expands the expressiveness of BX languages and opens up a route for programmers to explore the connection between BX programming and mainstream uni-directional programming. Moreover, it appears that many applications of bidirectional transformations (e.g., parsers and printers [17]) do not share the lens get/put pattern, and as a result have not been sufficiently explored. However, monadic composition is known to be an effective way to construct at least one direction of such transformations (e.g., parsers).

Contributions. In this paper, we deliberately avoid the well-tried approach of specialised lens languages, instead exploring a novel point in the BX design space based on monadic programming, naturally reusing host language constructs. We revisit lenses, and two more bidirectional patterns, demonstrating how they can be subject to monadic programming. By being uncompromising about the monad interface, we expose the essential ideas behind our framework whilst maximising its utility. The trade off with our approach is that we can no longer enforce correctness in the same way as conventional lenses: our interface does not rule out all non-round-tripping BXs. We tackle this issue by proposing a new compositional reasoning framework that is flexible enough to characterise a variety of round-tripping properties, and simplifies the necessary reasoning.

Specifically, we make the following contributions:

  • We describe a method to enable monadic composition for bidirectional programs (Sect. 3). Our approach is based on a construction which generates a monadic profunctor, parameterised by two application-specific monads which are used to generate the forward and backward directions.

  • To demonstrate the flexibility of our approach, we apply the above method to three different problem domains: parsers/printers (Sects. 3 and 4), lenses (Sect. 5), and generators/predicates for structured data (Sect. 6). While the first two are well-explored areas in the bidirectional programming literature, the third one is a completely new application domain.

  • We present a scalable reasoning framework, capturing notions of compositionality for bidirectional properties (Sect. 4). We define classes of round-tripping properties inherent to bidirectionalism, which can be verified by following simple criteria. These principles are demonstrated with our three examples. We include some proofs for illustration in the paper. The supplementary material [12] contains machine-checked Coq proofs for the main theorems.

    An extended version of this manuscript [36] includes additional definitions, proofs, and comparisons in its appendices.

  • We have implemented these ideas as Haskell libraries [12], with two wrappers around attoparsec for parsers and printers, and QuickCheck for generators and predicates, showing the viability of our approach for real programs.

We use Haskell for concrete examples, but the programming patterns can be easily expressed in many functional languages. We use the Haskell notation of assigning type signatures to expressions via an infix double colon “ ”.

1.1 Further Examples of BX

We introduced lenses briefly above. We now introduce the other two examples used in this paper: parsers/printers and generators/predicates.

Parsing and printing. Programming language tools (such as interpreters, compilers, and refactoring tools) typically require two intimately linked components: parsers and printers, respectively mapping from source code to ASTs and back. A simple implementation of these two functions can be given with types:

figure k

Parsers and printers are rarely actual inverses to each other, but instead typically exhibit a variant of round-tripping such as:

figure l

The left equation describes the common situation that parsing discards information about source code, such as whitespace, so that printing the resulting AST does not recover the original source. However, printing retains enough information such that parsing the printed output yields an AST which is equivalent to the AST from parsing the original source. The right equation describes the dual: printing may map different ASTs to the same string. For example, printed code \(1+2+3\) might be produced by left- and right-associated syntax trees.

For particular AST subsets, printing and parsing may actually be left- or right- inverses to each other. Other characterisations are also possible, e.g., with equivalence classes of ASTs (accounting for reassociations). Alternatively, parsers and printers may satisfy properties about the interaction of partially-parsed inputs with the printer and parser, e.g., if :

figure n

Thus, parsing and printing follows a pattern of inverse-like functions which does not fit the lens paradigm. The pattern resembles lenses between a source (source code) and view (ASTs), but with a compositional notion for the source and partial “gets” which consume some of the source, leaving a remainder.

Writing parsers and printers by hand is often tedious due to the redundancy implied by their inverse-like relation. Thus, various approaches have been proposed for reducing the effort of writing parsers/printers by generating both from a common definition [17, 19, 30].

Generating and checking. Property-based testing (e.g., QuickCheck) [10] expresses program properties as executable predicates. For instance, the following property checks that an insertion function , given a sorted list—as checked by the predicate —produces another sorted list. The combinator represents implication for properties.

figure r

To test this property, a testing framework generates random inputs for and . The implementation of applied here first checks whether is sorted, and if it is, checks that is sorted as well. This process is repeated with further random inputs until either a counterexample is found or a predetermined number of test cases pass.

However, this naïve method is inefficient: many properties such as have preconditions which are satisfied by an extremely small fraction of inputs. In this case, the ratio of sorted lists among lists of length n is inversely proportional to n!, so most generated inputs will be discarded for not satisfying the precondition. Such tests give no information about the validity of the predicate being tested and thus are prohibitively inefficient.

When too many inputs are being discarded, the user must instead supply the framework with custom generators of values satisfying the precondition: .

One can expect two complementary properties of such a generator. A generator is sound with respect to the predicate if it generates only values satisfying ; soundness means that no tests are discarded, hence the tested property is better exercised. A generator is complete with respect to if it can generate all satisfying values; completeness ensures the correctness of testing a property with as a precondition, in the sense that if there is a counterexample, it will be eventually generated. In this setting of testing, completeness, which affects the potential adequacy of testing, is arguably more important than soundness, which affects only efficiency.

It is clear that generators and predicates are closely related, forming a pattern similar to that of bidirectional transformations. Given that good generators are usually difficult to construct, the ability to extract both from a common specification with bidirectional programming is a very attractive alternative.

Roadmap. We begin by outlining a concrete example of our monadic approach via parsers and printers (Sect. 2), before explaining the general approach of using monadic profunctors to structure bidirectional programs (Sect. 3). Section 4 then presents a compositional reasoning framework for monadic bidirectional programs, with varying degrees of strength adapted to different round-tripping properties. We then replay the developments of the earlier sections to define lenses as well as generators and predicates in Sects. 5 and 6.

2 Monadic Bidirectional Programming

A bidirectional parser, or biparser, combines both a parsing direction and printing direction. Our first novelty here is to express biparsers monadically.

In code samples, we use the Haskell pun of naming variables after their types, e.g., a variable of some abstract type will also be called . Similarly, for some type constructor , a variable of type will be called . A function (a Kleisli arrow for a monad ) will be called .

Monadic parsers. The following data type provides the standard way to describe parsers of values of type which may consume only part of the input string:

figure an

It is well-known that such parsers are monadic [35], i.e., they have a notion of monadic sequential composition embodied by the interface:

figure ao

The sequential composition operator , called bind, describes the scheme of constructing a parser by sequentially composing two sub-parsers where the second depends on the output of the first; a parser of values is made up of a parser of and a parser of that depends on the previously parsed . Indeed, this is the implementation given to the monadic interface:

figure au

Bind first runs the parser on an input string , resulting in a value which is used to create the parser , which is in turn run on the remaining input to produce parsed values of type . The operation creates a trivial parser for any value which does not consume any input but simply produces .

In practice, parsers composed with often have a relationship between the output types of the two operands: usually that the former “contains” the latter in some sense. For example, we might parse an expression and compose this with a parser for statements, where statements contain expressions. This relationship will be useful later when we consider printers.

As a shorthand, we can discard the remaining unparsed string of a parser using projection, giving a helper function .

Monadic printers. Our goal is to augment parsers with their inverse printer, such that we have a monadic type which provides two complementary (bi-directional) transformations:

figure bh

However, this type of printer (shown also in Sect. 1.1) cannot form a monad because it is contravariant in its type parameter . Concretely, we cannot implement the bind ( ) operator for values with types of this form:

figure bl

We are stuck trying to fill the hole ( ) as there is no way to get a value of type to pass as an argument to (first printer) and (second printer which depends on a ). Subsequently, we cannot construct a monadic biparser by simply taking a product of the parser monad and and leveraging the result that the product of two monads is a monad.

But what if the type variables of were related by containment, such that is contained within and thus we have a projection ? We could use this projection to fill the hole in the failed attempt above, defining a bind-like operator:

figure bw

This is closer to the monadic form, where resolves the difficulty of contravariance by “contextualizing” the printers. Thus, the first printer is no longer just “a printer of ”, but “a printer of extracted ”. In the context of constructing a bidirectional parser, having such a function to hand is not an unrealistic expectation: recall that when we compose two parsers, typically the values of the first parser for are contained within the values returned by the second parser for , thus a notion of projection can be defined and used here to recover a in order to build the corresponding printer compositionally.

Of course, this is still not a monad. However, it suggests a way to generate a monadic form by putting the printer and the contextualizing projection together, and fusing them into . This has the advantage of removing the contravariant occurence of , yielding a data type:

figure ci

If we fix the first parameter type , then the type of printers for values is indeed monadic, combining a reader monad (for some global read-only parameter of type ) and a writer monad (for strings), with implementation:

figure cn

The printer ignores its input and prints nothing. For bind, an input is shared by both printers and the resulting strings are concatenated.

We can adapt the contextualisation of a printer by the following operation which amounts to pre-composition, witnessing the fact that is a contravariant functor in its first parameter:

figure cr

2.1 Monadic Biparsers

So far so good: we now have a monadic notion of printers. However, our goal is to combine parsers and printers in a single type. Since we have two monads, we use the standard result that a product of monads is a monad, defining biparsers:

figure cs

By pairing parsers and printers we have to unify their covariant parameters. When both the type parameters of are the same it is easy to interpret this type: a biparser is a parser from strings to values and printer from values to strings. We refer to biparsers of this type as aligned biparsers. What about when the type parameters differ? A biparser of type provides a parser from strings to values and a printer from values to strings, but where the printers can compute values from values, i.e., is some common broader representation which contains relevant -typed subcomponents. A biparser can be thought of as printing a certain subtree from the broader representation of a syntax tree .

The corresponding monad for is the product of the previous two monad definitions for and , allowing both to be composed sequentially at the same time. To avoid duplication we elide the definition here which is shown in full in Appendix A of the extended version [36]

We can also lift the previous notion of from printers to biparsers, which gives us a way to contextualize a printer:

figure dl

In the rest of this section, we use the alias “ ” for with flipped parameters where we read as applying the printer of on a subpart of an input of type calculated by , thus yielding a biparser of type .

An example biparser. Let us write a biparser, , for strings which are prefixed by their length and a space. For example, the following unit tests should be true:

figure du

We start by defining a primitive biparser of single characters as:

figure dv

A character is parsed by deconstructing the source string into its head and tail. For brevity, we do not handle the failure associated with an empty string. A character is printed as its single-letter string (a singleton list) paired with .

Next, we define a biparser for an integer followed by a single space. An auxiliary biparser (on the right) parses an integer one digit at a time into a string. Note that in Haskell, the -notation statement desugars to “ ...” which uses and a function binding in the scope of the rest of the desugared block.

figure ef

On the right, extracts a consisting of digits followed by a single space. As a parser, it parses a character ( ); if it is a digit then it continues parsing recursively ( ) appending the first character to the result ( ). Otherwise, if the parsed character is a space the parser returns . As a printer, expects a non-empty string of the same format; extracts the first character of the input, then prints it and returns it back as ; if it is a digit, then extracts the rest of the input to print recursively. If the character is a space, the printer returns a space and terminates; otherwise (not digit or space) the printer throws an error.

On the left, the biparser uses to convert an input string of digits (parsed by ) into an integer, and to convert an integer to an output string printed by . A safer implementation could return the type when parsing but we keep things simple here for now.

After parsing an integer , we can parse the string following it by iterating times the biparser . This is captured by the combinator below, defined recursively like but with the termination condition given by an external parameter. To iterate times a biparser : if , there is nothing to do and we return the empty list; otherwise for , we run once to get the head , and recursively iterate times to get the tail .

Note that although not reflected in its type, expects, as a printer, a list of length : if , there is nothing to print; if , extracts the head of to print it with , and extracts its tail, of length , to print it recursively.

figure fu

(akin to from Haskell’s standard library). We can now fulfil our task:

figure fw

Interestingly, if we erase applications of , i.e., we substitute every expression of the form with and ignore the second parameter of the types, we obtain what is essentially the definition of a parser in an idiomatic style for monadic parsing. This is because is the identity on the parser component of . Thus the biparser code closely resembles standard, idiomatic monadic parser code but with “annotations” via expressing how to apply the backwards direction of printing to subparts of the parsed string.

Despite its simplicity, the syntax of length-prefixed strings is notably context-sensitive. Thus the example makes crucial use of the monadic interface for bidirectional programming: a value (the length) must first be extracted to dynamically delimit the string that is parsed next. Context-sensitivity is standard for parser combinators in contrast with parser generators, e.g., Yacc, and applicative parsers, which are mostly restricted to context-free languages. By our monadic BX approach, we can now bring this power to bear on bidirectional parsing.

3 A Unifying Structure: Monadic Profunctors

The biparser examples of the previous section were enabled by both the monadic structure of and the operation (also called , with flipped arguments). We describe a type as being a monadic profunctor when it has both a monadic structure and a operation (subject to some equations). The notion of a monadic profunctor is general, but it characterises a key class of structures for bidirectional programs, which we explain here. Furthermore, we show a construction of monadic profunctors from pairs of monads which elicits the necessary structure for monadic bidirectional programming in the style of the previous section.

Profunctors. In Sect. 2.1, biparsers were defined by a data type with two type parameters ( ) which is functorial and monadic in the second parameter and contravariantly functorial in the first parameter (provided by the operation). In standard terminology, a two-parameter type which is functorial in both its type parameters is called a bifunctor. In Haskell, the term profunctor has come to mean any bifunctor which is contravariant in the first type parameter and covariant in the second.Footnote 1 This differs slightly from the standard category theory terminology where a profunctor is a bifunctor \(\mathsf {F} : \mathcal {D}^{\mathsf {op}} \times \mathcal {C} \rightarrow \) Set. This corresponds to the Haskell community’s use of the term “profunctor” if we treat Haskell in an idealised way as the category of sets.

We adopt this programming-oriented terminology, capturing the operation via a class . In the preceding section, some uses of involved a partial function, e.g., . We make the possibility of partiality explicit via the type, yielding the following definition.

Definition 1

A binary data type is a profunctor if it is a contravariant functor in its first parameter and covariant functor in its second, with the operation:

figure gp

which should obey two laws:

figure gq

where composes partial functions (left-to-right), captured by Kleisli arrows of the Maybe monad.

The constraint captures a universally quantified constraint [6]: for all types then has an instance of the class.Footnote 2

The requirement for to take partial functions is in response to the frequent need to restrict the domain of bidirectional transformations. In combinator-based approaches, combinators typically constrain bidirectional programs to be bijections, enforcing domain restrictions by construction. Our more flexible approach requires a way to include such restrictions explicitly, hence .

Since the contravariant part of the bifunctor applies to functions of type , the categorical analogy here is more precisely a profunctor \(\mathsf {F} : {\mathcal {C}_T}^{\mathsf {op}} \times \mathcal {C} \rightarrow \mathbf Set \) where \(\mathcal {C}_T\) is the Kleisli category of the partiality ( ) monad.

Definition 2

A monadic profunctor is a profunctor (in the sense of Definition 1) such that     is a monad for all . In terms of type class constraints, this means there is an instance and for all there is a instance. Thus, we represent monadic profunctors by the following empty class (which inherits all its methods from its superclasses):

figure hi

Monadic profunctors must obey the following laws about the interaction between profunctor and monad operations:

figure hj

(for all , , ). These laws are equivalent to saying that lifts (partial) functions into monad morphisms. In Haskell, these laws are obtained for free by parametricity [34]. This means that every contravariant functor and monad is in fact a monadic profunctor, thus the following universal instance is lawful:

figure ho

Corollary 1

Biparsers form a monadic profunctor as there is an instance of and satisfying the requisite laws.

Lastly, we introduce a useful piece of terminology (mentioned in the previous section on biparsers) for describing values of a profunctor of a particular form:

Definition 3

A value of a profunctor is called aligned if = .

3.1 Constructing Monadic Profunctors

Our examples (parsers/printers, lenses, and generators/predicates) share monadic profunctors as an abstraction, making it possible to write different kinds of bidirectional transformations monadically. Underlying these definitions of monadic profunctors is a common structure, which we explain here using biparsers, and which will be replayed in Sect. 5 for lenses and Sect. 6 for bigenerators.

There are two simple ways in which a covariant functor (resp. a monad) gives rise to a profunctor (resp. a monadic profunctor). The first is by constructing a profunctor in which the contravariant parameter is discarded, i.e., ; the second is as a function type from the contravariant parameter to , i.e., . These are standard mathematical constructions, and the latter appears in the Haskell profunctors package with the name . Our core construction is based on these two ways of creating a profunctor, which we call and respectively:

figure id

The naming reflects the idea that these two constructions will together capture a bidirectional transformation and are related by domain-specific round-tripping properties in our framework. Both and map any functor into a profunctor by the following type class instances:

figure ig

There is an additional constraint here for , enforcing that the monad is a member of the class which we define as:

figure ik

This provides an interface for monads which can internalise a notion of failure, as captured at the top-level by in .

Furthermore, and both map any monad into a monadic profunctor:

figure ip

The product of two monadic profunctors is also a monadic profunctor. This follows from the fact that the product of two monads is a monad and the product of two contravariant functors is a contravariant functor.

figure iq
figure ir

3.2 Deriving Biparsers as Monadic Profunctor Pairs

We can redefine biparsers in terms of the above data types, their instances, and two standard monads, the state and writer monads:

figure is

The backward direction composes the writer monad with the monad using (the writer monad transformer, equivalent to composing two monads with a distributive law). Thus the backwards component of corresponds to printers (which may fail) and the forwards component to parsers:

figure iw

For the above code to work in Haskell, the and types need to be defined via either a type or in order to allow type class instances on partially applied type constructors. We abuse the notation here for simplicity but define smart constructors and deconstructors for the actual implementation:Footnote 3

figure jb

The monadic profunctor definition for biparsers now comes for free from the constructions in Sect. 3.1 along with the following instance of for the writer monad transformer with the monad:

figure je

In a similar manner, we will use this monadic profunctor construction to define monadic bidirectional transformations for lenses (Sect. 5) and bigenerators (Sect. 6).

The example biparsers from Sect. 2.1 can be easily redefined using the structure here. For example, the primitive biparser becomes:

figure jg

Codec library. The codec library [8] provides a general type for bidirectional programming isomorphic to our composite type :

figure ji

Though the original codec library was developed independently, its current form is a result of this work. In particular, we contributed to the package by generalising its original type ( ) to the one above, and provided and instances to support monadic bidirectional programming with codecs.

4 Reasoning about Bidirectionality

So far we have seen how the monadic profunctor structure provides a way to define biparsers using familiar operations and syntax: monads and -notation. This structuring allows both the forwards and backwards components of a biparser to be defined simultaneously in a single compact definition.

This section studies the interaction of monadic profunctors with the round-tripping laws that relate the two components of a bidirectional program. For every bidirectional transformation we can define dual properties: backward round tripping (going backwards-then-forwards) and forward round tripping (going forwards-then-backwards). In each BX domain, such properties also capture additional domain-specific information flow inherent to the transformations. We use biparsers as the running example. We then apply the same principles to our other examples in Sects. 5 and 6. For brevity, we use as an alias for .

Definition 4

A biparser is backward round tripping if for all and then (recalling that ):

figure jt

That is, if a biparser when used as a printer (going backwards) on an input value produces a string , then using as a parser on a string with prefix and suffix yields the original input value and the remaining input .

Note that backward round tripping is defined for aligned biparsers (of type ) since the same value is used as both the input of the printer (typed by the first type parameter of ) and as the expected output of the parser (typed by the second type parameter of ).

The dual property is forward round tripping: a source string is parsed (going forwards) into some value which when printed produces the initial source :

Definition 5

A biparser is forward round tripping if for every and we have that:

figure km

Proposition 1

The biparser (Sect. 3.2) is both backward and forward round tripping. Proof by expanding definitions and algebraic reasoning.

Note, in some applications, forward round tripping is too strong. Here it requires that every printed value corresponds to at most one source string. This is often not the case as ASTs typically discard formatting and comments so that pretty-printed code is lexically different to the original source. However, different notions of equality enable more reasonable forward round-tripping properties.

Although one can check round-tripping properties of biparsers by expanding their definitions and the underlying monadic profunctor operations, a more scalable approach is provided if a round-tripping property is compositional with respect to the monadic profunctor operations, i.e., if these operations preserve the property. Compositional properties are easier to enforce and check since only the individual atomic components need round-tripping proofs. Such properties are then guaranteed “by construction” for programs built from those components.

4.1 Compositional Properties of Monadic Bidirectional Programming

Let us first formalize compositionality as follows. A property \(\mathcal {R}\) over a monadic profunctor is a family of subsets of indexed by types and .

Definition 6

A property \(\mathcal {R}\) over a monadic profunctor is compositional if the monadic profunctor operations are closed over \(\mathcal {R}\), i.e., the following conditions hold for all types , , :

figure kx

Unfortunately for biparsers, forward and backward round tripping as defined above are not compositional: is not backward round tripping and does not preserve forward round tripping. Furthermore, these two properties are restricted to biparsers of type (i.e., aligned biparsers) but compositionality requires that the two type parameters of the monadic profunctor can differ in the case of and . This suggests that we need to look for more general properties that capture the full gamut of possible biparsers.

We first focus on backward round tripping. Informally, backward round tripping states that if you print (going backwards) and parse the resulting output (going forwards) then you get back the initial value. However, in a general biparser , the input type of the printer differs from the output type of the parser , so we cannot compare them. But our intent for printers is that what we actually print is a fragment of , a fragment which is given as the output of the printer. By thus comparing the outputs of both the parser and printer, we obtain the following variant of backward round tripping:

Definition 7

A biparser is weak backward round tripping if for all , , and , then:

figure lm

Removing backward round tripping’s restriction to aligned biparsers and using the result of the printer gives us a property that is compositional:

Proposition 2

Weak backward round tripping of biparsers is compositional.

Proposition 3

The primitive biparser is weak backward round tripping.

Corollary 2

Propositions 2 & 3 imply is weak backward round tripping.

This property is “weak” as it does not constrain the relationship between the input of the printer and its output . In fact, there is no hope for a compositional property to do so: the monadic profunctor combinators do not enforce a relationship between them. However, we can regain compositionality for the stronger backward round-tripping property by combining the weak compositional property with an additional non-compositional property on the relationship between the printer’s input and output. This relationship is represented by the function that results from ignoring the printed string, which amounts to removing the main effect of the printer. Thus we call this operation a purification:

figure ls

Ultimately, when a biparser is aligned ( ) we want an input to the printer to be returned in its output, i.e, should equal . If this is the case, we recover the original backward round tripping property:

Theorem 1

If is weak backward round tripping, and for all . , then is backward round tripping.

Thus, for any biparser , we can get backward round tripping by proving that its atomic subcomponents are weak backward round tripping, and proving that . The interesting aspect of the purification condition here is that it renders irrelevant the domain-specific effects of the biparser, i.e., those related to manipulating source strings. This considerably simplifies any proof. Furthermore, the definition of is a monadic profunctor homomorphism which provides a set of equations that can be used to expedite the reasoning.

Definition 8

A monadic profunctor homomorphism between monadic profunctors and is a polymorphic function such that:

figure mg

Proposition 4

The operation for biparsers (above) is a monadic profunctor homomorphism between and the monadic profunctor .

Corollary 3

(of Theorem 1 with Corollary 2 and Proposition 4) The biparser is backward round tripping.

Proof

First prove (in Appendix B [36]) the following properties of biparsers , , and (writing for ):

(4.1)
(4.2)
(4.3)

From these and the homomorphism properties we can prove :

figure mr

Combining with Corollary 2 ( is weak backward round tripping) enables Theorem 1, proving that is backward round tripping.

The other two core examples in this paper also permit a definition of . We capture the general pattern as follows:

Definition 9

A purifiable monadic profunctor is a monadic profunctor with a homomorphism from to the monadic profunctor of partial functions . We say that is the pure projection of .

Definition 10

A pure projection is called the identity projection when for all .

Here and in Sects. 5 and 6, identity projections enable compositional round-tripping properties to be derived from more general non-compositional properties, as seen above for backward round tripping of biparsers.

We have neglected forward round tripping, which is not compositional, not even in a weakened form. However, we can generalise compositionality with conditions related to injectivity, enabling a generalisation of forward round tripping. We call the generalised meta-property quasicompositionality.

4.2 Quasicompositionality for Monadic Profunctors

An injective function \(f : A \rightarrow B\) is a function for which there exists a left inverse \(f^{-1} : B \rightarrow A\), i.e., where \(f^{-1} \circ f = id\). We can see this pair of functions as a simple kind of bidirectional program, with a forward round-tripping property (assuming f is the forwards direction). We can lift the notion of injectivity to the monadic profunctor setting and capture forward round-tripping properties that are preserved by the monadic profunctor operations, given some additional injectivity-like restriction. We first formalise the notion of an injective arrow.

Informally, an injective arrow produces an output from which the input can be recalculated:

Definition 11

Let be a monad. A function is an injective arrow if there exists (the left arrow inverse of ) such that for all :

figure nl

Next, we define quasicompositionality which extends the compositionality meta-property with the requirement for to be applied to injective arrows:

Definition 12

Let be a monadic profunctor. A property indexed by types and is quasicompositional if the following holds

figure nr

We now formulate a weakening of forward round tripping. As with weak backward round tripping, we rely on the idea that the printer outputs both a string and the value that was printed, so that we need to compare the outputs of both the parser and the printer, as opposed to comparing the output of the parser with the input of the printer as in (strong) forward round tripping. If running the parser component of a biparser on a string yields a value and a remaining string , and the printer outputs that same value along with a string , then is the prefix of that was consumed by the parser, i.e., .

Definition 13

A biparser is weak forward round tripping if for all , , and then:

figure oe

Proposition 5

Weak forward round tripping is quasicompositional.

Proof

We sketch the qcomp-bind case, where for some and that are weak forward roundtripping. From , it follows that there exists , such that and . Similarly implies there exists , such that and and . Because is an injective arrow, we have (see appendix). We then use the assumption that and are weak forward roundtripping on and on , and deduce that and therefore .

Proposition 6

The biparser is weak forward round tripping.

Corollary 4

Propositions 5 and 6 imply that is weak forward round tripping if we restrict the parser to inputs whose digits do not contain redundant leading zeros.

Proof

All of the right operands of in the definition of are injective arrows, apart from at the end of the auxiliary biparser. Indeed, the function is not injective since multiple strings may parse to the same integer: . But the pre-condition to the proposition (no redundant leading zero digits) restricts the input strings so that is injective. The rest of the proof is a corollary of Propositions 5 and 6.

Thus, quasicompositionality gives us scalable reasoning for weak forward round tripping, which is by construction for biparsers: we just need to prove this property for individual atomic biparsers. Similarly to backward round tripping, we can prove forward round tripping by combining weak forward round tripping with the identity projection property:

Theorem 2

If is weak forward round-tripping, and for all , , then is forward round tripping.

Corollary 5

The biparser is forward round tripping by the above theorem (with identity projection shown in the proof of Corollary 3) and Corollary 4.

In summary, for any BX we can consider two round-tripping properties: forwards-then-backwards and backwards-then-forwards, called just forward and backward here respectively. Whilst combinator-based approaches can guarantee round-tripping by construction, we have made a trade-off to get greater expressivity in the monadic approach. However, we regain the ability to reason about bidirectional transformations in a manageable, scalable way if round-tripping properties are compositional. Unfortunately, due to the monadic profunctor structuring, this tends not to be the case. Instead, weakened round-tripping properties can be compositional or quasicompositional (adding injectivity). In such cases, we recover the stronger property by proving a simple property on aligned transformations: that the backwards direction faithfully reproduces its input as its output (identity projection). Appendix C in our extended manuscript [36] compares this reasoning approach to a proof of backwards round tripping for separately implemented parsers and printers (not using our combined monadic approach).

5 Monadic Bidirectional Programming for Lenses

Lenses are a common object of study in bidirectional programming, comprising a pair of functions satisfying well-behaved lens laws shown in Sect. 1. Previously, when considering the monadic structure of parsers and printers, the starting point was that parsers already have a well-known monadic structure. The challenge came in finding a reasonable monadic characterisation for printers that was compatible with the parser monad. In the end, this construction was expressed by a product of two monadic profunctors and for monads and . For lenses we are in the same position: the forwards direction ( ) is already a monad—the reader monad. The backwards direction is not a monad since it is contravariant in its parameter; the same situation as printers. We can apply the same approach of “monadisation” used for parsers and printers, giving the following new data type for lenses:

figure qd

The result of is paired with a covariant parameter (the result type of ) in the same way as monadic printers. Instead of mapping a view and a source to a source, now maps values of a different type , which we call a pre-view, along with a source into a pair of a view and source . This definition can be structured as a monadic profunctor via a pair of and constructions:

figure qo

Thus by the results of Sect. 3, we now have a monadic profunctor characterisation of lenses that allows us to compose lenses via the monadic interface.

Ideally, and should be total, but this is impossible without a way to restrict the domains. In particular, there is the known problem of “duplication” [23], where source data may appear more than once in the view, and a necessary condition for put to be well-behaved is that the duplicates remain equal amid view updates. This problem is inherent to all bidirectional transformations, and bidirectional languages have to rule out inconsistent updates of duplicates either statically [13] or dynamically [23]. To remedy this, we capture both partiality of and a predicate on sources in for additional dynamic checking. This is provided by the following and monadic profunctors:

figure qv

Going forwards, getting a view from a source may fail if there is no view for the current source. Going backwards, putting a pre-view updates some source (via the state transformer ), but with some further structure returned, provided by (similar to the writer transformer used for biparsers, Sect. 3.2). The here captures the possibility that can fail. The structure provides a predicate which detects the “duplication” issue mentioned earlier. Informally, the predicate can be used to check that previously modified locations in the source are not modified again. For example, if a lens has a source made up of a bit vector, and a sets bit i to 1, then the returned predicate will return for all bit vectors where bit i is 1, and otherwise. This predicate can then be used to test whether further operations on the source have modified bit i.

Similarly to biparsers, a pre-view can be understood as containing the view that is to be merged with the source, and which is returned with the updated source. Ultimately, we wish to form lenses of matching input and output types (i.e. ) satisfying the standard lens well-behavedness laws, modulo explicit management of partiality via and testing for conflicts via the predicate:

figure rn

L-PutGet and L-GetPut are backward and forward round tripping respectively. Some lenses, such as the later example, are not defined for all views. In that case we may say that the lens is backward/forward round tripping in some subset when the above properties only hold when is an element of .

For every source type , the lens type is automatically a monadic profunctor by its definition as the pairing of and (Sect. 3.1), and the following instance of for handling failure and instance of to satisfy the requirements of the writer monad:

figure rx

A simple lens example operates on key-value maps. For keys of type and values of type , we have the following source type and a simple lens:

figure sa

The component of the lens does a lookup of the key in a map, producing of a . The component inserts a value for key . When the key already exists, overwrites its associated value.

Due to our approach, multiple calls to can be composed monadically, giving a lens that gets/sets multiple key-value pairs at once. The list of keys and the list of values are passed separately, and are expected to be the same length.

figure sk

We refer interested readers to our implementation [12] for more examples, including further examples involving trees.

Round tripping. We apply the reasoning framework of Sect. 4, taking the standard lens laws as the starting point (neither of which are compositional).

We first weaken backward round tripping to be compositional. Informally, the property expresses the idea, that if we some value in a source , resulting in a source , then what we from is . However two important changes are needed to adapt to our generalised type of lenses and to ensure compositionality. First, the value that was put is now to be found in the output of , whereas there is no way to constrain the input of because its type is abstract. Second, by sequentially composing lenses such as in , the output source of will be further modified by , so this round-tripping property must constrain all potential modifications of . In fact, the predicate ensures exactly that the view has not changed and is still . It is not even necessary to refer to , which is just one source for which we expect to be .

Definition 14

A lens is weak backward round tripping if for all , , for all sources , , and for all , we have:

figure tn

Theorem 3

Weak backward round tripping is a compositional property.

Again, we complement this weakened version of round tripping with the notion of purification.

Proposition 7

Our lens type is a purifiable monadic profunctor (Definition 9), with a family of pure projections indexed by a source , defined:

figure tr

Theorem 4

If a lens is weak backward round tripping and has identity projections on some subset (i.e., for all , then ) then is also backward round tripping on all .

To demonstrate, we apply this result to .

Proposition 8

The lens is weak backward round tripping.

Proposition 9

The lens has identity projection: .

Our lens is therefore weak backward round tripping by construction. We now interpret/purify as a partial function, which is actually the identity function when restricted to lists of the same length as .

Proposition 10

For all such that , and for all then .

Corollary 6

By the above results, for all is backward round tripping on lists of length .

The other direction, forward round tripping, follows a similar story. We first restate it as a quasicompositional property.

Definition 15

A lens is weak forward round tripping if for all , , for all sources , , and for all , we have:

figure uw

Theorem 5

Weak forward round tripping is a quasicompositional property.

Along with identity projection, this gives the original forward L-GetPut property.

Theorem 6

If a lens is weak forward round tripping and has identity projections on some subset (i.e., for all , then ) then is also forward round tripping on .

We can thus apply this result to our example (details omitted).

Proposition 11

For all , the lens is forward round tripping on lists of length .

6 Monadic Bidirectional Programming for Generators

Lastly, we capture the novel notion of bidirectional generators (bigenerators) extending random generators in property-based testing frameworks like QuickCheck [10] to a bidirectional setting. The forwards direction generates values conforming to a specification; the backwards direction checks whether values conform to a predicate. We capture the two together via our monadic profunctor pair as:

figure vh

The forwards direction of a bigenerator is a generator, while the backwards direction is a partial function . A value represents a subset of , where is a generator of values in that subset and maps pre-views u to members of the generated subset. In the backwards direction, defines a predicate on , which is true if and only if is of some value. The function extracts this predicate from the backward direction:

figure vs

The bigenerator type is automatically a monadic profunctor due to our construction (Sect. 3). Thus, monad and profunctor instances come for free, modulo (un)wrapping of constructors and given a trivial instance of :

figure vv

Due to space limitations, we refer readers to Appendix E [36] for an example of a compositionally-defined bigenerator that produces binary search trees.

Round tripping. A random generator can be interpreted as the set of values it may generate, while a predicate represents the set of values satisfying it. For a bigenerator , we write when is a possible output of the generator. The generator of a bigenerator should match its predicate . This requirement equates to round-tripping properties: a bigenerator is sound if every value which it can generate satisfies the predicate (forward round tripping); a bigenerator is complete if every value which satisfies the predicate can be generated (backward round tripping). Completeness is often more important than soundness in testing because unsound tests can be filtered out by the predicate, but completeness determines the potential adequacy of testing.

Definition 16

A bigenerator is complete (backward round tripping) when implies .

Definition 17

A bigenerator is sound (forward round tripping) if for all , implies that .

Similarly to backward round tripping of biparsers and lenses, completeness can be split into a compositional weak completeness and a purifiable property.

As before, the compositional weakening of completeness relates the forward and backward components by their outputs, which have the same type.

Definition 18

A bigenerator is weak-complete when

figure wj

Theorem 7

Weak completeness is compositional.

In a separate step, we connect the input of the backward direction, i.e., the checker, by reasoning directly about its pure projection (via a more general form of identity projection) which is defined to be the checker itself:

Theorem 8

A bigenerator is complete if it is weak-complete and its checker satisfies a pure projection property:

Thus to prove completeness of a bigenerator , we first have weak-completeness by construction, and we can then show that is a restriction of the identity function, interpreting all bigenerators simply as partial functions.

Considering the other direction, soundness, there is unfortunately no decomposition into a quasicompositional property and a property on pure projections. To see why, let be a random uniform bigenerator of booleans, then consider for example, and , where and . Both satisfy any quasicompositional property satisfied by , and both have the same pure projection , and yet the former is unsound—it can generate , which is rejected by —while the latter is sound. This is not a problem in practice, as unsoundness, especially in small scale, is inconsequential in testing. But it does raise an intellectual challenge and an interesting point in the design space, where ease of reasoning has been traded for greater expressivity in the monadic approach.

7 Discussion and Related Work

Bidirectional transformations are a widely applicable technique used in many domains [11]. Among language-based solutions, the lens framework is most influential [3, 4, 13, 14, 24, 29]. Broadly speaking, combinators are used as programming constructs with which complex lenses are created by combining simpler ones. The combinators preserve round tripping, and therefore the resulting programs are correct by construction. A problem with lens languages is that they tend to be disconnected from more general programming. Lenses can only be constructed by very specialised combinators and are not subject to existing abstraction mechanisms. Our approach allows bidirectional transformations to be built using standard components of functional programming, and gives a reasoning framework for studying compositionality of round-tripping properties.

The framework of applicative lenses [18] uses a function representation of lenses to lift the point-free restriction of the combinator-based languages, and enables bidirectional programming with explicit recursion and pattern matching. Note that the use of “applicative” in applicative lenses refers to the transitional sense of programming with \(\lambda \)-abstractions and functional applications, which is not directly related to applicative functors. In a subsequent work, the authors developed a language known as HOBiT [20], which went further in featuring proper binding of variables. Despite the success in supporting \(\lambda \)-abstractions and function applications in programming bidirectional transformations, none of the languages have explored advanced patterns such as monadic programming.

The work on monadic lenses [1] investigates lenses with effects. For instance, a “put” could require additional input to resolve conflicts. Representing effects with monads helps reformulate the laws of round-tripping. In contrast, we made the type of lenses itself a monad, and showed how they can be composed monadically. Our method is applicable to monadic lenses, yielding what one might call monadic monadic lenses: monadically composable lenses with monadic effects. We conjecture that laws for monadic lenses can be adapted to this setting with similar compositionality properties, reusing our reasoning framework.

Other work leverages profunctors for bidirectionality. Notably, a Profunctor optic [26] between a source type and a view type is a function of type , for an abstract profunctor . Profunctor optics and our monadic profunctors offer orthogonal composition patterns: profunctor optics can be composed “vertically” using function composition, whereas monadic profunctor composition is “horizontal” providing sequential composition. In both cases, composition in the other direction can only be obtained by breaking the abstraction.

It is folklore in the Haskell community that profunctors can be combined with applicative functors [22]. The pattern is sometimes called a monoidal profunctor. The codec library [8] mentioned in Sect. 3 prominently features two applications of this applicative programming style: binary serialisation (a form of parsing/printing) and conversion to and from JSON structures (analogous to lenses above). Opaleye [28], an EDSL of SQL queries for Postgres databases, uses an interface of monoidal profunctors to implement generic operations such as transformations between Haskell datatypes and database queries and responses.

Our framework adapts gracefully to applicative programming, a restricted form of monadic programming. By separating the input type from the output type, we can reuse the existing interface of applicative functors without modification. Besides our generalisation to monads, purification and verifying round-tripping properties via (quasi)compositionality are novel in our framework.

Rendel and Ostermann proposed an interface for programming parsers and printers together [30], but they were unable to reuse the existing structure of , and classes (because of the need to handle types that are both covariant and contravariant), and had to reproduce the entire hierarchy separately. In contrast, our approach reuses the standard type class hierarchy, further extending the expressive power of bidirectional programming in Haskell. FliPpr [17, 19] is an invertible language that generates a parser from a definition of a pretty printer. In this paper, our biparser definitions are more similar to those of parsers than printers. This makes sense as it has been established that many parsers are monadic. Similar to the case of HOBiT, there is no discussion of monadic programming in the FliPpr work.

Previous approaches to unifying random generators and predicates mostly focused on deriving generators from predicates. One general technique evaluates predicates lazily to drive generation (random or enumerative) [7, 9], but one loses control over the resulting distribution of generated values. Luck [15] is a domain-specific language blending narrowing and constraint solving to specify generators as predicates with user-provided annotations to control the probability distribution. In contrast, our programs can be viewed as generators annotated with left inverses with which to derive predicates. This reversed perspective comes with trade-offs: high-level properties would be more naturally expressed in a declarative language of predicates, whereas it is a priori more convenient to implement complex generation strategies in a specialised framework for random generators.

Conclusions. This paper advances the expressive power of bidirectional programming; we showed that the classic bidirectional patterns of parsers/printers and lenses can be restructured in terms of monadic profunctors to provide sequential composition, with associated reasoning techniques. This opens up a new area in the design of embedded domain-specific languages for BX programming, that does not restrict programmers to stylised interfaces. Our example of bigenerators broadened the scope of BX programming from transformations (converting between two data representations) to non-transformational applications.

To demonstrate the applicability of our approach to real code, we have developed two bidirectional libraries [12], one extending the attoparsec monadic parser combinator library to biparsers and one extending QuickCheck to bigenerators. One area for further work is studying biparsers with lookahead. Currently lookahead can be expressed in our extended attoparsec, but understanding its interaction with (quasi)compositional round-tripping is further work.

However, this is not the final word on sequentially composable BX programs. In all three applications, round-tripping properties are similarly split into weak round tripping, which is weaker than the original property but compositional, and purifiable, which is equationally friendly. An open question is whether an underlying structure can be formalised, perhaps based on an adjunction model, that captures bidirectionality even more concretely than monadic profunctors.