Strict Bidirectional Type Checking

Adam Chlipala, Leaf Petersen, Robert Harper. Strict Bidirectional Type Checking. Proceedings of the 2nd ACM SIGPLAN Workshop on Types in Language Design and Implementation (TLDI'05). January 2005.

Paper as PDF, Paper as PS

Completely annotated lambda terms (such as are arrived at via the straightforward encodings of various types from System F) contain much redundant type information. Consequently, the completely annotated forms are almost never used in practice, since partially annotated forms can be defined which still allow syntax directed typechecking. An additional optimization that is used in some proof and type systems is to take advantage of the context of occurrence of terms to further elide type information using bi-directional typechecking rules. While this technique is generally effective, we show that there exist bi-directional terms which exhibit asymptotic increases in the size of their type decorations when sequentialized into a named-form calculus (a common first step in compilation). In this paper, we introduce a refinement of the bi-directional type system based on strict logic which allows additional type decorations to be eliminated, and show that it is well-behaved under sequentialization.