• L. Thomas van Binsbergen (Speaker)

Activity: Participating in or organising an eventParticipation in workshop, seminar, course


Formal, Executable and Reusable Components for Syntax Specification

Developing a programming language formally is cumbersome and maintaining the language definition as it evolves is tedious and error-prone. But programming languages have syntactic and semantic commonalities that can be captured once and for all, potentially easing the task of developing and maintaining language definitions. Languages often share features, even across paradigms, such as scoping rules, function calls, and control operators. Moreover, some concrete syntaxes share patterns such as repetition with a separator, delimiters around blocks, and the application of prefix and infix operators.

In this talk we contrast two possible routes for capturing syntactic features of languages in a library of reusable components. The components should be executable, so that a syntax definition can be tested as it is being developed, and formal, so that mathematical claims can be made about specifications and the languages being defined.

In the first route, the well-known BNF formalism is extended with a mechanism for abstraction, borrowed from modern programming languages. With the abstraction mechanism, it is possible to define syntactic templates in which certain elements are variable and can be instantiated as needed. Complete syntax specifications are mechanically translated into conventional BNF. The formalism thus inherits all the advantages of conventional BNF: a rich formal theory and generalised parsing technology. An example implementation is found in Happy, the standard parser generator for Haskell.

In the second route, we demonstrate the expressive power of parser combinators. We define parser combinators that satisfy certain combinator laws, allowing us to reason formally about the parsers defined with these combinators. However, care must be taken to avoid non-terminating and inefficient parsers. Several authors have made suggestions to overcome these issues. However, these suggestions significantly complicate the combinator definitions, making it hard to maintain the combinator laws.

We have taken a third route, which is to define *grammar* combinators, simultaneously generating grammars and parsers, effectively implementing the BNF formalism as an embedded DSL. Implemented in Haskell, the the grammar combinators piggyback on Haskell's abstraction mechanism and on Haskell's strong type-system to integrate semantic actions in grammar specifications. The grammar combinators are at the heart of a library of formal, executable and reusable components. With this library, it is possible to apply software design principles like "reuse via abstraction" and "test-driven development" to the development of programming languages.
Period25 May 2018
Event typeWorkshop
Conference number9
LocationBrighton, United KingdomShow on map