TypecheckingA Typechecker for STLC

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, tell us how to check whether or not a term is well typed. Fortunately, the rules defining has_type are syntax directed — they exactly follow the shape of the term. 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. This short chapter constructs such a function and proves it correct.

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 beq_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 tapp 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 TArrow T₁₁ T₁₂ for some T₁ and T₂).

Properties

To verify that this 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.