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

4 Parameterization and Bounded Parametric Polymorphism

4.3 Constraint Solving and Type Inference

The following typechecking tasks in Cecil lead to constraint solving:

Given a constraint to solve, constraint solving proceeds as follows. A "set-to-be-solved" of constraints is created, initially containing this one constraint. One constraint at a time is picked and removed from this set. A matching constraint is produced from the program declarations, if possible, otherwise constraint solving fails. Two constraints match if they have the same structure (e.g., both are signature constraints for the same message name and number of arguments) and the types in the corresponding positions are the same; fresh type variables may be instantiated with types during matching. While producing the matching constraint, new constraints to be solved may arise, in which case they are added to the set-to-be-solved. Constraint solving succeeds when the set-to-be-solved becomes empty.

The matching constraint can be produced either by taking a constraint or declaration available in the program, or by combining other constraints produced from the program declarations. More specifically:

Inference of instantiating types is the part of constraint solving whereby the typechecker decides how to instantiate polymorphic declarations, i.e., what types to substitute for type variables. Intuitively, when typechecking a message send, the typechecker tries to find the "best" instantiations of declarations involved in solving the signature constraint, i.e., the instantiations that lead to the most precise result type. When checking whether a type is a subtype of another, the typechecker only needs to prove that some appropriate instantiations exist.

Consider, for example, typechecking the message send print(my_coll) in the context of the following declarations:

abstract object printable;
signature print(p:printable):void;

abstract object collection[T];
extend collection['T <= printable] isa printable;
method print(a@:collection['T <= printable]):void
{  print("[");  a.do(&(e:T){ print(e) });  print("]")  }

extend string isa printable;              -- assume string implements print  

let my_coll:collection[string] := ...;
print(my_coll);

Since my_coll has type collection[string], in order to check this send, the typechecker needs to solve the constraint signature print(collection[string]):Tresult where Tresult is a fresh type variable; this is the first constraint in the set-to-be-solved. A matching constraint can be produced by instantiating the signature corresponding to method print (collection['T<=printable]):void. Two substitutions need to take place to achieve matching: void for Tresult and string for T. Also, the signature's instantiated subtype constraint string <= printable is added to the set-to-be-solved. This time, the program already contains an exactly matching declaration (the subtype declaration corresponding to extend string isa printable). No more constraints are added to the set-to-be-solved, so constraint solving is complete. The instantiating type string was automatically inferred for the type variable T of the polymorphic method declaration.