Parser combinators are one of the best-known examples of the advantages of functional programming, as they make essential use of functions as arguments and results of functions. They are also one of the longest standing examples, going back to Burge’s groundbreaking 1975 work [1]. In this model, parsers are represented as functions, which partially consume input streams and return parse trees. Parser combinators directly represent grammar operations like alternation, repetition, and sequencing; complex parsers are built by applying these combinators to simpler ones, generally in a recursive definition. With recursion comes the possibility--indeed probability--of nontermination.

Dependent types have come into functional programming from constructive mathematics, particularly from the work of Per Martin-L¿f, which also began in the 1970s. Dependent types are types that depend on values, and this simple mechanism establishes a correspondence between types and logical predicates, and between the values those types contain and proofs of the predicates. Dependent types thus have the power to express constraints far more fine grained than traditional type systems. For the programming-logic correspondence to work properly, the logic needs to be consistent: that is, not everything should be provable. To do this, general recursion needs to be banned, and only terminating forms of recursion and co-recursion can be permitted; this is precisely what the Agda language, in which the work of this paper is implemented, supports.

Terminating recursion is straightforward: progress towards termination can be measured by the arguments shrinking. Co-recursion is less familiar, and is dual to recursion: instead of consuming arguments, co-recursion generates results, and for co-recursion to be acceptable, it needs to be “productive”; that is, co-recursively defined objects, like infinite lists, need to be unfoldable indefinitely.

There are several contributions of this paper. First, it gives an implementation of parser combinators in a total language, in a way that supports left recursion. For this to work, it is essential that certain parsers must not accept the empty string, and this constraint can be expressed in dependent types (it’s a simple predicate, after all). More generally, it gives a tutorial example in combining recursion--for grammatical structure--and co-recursion--for controlled recursive grammar definitions. The author concludes the paper with a persuasive argument that this approach gives a framework for understanding the behavior of lazy programming in languages like Haskell, where recursion and co-recursion overlap.

This well-written paper contains a particularly useful survey of related work right at the start, helping to contextualize the contribution. It should be essential reading for anyone interested in parsing and advances in dependently typed functional programming.