Type Checking

The Cool type system guarantees at compile time that execution of a program cannot result in runtime type errors. Using the type declarations for identifiers supplied by the programmer, the type checker infers a type for every expression in the program.

It is important to distinguish between the type assigned by the type checker to an expression at compile time, which we shall call the static type of the expression, and the type(s) to which the expression may evaluate during execution, which we shall call the dynamic types.

The distinction between static and dynamic types is needed because the type checker cannot, at compile time, have perfect information about what values will be computed at runtime. Thus, in general, the static and dynamic types may be different. What we require, however, is that the type checker's static types be sound with respect to the dynamic types.

Definition 4.2   For any expression e, let $\tt D_e$ be a dynamic type of e and let $\tt S_e$ be the static type inferred by the type checker. Then the type checker is sound if for all expressions e it is the case that $\tt D_e \leq S_e$.

Put another way, we require that the type checker err on the side of overestimating the type of an expression in those cases where perfect accuracy is not possible. Such a type checker will never accept a program that contains type errors. However, the price paid is that the type checker will reject some programs that would actually execute without runtime errors.