[Next] [Previous] [Up] [Top] [Contents] [Index]
4 Parameterization and Bounded Parametric Polymorphism
The following typechecking tasks in Cecil lead to constraint solving:
signature
m[T1¢,...,Tm¢] (T1,...,Tn):Tresult
is solved. Here Tresult
is a fresh type variable and can be instantiated with some type. The type of the message send is the most specific type that Tresult
can take on while the signature constraint can be solved successfully.
<=
S2 is solved. S1 is a subtype of S2 iff the constraint can be solved successfully.
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:
signature
=(num,num):bool
and extend
int
isa
num
, they can be combined to yield the constraint signature
=(int,num):bool
. Matching of types and substitutions of types for fresh type variables are performed as needed.
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.
[Next] [Previous] [Up] [Top] [Contents] [Index]
Generated with Harlequin WebMaker