Structurally Recursive Descent Parsing

Structurally Recursive Descent Parsing
Dependently Typed Programming 2008, Nottingham, 2008-02-18. [pdf, pdf (n-up)]

Abstract

Parser combinators provide a high-level approach to parsing, and we would like to make use of this method in Agda. However, when using parser combinators the cyclic nature of many grammars is reflected as cyclic code, which is rejected by Agda and other languages which require code to be structurally recursive. Furthermore the use of left recursive grammars leads to non-termination with many implementations of parser combinators.

We get around these problems by using a more explicit representation of grammars and by using the type system to statically disallow left recursion. This is done in such a way that most of the flavour of ordinary parser combinators is retained. For instance, users can still define parameterised parsers. Furthermore the type indices used to rule out left recursion can in many cases be inferred automatically by Agda.