Let Arguments Go First

Abstract

Bi-directional type checking has proved to be an extremely useful and versatile tool for type checking and type inference. The conventional presentation of bi-directional type checking consists of two modes: inference mode and checked mode. In traditional bi-directional type-checking, type annotations are used to guide (via the checked mode) the type inference/checking procedure to determine the type of an expression, and type information flows from functions to arguments . This paper presents a variant of bi-directional type checking where the type information flows from arguments to functions . This variant retains the inference mode, but adds a so-called application mode. Such design can remove annotations that basic bi-directional type checking cannot, and is useful when type information from arguments is required to type-check the functions being applied. We present two applications and develop the meta-theory (mostly verified in Coq) of the application mode. These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.