Typechecker

The type checker is in fact a type inference machine that synthesizes missing type information by type unification. It may be (and often is) used as a type-checking automaton when types are (partially) present.

Each expression must specify its own typeCheck(TypeChecker t) method that encodes a formal typing rule of the form:

$$\typerule {\hastype {\Gamma_1}{e_1}{T_1},\;\ldots,\;\hastype {\Gamma_n}{e_n}{T_n}}{\gammahastype {e}{T}}$$ (3.1)

or, in (unconditional) axiom form:

$$\typerule {}{\gammahastype {e}{T}}$$ (3.2)

or (conditional) axiom form:

$$\typerule {c(\Gamma,e,T)}{\gammahastype {e}{T}}$$ (3.3)

where $c(\Gamma,e,T)$ is a boolean condition on typing context $\Gamma$, expression $e$, and type $T$. A typing judgement &Gamma#Gamma;&vdash#vdash;e:T is read as ``under typing context $\Gamma$, expression $e$ has type $T$.'' A type rule or (conditional) axiom is read from the ``denominator'' to the ``numerator.'' For example,

$$\typerule {\gammahastype {c}{\textit{\BOOL }},\; \gammahastype {e... ...t{T}}}<tex2html_comment_mark>107 {\gammahastype {\IfThenElse {c}{e_1}{e_2}}{T}}$$ (3.4)

is read thus: ``the expression $\IfThenElse {c}{e_1}{e_2}$ has type $T$ under typing context $\Gamma$ if the expression $c$ has type boolean under typing context $\Gamma$ and if the expressions $e_1$ and $e_2$ have same type $T$ under typing context $\Gamma$.

In its simplest form, a typing context $\Gamma$ is logical variable substitution: i.e., a mapping from type parameters to types. Since type parameters are also types, we do have to compose substitutions. In the formal presentation of an expression's typing rule, the context keeps the type binding under which the typiung derivation has progressed up to applying the rule in which it occurs.

Hence, we shall treat typing contexts as (composable) substitutions mapping type parameter variables to types. The notation $\Gamma\tsubst{x}{T}$ denotes the context defined from $\Gamma$ by:

$$\Gamma\tsubst{x}{T}(y) = \left\{ \begin{array}{ll} T & \mbox{if $y=x$}; \Gamma(x) & \mbox{otherwise}. \end{array}\right.$$ (3.5)