  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 support features for which inference is undecidable; 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.
