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, even in the presence of
subtyping. The first contribution is a bidirectional type system that supports
first-class (higher-rank and impredicative) polymorphism but is complete for predicative
polymorphism (including ML-style polymorphism and higher-rank polymorphism). This power
comes from bidirectionality combined with a "greedy" method of finding polymorphic
instances inspired by Cardelli's early work on System F<:.
The second contribution adds subtyping; combining bidirectional typechecking with
intersection and union types fortuitously yields a simple but rather powerful system.
Finally, I present a more powerful algorithm that forms intersections and unions
automatically. This paper demonstrates that bidirectionality is a strong foundation
for traditionally vexing features like first-class polymorphism and subtyping.
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;
a later draft omits union and intersection types to focus on
the first-class polymorphic aspects.
Draft of 2009-04-07, with minor corrections to submitted version