Type Environments

To a first approximation, type checking in Cool can be thought of as a bottom-up algorithm: the type of an expression $e$ is computed from the (previously computed) types of $e$'s subexpressions. For example, an integer 1 has type Int; there are no subexpressions in this case. As another example, if $\tt e_n$ has type $\tt X$, then the expression $\tt\mbox {\tt\{}\ e_1; \ldots; e_n;\ \mbox {\tt\}}$ has type $\tt X$.

A complication arises in the case of an expression $\tt v$, where $\tt v$ is an object identifier. It is not possible to say what the type of $\tt v$ is in a strictly bottom-up algorithm; we need to know the type declared for $\tt v$ in the larger expression. Such a declaration must exist for every object identifier in valid Cool programs.

To capture information about the types of identifiers, we use a type environment. The environment consists of three parts: a method environment $M$, an object environment $O$, and the name of the current class in which the expression appears. The method environment and object environment are both functions (also called mappings). The object environment is a function of the form

$$O(v) = T$$

which assigns the type $T$ to object identifier $v$. The method environment is more complex; it is a function of the form

$$M(C,f) = (T_1,\ldots,T_{n-1},T_n)$$

where $C$ is a class name (a type), $f$ is a method name, and $t_1,\ldots,t_n$ are types. The tuple of types is the signature of the method. The interpretation of signatures is that in class $C$ the method $f$ has formal parameters of types $(t_1,\ldots,t_{n-1})$--in that order--and a return type $t_n$.

Two mappings are required instead of one because object names and method names do not clash--i.e., there may be a method and an object identifier of the same name.

The third component of the type environment is the name of the current class, which is needed for type rules involving SELF_TYPE.

Every expression $e$ is type checked in a type environment; the subexpressions of $e$ may be type checked in the same environment or, if $e$ introduces a new object identifier, in a modified environment. For example, consider the expression

  let c : Int <- 33 in
    ...

The let expression introduces a new variable c with type Int. Let $O$ be the object component of the type environment for the let. Then the body of the let is type checked in the object type environment

$$O[Int/c]$$

where the notation $O[T/c]$ is defined as follows:

$$\begin{eqnarray*} O[T/c](c) & = & T \\ O[T/c](d) & = & O(d)\ \ \mbox {\rm if\ }d \neq c \end{eqnarray*}$$