Structurally Recursive Descent Parsing

Structurally Recursive Descent Parsing
Nils Anders Danielsson and Ulf Norell
Draft, never submitted, 2008. For another, arguably more elegant, approach to total parsing, see Total Parser Combinators. [pdf, highlighted code (does not match the paper exactly)]

Abstract

Recursive descent parsing does not terminate for left recursive grammars. We turn recursive descent parsing into structurally recursive descent parsing, acceptable by total dependently typed languages like Agda, by using the type system to rule out left recursion.

The resulting library retains much of the flavour of ordinary "list of successes" combinator parsers. In particular, the type indices used to rule out left recursion can in many cases be inferred automatically, so that library users do not have to write them out manually.

Update

The paper contains a mistake. In Section 3.2 it is claimed that the second argument to bind cannot have a type in which the parser index depends on the argument, p₂ : (x : R₁) → Parser Tok (i₂ x) R₂. The supposed reason is that x is not known statically. However, given a parser p₁ : Parser Tok i₁ R₁ one can statically compute the list of results which the parser would return if it were applied to the empty string, and when p₁ is combined with p₂ in p₁ >>= p₂ these results are the ones that are needed to instantiate x. A variant of this approach is used to give a general type to bind in Total Parser Combinators.