Next: , Previous: Existential types, Up: Top   [Contents]

13 Type conversions

(This is a new and experimental feature, subject to change.)

A term may be converted from one type FromType to another type ToType using a type conversion expression of the form:


The expression is type-correct iff FromType and ToType are both discriminated union types, and after replacing the principal type constructors with base types (see Subtypes) the two types have the same type constructor, and the arguments of the common type constructor satisfy the type parameter variance restrictions below.

Let FromType expand out to ‘base(S1, ..., Sn)’ and ToType expand out to ‘base(T1, ..., Tn)’, where ‘base(B1, ..., Bn)’ is the common base type, and Bi is the i’th type parameter, which is bound to Si in FromType and Ti in ToType.

For each pair of corresponding type arguments, one of the following must be true:

Otherwise, the coerce expression is not type-correct.

Furthermore, ‘Si = Ti’ must be true if Bi occurs in one or more of these locations in the ‘base/n’ type definition:

Mode checking

Type conversion expressions must also be mode-correct. Intuitively, conversion from a subtype to its supertype is safe, but a conversion from a supertype to one of its subtypes is safe only if the inst approximating the term to be converted indicates that the result would also be valid in the subtype.

Mode checking proceeds by simultaneously traversing the inst tree of the coerce argument, the type tree of the coerce argument, and the type tree of the result term, and producing the inst tree of the result term if the conversion is valid. Let

In the following, X < Y means X is a subtype of Y by visible subtype definitions.

For each node InstX:

To construct a ‘bound’ node InstY from a ‘ground’ node InstX:


Assume we have:

:- type fruit
   --->    apple
   ;       lemon
   ;       orange.

:- type citrus =< fruit
   --->    lemon
   ;       orange.

This function is type and mode-correct:

:- func f1(citrus) = fruit.

f1(X) = coerce(X).

This function is type-correct but not mode-correct because some fruits are not citrus:

:- func f2(fruit) = citrus.

f2(X) = coerce(X).  % incorrect

This function is mode-correct because the initial inst of the input argument limits the range of fruit values to those that would also be valid in citrus:

:- inst citrus for fruit/0
    --->    lemon
    ;       orange.

:- func f3(fruit) = citrus.
:- mode f3(in(citrus)) = out is det.

f3(X) = coerce(X).

Finally, this function is type-incorrect because in the coerce expression, the type parameter T of wrap/1 is bound to fruit in the input type, but citrus in the result type.

:- type wrap(T)
    --->    wrap(T).

:- func f4(func(fruit) = int) = (func(citrus) = int).

f4(X) = Y :-
    wrap(Y) = coerce(wrap(X)).  % incorrect

Next: , Previous: Existential types, Up: Top   [Contents]