Escaping Types

There are two ways to escape type checking in CLAIRE. The first one is casting, which means giving an explicit type to an expression. The syntax is quite explicit :

<cast> = (<expression> as <type>)

This will tell the compiler that <expression> should be considered as having type <type>. Casting is ignored by the interpreter and should only be used as a compiler optimization. There is, however, one convenient exception to this rule, which is the casting into a list parametric type. When an untyped list is casted into a typed list, the value of its of parameter is actually modified by the interpreter, once the correct typing of all members has been verified. For instance, the two following expressions are equivalent :

list<integer>(1,2,3,4)  list(1,2,3,4) as list<integer>

The second type escaping mechanism is the non-polymorphic method call, where we tell what method we want to use by forcing the type of the first argument. This is equivalent to the supermessage passing facilities of many object-oriented languages.

<super> = <selector>@<type>(<exp>seq)

The instruction f@c(...) will force CLAIRE to use the method that it would use for f(...) if the first argument was of type c (CLAIRE only checks that this first argument actually belongs to c).

A language is type-safe if the compiler can use type inference to check all type constraints (ranges) at compile-time and ensure that there will be no type checking errors at run-time. CLAIRE is not type-safe because it admits expressions for which type inference is not possible such as read(p) + read(p). On the other hand, most expressions in CLAIRE may be statically type-checked and the CLAIRE compiler uses this property to generate code that is very similar to what would be produced with a C++ compiler. A major difference between CLAIRE 3.0 and earlier versions is the fact that lists may be explicitly typed, which removes the problems that could happen earlier with dynamic types. Lists and sets subtypes support inclusion polymorphism, which means that if A is a subtype of B, list[A] is a subtype of list[B]; for instance list[(0 .. 1)] <= list[integer]. Thus only read operations can be statically type-checked w.r.t. such type information. On the other hand, array subtypes, as well as list or set parametric subtypes, are monomorphic, since A[] is not the set of arrays which contain members of A, but the set of arrays whose member type (the of slot) contains the value A. Thus if A is different from B, A[] is not comparable with B[], and list<A> is not comparable with list<B>. This enables the static type-checking of read and write operations on lists. The fact that CLAIRE supports all styles of type disciplines is granted by the combination of a rich dynamic type system coupled with a powerful type inference mechanism within the compiler, and is a key feature of CLAIRE.