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

12 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. For an expression where:

the type conversion expression is mode-correct iff:

The bound instantiatedness tree for ‘t’ is derived by producing a bound node containing each possible constructor of ‘t’, where the arguments of each bound functor are also bound instantiatedness trees. Where a constructor argument type is not a discriminated union or tuple type, or if the argument is a recursive node in the type tree, the inst of the argument is replaced with ground.

The abstract unification of two instantiation states is the abstract equivalent of the unification on terms. It is defined in Precise and Expressive Mode Systems for Typed Logic Programming Languages by David Overton. See [6].

Intuitively, coercing a ground term from a subtype to a supertype is safe, but coercing a term from a supertype to a subtype is safe only if the inst of the term being coerced indicates that the term would also be valid in the subtype.


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]