AbstractBidirectional 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 guideThis 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. |
@InProceedings{Dunfield09:polymorphism,
author = {Joshua Dunfield},
title = {Greedy Bidirectional Polymorphism},
booktitle = {ML Workshop (ML '09)},
pages = {15--26},
month = aug,
year = 2009,
note = {\url{http://www.cs.cmu.edu/~joshuad/papers/poly/}}
}