We expound a view of type checking as evaluation with `abstract values'. Whereas dynamic semantics, evaluation, deals with (dynamic) values like 0, 1, etc., static semantics, type checking, deals with approximations like int
. A type system is sound if it correctly approximates the dynamic behavior and predicts its outcome: if the static semantics predicts that a term has the type int
, the dynamic evaluation of the term, if it terminates, will yield an integer.
As object language, we will use simply typed and let-polymorphic lambda calculi with constants (integers and integer operations). We will use Haskell as a metalanguage: the language to write evaluators, type checkers, type reconstructors for the object language.
Just as our evaluator avoids the explicit environment in favor of substitutions, our type checker avoids the explicit type environment. This technique is particularly suitable if the object language is represented in higher-order abstract syntax (HOAS).