Software frequently converts data from one representation to another and vice versa. Naïvely specifying both conversion directions separately is error prone and introduces conceptual duplication. Instead, bidirectional programming techniques allow programs to be written which can be interpreted in both directions. However, these techniques often employ unfamiliar programming idioms via restricted, specialised combinator libraries. Instead, we introduce a framework for composing bidirectional programs monadically, enabling bidirectional programming with familiar abstractions in functional languages such as Haskell. We demonstrate the generality of our approach applied to parsers/printers, lenses, and generators/predicates. We show how to leverage compositionality and equational reasoning for the verification of round-tripping properties for such monadic bidirectional programs.
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.
Anzeige
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.
Anzeige
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:
×
Parsers and printers are rarely actual inverses to each other, but instead typically exhibit a variant of round-tripping such as:
×
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
:
×
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.
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:
×
It is well-known that such parsers are monadic [35], i.e., they have a notion of monadic sequential composition embodied by the interface:
×
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:
×
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:
×
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:
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:
×
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:
×
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:
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:
×
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:
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:
×
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:
We start by defining a primitive biparser of single characters as:
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.
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.
(akin to
from Haskell’s standard library). We can now fulfil our task:
×
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.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:
×
which should obey two laws:
×
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.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):
×
Monadic profunctors must obey the following laws about the interaction between profunctor and monad operations:
×
(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:
×
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:
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:
×
There is an additional constraint here for
, enforcing that the monad
is a member of the
class which we define as:
×
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:
×
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.
×
×
×
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:
×
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:
×
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:3
×
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:
×
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:
×
Codec library. The codec library [8] provides a general type for bidirectional programming isomorphic to our composite type
:
×
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
):
×
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:
×
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
,
,
:
×
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:
×
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:
×
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:
×
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
:
×
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
:
×
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
×
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:
×
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:
×
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:
×
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:
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:
×
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:
×
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:
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.
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:
×
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:
×
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:
×
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:
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:
×
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
:
×
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
×
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.
Acknowledgments
We thank the anonymous reviewers for their helpful comments. The second author was supported partly by EPSRC grant EP/M026124/1.
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
As of GHC 8.6, the
extension allows universal quantification in constraints, written as forall u. Functor (p u), but for simplicity we use the constraint constructor
from the constraints package: http://hackage.haskell.org/package/constraints.
\(: 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
.
”.
:
, given a sorted list—as checked by the predicate
—produces another sorted list. The combinator
represents implication for properties.
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.
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.
.
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.
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
.
which may consume only part of the input string:
, 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: 
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
.
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.
.
which provides two complementary (bi-directional) transformations:
(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:
) 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.
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:
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.
and fusing them into
. This has the advantage of removing the contravariant occurence of
, yielding a data 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:
ignores its input and prints nothing. For bind, an input
is shared by both printers and the resulting strings are concatenated.
is a contravariant functor in its first parameter:
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
.
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]
from printers to biparsers, which gives us a way to contextualize a printer:
” 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
.
, for strings which are prefixed by their length and a space. For example, the following unit tests should be true:
is printed as its single-letter string (a singleton list) paired with
.
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.
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.
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.
, 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
.
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.
from Haskell’s standard library). We can now fulfil our task:
, 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.
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.
) 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.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.
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.
composes partial functions (left-to-right), captured by Kleisli arrows of the 
captures a universally quantified constraint [6]: for all types
then
has an instance of the
class.2
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
.
, 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.
(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):
,
,
). 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: 
and
satisfying the requisite laws.
of a profunctor
is called aligned if
=
.
(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:
and
map any functor into a profunctor by the following type class instances:
, enforcing that the monad
is a member of the
class which we define as:
in
.
and
both map any monad into a monadic profunctor:
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: 
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:3
for the writer monad transformer with the
monad: 
becomes:
:
) to the one above, and provided
and
instances to support monadic bidirectional programming with codecs.
-notation. This structuring allows both the forwards and backwards components of a biparser to be defined simultaneously in a single compact definition.
as an alias for
.
is backward round tripping if for all
and
then (recalling that
): 
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
.
) 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
).
is parsed (going forwards) into some value
which when printed produces the initial source
:
is forward round tripping if for every
and
we have that:
(Sect. 3.2) is both backward and forward round tripping. Proof by expanding definitions and algebraic reasoning.
is a family of subsets
of
indexed by types
and
.
is compositional if the monadic profunctor operations are closed over \(\mathcal {R}\), i.e., the following conditions hold for all types
,
,
: 
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.
, 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:
is weak backward round tripping if for all
,
, and
,
then: 
of the printer gives us a property that is compositional:
is weak backward round tripping.
is weak backward round tripping.
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:
) 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:
is weak backward round tripping, and for all
.
, then
is backward round tripping.
, 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.
and
is a polymorphic function
such that: 
operation for biparsers (above) is a monadic profunctor homomorphism between
and the monadic profunctor
.
is backward round tripping.
,
, and
(writing
for
):
From these and the homomorphism properties we can prove
: 
with Corollary 
is weak backward round tripping) enables Theorem 
is backward round tripping.
. We capture the general pattern as follows:
with a homomorphism
from
to the monadic profunctor of partial functions
. We say that
is the pure projection of
.
is called the identity projection when
for all
.
produces an output from which the input can be recalculated:
be a monad. A function
is an injective arrow if there exists
(the left arrow inverse of
) such that for all
: 
to be applied to injective arrows:
be a monadic profunctor. A property
indexed by types
and
is quasicompositional if the following holds 
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.,
.
is weak forward round tripping if for all
,
, and
then: 
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
.
biparser is weak forward round tripping.
is weak forward round tripping if we restrict the parser to inputs whose digits do not contain redundant leading zeros.
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.
is weak forward round-tripping, and for all
,
, then
is forward round tripping.
is forward round tripping by the above theorem (with identity projection shown in the proof of Corollary 
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:
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: 
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 
and a predicate on sources in
for additional dynamic checking. This is provided by the following
and
monadic profunctors:
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.
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:
when the above properties only hold when
is an element of
.
, 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:
and values of type
, we have the following source type and a simple lens:
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.
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.
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
.
is weak backward round tripping if for all
,
, for all sources
,
, and for all
, we have: 
is a purifiable monadic profunctor (Definition 9), with a family of pure projections
indexed by a source
, defined:
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
.
.
is weak backward round tripping.
has identity projection:
.
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
.
such that
, and for all
then
.
for all
is backward round tripping on lists of length
.
is weak forward round tripping if for all
,
, for all sources
,
, and for all
, we have: 
is weak forward round tripping and has identity projections on some subset
(i.e., for all
,
then
) then
is also forward round tripping on
.
, the lens
is forward round tripping on lists of length
.
. A value
represents a subset of
, where
is a generator of values in that subset and
maps pre-views 
defines a predicate on
, which is true if and only if
is
of some value. The function
extracts this predicate from the backward direction:
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
:
, 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.
is complete (backward round tripping) when
implies
.
is sound (forward round tripping) if for all
,
implies that
.
is weak-complete when 
is complete if it is weak-complete and its checker satisfies a pure projection property:
, 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.
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.
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.
,
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.
extension allows universal quantification in constraints, written as 
from the