Total Parser Combinators

Total Parser Combinators
MGS Christmas Seminars 2009, Sheffield, 2009-12-15. For more information, see Total Parser Combinators. [pdf]

Abstract

Parser combinators provide an elegant method for implementing parsers. However, most parser combinator libraries fail to guarantee that parsing will terminate. I will talk about a library which provides such a guarantee.

The library's interface is similar to that of many other parser combinator libraries, with three main differences: one is that the interface clearly specifies which parts of the constructed parsers may be infinite, and which parts have to be finite, using a combination of induction and coinduction; another is that the interface allows many forms of left recursion; and the last is that the parser type is unusually informative. The parser combinators come with a formal semantics, and are as expressive as possible: every language which can be decided by the host language can also be decided using the combinators.