Bidirectional Polymorphism Through Greed and Unions

Unpublished manuscript

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

Older draft submitted to ICFP (March 2009)

BibTeX entry

  @Unpublished{Dunfield09:polymorphism-unionsDRAFT,
    author =    {Joshua Dunfield},
    title =     {Bidirectional Polymorphism Through Greed and Unions},
    month =     apr,
    year =      2009,
    note =      {\url{http://www.cs.cmu.edu/~joshuad/papers/polyunions/}}
  }
  

all papers * related papers
Joshua Dunfield