4 Parameterization and Bounded Parametric Polymorphism

## 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`.