Next: Exception handling, Previous: Existential types, Up: Top [Contents]
(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:
coerce(Term)
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:
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
coerce
argument’s inst tree,
coerce
argument’s type tree,
In the following, X < Y means X is a subtype of Y by visible subtype definitions.
For each node InstX:
bound
node,
then each of the function symbols listed in the bound
inst
must name a constructor in TypeCtorY.
Let InstY be a bound
inst containing the same
function symbols;
the insts for the arguments of each function symbol
are then checked and constructed recursively.
ground
node
and TypeX = TypeY,
then InstY = InstX.
ground
node
and TypeX < TypeY, then
let InstY be the bound
node constructed
using the process below.
coerce
expression is not mode-correct.
To construct a ‘bound’ node InstY from a ‘ground’ node InstX:
ground
.
bound
inst
containing all of the constructors in TypeCtorX;
the insts for the arguments of each function symbol
are constructed recursively.
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 fruit
s 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: Exception handling, Previous: Existential types, Up: Top [Contents]