Polymorphism

In addition to the traditional "objet-oriented" polymorphism, CLAIRE also offers two forms of parametric polymorphism, which can be skipped by a novice reader.

(1) There often exists a relation between the types of the arguments of a method. Capturing such a relation is made possible in CLAIRE through the notion of an "extended signature". For instance, if we want to define the operation "push" on a stack, we would like to check that the argument y that is being pushed on the stack s belongs to the type of(s), that we know to be a parameter of s. The value of this parameter can be introduced as a variable and reused for the typing of the remaining variables (or the range) as follows :

push(s:stack<X>, y:X) -> (s.content :add y, s.index :+ 1)

The declaration s:stack<X> introduced X as a type variable with value s.of, since stack[of] was defined as a parameterized class. Using X in y:X simply means that y must belong to the type s.of. Such intermediate type variables must be free identifiers (the symbol is not used as the name of an object) and must be introduced with the following template :

<class>[pi=vi, ...]

The use of type variables in the signature can be compared to pattern matching. The first step is to bind the type variable. If (p = V) is used in c[ ...] instead of p:t, it means that we do not put any restriction on the parameter p but that we want to bind its value to V for further use. Note that this is only interesting if the value of the parameter is a type itself. Once a type variable V is defined, it can be used to form a pattern (called a <type with var> in the CLAIRE syntax) as follows:

<type with var> = <type> | <var> | {<var>} |      tuple(<type with var>seq+) |      <class>[< <var>:<type with var> | <var>=<var> >seq+]

(2) The second advanced typing feature of CLAIRE is designed to capture the fine relationship between the type of the output result and the types of the input arguments. When such a relationship can be described with a CLAIRE expression e(x1,...,xn), where x1, ..., xn are the types of the input parameters, CLAIRE allows to substitute type[e] to the range declaration. It means that the result of the evaluation of the method should belong to e(t1,...,tn) for any types t1,...,tn that contain the input parameters.

For instance, the identity function is known to return a result of the same type as its input argument (by definition !). Therefore, it can be described in CLAIRE as follows :

id(x:any) : type[x] -> x

In the expression that we introduce with the type[e] construct, we can use the types of the input variables directly through the variables themselves. For instance, in the "type[x]" definition of the id example, the "x" refers to the type of the input variable. Notice that the types of the input variables are not uniquely defined. Therefore, the user must ensure that her "prediction" e of the output type is valid for any valid types t1, ..., tn of the input arguments.

The expression e may use the extra type variables that were introduced earlier. For instance, we could define the "top" method for stacks as follows :

top(s:stack<X>) : type[X] -> s.content[s.index]

The "second-order type" e (second-order means that we type the method, which is a function on objects, with another function on types) is built using the basic CLAIRE operators on types such as U, ^ and some useful operations such as "member". If c is a type, member(c) is the minimal type that contains all possible members of c. For instance, member({c}) = c by definition. This is useful to describe the range of the enumeration method set!. This method returns a set, whose members belong to the input class c by definition. Thus, we know that they must belong to the type member(X) for any type X to whom c belongs (cf. definition of member). This translates into the following CLAIRE definition :

set!(c:class) : type[set[member(c)]] -> c.instances

For instance, if c belongs to subtype[B] then set!(c) belongs to set[B].

To summarize, here is a more precise description of the syntax for defining a method :

<function>(<vi>:<ti>i E (1 .. n)) : <range> -> <exp>

Each type ti for the variable vi is an "extended type" that may use type variables introduced by the previous extended types t1, t2 ... ti-1 . An extended type is defined as follows :

<et> = <class> | <set> | <var> | (<et> ^ | U <et>) | (<integer> .. <integer>) |      set[<et>] | list[<et>] | <et>[] | tuple(<et>seq) |      <class>[< <var>:<et> | <var>=< <var> | <const> > >seq+]

The <range> expression is either a regular type or a "second order type", which is a CLAIRE expression e introduced with the type[e] syntactical construct :

<range> = <type> | type[<expression>]