3.2 Types and Signatures

A type in Cecil is an abstraction of an object. A type represents a machine-checkable interface and an implied but unchecked behavioral specification, and all objects that conform to the type must support the type's interface and promise to satisfy its behavioral specification. One type may claim to be a subtype of another, in which case all objects that conform to the subtype are guaranteed also to conform to the supertype. The type checker verifies that the interface of the subtype conforms to the interface of the supertype, but the system must accept the programmer's promise that the subtype satisfies the implied behavioral specification of the supertype. Subtyping is explicit in Cecil just so that these implied behavior specifications can be indicated. A type may have multiple direct supertypes, and in general the explicit subtyping relationships form a partial order. As described in subsection 3.4, additional type constructors plus a few special types expand the type partial order to a full lattice.

A signature in Cecil is an abstraction of a collection of overloaded methods, specifying both an interface (a name, a sequence of argument types, and a result type) and an implied but uncheckable behavioral specification. The interface of a type is defined as the set of signatures that mention that type as one of their argument or result types.

For example, the following types and signatures describe the interface to lists of integers:

type int_list subtypes int_collection;
	signature is_empty(int_list):bool;
	signature length(int_list):int;
	signature do(int_list, &(int):void):void;
	signature pair_do(int_list, int_list, &(int,int):void):void;
	signature prepend(int, int_list):int_list;

Types and signatures represent a contract between clients and implementors that enable message sends to be type-checked. The presence of a signature allows clients to send messages whose argument types are subtypes of the corresponding argument types in the signature, and guarantees that the type of the result of such a message will be a subtype of the result type appearing in the signature. Any message not covered by some signature will produce a "message not understood" error. Signatures also impose constraints on the implementations of methods, in order to make the above guarantees to clients. The collection of methods implementing a signature must be conforming, complete, and consistent:

• Conformance implies that each method implementing a signature has unspecialized argument types that are supertypes of the corresponding argument types of the signature and a result type that is a subtype of the signature's result type; conformance is Cecil's version of the standard contravariance rule found in singly-dispatched statically-typed languages.
• Completeness implies that the methods must handle all possible argument types that might appear at run-time as an argument to a message declared legal by the signature.
• Consistency implies that the methods must not be ambiguous for any combination of run-time arguments.

Checking completeness and consistency is the subject of section 3.6.2.

In a singly-dispatched language, each type has an associated set of signatures that defines the interface to the type. This association relies on the asymmetry of message passing in such languages, where only the receiver argument impacts method lookup. When type-checking a singly-dispatched message, the type of the receiver determines the set of legal operations, i.e., the set of associated signatures. If a matching signature is found, then the message will be understood at run-time; the static types of the remaining message arguments is checked against the static argument types listed in the signature. For Cecil, we wish to avoid the asymmetry of this sort of type system. Consequently, we view a signature as associated with each of its argument types, not just the first, much as a multi-method in Cecil is associated with each of its argument specializer objects. For example, the prepend signature above is considered part of both the int type and the int_list type.

In most object-oriented languages, the code inheritance graph and the subtyping graph are joined: a class is a subtype of another class if and only if it inherits from that other class. Sometimes this constraint becomes awkward [Snyder 86], for example when a class supports the interface of some other class or type, but does not wish to inherit any code. Other times, a class reusing another class's code cannot or should not be considered a subtype; covariant redefinition as commonly occurs in Eiffel programs is one example of this case [Cook 89].

To increase flexibility and expressiveness, Cecil separates subtyping from code inheritance. Types and signatures can be declared independently of object representations and method implementations. However, since in most cases the subtyping graphs and the inheritance graphs are parallel, requiring programmers to define and maintain two separate hierarchies would become too onerous to be practical. To simplify specification and maintenance of the two graphs, in Cecil the programmer can specify both a type and a representation, and the associated subtyping, conformance, and inheritance relations, with a single declaration. Similarly, a single declaration can be used to specify both a signature and a method implementation. In this way we hope to provide the benefits of separating subtyping from code inheritance when it is useful, without imposing additional costs when the separation is not needed.