Type rules

Subtyping relationship

The subtyping relationship is given with respect to an environment that maps each type variable X to its set of bounds {H1 ... Hn}. The relationship is reflexive and transitive as usual.

Note that subtyping relationship is invariant with regard to type parameters; S <: S' does not imply that R<S> <: R<S'>.

Inclusion relationship

The inclusion relationship is identical to the definition in IMCPI.

Well-formed types

We introduce a new category of rules for well-formedness of instantiated (closed) types.

Expression typing

The primitive axioms for expressions remain the same as in IMCPI. The rule T-INVK for method invocation becomes considerably more complex, however. Because we do not support fully qualified interface implementation, we must deal with any ambiguities when a method or field of a type parameter is accessed. These restrictions are based on similar conditions in the specification for Java generics. The ambiguity arises when 'a type parameter X has more than one bound, and if different bounds have member methods with the same signature and different return types, then any reference to such members of a value of type X is ambiguous and is a compile-time error'. Here is an example in IMCPG:

(* ... *)
TYPE
  I = INTERFACE RECORD (ANYIFACE) END;
  PI = POINTER TO I;

  J = INTERFACE RECORD (ANYIFACE) END;
  PJ = POINTER TO J;

  R<X:PI+PJ> = EXTENSIBLE RECORD (ANYREC) ... END;

PROCEDURE (this:PI) Foo (): INTEGER, NEW, ABSTRACT;

PROCEDURE (this:PJ) Foo (): BOOLEAN, NEW, ABSTRACT;

PROCEDURE (this:R<X:PI+PJ>) Bar (x: X), NEW; BEGIN ... x.Foo() ...
END Bar;

(* ... *)

In the above example, the call to x.Foo() is ambiguous -- which definition of Foo() is being invoked, the definition that returns INTEGER or the definition that returns BOOLEAN? It is also clear that there is no type that can instantiate X in R as (a) overloading is not supported in MCP and (b) even if it were, overloading with different return types would not be permitted.

The first line of rule T-INVK that the receiver is some type J -- that is, either a pointer type or a type parameter. The second line states that there exists some bound J' on type J that defines a method p matching the type of the method invocation. (Note that the definition of the function bound returns the type itself if the type is not a type variable). The third line states that for all bounds K on type J, if a method p is defined in that bound then the signature must match the definition in J' -- i.e. that no ambiguities can arise like those described above. The fourth line states that the method type instantiations J'' must be well-formed, and must be subtypes of their corresponding bounds. The fifth line states that the actual parameters must be subtypes of the formal parameters (instantiated with the types J'').

Left-expression typing

Statement typing

Module typing

Type declaration typing

The rule T-RECORD for record declaration typing is similar to its definition in IMCPI. However, we strengthen the premises for interface implementation to state that a record must implement the methods defined in its interfaces, with all type variables replaced by their type instantiations. For example, given the following generic interface declaration:

(* ... *)
I<X:ANYPTR> = INTERFACE RECORD (ANYIFACE) END;
PI<X:ANYPTR> = POINTER TO I<X:ANYPTR>;
(* ... *)
PROCEDURE (this: PI<X:ANYPTR>) Compare (x: X; y: X), NEW, ABSTRACT;
(* ... *)

An example of a record implementing this interface would be:

(* ... *)
R = RECORD (ANYREC + I<PS>) ... END;
PR = POINTER TO R;
S = RECORD ... END;
PS = POINTER TO S;
(* ... *)
PROCEDURE (this: PR) Compare (x: PS; y: PS);
(* ... *)

This condition is enforced by lines three to five of T-RECORD.

Method typing

The rule T-MTHD for method typing is similar to its definition in IMCPI, with a few extra premises regarding type parameters. The first line retrieves the record type of the receiver and its sequence of supertypes. The second line constructs an environment mapping the type variables X (associated with the receiver type) and X' (associated with the procedure) to their respective bounds; it also checks that the parameter types, return type, and type parameter bounds are well-formed.

The rest of the rule is similar to IMCPI. The differences are in line five (which checks that the body statements are well-formed with respect to both environments and and that the types of the local variables are well-formed), and line nine (which states that the signature of an overriding method must be identical to the signature of the overridden method -- including the type parameters).