Introduction: To do type checking a compiler needs to assign a type expression to each component of the source program. The compiler must then determine that these type expressions conform to a collection of logical rules that is called the type system for the source language.
Type checking has the potential for catching errors in programs. In principle, any check can be done dynamically, if the target code carries the type of an element along with the value of the element. A sound type system eliminates the need for dynamic checking for type errors, because it allows us to determine statically that these errors cannot occur when the target program runs. An implementation of a language is strongly typed if a compiler guarantees that the programs it accepts will run without type errors. Besides their use for compiling, ideas from type checking have been used to improve the security of systems that allow software modules to be imported and executed. Java programs compile into machine-independent bytecodes that include detailed type information about the operations in the bytecodes. Imported code is checked before it is allowed to execute, to guard against both inadvertent errors and malicious misbehavior.
Rules for Type Checking: Type checking can take on two forms: synthesis and inference. Type synthesisbuilds up the type of an expression from the types of its subexpressions. Itrequires names to be declared before they are used. The type of E\ E2 isdefined in terms of the types of E\ and E2 • A typical rule for type synthesishas the form
if / has type s —>• t a n d x has type s, 00
then expression f(x) has type t
Here, / and x denote expressions, and s ->• t denotes a function from s to t. This rule for functions with one argument carries over to functions with several arguments. The rule (6.8) can be adapted for E\ E2 by viewing it as a function application add (Ei, E2).Q
Type inference determines the type of a language construct from the way it is used. Looking ahead to the examples in Section 6.5.4, let null be a function that tests whether a list is empty. Then, from the usage null(x), we can tell that x must be a list. The type of the elements of x is not known; all we know is that x must be a list of elements of some type that is presently unknown.
Variables representing type expressions allow us to talk about unknown types. We shall use Greek letters a, (3, . . . for type variables in type expressions. A typical rule for type inference has the form
if f(x) is an expression,
then for some a and 0, f has type a —> (3 a n d x has type a
Type inference is needed for languages like ML, which check types, but do not require names to be declared.
“We shall use the term "synthesis" even if some context information is used to determine types. With overloaded functions, where the same name is given to more than one function, the context of E\ E2 may also need to be considered in some languages.
In this section, we consider type checking of expressions. The rules for checking statements are similar to those for expressions. For example, we treat the conditional statement "if (E) S;" as if it were the application of a function if to E and S. Let the special type void denote the absence of a value. Then function if expects to be applied to a boolean and a void; the result of the application is a void.