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. For an expression where:
the type conversion expression is mode-correct iff:
bound
instantiatedness tree derived from ‘t’,
and FinalY does not approximate any term
that is invalid in ‘t’.
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 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]