4.1.1 Type Parameters, Type Variables, and Instantiating Types

Cecil supports parametric polymorphism by allowing declarations to be parameterized with type variables. (This facility is not provided for variable declarations, for which it would be unsound.) A forall T1, ... ,Tn prefix introduces type variables T1, ... ,Tn in a declaration. The scope of these type variables is the declaration that has this prefix, within which the type variables may be used as regular types:

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

To use a polymorphic declaration, it must be instantiated by providing the instantiating type for each type variable. Type variables are "formals" and instantiating types are "actuals" of a parameterized declaration. In the following example an immutable vector object i_vector, method fetch, and an extend declaration are parameterized with type variable T (intended to denote the type of the vector elements):

forall T: template object i_vector[T];
forall T: extend i_vector[T] isa collection[T];
forall T: method fetch(a@:i_vector[T], index:int):T  { ... }
var my_vec:i_vector[num] := concrete object isa i_vector[num];
var result:num := fetch(my_vec, 5); 

Note that parameterization is unsound and is disallowed in the following cases:

• Variable (let) declarations cannot be parameterized.
• The type of a field cannot reference any type parameters except those of the object to which the field is attached. Moreover, the type of a field attached to a concrete object cannot reference any type parameters.