(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:
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
the type tree of the
and the type tree of the result term,
and producing the inst tree of the result term
if the conversion is valid.
coerceargument’s inst tree,
coerceargument’s type tree,
In the following, X < Y means X is a subtype of Y by visible subtype definitions.
For each node InstX:
boundnode, then each of the function symbols listed in the
boundinst must name a constructor in TypeCtorY. Let InstY be a
boundinst containing the same function symbols; the insts for the arguments of each function symbol are then checked and constructed recursively.
groundnode and TypeX = TypeY, then InstY = InstX.
groundnode and TypeX < TypeY, then let InstY be the
boundnode constructed using the process below.
coerceexpression is not mode-correct.
To construct a ‘bound’ node InstY from a ‘ground’ node InstX:
boundinst 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
fruits are not
:- 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
to those that would also be valid in
:- inst citrus for fruit/0 ---> lemon ; orange. :- func f3(fruit) = citrus. :- mode f3(in(citrus)) = out is det. f3(X) = coerce(X).
this function is type-incorrect because
in the coerce expression,
the type parameter T of
is bound to
fruit in the input type,
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