## Structurally Recursive Descent ParsingStructurally Recursive Descent Parsing ## AbstractRecursive 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. ## UpdateThe 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, Last updated Thu Dec 16 01:28:58 UTC 2010. |