Bidirectional typing

Draft, arXiv:1908.05839 [cs.PL]

Joshua Dunfield and Neelakantan R. Krishnaswami

Abstract

Bidirectional typing combines two modes of typing: type checking, which checks that a program satisfies a known type, and type synthesis, which determines a type from the program. Using checking enables bidirectional typing to break the decidability barrier of Damas–Milner approaches; using synthesis enables bidirectional typing to avoid the large annotation burden of explicitly typed languages. In addition, bidirectional typing improves error locality. We highlight the design principles that underlie bidirectional type systems, survey the development of bidirectional typing from the prehistoric period before Pierce and Turner's local type inference to the present day, and provide guidance for future investigations.

Submitted version (August 2019)

BibTeX entry

  @Unpublished{Dunfield19:bidir-survey,
    author =    {Joshua Dunfield and Neel Krishnaswami},
    title =     {Bidirectional Typing},
    month =     aug,
    year =      {2019},
    note =      {\url{arXiv:1908.05839 [cs.PL]}}
  }
  

all papers
J. Dunfield