4.2 Bounded Polymorphism and Type Constraints

It is often necessary to express some assumptions or restrictions on type parameters. For example, a sort method can only sort collections whose elements can be compared with each other. A matrix_multiply method may require that matrix elements be numbers. This situation is known as bounded polymorphism [Cardelli & Wegner 85]. Cecil supports bounded polymorphism by allowing type constraints on type parameters.

There are two kinds of type constraints in Cecil. A subtype constraint specifies the requirement that one type be a subtype of another. A common use of subtype constraints is to specify upper or lower bounds of type variables. In the following example, the type of matrix elements is constrained to be a subtype of num:

method matrix_multiply(a:matrix['T], b:matrix['T]):matrix[T]
	where T<=num
{
	...
}

A signature constraint specifies the requirement that the given signature hold. A common use of signature constraints is to require certain operations to be provided for the type parameters. In the following example, the message send of <= in the body of sort is guaranteed to be legal as long as the constraint is satisfied:

method sort(a:array['T]):void
	where signature <=(T,T):bool
{
	...
	let a_i:T := a!i;
	let a_j:T := a!j;
	if(a_i <= a_j, { ... swap a!i and a!j ... });
	...
}

Type constraints are allowed in the where part of the forall clause and in a where clause following the header of a declaration. The common case of the subtype constraints, type variables' upper bounds, are also allowed wherever that type variable is introduced (in a forall clause, using the backquote sugar, or as an explicit type parameter).

type_cxt	::=	"forall" formal_param { "," formal_param } [type_cons] ":"
type_cons	::= "where" type_constraint { "," type_constraint }
type_constraint	::=	sub_constraint | sig_constraint
sub_constraint	::=	type ("<=" | ">=") type
sig_constraint	::=	"signature" (msg_name [params] | op_name)
		    "(" [arg_types] ")" type_decl 
name_binding	::=	name [">=" type] ["<=" type]

tp_decl 	::=	[type_cxt] [privacy] "type" name [formal_params]
		    {type_relation} [type_cons] ";"	 
object_decl 	::=	[type_cxt] [privacy] rep_role rep_kind name [formal_params]
		    {relation} [type_cons] [field_inits] ";"
predicate_decl 	::=	[type_cxt] [privacy] "predicate" name [formal_params]
		    {relation} [type_cons] [field_inits] ["when" expr] ";"
type_ext_decl	::=	[type_cxt] [privacy] "extend" "type" named_type
		    [type_cons] {type_relation} ";"
obj_ext_decl	::=	[type_cxt] [privacy] "extend" extend_kind named_object
		    {relation} [type_cons] [field_inits] ";"
signature_decl	::=	[type_cxt] [privacy] "signature" method_name
		    "(" [arg_types] ")" [type_decl] [type_cons] ";"
method_decl	::=	[type_cxt] [privacy] impl_kind method_name
		    "(" [formals] ")" [type_decl] [type_cons] {pragma}
		    "{" (body | prim_body) "}" [";"]
field_sig_decl	::=	[type_cxt] [field_privacy] ["var"] "field" "signature"
		    msg_name [formal_params] "(" arg_type ")"
		    [type_decl] [type_cons] ";"
field_decl	::=	[type_cxt] [field_privacy] ["shared"] ["var"] "field"
		    field_kind msg_name [formal_params] "(" formal ")"
		    [type_decl] [type_cons] {pragma} [":=" expr] ";"

The matrix_multiply method in the above example can be re-written more concisely as follows (this sacrifices the visual symmetry between the arguments a and b, but is semantically equivalent, because it introduces exactly the same type variable and constraint):

method matrix_multiply(a:matrix['T<=num], b:matrix[T]):matrix[T]
{ ... }

The @: syntactic sugar is extended to allow a type variable with an upper bound. This idiom is used when it is desirable to give a more precise type to a formal that is specialized on some object (and the type of the formal is expected to subtype the specializer object). For example,

method foo(x@:'T<=bar):T { ... }

desugars into

method foo(x@bar:'T<=bar):T { ... }

It is a useful programming idiom to associate constraints with parameterized types. For example, the type of a binary search tree may require that the comparison operation be defined on the type of the tree element, similarly to the sorting method above:

template object binary_tree[T] where signature <=(T,T):bool;

Cecil provides a syntactic sugar that automatically inserts these associated constraints. If a backquoted type variable is used as an explicit instantiating parameter of a parameterized type, the constraints that the type associates with its explicit parameter in the corresponding position are imposed on the type variable. For example, in the following method:

method insert(t@:binary_tree['T], elm:T):void { ... }

the constraint where signature <=(T,T):bool is automatically added, so in the body of insert it is legal to send the message <= to tree elements and elm.