The has_type relation of the STLC defines what it means for a term to belong to a type (in some context). But it doesn't, by itself, give us an algorithm for checking whether or not a term is well typed. Fortunately, the rules defining has_type are syntax directed -- that is, for every syntactic form of the language, there is just one rule that can be used to give a type to terms of that form. This makes it straightforward to translate the typing rules into clauses of a typechecking function that takes a term and a context and either returns the term's type or else signals that the term is not typable.

Comparing Types

First, we need a function to compare two types for equality...

... and we need to establish the usual two-way connection between the boolean result returned by eqb_ty and the logical proposition that its inputs are equal.

The Typechecker

The typechecker works by walking over the structure of the given term, returning either Some T or None. Each time we make a recursive call to find out the types of the subterms, we need to pattern-match on the results to make sure that they are not None. Also, in the app case, we use pattern matching to extract the left- and right-hand sides of the function's arrow type (and fail if the type of the function is not Arrow T₁₁ T₁₂ for some T₁₁ and T₁₂).

Digression: Improving the Notation

Before we consider the properties of this algorithm, let's write it out again in a cleaner way, using "monadic" notations in the style of Haskell to streamline the plumbing of options. First, we define a notation for composing two potentially failing (i.e., option-returning) computations:

Second, we define return and fail as synonyms for Some and None:

Now we can write the same type-checking function in a more imperative-looking style using these notations.

Properties

To verify that the typechecking algorithm is correct, we show that it is sound and complete for the original has_type relation -- that is, type_check and has_type define the same partial function.