Total Parser Combinators

Total Parser Combinators
Nils Anders Danielsson
Proceedings of the 15th ACM SIGPLAN international conference on Functional programming (ICFP 2010). © ACM, 2010. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in ICFP'10, http://doi.acm.org/10.1145/1863543.1863585. [pdf, highlighted code, tarball with code, Git repository (includes more recent developments, does not match the tarball)]

Abstract

A monadic parser combinator library which guarantees termination of parsing, while still allowing many forms of left recursion, is described. The library's interface is similar to those of many other parser combinator libraries, with two important 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 dependent types and a combination of induction and coinduction; and the other is that the parser type is unusually informative.

The library comes with a formal semantics, using which it is proved that the parser combinators are as expressive as possible. The implementation is supported by a machine-checked correctness proof.

Erratum

Paul Lickman's master's thesis was produced at Oxford, not Cambridge.