Greedy bidirectional polymorphism

ML Workshop '09 (Edinburgh, Aug. 2009)

Jana Dunfield

Abstract

Bidirectional typechecking has become popular in advanced type systems because it works in many situations where inference is undecidable. In this paper, I show how to cleanly handle parametric polymorphism in a bidirectional setting. The key contribution is a bidirectional type system for a subset of ML that supports first-class (higher-rank and even impredicative) polymorphism, and is complete for predicative polymorphism (including ML-style polymorphism and higher-rank polymorphism). The system's power comes from bidirectionality combined with a "greedy" method of finding polymorphic instances inspired by Cardelli's early work on System F_<:. This work demonstrates that bidirectionality is a good foundation for traditionally vexing features like first-class polymorphism.

Reader’s guide
This paper develops an idea noted as future work in my dissertation ("Be greedy", pp. 236-238). (The application to first-class polymorphism was unexpected.)
An earlier draft encompasses this work and several related systems with intersection and union types.

warning sign Important: Two of the proofs in this paper are wrong:
Completeness is false (the case for unit omits the subcase where the existential variable is unsolved), but (I think) fixable by adding a rule corresponding to →Iα̂.

Decidability could hold, but the given proof is utterly wrong: the so-called induction measure is not even transitive!
Correct (to the best of our knowledge) proofs for a system in the same spirit, but simpler and better, can be found with "Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism".

Workshop version (June 2009)

BibTeX entry

  @InProceedings{Dunfield09:polymorphism,
    author =    {Jana Dunfield},
    title =     {Greedy Bidirectional Polymorphism},
    booktitle = {ML Workshop (ML '09)},
    pages =     {15--26},
    month =     aug,
    year =      2009,
    note =      {\url{http://www.cs.queensu.ca/~jana/papers/poly/}}
  }

all papers * related papers

J. Dunfield