On the relationship between parsing and pretty-printing
Clovis Eberhart
August 27, 2012

Contents
1 State of the Art
1.1 Parsing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
1.2 Pretty-Printing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
1.3 Unification of Parsing and Pretty-Printing . . . . . . . . . . . . . . . . . . . . . .

3
3
5
6

2 Global Parsing and Pretty-Printing
2.1 Attempt at Defining Parsing and Pretty-Printing . . . . . . . . . . . . . . . . . .
2.2 Definition of a Parser/Pretty-Printer Pair . . . . . . . . . . . . . . . . . . . . . .
2.3 Properties . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
2.4 Example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
2.4.1 Optional Spacing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
2.4.2 Priority and Associativity . . . . . . . . . . . . . . . . . . . . . . . . . . .
2.4.3 A More Advanced Pretty-Printer . . . . . . . . . . . . . . . . . . . . . . .

8
8
9
11
12
13
13
14

3 Functional Parsing and Pretty-Printing
15
3.1 Limits of Global Parsing and Pretty-Printing . . . . . . . . . . . . . . . . . . . . 15
3.2 Attempts at Defining a Functional Parser/Pretty-Printer Pair . . . . . . . . . . . 15

1

Introduction
Parsing and pretty-printing are both very important in computer science. Parsing maps strings
to structured internal pieces of data that corresponds to them, while pretty-printing maps thesestructured internal pieces of data to strings that correspond to them.
Because communication in a computer can only be achieved by use of (bit)string, parsing
and printing are ubiquitous in computer science. Every time some data is printed onto a screen
for someone to read, it has to be printed in a human-readable way. Every time a human inserts
data into a computer, this human-readable data is parsed into easily usable data. Every timesome data is transferred through any protocol, this data must first be printed by the sender
into a (bit)string and sent to the receiver, who has to parse this string to recover the data.
Moreover, parsers and pretty-printers are also important in other fields that use them, forexample in linguistics to find the structure of and produce natural language sentences or in
biology to analyse DNA sequences.
On the one hand, it is quite obvious that parsers and pretty-printers are somehow related
to each other. On the other hand, they are typically implemented separately, which leads toredundancy, which in turn may lead to inconsistency in protocols that use those parsers andpretty-printers, and even security holes in these protocols.
Recently, some frameworks have been suggested to unify parsing and pretty-printing, forexample [9]. They aim at implementing parsing and pretty-printing together to reduce theworkload and avoid inconsistencies between parsers and pretty-printers. However, as far as weknow, no formal definition of what consistency between a parser and a pretty-printer is has everbeen given. Therefore, if implementing parsing and pretty-printing together does reduce theprogrammer’s workload, it does not ensure that the parser and pretty-printer will be consistent.
The problem I tried to solve during my internship was to find a definition of what consistency
between a parser and a pretty-printer is. Even though this problem may sound easy at first,
the fact that there is no answer to it yet even though parsers and pretty-printers are crucial incomputer science hints that this problem is actually quite complicated.
We will first see a brief state of art of parsing and pretty-printing. Then, I will show how
I found a definition for consistency between parsing and pretty-printing, give this definition,some properties that can be ensured for consistent parsers and pretty-printers, and work on an
example. I’ll finish by showing the limits of this definition and studying the case of functional
parsing and pretty-printing, which could prove to be very interesting as it could lead to a morepractical definition than the general one.
I will warn readers beforehand that, since what I did was search a definition, there is no
definite answer here, as there is no way to prove that my definition is the ‘right’ one. All I can
do is give some ideas of why I think it is a good definition, give properties that result from thisdefinition and show that it works on some non-trivial examples.

2

Chapter 1

State of the Art
1.1

Parsing

The notion of parsing is linked to that of grammar in general, and most of the time to thatof context-free grammar (when I will write grammar from now on, it will mean context-freegrammar unless specified otherwise). We suppose that the reader is familiar with them, as wellas the notions of production of a grammar and derivation tree associated to a production.
What we call parsing here is the action of mapping a string to a structured internal piece ofdata. However, most of the time, when someone refers to parsing in computer science, they arethinking of an algorithm that takes a string as its input and returns a (or all the) derivationtree(s) that produce this string according to a given grammar. I will call this parsing according
to a grammar.
This has been thoroughly studied from an algorithmic point of view, and there are a lot ofalgorithms to parse according to a grammar. One of the, if not the, most well-known of thesealgorithms is the Earley algorithm [3]. Dick Grune and Ceriel J.H. Jacobs have published abook about parsing in which many algorithms and techniques to parse according to a grammar
can be found [4]. There are some very advanced features in these parsers to improve theircomplexity and parse according to larger classes of context-free grammars, but, in our case,
we’re not interested in which particular algorithm to use as long as it returns all the derivation
trees associated to the string, so we won’t consider a particular algorithm and just treat parsing
according to a grammar as a function that returns all the derivation trees associated to an input
string.
Let us introduce a ‘toy’ grammar for the sake of example. This grammar is theoreticallyused to parse arithmetic expressions:Gtoy = (N , T , R, E) where the set of non-terminals is N = {E, T, F }, the set of terminals is
T = N ∪ {+, -, *, /, (, )} (even if this not authorized in the definition of a grammar because T is
infinite, this could be simulated, but would just make the example much more complicated without adding anything interesting), the set of derivation rules is R = {E → E+T | E-T | T, T →T *F | T /F | F, F → (E) | i for i ∈ N} and the start symbol is E.
Setting aside the particular algorithm used, parsing "(1+2)*3" according to Gtoy gives (thederivation tree has been rotated for space efficiency matters):

3

E
T
T

*

F

F
3

(

E

)

E

+

T

T

F

F

2

1

However, most of the time, parsing according to a grammar is not what real parsers do.
When a string is parsed, the result is not the derivation tree in a given grammar. For example, inthe example above, the parentheses hold no information, as the expression is already organized
as a tree. Moreover, the imbrication of Es, T s and F s does not give any information either. The
result that one could expect from a parser parsing arithmetic expressions would be somethingalong the lines of:
E
*
+

3

*

E

+

E

3

or
E

1

E

2
1

2

It is crucial to note that these trees, if they are seen as derivation trees, are derivations of"123" and "1+2*3" respectively, and not "(1+2)*3". Therefore, parsing cannot be defined
as a function that maps strings to their derivation trees in a certain grammar, but has to besomething more general.
A functional way of seeing a parser is to say that parsers map strings to some internal data
type α. But, to use the full power of functional programming, an interesting approach is tocombine simple parsers to create more complex ones by using parser combinators [6], which
are higher-order functions that accept parsers as their input and produce a new parser. Oneof these combinators is the sequential combinator <*>. When it is applied to two parsers p1
and p2 , the result p1 <*>p2 uses p1 to parse the start of the string, and p2 to parse the rest of
the string (the result being the result of p1 (that has to be a function) applied to the result of
p2 ). This indicates that a natural way to describe a functional parser is to say that not only it
returns an element with type α, but it also returns a string that is ‘the part of the string that4

hasn’t been parsed’. Moreover, such a parser is typically non-deterministic, so a parser has type
P (α) = α → List(α × String).
For example, if p is a parser that parses decimal integers and maps them to integers, itwould have type P (int) = α → List(int × String) and the result of the parser on "0123" wouldbe:p("0123") = [(0, "123"); (1, "23"); (12, "3"); (123, ε)]Wadler showed very early that parsers form a monad [11], a structure stemming from category theory that was proved useful in handling a number of computational problems (e.g.
adding side effects to purely functional programming languages [7]).
Definition (monad). A monad (T, return, bind) is a triple made of a type constructor T thatmaps every type α to T α and two functions: return with type α → T α and bind with type
T α → (α → T β) → T β. They must fulfill the following properties:• ∀x. bind x return = x• ∀x, f. bind (return x) f = f x• ∀x, f, g. bind (bind x f ) h = bind x (λx.bind (f x) g)
For parsers, the type constructor is P (α) = α → List(α × String), return x is the parser
that doesn’t consume any input and returns x. bind p f is a little bit more complex: the parser
bind p f first applies p which returns a list of (value, string) pairs, applies f to each value,
resulting in a parser, which in turn is used to parse the corresponding strings, then, all the
resulting lists are flattened into a single list (even though this may sound twisted, this is only
a way to represent sequential composition).
In the end, even though monads are a framework that is adapted to the study of parsers,
I still haven’t given the definition of parsing. That is because I found no formal definitionof parsing other than that of parsing according to a grammar. Even in the case of parsing
according to a grammar, when one tries to define parsing for more classes of grammars thancontext-free grammars, the definition is not formal any longer. The best definition I found forparsing according to a grammar is the following [4]:Parsing is the process of structuring a linear representation in accordance with a given
grammar.

1.2

Pretty-Printing

Pretty-printing is the action of associating to some internal structured data a ‘pretty’ string that
represents it. Compared to the literature and research on parsing, the literature and researchon pretty-printing is slim. There is no solid theory behind pretty-printing. Contrary to parsing,for which parsing according to a grammar is non-trivial, (pretty-)printing a given tree where
the terminal symbols are exactly the leaves of the tree is very easy. Therefore, there is no suchthing as pretty-printing according to a grammar.
Even though there are a libraries in a lot of languages to pretty-print (Haskell, OCaml,
Coq...), the techniques used differ in all those libraries and they’re all ad hoc (for example, theOCaml library uses what they call boxes, while Hughes’s library (in Haskell [5]) uses horizontal
and vertical composition of documents).
Pretty-printing can also be seen from a functional point of view (for example, it is seen froma functional point of view in Hughes’s library). In that case, since a pretty-printer maps internal
5structured data to a ‘pretty’ string, it can be seen as a function with type P (α) = α → String.
However, as far as I know, there is no counterpart of the classic parser-combinator frameworkfor pretty-printers.
However, the question of knowing what pretty-printing is is pretty tricky, since the notionof beauty is subjective. For some people, writing a moderately complex function on a single
line is what they prefer, while others like skipping lines and putting lots of indentations. Thissuggests that there is something that looks somewhat arbitrary in pretty-printers.

1.3

Unification of Parsing and Pretty-Printing

Some frameworks have been suggested to unify parsing and pretty-printing. One of them,called invertible syntax descriptions has been suggested by Rendel and Ostermann [9]. It aims
at producing parsers and pretty-printers using two instances of the same description. This helps
reduce the programmer’s workload when he has to program a parser and a pretty-printer, andit also aims at avoiding inconsistency between the parser and the pretty-printer (however, since
there is no definition of what inconsistency is in their paper, they do not prove anything). They
recursively build parsers and pretty-printers using some combinators inspired by the classic
parser combinators.
The combinator <$> has type (α → β) → P (α) → P (β) (where P can be instantiated asa parser or a pretty-printer). It is inspired from a classic parser combinator, f <$>p parses thestring using p and then applies f to the result. However, for pretty-printers, f <$>p may print
according to p, but there is nothing to apply f to. What we actually want to do is somethingthat would be more or less the inverse of parsing, that is use f −1 on the input, then print usingp. This is why we need some sort of inverse to this function.
Let us note Just(A) the set A ∪ {∗} where ∗ is not in A.
Definition (partial isomorphism). A partial isomorphism between A and B a function f : A →Just(B) such that there exists a function noted f −1 : B → Just(A) that satisfies the property:∀a ∈ A, ∀b ∈ B. f (a) = b ⇔ a = f −1 (b).
The isomorphisms are partial to allow parsers and pretty-printers to fail.
Now, if we allow <$> to be used only with partial isomorphisms, we can instantiate f <$>pfor both parsers and pretty-printers. Therefore, it is necessary to change the type of <$> toIso(α, β) → P (α) → P (β), where Iso(α, β) is the type of partial isomorphisms between α andβ. The instantiation is the same as above for parsers, and for pretty-printers, we use f −1 on
the input and then print with p.
The combinator <*> has type P (α) → P (β) → P (α × β). It is inspired from the classic
sequential parser combinator, that has type P (α → β) → P (α) → P (β) (but it is more general,
because the classic combinator cannot be defined for pretty-printers). For parsers, p1 <*>p2 uses
p1 to parse the beginning of the string, then p2 to parse the rest of the string, and returns thepair of their results. For pretty-printers, p1 <*>p2 uses p1 to print the first element of the pair,
p2 to print the second and concatenates the results.
The combinator <|> has type P (α) → P (α) → P (α). It expresses choice between twoparsers/pretty-printers. The instantiation is easy this time: p1 <|>p2 tries both parsers/prettyprinters, uses p1 if it returns something and uses p2 otherwise.
They also define basic parsers and pretty-printers. pure has type α → P (α). pure x canbe instantiated as a parser that associates x to the empty string, and as a pretty-printer thatprints the empty string when it has input x and fails otherwise. token has type P (Char), it
can be instantiated as a parser that associates to each character itself and fails on the empty
string, and as a pretty-printer that prints the character it receives as its input.
6

They then show how to use the basic parsers/pretty-printers and the combinators to describe
more complex parsers and pretty-printers, giving the example of a parser/pretty-printer for lists.
More recently, Affeldt, Nowak and Oiwa have used invertible syntax descriptions to provethat a parser and a pretty-printer for a network protocol (a fragment of TLS) are consistent [1].
In this specific case, since the parser and pretty-printer are inverse to each other, it is obviousthat they are consistent (the hard part was to prove that they are inverse to each other). The
idea of studying the relation between parsing and pretty-printing stems from this work.

7

Chapter 2

Global Parsing and Pretty-Printing
2.1

Attempt at Defining Parsing and Pretty-Printing

After having read a few articles about parsing and pretty-printing, it came to me that there
was no formal definition of parsing and pretty-printing. The obvious thing to do to study the
relation between parsing and pretty-printing was first to define parsing and pretty-printing.
Seeing how there is a convenient framework for parsing (monads), I wondered whether thesame kind of framework could be found for pretty-printing. It is well-known to people whohave studied parsing and pretty-printing that pretty-printing cannot be expressed as a monad.
Indeed, as I wrote above, a pretty-printer can be seen as a function that has type α → String,
since it prints internal data. If pretty-printing could be expressed as a monad, one should be
able to write a bind function with type (α → String) → (α → β → String) → String → β,which is impossible because we need to produce an element with type β but no function can
produce it. The only solution left is that bind p f must always fail, but then result and bindcannot verify the laws of the monad. Parametrized monads, which can express more thanmonads (for example, it can express memory usage with changing types while monads can only
express memory usage without changing types) aren’t more useful than monads here as the verysame argument shows that they can’t express pretty-printing.
Then, I wondered if it is possible to express pretty-printing using comonads. A comonadhas a type constructor W and two functions extract with type W α → α and cobind with typeW α → (W α → β) → W β, which must also satisfy some properties. However, they cannot
express pretty-printing as we cannot write the extract function for pretty-printing. Indeed, thisfunction would have type (α → String) → α, so we need to produce an alpha no function can
produce. The only choice left is that the pretty-printer must always fail, but as above, thiscontradicts the comonad laws.
These attempts at defining parsing and pretty-printing made me realise that maybe there
is no way to define parsing and pretty-printing separately. The problem that arises when I
tried to define them separately was that there is always something arbitrary in their definition.
When a parser parses a string, the result depends entirely on what we want to do with it. In
real parsers, for example parsers produced using yacc, parsers parse the string according toa given grammar, but they then transform the derivation tree they obtain into internal data.
How they transform this derivation tree into internal data is arbitrary. Like in the example inthe beginning, I gave two possible trees that a parser that parses "(1+2)*3" can return, but it
could also return 9, arithmetic expression, non-empty string or a variety of other results...
What a string is parsed into makes sense only because there is a pretty-printer to print thedata that was parsed. Since both the data and the strings don’t have other meanings than the8

ones we give them, the data is not related to the strings a priori. That is why I say that whena parser parses a string into some data or when a pretty-printer prints some data into a string,
what string is linked to what internal element is arbitrary as long as parsers and pretty-printers
are considered on their own.

2.2

Definition of a Parser/Pretty-Printer Pair

Before I began my internship, my supervisor, David Nowak, had studied parsing and prettyprinting and had tried to find a definition of the consistency between parsing and pretty-printing.
He found some relations that he thought parsing and pretty-printing should verify. The mostimportant are, if we note f a parser and g the corresponding pretty-printer, f ◦ g ◦ f = f
and g = g ◦ f ◦ g (with the formalism he used (functional parsing), the relation f ◦ g = iddidn’t hold, while it holds with the formalism I use). These relations and the fact that parsing
and pretty-printing are nearly inverse to each other made him think that maybe parsing andpretty-printing form a Galois connection. Therefore, my approach was to see if the notion of
Galois connection could be used to define parsing and pretty-printing.
There are two points we saw only retrospectively and that support the idea that the notionof Galois connection is appropriate to define parsing and pretty-printing. A Galois connection
is made of two functions. The previous attempts I made at defining parsing and pretty-printing
failed inter alia because parsing and pretty-printing were considered on their own, which is not
the case with Galois connections. The other point is that there is a notion of ‘beauty’ necessary
to define pretty-printers, so we need to be able to say if a string is prettier than another one.
This means that there is an order (actually a pre-order) on strings induced by the pretty-printer.
Since Galois connections are defined between pre-ordered sets, the fact that there is a natural
pre-order on strings supports the idea of using Galois connections.
We remind the reader that a pre-order is a reflexive and transitive binary relation and a(partial) order is a reflexive, transitive and antisymmetric relation.
We will note S the set of strings, TG the set of derivation trees induced by G, and A will
denote a set of semantics. We will note A, A1 , A2 ... subsets of A and S, S1 , S2 ... subsets of S.
Let us recall what a Galois connection is:
Definition (Galois connection). A Galois connection between two pre-ordered sets (A, 6) and(B, ) is a pair of functions (f, g), with f : A → B and g : B → A, that verifies:
f and g are monotone∀a ∈ A, ∀b ∈ B. a 6 g(f (a)) and f (g(b))  b
I roughly describe here my vision of how parsers and pretty-printers operate. A parser
parses a string according to a given grammar and then associates a semantics in A to theresulting derivation tree. A pretty-printer chooses the ‘prettiest’ derivation tree corresponding
to a semantics and then prints the corresponding string.
Therefore, there are three levels involved in parsing and pretty-printing: strings, derivation
trees and semantics. The arbitrary part is the link between the derivation trees and the semantics. Only when parsing and pretty-printing are considered together does the link between
strings and semantics make sense, as they intuitively have to verify some properties. In my
opinion, that is the heart of parsing and pretty-printing.
Using what I said before, we can see a parser as a function f : S → P(A), since there may
be several derivation trees corresponding to a single string and these trees may be associated9to different semantics. Therefore, parsers can be non-deterministic. However, a pretty-printeris a function g : A → S, since there is a single ‘prettiest’ derivation tree corresponding to asemantics, and therefore a single ‘prettiest’ string associated to a semantics.
Since there is an asymmetry between the domains and codomains of f and g, to define a
Galois connection, we need to lift the functions so that the range of f is the codomain of g andvice versa.
We will define two kinds of lifted functions. If f : A → B, we note f → : P(A) → P(B) the
function defined by f → ({ai | i ∈ I}) = {f (ai ) | i S∈ I}. If f : A → P(B), we note f ∗ : P(A) →P(B) the function defined by f ∗ ({ai | i ∈ I}) = i∈I f (ai ).
To pretty-print a semantics, a pretty-printer chooses the ‘prettiest’ derivation tree associatedto that semantics and prints the string that corresponds to that derivation tree. Therefore, weneed a formal way to define the ‘prettiest’ derivation tree. The way I formalized it was to use
a partial order.
Definition (beauty order). A partial order v on a set T of derivation trees is called a beautyorder corresponding to a set of semantics A if it verifies the following properties:
T is partitioned in Card(A) classes {Ci | i ∈ I} such that ∀t, t0 ∈ T . t v t0 implies that t
and t0 are in the same class ;for each class Ci there exists a strictly greatest element for v restricted to Ci , formally:∃t ∈ Ci .∀t0 ∈ Ci \{t}. t0 v t ∧ t 6v t0 .
The idea behind the definition of a beauty order is that t1 v t2 if and only if t2 is prettierthan t1 . The properties are meant to ensure that the derivation trees that can be compared
are only the ones that corresponds to the same semantics (each class is seen as the set of treesthat are associated to a given semantics, so we need as many classes as semantics) and that, foreach semantics, there is exactly one prettiest derivation tree (the greatest element of the classassociated to that semantics).
However, this is not enough yet. We would like to derive a pre-order on S using the beautyorder on TG by doing S1  S2 if and only if T1 v→ T2 where Ti is the set of derivation trees
corresponding to a string in Si . However, this requires that v be lifted to P(TG ).
After having searched for a canonical way to lift an order from any set A to P(A) withoutfinding any, I decided to lift the order on TG using the properties of the beauty order.
Definition (lifted order). If 6 is an order on any set A, we call lifted order and note 6→
the relation on P(A) defined by: A1 6→ A2 if and only if ∀a1 ∈ A1 .∃a2 ∈ A2 . a1 6 a2 and∀a2 ∈ A2 .∃a1 ∈ A1 .∃a+ ∈ A. a1 6 a+ ∧ a2 6 a+ .
In general, 6→ is not even a pre-order.
Properties. Here are two properties on lifted orders.
If 6 is the equality on A, then 6→ is the equality on P(A).
If v is a beauty order on TG , then v→ is a pre-order on P(TG ).
Proof. Let us prove these two properties.
Let us suppose that 6 is the equality on A. If A1 = A2 , then A1 6→ A2 (very easy, takea1 = a2 = a+ in the definition of lifted order). If A1 6→ A2 , then A1 ⊆ A2 (first part of thedefinition of lifted order) and A2 ⊆ A1 (second part of the definition), so A1 = A2 . Therefore
A1 6→ A2 if and only if A1 = A2 .
We need to prove that v→ is reflexive and transitive. Reflection was done above. Let us
suppose T1 v→ T2 and T2 v→ T3 . Be t1 ∈ T1 , according to the first part of the definition of10

lifted order, there is t2 ∈ T2 such that t1 v t2 , and using the definition a second time, there ist3 ∈ T3 such that t2 v t3 , so t1 v t3 . Be t3 ∈ T3 , using the second part of the definition, there
exists t2 and t+ such that t2 v t+ and t3 v t+ . Therefore, t2 and t3 are in the same class.
Using the definition one more time, we have there exists t1 ∈ T1 that is in the same class. Since
we know there is a greatest element in that class (let us note it t̃), we have t1 v t̃ and t3 v t̃.
Therefore, v→ is transitive.
We can now define the pre-order  on S derived from the pre-order v→ on P(TG ) as we
wanted to: S1  S2 if and only if T1 v T2 where Ti is the set of derivation trees associated to astring in Si ( is obviously a pre-order).
Since there is no natural way to compare the semantics (especially if we see that order as away to compare beauty), we will define the order on A as the equality. When we lift it to P(A),it is still the equality. With this, can finally give the definition of a parser/pretty-printer pair.
Definition (parser/pretty-printer pair). Let A be a set of semantics and G a context-free grammar. A parser/pretty-printer pair is a pair a functions (f, g) with f : S → P(A) and g : A → S
such that (f ∗ , g → ) is a Galois connection between the pre-ordered sets (P(S), ) and (P(A), =)where  is derived from a lifted beauty order on TG corresponding to A.

2.3

Properties

Let us look in greater detail at the definition of a parser/pretty-printer pair. Let us translate
the definition of a Galois connection in the particular case of parsing and pretty-printing.
The parser f ∗ must be monotone, which means that if S1  S2 then f ∗ (S1 ) = f ∗ (S2 ). Thismeans that two sets of strings are comparable only if they have the same semantics, which ispretty natural, since that pre-order is supposed to measure the beauty of a string, two strings
that don’t have the same semantics cannot be compared.
The pretty-printer g → must be monotone, which means that if A1 = A2 then g → (A1 ) →g (A2 ), which is obviously always true.
∀S ⊆ S. S  g → (f ∗ (S)), which means that every set of strings is smaller, i.e. less beautiful,than when it is parsed and pretty-printed (so we really are pretty-printing).
∀A ⊆ A. f ∗ (g → (A)) = A, which means that semantics are unchanged through prettyprinting and parsing.
The properties f ◦g◦f = f and g◦f ◦g = g we wanted to verify cannot be verified because therange and codomains don’t match, but the same properties are verified for the lifted functionsf ∗ ◦ g → ◦ f ∗ = f ∗ and g → ◦ f ∗ ◦ g → = g → (since f ∗ ◦ g → = id).
Another property we have is that when the prettiest string associated to a semantics isparsed, the result is exactly that semantics. Indeed, if g(a) = s and f (s) = A where A 6= {a},this contradicts the fact that f ∗ (g → ({a})) = {a}. It seems reasonable to ask for the prettiest
string associated to a semantics to be associated to this semantics only. A counter-example one
may think of could be the programming language C, where the prettiest form of the integer
1 could be "1", and "1" would have two semantics: 1 as an integer and 1 as a real number.
However, this is not really a counter-example, as "1" does not have two semantics. What is
important to notice here is that the definition given is for global parsing and pretty-printing,which means that "1" is not seen as a substring of another expression to be parsed (for example"1 + 0.2"), in which "1" has a real number semantics, but is seen as a string on its own. If"1" is typed on its own in C, its semantics is only that of the integer 1.

11

2.4

ExampleThis time, let us give another, more flexible, grammar for arithmetic expressions.
Gex = (N , T , R, E) where the set of non-terminals is N = {E, T, F, OS}, the set of terminals
is T = N ∪ {+, -, *, /, (, ), ↓, } (as before, this is not authorized, but could be simulated), theset of derivation rules is R = {E → OS E OS+OS T OS | OS E OS-OS T OS | OS T OS, T →T OS*OS F | T OS/OS F | F, F → (E) | i for i ∈ N, OS →↓ OS | OS | ε} and the startsymbol is E. represents a space and ↓ a line break. OS thus indicates optional spacing. This
grammar is more flexible than Gtoy and can typically be used to parse arithmetic expressions
written by humans. It can parse strings such as "(1+2)*3", but also "(1 + 2) * 3" and" (1 + 2)↓ *↓ 3". I apologize for the notations which aren’t exactly easy to read.
For example, the derivation tree of " (1 + 2)↓ *↓ 3" is:
E
OS

T

E

OS

T

ε

F

OS
↓

E

)

OS

+

OS

↓

OS

OS

OS F

F

ε

ε 2

F

OS

ε

3

OS
ε

T

T

OS

*

ε

(

OS

1
Let us define a set of semantics A as the set of binary trees with nodes labelled with +, −,∗ or / and leaves are labelled with integers.
Let us define the following parser: f : S → P(A) that parses the string according to thegrammar G and then translates the result into the ‘expected’ semantics in A (the link between
trees in TG and A is very simple).
There are pretty much no constraints on pretty-printers. Since they’re just functions, we
can choose ‘manually’ a derivation tree associated to a semantics (the only thing it must verify
is that it is associated to this semantics) and claim that it is the prettiest one. However, it may
be useful to have a pretty-printer that is easily computable.
We will define different pretty-printers for these semantics using a slightly simplified versionof the formalism of boxes used in the pretty-printing library in OCaml (this method is ad hoc,
but this is only meant to be an example). The idea behind boxes is that when a string is inside
a box, if there is a line break in this string, instead of going to the start of the next line, there
is a tabulation that is aligned with the start of the box.
Here is an example: if we write [] to denote a box, then the string "([foo↓bar])" is"(foo↓ bar)" and the string "1 + [foo↓bar]" is "1 + foo↓bar".
The way we will use boxes is very simple: we will define the prettiest form recursively on
the semantics tree, and the prettiest forms of the subtrees will be put inside boxes. In the next
paragraphs, I will often write ‘pretty-print’ for ‘parse then pretty-print’ for a lighter style.

122.4.1

Optional Spacing

The first and most simple pretty-printer we can define is the following: write everything on thesame line, with parentheses around every sub-expression and a single space around each operator. This would pretty-print " (1 + 2)↓ *↓ 3" to "((1) + (2)) * (3)". Another very simple
pretty-printer that can be defined is the following: write the tree op(t1 , t2 ) as " (s1 )↓o↓ (s2 )"where si is the prettiest form of ti and o corresponds to the operator. This would pretty-print" (1 + 2)↓ *↓ 3" to " ( (1)↓ +↓ (2))↓*↓ (3)".
Let us explain why they are parser/pretty-printer pairs according
F to the definition we gave.
First, we need to define the beauty order. The classes are TGex = a∈A Ca where Ca contains
all the trees associated to the semantics a (we will always define the classes this way). The
beauty order v on Ca is defined by ∀t, t0 ∈ Ca . t v t0 if and only if t = t0 ∨ t0 = t̃ where t̃ isthe tree we defined recursively as the prettiest one. Then, the properties that define a Galois
connection follow easily:f ∗ is monotone: if S1  S2 , that means that T1 v T2 (where Ti is the set of derivation trees
associated to Si ), which implies that T1 and T2 have trees in exactly the same classes Cai , so
are associated to exactly the same semantics, so f ∗ (S1 ) = f ∗ (S2 ).
∀S ⊆ S. S  g → (f ∗ (S)): be S ⊆ S, then g → (f ∗ (S)) is a set the set of prettiest strings
corresponding to the semantics f ∗ (S) (by definition of f , g and v). Since the prettiest strings
correspond to a single semantics, we have that the set of derivation trees associated to g → (f ∗ (S))
has trees in exactly the same classes as the set of derivation trees associated to S. Moreover,the former possesses all the greatest elements of these classes, so S  g → (f ∗ (S)).
∀A ⊆ A. f ∗ (g → (A)) = A: be A ⊆ A, (g → (A)) is the set of prettiest strings associated tothese semantics. Since each prettiest string is associated to a single semantics, f ∗ (g → (A)) = A.
While these two parser/pretty-printers pairs handle optional spacing, they do not handle
operator priority nor associativity, since the pretty-printers put parentheses everywhere.

2.4.2

Priority and Associativity

What we can do is get rid of the useless parentheses (here, it is done for the first prettyprinter, but it could be done for the second one as well). To do that, one possibility is totry to pretty-print op(t1 , t2 ) as the following in order and reject if the semantics is wrong (wejust need to parse the resulting string to know that): "s1 o s2 ", "(s1 ) o s2 ", "s1 o (s2 )"and "(s1 ) o (s2 )" (we know that the last one will work anyway). This would pretty-print" (1 + 2)↓ *↓ 3" to "(1 + 2) * 3". It would also pretty-print "(1 * 2) + 3" to "1 * 2 + 3".
This handles operator priority. It also handles left associativity: "(1 + 2) + 3" would bepretty-printed to "1 + 2 + 3" (it would be the same for other operators). However, it doesn’t
handle right associativity: "1 + (2 + 3)" will be pretty-printed to "1 + (2 + 3)". That is
because "1 + (2 + 3)" will be parsed to +(1, +(2, 3)), which is different from +(+(1, 2), 3),
which is the semantics associated to "1 + 2 + 3".
Like in the previous part, we could show that they define parser/pretty-printer pairs (thebeauty order is defined more or less the same way).
Therefore, we want to review our semantics and how we parse. When we see a tree with asubtree +(t1 , +(t2 , t3 )) or ∗(t1 , ∗(t2 , t3 )) after parsing, we change the subtree to +(+(t1 , t2 ), t3 )or ∗(∗(t1 , t2 ), t3 ) respectively. We have created a parser for a new set of semantics (morecomplicated than the previous one, but that will handle right associativity as well). If we

13

do the same as above, we handle optional spacing, operator priority and associativity, threeimportant features of parsing and pretty-printing.

2.4.3

A More Advanced Pretty-PrinterThe pretty-printers we have defined until now are still really simple. Even though we don’t
want to do something too complex, a few other features would be nice. The feature I propose
here is one that could in my opinion be useful. There are a lot of pretty-printers that are meant
to print human-readable data. However, all the examples I know except one [8] disregard avery important point: when data is printed, it is printed onto a screen (most of the time), andthat screen’s width is bounded. The pretty-printer I want to write will write everything on asingle line until it grows too long for the line, at which point it will decompose the arithmetic
expression according to its structure.
The algorithm proceeds as follows: to pretty-print op(t1 , t2 ), we suppose we have a listof strings associated to t1 and t2 ordered by decreasing beauty order (let us call them li =[si,1 , ..., si,ni ]) and we want to create the list of strings associated to op(t1 , t2 ) ordered by decreasing beauty order (the prettiest string associated with op(t1 , t2 ) will be the head of thelist).
If s1,1 and s2,1 are shorter than the line, consider the string "s1,1 o s2,1 ". There are threepossibilities: if the semantics is wrong then discard the string, if it is longer than the line thenput it at the end of the list, if it is smaller than the line then put it at the head of the list. Do
the same for the strings "(s1,1 ) o s2,1 ", "s1,1 o (s2,1 )" and "(s1,1 ) o (s2,1 )" in that order. If
a string has already been put at the head or the end of the list, the new string is put ‘inside’
the list (once a string is put somewhere in the list, it ‘does not move’). Repeat the same with
s1,j1 and s2,j2 as long as these strings are smaller than the line (the exact order in which thes1,j1 and s2,j2 are considered is not really important, si,j must only be considered before si,j+1 ).
Only for si,j smaller than the line (with the same constraint on the order as above), consider
the following strings in order " s1,j1 ↓o↓ s2,j2 ", " s1,j1 ↓o↓ (s2,j2 )", " (s1,j1 )↓o↓ s2,j2 " and" (s1,j1 )↓o↓ (s2,j2 )" and do the same as above.
Now, for every s1,j1 and s2,j2 (the order in which they are considered must still follow
the same rule as above), consider the strings " s1,j1 ↓o↓ s2,j2 ", " s1,j1 ↓o↓ (↓ s2,j2 ↓ )"," (↓ s1,j1 ↓ )↓o↓ s2,j2 " and " (↓ s1,j1 ↓ )↓o↓ (↓ s2,j2 ↓ )" in that order and do the sameas above.
The resulting list is associated to op(t1 , t2 ).
This time, the beauty order is a little more complex. Even though the classes are defined
the same way, we now have a list [s1 , ..., sn ] of strings ordered by decreasing beauty order. We
can then define v on Ca as s v sn v sn−1 v . . . v s2 v s1 for s 6∈ {s1 , ..., sn }. This timeagain, the properties that define a parser/pretty-printer pair follow (the reasoning is the same
as before).
Please note that this algorithm (and the previous ones as well) do not aim at being efficient,they’re only meant to be proofs of concept. Also, while this does seem to work on examples
with low tree depth, I don’t know how this handles examples with higher tree depth, since theorder on the strings associated to a semantics become complex.

14

Chapter 3

Functional Parsing andPretty-Printing
3.1

Limits of Global Parsing and Pretty-Printing

Even though the definition of global parsing and pretty-printing sounds very powerful there aresome limits to it. Actually, it is also because it is very powerful that there are some limits toit. Let us illustrate this point with a simple example. If we have a parser/pretty-printer pairthat parses integers that can be written in two different ways (let us say i can be written "i" indecimal and "0xi" in hexadecimal). And let us code Turing machines into integers. Now, theparser is very simple: it just maps the decimal and hexadecimal representations of an integer
to that integer. The pretty-printer is more complex: it maps i to its decimal representation
if the Turing machine that corresponds to i stops and to its hexadecimal representation if it
doesn’t stop. Theoretically, those two functions verify the definition of a parser/pretty-printerpair (and there is no reason to think they’re not a parser and a pretty-printer), but they cannot
be effectively computed. This shows that this definition is very general, but, because of thisgenerality, it cannot always be verified that two functions form a parser/pretty-printer pair.
Another practical limitation of global parsing and pretty-printing is that, to use this definition, we need a grammar to parse the expressions and we need to find a way to specify how
to associate derivation trees to semantics. This may become a very difficult task when theexpressions studied become complex (for example, if we want to write a parser/pretty-printerpair for a programming language like C or OCaml). Therefore, it seems reasonable to study
the case of functional parsing and pretty-printing, as there would be no need to explicitly define
the whole grammar and how the derivation trees of this grammar are associated to semantics:
we would only need to do that for basic parsers and pretty-printers, and show how semantics
are transformed when parsers and pretty-printers are combined.

3.2

Attempts at Defining a Functional Parser/Pretty-PrinterPair

The main difference between a global parser/pretty-printer pair and a functional one is that,while a global parser parses the whole string, a functional parser can parse the beginning of thestring and leave the rest for another functional parser to parse. Of course, when a functionalparser is considered as a global parser, the only relevant results are those that were found whileparsing the whole string. For example, a functional parser for arithmetic expressions that parse
the string "1*(2+3)" will return a list with the semantics associated to "1" and the remaining
15

string "*(2+3)" and the semantics associated to "1*(2+3)" and the remaining string ε. When it
is considered as a global parser, we’re only interested in the semantics associated to "1*(2+3)",
but when it is seen as a functional parser, both semantics are interesting because we don’t know
how much of the string that parser had to parse (because there are other parsers to parse therest of the string).
This difference in behavior induces a difference in the nature of the objects we manipulate.
While global parsers only had to associate semantics to strings, and therefore were functions
f : S → P(A), they now have to return strings with each semantics, and therefore are functions
f : S → P(A × S). Moreover, for pretty-printers to have a symmetrical behavior (because wehope that the definition of functional parsing and pretty-printing will still be based on Galois
connections), they will have to include the fact that semantics are paired with strings, so they
have type g : A × S → S, the idea being that g maps (a, s) to the prettiest string associated toa concatenated with s.
Another very important difference between global and functional parsing/pretty-printing isthat, in functional parsing/pretty-printing, pretty-printers can fail (this wasn’t the case with
global pretty-printing).
Therefore, the sets we need to consider are a little different: parsers are still functions
f : S → P(A × S), but pretty-printers are now functions g : A × S → Just(S), where ∗ denotes
failure. We can lift functions to f ∗ : P(Just(S)) → P(Just(A×S)) and g → : P(Just(A×S)) →P(Just(S)).
The idea I followed was to stick to the framework of invertible syntax descriptions: find adefinition that would be verified for basic parsers and that would be preserved when combining
parsers. Of course, this definition should also fall back on that of a global parser/pretty-printerpair when the strings are ignored. What we hope for is that by relaxing the definition of a
Galois connection, we will be able to define functional parsing and pretty-printing.
We tried to relax it this way: f ∗ and g → must still be monotone, ∀S ⊆ Just(S). S →g (f ∗ (S)) must still hold, but the last condition becomes:∀A ⊆ Just(A). π(f ∗ (g → ((map σ)(A)))) = A where σ : a 7→ (a, ε) and π returns the list ofas such that (a, ε) is in its input list.
What we’re trying to do here is considering f ∗ and g → as global: it doesn’t change anythingfrom the string’s point of view, but from the semantics point of view, we have to get rid of theplaces where strings appear.
However, this doesn’t work, as it is not preserved by sequential combination of parsers.
Here is a counter-example. Let f be the parser that parses a string to  if it is empty and¯ otherwise. Let g be a pretty-printer that corresponds to f : it maps  to ε and ¯ to "a".
Now, let us consider the parser f 0 = f <*>f , the corresponding pretty-printer g 0 = g<*>g
and the semantics (, ¯). We have g 0→ ({((, ¯), ε)}) = {(ε, "a"), ε} = {"a"} and f 0∗ ({"a"}) ={((, ), "a"); ((, ¯), ε); ((¯, ), ε)}, so π(f ∗ (g → ((map σ)({(, ¯)})))) = {(, ¯); (¯, )} =6 {(, ¯)}.
We haven’t found a definition for functional parsing/pretty-printing yet. It could prove to bea very interesting direction for future research, especially if someone wants to use this definition
to formally prove real parser/pretty-printer pairs.

16Conclusion
In my opinion, the subject I studied during my internship was very important, as the definition
I found of a parsing/pretty-printing pair, if it is accepted by the researchers of the community,
may help formally verify parsers and pretty-printers and perhaps lay the foundations of a formal
theory of parsing and pretty-printing. If it is not accepted, I hope that my work will at least
reawaken the interest of researchers for the question of knowing what it means for a parser anda pretty-printer to be consistent.
Though, in retrospect, the result I found doesn’t look so complicated, I think I could only
find it because I had a different way to look at the problem of parsing and pretty-printing, more
specifically that I couldn’t imagine them separately.
There are two main research directions that emerge now. The first one is to find a way
to make the definition I found practical. One way that looks very interesting is to find adefinition of functional parsing and pretty-printing, as it can be a very important definition
because it will probably be more practical. Another way of making the definition practicalis the implementation of a tool like yacc. yacc produces a parser based on a given grammar.
It could be interesting to develop a tool that produces both a parser and a pretty-printercorresponding to it at the same time.
Another possible research direction would be to work on the orders used in the definition.
It could prove interesting to see if the definition can be extended to other orders on semantics
than equality to model some functions for whose nature of parser/pretty-printer is disputable.
It would also be interesting to characterize the possible orders on strings without having to relyon the derivation trees as it could lead to a more simple definition.
Finally, I would like to thank everyone who welcomed me and helped me during my stay inJapan: David Nowak for supervising my internship, Philippe Codognet for doing a lot of thepaperwork for my admission at the University of Tokyo, all the members of the Japanese-French
Laboratory for Informatics for their warm welcome, Masami Hagiya, the Dean of the Graduate
School of Information Science and Technology at the University of Tokyo, for officially being
my supervisor and accepting my application to the Graduate School, Kaori Sato from the Officeof International Relations of the Graduate School for her help with the administration at the
University of Tokyo, and anyone else that I may have forgotten.

17

Bibliography[1] Reynald Affeldt, David Nowak, and Yutaka Oiwa. Formal network packet processing withminimal fuss: invertible syntax descriptions at work. In Proceedings of the sixth workshop
on Programming languages meets program verification, PLPV ’12, pages 27–36, New York,NY, USA, 2012. ACM.
[2] Artem Alimarine, Sjaak Smetsers, Arjen van Weelden, Marko van Eekelen, and Rinus
Plasmeijer. There and back again: arrows for invertible programming. In Proceedings ofthe 2005 ACM SIGPLAN workshop on Haskell, Haskell ’05, pages 86–97, New York, NY,
USA, 2005. ACM.
[3] Jay Earley. An efficient context-free parsing algorithm. Commun. ACM, 26(1):57–61,
January 1983.
[4] Dick Grune. Parsing Techniques: A Practical Guide. Springer Publishing Company, Incorporated, 2nd edition, 2010.
[5] John Hughes. The design of a pretty-printing library. In Advanced Functional Programming, First International Spring School on Advanced Functional Programming TechniquesTutorial Text, pages 53–96, London, UK, UK, 1995. Springer-Verlag.
[6] Graham Hutton and Erik Meijer. Monadic Parser Combinators. Technical Report
NOTTCS-TR-96-4, Department of Computer Science, University of Nottingham, 1996.
[7] Eugenio Moggi. Notions of computation and monads. Inf. Comput., 93(1):55–92, July
1991.
[8] Dereck C. Oppen. Pretty-printing. ACM Trans. Program. Lang. Syst., 2(4):465–483, October 1980.
[9] Tillmann Rendel and Klaus Ostermann. Invertible syntax descriptions: unifying parsing
and pretty printing. SIGPLAN Not., 45(11):1–12, September 2010.
[10] Peter Smith. The galois connection between syntax and semantics.
[11] Philip Wadler. Comprehending monads. In Proceedings of the 1990 ACM conference on
LISP and functional programming, LFP ’90, pages 61–78, New York, NY, USA, 1990.
ACM.

18