(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:
Type conversion expressions must also be mode-correct. For an expression where:
the type conversion expression is mode-correct iff:
boundinstantiatedness tree derived from ‘t’, and FinalY does not approximate any term that is invalid in ‘t’.
bound instantiatedness tree for ‘t’
is derived by producing a
containing each possible constructor of ‘t’,
where the arguments of each bound functor
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
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 .
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
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