Complete and easy bidirectional typechecking for higher-rank polymorphism

ICFP 2013 (Boston, September 2013); arXiv:1306.6032 [cs.PL]

Jana Dunfield and Neelakantan R. Krishnaswami


Bidirectional typechecking, in which terms either synthesize a type or are checked against a known type, has become popular for its scalability (unlike Damas-Milner type inference, bidirectional typing remains decidable even for very expressive type systems), its error reporting, and its relative ease of implementation. Following design principles from proof theory, bidirectional typing can be applied to many type constructs. The principles underlying a bidirectional approach to polymorphism, however, are less obvious. We give a declarative, bidirectional account of higher-rank polymorphism, grounded in proof theory; this calculus enjoys many properties such as η-reduction and predictability of annotations. We give an algorithm for implementing the declarative system; our algorithm is remarkably simple and well-behaved, despite being both sound and complete.

Reader’s guide

This paper is descended from Greedy Bidirectional Polymorphism, but is much better: the algorithm is different and simpler, the metatheory is different and cleaner, and the proofs actually work.

(Objective evidence that it's simpler: the algorithm has been implemented by at least two different people, with no assistance from the authors. See Neel's blog post, and a post by Ben Lippmeier.)

Conference slides

Final version (June 2013)

BibTeX entry

    author =    {Jana Dunfield and Neelakantan R. Krishnaswami},
    title =     {Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism},
    booktitle = {Int'l Conf. Functional Programming},
    month =     sep,
    year =      {2013},
    note =      {\url{arXiv:1306.6032 [cs.PL]}}

all papers * related papers
J. Dunfield