13 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:

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:

• ‘Si = Ti’ if the two types are the same
• ‘Si < Ti’ if Si is a subtype of Ti by the relation below
• ‘Ti < Si’ if Ti is a subtype of Si by the relation below

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:

• in a higher-order type
• in a foreign type
• in an abstract type
• in a solver type
• in a discriminated union type, other than a recursive type of the exact form ‘base(B1, ..., Bn)’

The relation ‘S < T’ is true when ‘S != T’ and either:

• ‘S’ and ‘T’ are both discriminated union types, and ‘S’ is a subtype of ‘T’ by visible subtype definitions; or
• ‘S’ and ‘T’ are both tuple types of the same arity, and for each pair of corresponding argument types ‘Si’ and ‘Ti’, ‘Si < Ti’ is true.

Mode checking

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

• InstX be the current node in the coerce argument’s inst tree,
• InstY be the current node in the result inst tree,
• TypeX be the current node in the coerce argument’s type tree,
• TypeY be the current node in the result type tree,
• TypeCtorX be the principal type constructor of TypeX,
• TypeCtorY be the principal type constructor of TypeY.

In the following, X < Y means X is a subtype of Y by visible subtype definitions.

For each node InstX:

• If InstX is a recursive node in the inst tree (i.e. it is its own ancestor), then we require TypeX =< TypeY. Let InstY = InstX.
• Otherwise, if InstX is a bound node:
  • If TypeX is an existentially quantified type variable, then InstY = InstX.
  • If TypeX is not an existentially quantified type variable, then each of the function symbols listed in InstX must name a constructor in TypeCtorY. Let InstY be a bound inst containing those same function symbols; the insts for the arguments of each function symbol are then checked and constructed recursively.
• Otherwise, if InstX is a ground node:
  • If TypeX = TypeY, or if TypeX is an existentially quantified type variable, then let InstY = InstX.
  • If TypeX < TypeY, then let InstY be the bound node constructed using the process below.
• Otherwise, the coerce expression is not mode-correct.

To construct a ‘bound’ node InstY from a ‘ground’ node InstX:

• If TypeX = TypeY or if TypeX is a recursive node in the type tree (i.e. it is its own ancestor), then let InstY be ground.
• Otherwise, let InstY be a bound inst containing all of the constructors in TypeCtorX; the insts for the arguments of each function symbol are constructed recursively.

Examples

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