Type Checking Rules

The general form a type checking rule is:

$$\frac{\vdots}{O,M,C \vdash e : T}\eqno\mbox{}$$

The rule should be read: In the type environment for objects $O$, methods $M$, and containing class $C$, the expression $e$ has type $T$. The dots above the horizontal bar stand for other statements about the types of sub-expressions of $e$. These other statements are hypotheses of the rule; if the hypotheses are satisfied, then the statement below the bar is true. In the conclusion, the ``turnstile'' (``$\vdash$'') separates context ($O,M,C$) from statement ($e : T$).

The rule for object identifiers is simply that if the environment assigns an identifier $Id$ type $T$, then $Id$ has type $T$.

$$\frac{O(Id) = T}{O,M,C \vdash Id : T}\eqno\mbox{[Var]}$$

The rule for assignment to a variable is more complex:

$$\frac{\begin{array}{l} O(Id) = T \\ O,M,C \vdash e_1 : T'... ...ray}}{O,M,C \vdash Id \leftarrow e_1 : T'}\eqno\mbox{[ASSIGN]}$$

Note that this type rule--as well as others--use the conformance relation $\leq$ (see Section 3.2). The rule says that the assigned expression $e_1$ must have a type $T'$ that conforms to the type $T$ of the identifier $Id$ in the type environment. The type of the whole expression is $T'$.

The type rules for constants are all easy:

$$\frac{}{O,M,C \vdash true : Bool}\eqno\mbox{[True]}$$

$$\frac{}{O,M,C \vdash false : Bool}\eqno\mbox{[False]}$$

$$\frac{i \mbox {\ is an integer constant}}{O,M,C \vdash i : Int}\eqno\mbox{[Int]}$$

$$\frac{s \mbox {\ is a string constant}}{O,M,C \vdash s : String}\eqno\mbox{[String]}$$

There are two cases for new, one for new SELF_TYPE and one for any other form:

$$\frac{ T' = \left\{ \begin{array}{rl} {\tt SELF\_TYPE}_C &... ...\end{array} \right.}{O,M,C \vdash new\ T: T'}\eqno\mbox{[New]}$$

Dispatch expressions are the most complex to type check.

$$\frac{ \begin{array}{l} O,M,C \vdash e_0 : T_0 \\ O,M,C \vd... ... \vdash e_0.f(e_1,\ldots,e_n) : T_{n+1}}\eqno\mbox{[Dispatch]}$$

$$\frac{ \begin{array}{l} O,M,C \vdash e_0 : T_0 \\ O,M,C \vd... ...e_0@T.f(e_1,\ldots,e_n) : T_{n+1}}\eqno\mbox{[StaticDispatch]}$$

To type check a dispatch, each of the subexpressions must first be type checked. The type $T_0$ of $e_0$ determines which declaration of the method $f$ is used. The argument types of the dispatch must conform to the declared argument types. Note that the type of the result of the dispatch is either the declared return type or $T_0$ in the case that the declared return type is $\tt SELF\_TYPE$. The only difference in type checking a static dispatch is that the class $T$ of the method $f$ is given in the dispatch, and the type $T_0$ must conform to $T$.

The type checking rules for if and {-} expressions are straightforward. See Section 7.5 for the definition of the $\sqcup$ operation.

$$\frac{ \begin{array}{l} O,M,C \vdash e_1 : Bool \\ O,M,C \v... ...box { else } e_3 \mbox { fi} : T_2 \sqcup T_3}\eqno\mbox{[If]}$$

$$\frac{ \begin{array}{l} O,M,C \vdash e_1 : T_1 \\ O,M,C \vd... ...e_1; e_2; \ldots e_n; \mbox { \}} : T_n}\eqno\mbox{[Sequence]}$$

The let rule has some interesting aspects.

$$\frac{ \begin{array}{l} T_0' = \left\{ \begin{array}{rl} {... ...0 \leftarrow e_1 \mbox { in } e_2 : T_2}\eqno\mbox{[Let-Init]}$$

First, the initialization $e_1$ is type checked in an environment without a new definition for $x$. Thus, the variable $x$ cannot be used in $e_1$ unless it already has a definition in an outer scope. Second, the body $e_2$ is type checked in the environment $O$ extended with the typing $x:T_0'$. Third, note that the type of $x$ may be SELF_TYPE.

$$\frac{ \begin{array}{l} T_0' = \left\{ \begin{array}{rl} {... ...let } x : T_0 \mbox { in } e_1 : T_1}\eqno\mbox{[Let-No-Init]}$$

The rule for let with no initialization simply omits the conformance requirement. We give type rules only for a let with a single variable. Typing a multiple let

$$\rm let\ x_1 : T_1\ [\leftarrow e_1],\ x_2: T_2\ [\leftarrow e2], \ldots,\ x_n :T_n\ [\leftarrow e_n]\ in\ e\$$

is defined to be the same as typing

$$\rm let\ x_1 : T_1\ [\leftarrow e_1]\ in\ (let\ x_2 :T_2\ [\leftarrow e_2],\ldots,\ x_n : T_n\ [\leftarrow e_n]\ in\ e\ )\$$

$$\frac{ \begin{array}{l} O,M,C \vdash e_0 : T_0 \\ O[T_1/x_1... ...{ esac} : \bigsqcup_{1 \leq i \leq n} T_i'}\eqno\mbox{[Case]}$$

Each branch of a case is type checked in an environment where variable $x_i$ has type $T_i$. The type of the entire case is the join of the types of its branches. The variables declared on each branch of a case must all have distinct types.

$$\frac{ \begin{array}{l} O,M,C \vdash e_1 : Bool \\ O,M,C \v... ...1 \mbox { loop } e_2 \mbox { pool} : Object}\eqno\mbox{[Loop]}$$

The predicate of a loop must have type $Bool$; the type of the entire loop is always $Object$. An isvoid test has type $Bool$:

$$\frac{O,M,C \vdash e_1 : T_1}{O,M,C \vdash \mbox {isvoid } e_1 : Bool}\eqno\mbox{[Isvoid]}$$

With the exception of the rule for equality, the type checking rules for the primitive logical and arithmetic operations are easy.

$$\frac{ O,M,C \vdash e_1 : Bool}{O,M,C \vdash \neg e_1 : Bool}\eqno\mbox{[Not]}$$

$$\frac{ O,M,C \vdash e_1 : Int}{O,M,C \vdash \mbox{\~{}} e_1 : Int}\eqno\mbox{[Neg]}$$

$$\frac{ \begin{array}{l} O,M,C \vdash e_1 : Int \\ O,M,C \vd... ...nd{array}}{O,M,C \vdash e_1\ op\ e_2 : Int}\eqno\mbox{[Arith]}$$

The wrinkle in the rule for equality is that any types may be freely compared except Int, String and Bool, which may only be compared with objects of the same type. The cases for < and <= are similar to the rule for equality.

$$\frac{ \begin{array}{l} O,M,C \vdash e_1 : T_1 \\ O,M,C \vd... ...\end{array}}{O,M,C \vdash e_1 = e_2 : Bool}\eqno\mbox{[Equal]}$$

The final cases are type checking rules for attributes and methods. For a class $C$, let the object environment $O_C$ give the types of all attributes of $C$ (including any inherited attributes). More formally, if $x$ is an attribute (inherited or not) of $C$, and the declaration of $x$ is $x:T$, then

$$O_C(x) = \left\{ \begin{array}{rl} {\tt SELF\_TYPE}_C & \mb... ...ELF\_TYPE} \\ T & \mbox {\rm otherwise} \end{array} \right.$$

The method environment $M$ is global to the entire program and defines for every class $C$ the signatures of all of the methods of $C$ (including any inherited methods).

The two rules for type checking attribute defininitions are similar the rules for let. The essential difference is that attributes are visible within their initialization expressions. Note that self is bound in the initialization.

$$\frac{ \begin{array}{l} O_C(x) = T_0 \\ O_C[{\tt SELF\_TYPE... ...O_C,M,C \vdash x : T_0 \leftarrow e_1;}\eqno\mbox{[Attr-Init]}$$

$$\frac{O_C(x) = T}{O_C,M,C \vdash x : T;}\eqno\mbox{[Attr-No-Init]}$$

The rule for typing methods checks the body of the method in an environment where $O_C$ is extended with bindings for the formal parameters and self. The type of the method body must conform to the declared return type.

$$\frac{ \begin{array}{l} M(C,f) = (T_1,\ldots,T_n,T_0) \\ O_... ...n:T_n) : T_0 \mbox { \{ } e \mbox { \}; }}\eqno\mbox{[Method]}$$