3.7 Type Checking Expressions, Statements, and Declarations

Type checking an expression or statement determines whether it is type-correct, and if type-correct also determines the type of its result. Type checking a declaration simply checks for type correctness. All constructs are type-checked in a typing context containing the following information:

a binding for each variable or object name in scope to either:
- the variable's declared type and an indication of whether the variable binding is assignable or constant, or
- to an object with a role annotation and a set of conformed-to types.
the set of inheritance relations currently in scope;
a binding for each type name in scope to the corresponding type;
the set of subtyping relations currently in scope;
the set of signatures currently in scope (for type checking messages);
the set of method declarations currently in scope (for type checking resends).

The type checking rules for expressions are as follows:

A literal constant is always type-correct. The type of the result of a literal constant is the corresponding predefined type.
A reference name is type-correct iff name is defined in the typing context (i.e., if there exists a declaration of that name earlier in the same scope or in a lexically-enclosing scope) as either a variable or an object. If a variable, then the reference is type-correct, with the type of the result being the associated type of the variable in the typing context. If an object, then the reference is type-correct iff the object is a concrete or dynamic object, with the type of the result being the type of the named object.
An object constructor expression of the general form

	role-annotation object inherits parent1, ..., parentK
	                  subtypes supertype1, ..., supertypeL
	                  isa parent-and-supertype1, ..., parent-and-supertypeM
	                  { field1@obj1 := expr1, ..., fieldN@objN := exprN }

is type-correct iff:
- each parenti name is bound to a non-abstract non-void object in the typing context;
- each supertypei notates a type other than none in the current typing context;
- each parent-and-supertypej name is bound to a non-abstract non-void object in the typing context;
- if @obji is present, then obji names an ancestor of the newly created object (if absent, it is considered to be the same as the newly created object);
- each fieldi names a field Fi specialized on or inherited unambiguously by obji, ignoring any overriding methods, and Fi is not shared;
- each expri is type-correct, returning an object of static type Ti, and Ti is a subtype of the type of the contents of the field Fi;
- no field Fi is initialized more than once;
- role-annotation is neither abstract nor template; and
- if role-annotation is concrete, then there do not exist any fields specialized on or inherited by the newly created object that do not have a default initial value and are not initialized as part of the object creation expression.
The representation keyword may be used in place of the object keyword without effect. The type of the result of an object constructor expression is a new anonymous type that is a subtype of each of the supertype_i types and each of the types of the parent-and-supertype_j objects.
A closure constructor expression of the general form

	&(x1:type1, ..., xN:typeN):typeR { body }

is type-correct iff:
- the xi, where provided, are distinct;
- each of the typei, if provided, notates a non-void type in the current typing context;
- typeR, if provided, notates a type in the current typing context;
- body is type-correct, checked in a typing context constructed by extending the current typing context with constant variable bindings for each of the xi to the corresponding type typei; and
- the type of the result of body is a subtype of typeR, if provided; if :typeR is omitted, then typeR is inferred to be the type of the result of body.
The type of the result of a closure constructor expression of the above form is

	&(type1, ..., typeN):typeR.

A vector constructor expression of the general form [expr1,...,exprN] type-correct iff each of the expri is type-correct, with static type Ti which is not void. The type of the result of a vector constructor expression is the predefined parameterized type i_vector instantiated with the least upper bound of the Ti. (See section 4 for information on parameterized types.)
A message expression of the general form name(expr1, ..., exprN) is type-correct iff:
- each of the expr_i is type-correct, with static type T_i which is not void;[13] and
- the set S = {S₁, ..., S_M} of applicable signatures is non-empty, where S is the set of signatures in the current typing context of the form S_i = signature name(ti1, ..., tiN):tiR where each T_i is a subtype of ti.
The type of the result of a message is the greatest lower bound of each of the result types tiR of the applicable signatures. Verifying correctness of the implementation of signatures is described in subsection 3.6.2.
A resend expression of the general form

	resend(..., xi@parenti, ..., exprj, ...)

is type-correct iff:
- each of the arguments x_i or expr_i is type-correct, with static type Ti which is not void;
- the resend is nested textually in the body of a method M;
- M takes the same number of arguments, N, as does the resend;
- for each specialized formal parameter formal_i of M, specialized on object_i, the i^th argument to the resend is formal_i, possibly suffixed with @parenti, and formal_i is not shadowed with a local variable of the same name;
- for each unspecialized formal parameter formal_j of M, the j^th argument to the resend is not be suffixed with @parentj;
- for each resend argument of the form formal_i@parenti, parenti is a proper ancestor of object_i, the specializer of formal_i, other than void; and
- when method lookup is simulated with a message name the same as M and with N arguments, where argument i is either any (if formal_i of M is unspecialized), parenti (if the argument of the resend is directed using the @parenti suffix notation), or object_i, the specializer of formal_i (otherwise), and where the resending method M is removed from the set of applicable methods in the current typing context, exactly one most-specific target method R is located, and the argument type declarations of this target method S_i are supertypes of the corresponding Ti.
The type of the result of a resend expression is the declared result type of the target method R.
A parenthetical expression of the form ( body ) is type-correct iff body is type-correct. The type of the result of a parenthetical expression is the type of the result of body.

The following rules define type-correctness of statements:

An assignment statement of the form name := expr is type-correct iff:
- expr is type-correct, with static type T_expr;
- name is bound to an assignable variable of type T_name in the current typing context; and
- T_expr is a subtype of T_name.
The type of the result of an assignment statement is void.
A declaration block is type-correct iff its declarations are type-correct, when checked in a typing context where all names in the declaration block are available throughout the declaration block. The type of the result of a declaration block is void.
An expression statement is type-correct iff the expression is type-correct, with static type T. The type of the result of the expression statement is T.
A non-local return statement, of the form ^ expr, is type-correct iff:
- expr is type-correct, with static type T;
- the non-local return statement is nested textually inside the body of a method M; and
- T is a subtype of the declared result type of M.
The type of the (local) result of a non-local return is none.

The body of a method, closure, or parenthetical expression is type-correct iff its statements are type-correct. The type of the result of a body is the type of its last statement, if present, or void, otherwise.

The following rules define type-correctness of declarations:

A variable declaration of the form let var name:type := expr, where var is either var or empty, is type-correct iff:
- name is not otherwise defined in the same scope;
- type notates a type in the current typing context; and
- expr is type-correct in a typing context where name and all variables defined later in the same declaration block are unbound, resulting in static type T, and T is a subtype of type.
The typing context is extended to include a variable binding for name to the type type that is assignable if var is var and constant otherwise.
A type declaration of the form

	type name subtypes supertype1, ..., supertypeN

is type-correct iff each of the supertype_i notates a type other than none in the current typing context and no cycles are introduced into the subtyping graph as a result of the declaration. As a result of the declaration, the typing context is extended to include a type binding from name to a new type that is a subtype of each of the supertype_i types.
A representation declaration of the form

	role-annotation kind name inherits parent1, ..., parentK
	                    subtypes supertype1, ..., supertypeL
	                    isa parent-and-supertype1, ..., parent-and-supertypeM
	                    { field1@obj1 := expr1, ..., fieldN@objN := exprN }

is type-correct under the same conditions as the analogous object constructor expression, with the following changes:
- abstract objects may be named in inherits and isa clauses;
- the abstract and template role annotations are allowed; and
- no cycles are allowed to be introduced into the inheritance and subtyping graphs.
The typing context is extended to include an object binding from name to a new object with role role-annotation that inherits from the parent_i objects and the parent-and-supertype_j objects. If kind is the representation keyword, then the new object conforms to the supertype_k types. Otherwise, kind is the keyword object, and the typing context is also extended with a type binding from name to a new type that is a subtype of each of the supertype_i types, and the new object conforms to the new type.
A type extension declaration of the form

	extend type name subtypes supertype1, ..., supertypeN

is type-correct iff:
- name is bound in the typing context to a type other than void, any, none, and dynamic; and
- the same constraints on the subtypes clause as with the type declaration are satisfied.
As a result of the declaration, the typing context is extended to reflect that the type name is a subtype of each of the supertype_i types.
A representation extension declaration of the form

	extend kind name inherits parent1, ..., parentK
	   					subtypes supertype1, ..., supertypeL
						isa parent-and-supertype1, ..., parent-and-supertypeM
					 	{ field1@obj1 := expr1, ..., fieldN@objN := exprN }

is type-correct iff:
- name is bound in the typing context to an object other than void and any;
- if kind is object or omitted, then name also is bound in the typing context to a type other than void, any, none, and dynamic;
- the same constraints on the inherits, subtypes, isa, and field initialization clauses as with the object representation declaration are satisfied; and
- none of the fieldi@obji initialize fields already specialized on or inherited by the object before the extension.
As a result of the declaration, the typing context is extended to reflect that the object name inherits from the parent_i objects and the parent-and-supertype_j objects. If kind is the representation keyword, then the typing context is extended to reflect that the object conforms to the supertype_k types. Otherwise, kind is the keyword object, and the typing context is extended to reflect that the name type is a subtype of each of the supertype_i types and that the name object conforms to the name type.
A signature declaration of the form

	signature name(x1:type1,...,xN:typeN):typeR

is type-correct iff:
- the xi, when provided, are distinct;
- each of the typei notates a type other than void in the typing context; and
- typeR notates a type in the typing context.
The typing context is extended to include the corresponding signature.
A field signature declaration of the form

	var field signature name(x:type):typeR

is type-correct iff:
- type notates a type other than void in the typing context; and
- typeR notates a type other than void in the typing context.
The typing context is extended to include the signature

	signature name(type):typeR

and, if var is var, the signature

	signature set_name(type,typeR):void

A method implementation declaration of the general form

	method kind name(x1@obj1:type1,...,xN@objN:typeN):typeR { body }

is type-correct iff:
- the xi, when provided, are distinct;
- each of the typei notates a type other than void in the typing context;
- if @obji is present, then obji conforms to typei;
- typeR notates a type in the typing context;
- body is type-correct when checked in a typing context constructed by extending the current typing context with constant variable bindings for each of the xi to the corresponding type typei; and
- the type of the result of body is a subtype of typeR.
The typing context is extended to include the declared method implementation. If kind is not implementation, then the typing context is also extended to include the signature

	signature name(type1,...,typeN):typeR

A field implementation declaration of the general form

	shared var field kind name(x@obj:type):typeR := expr;

is type-correct iff:
- type notates a type other than void in the typing context;
- if @obj is present, then obj conforms to type;
- typeR notates a type other than void in the typing context;
- if := expr is provided, then expr is type-correct, with static type T, and T is a subtype of typeR; and
- if shared is shared, then := expr is provided.
The typing context is extended to include the declared field get accessor method implementation, plus the set accessor method implementation if var is var, plus the get (and possibly set) signature(s) if kind is not implementation.

[13] The check that the argument type is not void is not strictly necessary, since no signature will have an argument type that is a supertype of void.