Formal, Executable and Reusable Components
for Syntax Specification
L. Thomas van Binsbergenltvanbinsbergen@acm.org
http://hackage.haskell.org/package/gll
Royal Holloway, University of London

25 May, 2018

Observation 1
Semantically different constructs sometimes have identical syntax.
For example, variable and parameter declarations.
class Coordinate (val x : Int = 0, val y : Int = 0)val someVal : String = "Royal Wedding"

The parameter and variable declarations follow the pattern:(“val” or “var”) identifier ‘:’ type ‘=’ expression

Observation 1
Semantically different constructs sometimes have identical syntax.
For example, variable and parameter declarations.
class Coordinate (val x : Int = 0, val y : Int = 0)val someVal : String = "Royal Wedding"

The parameter and variable declarations follow the pattern:(“val” or “var”) identifier ‘:’ type ‘=’ expression
var decl ::= var key ID ’:’ TYPE opt expr
var key ::= "val" | "var"opt expr ::= expr | expr::= ...

Observation 2
Different constructs of a language may have similar syntax.
For example, a parameter list and an argument list.
class Coordinate (val x : Int = 0, val y : Int = 0)
new Coordinate (4,2);

Observation 2
Different constructs of a language may have similar syntax.
For example, a parameter list and an argument list.
class Coordinate (val x : Int = 0, val y : Int = 0)
new Coordinate (4,2);

param list::= ’(’ multiple params ’)’multiple params ::=  | var decl multiple params 0
multiple params 0 ::=  | ’,’ var decl multiple params 0::= ’(’ multiple exprs ’)’args list
multiple exprs ::=  | expr multiple exprs 0
multiple exprs 0 ::=  | ’,’ expr multiple exprs 0

Observation 3

Programming languages often have syntax in common.
For example, if-then-else, or “assignment” to a variable using ‘=’.
However, there are often subtle differences:---- JAVA ---if (i < y) {System.out.println(...);} else {arr[i] = myObj.getField();}---- HASKELL ---if (i < y)then i+1
else let {f x = x + i;g x = x + 2}
in ...GoalTechniques for reuse within and between syntax specifications.
formal: We should be able to make mathematical claims about
the defined languages, and support these claims by proofs
executable: A parser for the language is mechanically derivable
Motivation
Simplify the process of defining syntax by reusing aspects oflanguage itself as well as from other languages
Rapid prototyping
Apply test-driven development in language design
Syntax comparison based on specification (a.o.t. examples)BNF (Backus-Naur Form)var decl ::= var key ID ’:’ TYPE opt exprvar key ::= "val" | "var"opt expr ::= expr | Formal
A BNF specification captures context-free grammars directly.
A string is derived from a nonterminal according to productions:
var_decl=> var_key ID ’:’ TYPE opt_expr=> var_key ID ’:’ TYPE => "val" ID ’:’ TYPE

Executable
Generalised parsing, O(n3 ) parsers for all grammars:
Earley (1970), GLR (1985), GLL (2010/2013)

BNF (Backus-Naur Form)var decl ::= var key ID ’:’ TYPE opt expr
var key ::= "val" | "var"opt expr ::= expr | Formal
A BNF specification captures context-free grammars directly.
A string is derived from a nonterminal according to productions:
var_decl=> var_key ID ’:’ TYPE opt_expr=> var_key ID ’:’ TYPE => val x : Int

Executable
Generalised parsing, O(n3 ) parsers for all grammars:
Earley (1970), GLR (1985), GLL (2010/2013)

Extended BNF (EBNF)
Extensions to BNF capture common patterns.
var decl::= ("val" | "var") ID ’:’ TYPE expr ?

param list ::= ’(’ {var decl ’,’} ’)’’)’
args list ::= ’(’ {expr ’,’}The extensions either generate underlying BNF,
or are associated with implicit production rules:(a | b) => a(a | b) => b{a b}=>{a b}=> a b a{a b}=> a b a b a...
What if the provided extensions are not sufficient?

Parameterised BNF (PBNF)
Parameterised non-terminals enable user-defined extensions:var decl::= either ("val", "var") ID ’:’ TYPE maybe(expr )either (a, b)
maybe(a)::= a | b::= a | param list
args list
tuple(a)::= tuple(var decl)::= tuple(expr )::= ’(’ sepBy (a, ’,’) ’)’sepBy (a, b) ::=  | sepBy1 (a, b)
sepBy1 (a, b) ::= a | a b sepBy1 (a, b)

A simple algorithm transforms such specifications into BNF.
This algorithm fails to terminate when there is no “fixed point”.

PBNF - algorithm

Algorithm
Copy all nonterminals without parameters; add their rules
While there is a right-hand side application f (a1 , . . . , an ):Generate nonterminal fa1 ,...,an , if necessary, and if so‘Instantiate’ the alternates for f and add to fa1 ,...,anReplace application with fa1 ,...,anPBNF - algorithm
Algorithm
Copy all nonterminals without parameters; add their rules
While there is a right-hand side application f (a1 , . . . , an ):Generate nonterminal fa1 ,...,an , if necessary, and if so‘Instantiate’ the alternates for f and add to fa1 ,...,anReplace application with fa1 ,...,anvar decl
either (a, b)
maybe(a)::= either ("val", "var") ID ’:’ TYPE maybe(expr )::= a | b::= a | 

PBNF - algorithm
Algorithm
Copy all nonterminals without parameters; add their rules
While there is a right-hand side application f (a1 , . . . , an ):Generate nonterminal fa1 ,...,an , if necessary, and if so‘Instantiate’ the alternates for f and add to fa1 ,...,anReplace application with fa1 ,...,anvar decl
either (a, b)
maybe(a)::= either ("val", "var") ID ’:’ TYPE maybe(expr )::= a | b::= a | var decl::= either "val","var" ID ’:’ TYPE maybe expr
either "val","var" ::= "val" | "var"maybe expr::= expr | 

PBNF - algorithm

Fails to terminate when arguments are ‘growing’:
scales(a)parens(a)::= a | a scales(parens(a))::= ’(’ a ’)’PBNF - algorithm

Fails to terminate when arguments are ‘growing’:
scales(a)parens(a)::= a | a scales(parens(a))::= ’(’ a ’)’scales ’a’::= ’a’ | ’a’ scales parens ’a’scales parens ’a’::= parens ’a’ | parens ’a’ scales parens parens ’a’...
parens ’a’::= ’(’ a ’)’parens parens ’a’::= ’(’ parens ’a’ ’)’parens parens parens ::= ’(’ parens parens ’a’ ’)’’a’...

Overview
BNF route
EBNF
BNF

Generalised parsing
PBNF
expressivity

formality
Parser combinator routeHO-functions
expressivity

Parsercombinators

Languages L?
Combinator lawsformality

The Parser Combinator Approach

A parse function p takes an input string I and an index k andreturns indices r ∈ p(I , k) if p recognises string Ik,r({k + 1}
tm(x)(I , k) =∅if Ik = xotherwise

For example, tm(x) is a parse function recognising Ik,k+1 for all I
and k with Ik = x

The Parser Combinator Approach
Parsers are formed by combining parse functions with combinators:seq(p, q)(I , k) = {r | r 0 ∈ p(I , k), r ∈ q(I , r 0 )}alt(p, q)(I , k) = p(I , k) ∪ q(I , k)
succeeds(I , k) = {k}fails(I , k) = ∅Parse function p recognises string I if |I | ∈ p(I , 0)
(true if |I | ∈ p(I , 0)
recognise(p)(I ) =false otherwise

Example parsers

parens(p) = seq(tm(’(’), seq(p, tm(’)’)))
sepBy1 (p, s) = alt(p, seq(p, seq(s, sepBy1 (p, s))))Parse function parens(sepBy1 (tm(’a’), tm(’,’))) recognises:{"(a)", "(a,a)", "(a,a,a)", . . .}scales(p) = alt(p, seq(p, scales(parens(p))))Parse function scales(tm(’a’)) recognises:{"a", "a(a)", "a(a)((a))", "a(a)((a))(((a)))", . . .}Formal reasoning I - Languages
What is the language recognised by a parse function?
L(p) = {I | I ∈ W ∗ , recognise(p)(I )}How about a constructive definition?
L(tm(x)) = {x}L(seq(p, q)) = {αβ | α ∈ L(p), β ∈ L(q)}L(alt(p, q)) = L(p) ∪ L(q)L(succeeds) = {}L(fails) = ∅Can be used to attempt proofs of the form: L(p) = L(q)Formal reasoning II - Equalities
The combinators are defined such that the following laws hold:alt(fails, q) = q
alt(p, fails) = palt(p, p) = palt(p, q) = alt(q, p)alt(p, alt(q, r )) = alt(alt(p, q), r )seq(succeeds, q) = q
seq(p, succeeds) = p
seq(fails, q) = fails
seq(p, fails) = fails
seq(p, seq(q, r )) = seq(seq(p, q), r )Formal reasoning II - Equalities

We can also prove distributivity of seq over alt
seq(p, alt(q, r )) = alt(seq(p, q), seq(p, r ))seq(alt(p, q), r ) = alt(seq(p, r ), seq(q, r ))The first law can be used to ‘refactor’ the definition of sepBy1
sepBy1 (p, s) = alt(p, seq(p, seq(s, sepBy1 (p, s))))= alt(seq(p, succeeds), seq(p, seq(s, sepBy1 (p, s))))= seq(p, alt(succeeds, seq(s, sepBy1 (p, s))))Problems
In practice, many more combinators are provided
eof (p)(I , k) = {k | k = |I |}L(eof (p)) = {} or ∅ ??
In practice, parsers produce a single result, or a list of results
Common variations of alt and seq do not have the same laws(p(I , k)alt(p, q)(I , k) =q(I , k)if p(I , k) 6= ∅otherwise

Parsers often require refactoring for efficiency (backtracking)or even termination (left-recursion)
Generalisations complicate combinators definitions

A third route: Grammar Combinators (Embedded BNF)
FormalCombinator expressions produce grammar objects.
The usual notions of productions and derivations apply.
ExecutableGrammars given to stand-alone parsing procedure. (Ljunglöf 2002)
So-called “semantic actions” can be integrated.
(Ridge 2014)

A third route: Grammar Combinators (Embedded BNF)
FormalCombinator expressions produce grammar objects.
The usual notions of productions and derivations apply.
Executable
Grammars given to stand-alone parsing procedure. (Ljunglöf 2002)
So-called “semantic actions” can be integrated.
(Ridge 2014)+ Rich abstraction mechanism provided by the host language+ Borrows host language’s module-system, type-system, etc.
+ Generalised parsing techniques available

A third route: Grammar Combinators (Embedded BNF)
FormalCombinator expressions produce grammar objects.
The usual notions of productions and derivations apply.
Executable
Grammars given to stand-alone parsing procedure. (Ljunglöf 2002)
So-called “semantic actions” can be integrated.
(Ridge 2014)+ Rich abstraction mechanism provided by the host language+ Borrows host language’s module-system, type-system, etc.
+ Generalised parsing techniques available− Not as flexible and expressive as parser combinators− Inherently restricted to (context-free) grammars(The types of grammars accepted by the parsing procedure.)− Static computation requires meta-programming (lookahead)

Conclusion

We saw three methods for achieving reuse in syntax specifications:
PBNF
Parser combinatorsGrammar combinators
PBNF is formal and executable, but restricted to BNF.
Parser combinators offer tremendous power and flexibility.
However, formality and expressivity are at odds.
Grammar combinators implement BNF with the benefits of EDSLs:
abstraction (PBNF), user-extensible, static type-checking, etc.

Formal, Executable and Reusable Components
for Syntax Specification
L. Thomas van Binsbergenltvanbinsbergen@acm.org
http://hackage.haskell.org/package/gll
Royal Holloway, University of London

25 May, 2018