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

4 Parameterization and Bounded Parametric Polymorphism

The following typechecking tasks in Cecil lead to constraint solving:

- To typecheck a message send
*m*[*T*,...,_{1¢}*T*](_{m¢}*E*,...,_{1}*E*), where the types of_{n}*E*,...,_{1}*E*are_{n}*T*,...,_{1}*T*, the signature constraint_{n}`signature`

*m*[*T*,...,_{1¢}*T*] (_{m¢}*T*,...,_{1}*T*):_{n}`T`

is solved. Here_{result}`T`

is a fresh type variable and can be instantiated with some type. The type of the message send is the most specific type that_{result}`T`

can take on while the signature constraint can be solved successfully._{result} - To check whether
*S*is a subtype of_{1}*S*, the subtype constraint_{2}*S*_{1}`<=`

*S*is solved._{2}*S*is a subtype of_{1}*S*iff the constraint can be solved successfully._{2} - Whenever a declaration with constraints in its header is instantiated, the instantiated constraints must be solved. If they cannot be solved successfully, such instantiation is not
*legal*and so is disallowed.

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:

- A polymorphic subtype or signature declaration present in the program can be instantiated by substituting types or fresh type variables for its type variables; its constraints, if any, need to be solved and are added to the set-to-be-solved. A subtype of signature declaration with no type variables is treated as an available constraint itself.
- When typechecking the body of a polymorphic declaration, the constraints in its header are available.
- Constraints can be combined based on the standard properties of subtyping, such as transitivity, and of signatures, such as contravariance. For example, if the program contains declarations
`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 objectprintable;signatureprint(p:printable):void;abstract objectcollection[T];extendcollection['T <= printable]isaprintable;methodprint(a@:collection['T <= printable]):void { print("["); a.do(&(e:T){ print(e) }); print("]") }extendstringisaprintable; --assume`string implements print`

letmy_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]):T`

where _{result}`T`

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 _{result}`method`

`print`

`(collection['T<=printable]):void`

. Two substitutions need to take place to achieve matching: `void`

for `T`

and _{result}`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.

"The Cecil Language: Specification and Rationale" - 7 Feb 1999

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

Generated with Harlequin WebMaker