Structurally Recursive Descent Parsing

Structurally Recursive Descent Parsing
Logic and Semantics Seminar, Cambridge, 2009-03-20. [pdf]

Abstract

Parser combinators provide an elegant method for writing executable specifications of grammars. Implementations of parser combinators using recursive descent have a problem, though: if the specified grammar is left recursive, then parsing fails to terminate.

We address this problem by defining a type of grammars without left recursion. The type is defined using a mixture of induction and coinduction, in order to avoid left recursion (induction) but still allow the definition of cyclic grammars (coinduction). Dependent types ensure that coinduction is only used in positions where a token will have been consumed. Parsing can then be implemented using recursion over the structure of a grammar's inductive part and a bound on the input string's length.

On top of this type we have implemented a library of parser combinators which retains much of the flavour of ordinary "list of successes" combinator parsers. The library is implemented in the total dependently typed functional language Agda.

This is joint work with Ulf Norell.