[Next] [Previous] [Up] [Top] [Contents] [Index]

3.6 Type Checking Messages

3.6.2 Checking Signatures Against Method Implementations

The type checker ensures that, for every signature in the program, all possible messages that could be declared type-safe by the signature would in fact locate a single most-specific method with appropriate argument and result type declarations, given the current set of representation and type declarations in the program. This involves locating all methods to which the signature is applicable (i.e., all those that could be invoked by a message covered by the signature) and ensuring that they conformingly, completely, and consistently implement the signature.

More precisely:

Conformance of a method against a signature can be checked in isolation of any other methods and signatures in the program. However, in the presence of multi-methods, it is not possible to check individual methods in isolation for completeness and consistency, since interactions among multi-methods can introduce ambiguities where none would exist if the multi-methods were not jointly defined within one program.

To type-check in the presence of Cecil's prototype-based object model, object representatives are extracted from the program. Each named template, concrete, and dynamic object is considered a distinct object representative, and each static occurrence of an object constructor expression is considered an object representative. A finite number of representatives are extracted from any given program. Representatives are then used as the potential run-time argument objects when testing whether a signature is applicable to a method and whether a set of methods completely and consistently implement a signature. The object representative for an object constructor expression acts as a proxy for all the objects created at run-time by executing that object constructor expression. Since each object created by a particular object constructor expression inherits the same set of methods and has the same type, only one representative need be checked to ensure type safety of all objects created by the object constructor expression at run-time. Object representatives are analogous to concrete classes in a class-based language and maps in the Self implementation [Chambers et al. 89].

Conceptually, for each signature, the type checker enumerates all possible message representatives that are covered by the signature, where the arguments to the message representative are object representatives that conform to the signature's argument types. (A much more efficient algorithm to perform this checking is described elsewhere [Chambers & Leavens 94].) For each message representative, the type checker simulates method lookup and checks that the simulated message would locate exactly one most-specific method. If no method is found, the type checker reports a "signature implemented incompletely" error. If multiple mutually ambiguous methods are found, the type checker reports a "signature implemented inconsistently" error. Otherwise, the single most-specific method has been found for the message representative. In this case, the type checker also verifies that the argument object representatives conform to the declared argument types of the target method and that the declared result type of the method is a subtype of the signature's result type. If all these tests succeed, then all run-time messages matching the message representative are guaranteed to execute successfully.

For example, consider type-checking the implementation of the following signature:

signature pair_do(collection, collection, &(int,int):void):void;

The type checker would first collect all object representatives that conform to collection and all those that conform to &(int,int):void. For a small system, the collection-conforming object representatives might be the following:

representation nil inherits list;
representation cons inherits list;
representation inherits cons;
representation array inherits collection;

The list and collection objects are not enumerated because they are abstract. The third representative is extracted from the object constructor expression in the prepend method. A single object representative stands for the closure object.

Once the applicable object representatives are collected, the type checker enumerates all possible combinations of object representatives conforming to the argument types in the signature to construct message representatives. These message representatives are the following:

pair_do(nil,nil,closure);
pair_do(nil,cons,closure);
pair_do(nil,representation inherits cons,closure);
pair_do(nil,array,closure);
pair_do(cons,nil,closure);
pair_do(cons,cons,closure);
...
pair_do(array,representation inherits cons,closure);
pair_do(array,array,closure);

For each message representative, method lookup is simulated to verify that the message is understood, that the declared argument types are respected, and that the target method returns a subtype of the signature's type.