Bidirectional polymorphism through greed and unions

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, 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.