Previous: Abstract types, Up: User-defined types   [Contents]


3.2.4 Subtypes

(This is a new and experimental feature, subject to change.)

A subtype is a discriminated union type that is a subset of a supertype, in that every term of a subtype is a valid term in the supertype. It is possible to convert terms between subtype and supertype using type conversion expressions (see Type conversions).

A subtype is defined using the form

:- type subtype =< supertype ---> body.

subtype must be a name term whose arguments (if any) are distinct variables.

supertype must be a type (that may contain variables). After expanding out equivalences, the principal constructor must specify a discriminated union type whose definition is in scope where the subtype definition occurs, by normal module visibility rules.

The discriminated union type specified by supertype may itself be a subtype. Following a chain of visible subtype definitions, it must be possible to arrive at a base type, which is not a subtype.

Any variable that occurs in supertype must occur in subtype.

The body term is defined as a sequence of constructor definitions separated by semicolons. Any universally quantified type variable that occurs in body must occur in subtype.

The constructor definitions must be a subset of the constructors of the supertype; we recommend they appear in the same relative order as in the supertype definition. If the supertype ‘t’ has constructor ‘f(T1, ..., Tn)’ then a subtype ‘s =< t’ may have a constructor ‘f(S1, ..., Sn)’. For each Si, it must be that ‘Si =< Ti’.

(In the following discussion, assume that equivalence types are expanded out as required.)

S =< T’ holds if ‘S = f(S1, ..., Sn)’ and ‘T = f(T1, ..., Tn)’ and for each pair of corresponding arguments ‘Si =< Ti’.

Otherwise, ‘S =< T’ holds if ‘S = f(S1, ..., Sn)’ and there is a visible definition ‘:- type f(R1, ..., Rn) =< U, and for each pair of corresponding arguments ‘Si = Ri (unification), and ‘U =< T’. In other words, any occurrences of Ri in U are substituted for Si to give Usub, and ‘Usub =< T’ must hold.

P =< Q’ holds for two higher-order types P and Q iff P and Q are both ‘pred’ types or both ‘func’ types with the same arity, and P and Q have the same argument types. In addition, if either of P and Q has higher-order inst information, then P and Q must have the same argument modes, determinism, and purity. (The current implementation does not admit subtyping in higher-order arguments.)

P =< Q’ holds if P and Q are both existentially quantified type variables, and ‘P = Q’.

There must be a one-to-one mapping between existentially quantified type variables for a constructor in the subtype definition and the same constructor in the supertype definition. The subtype constructor must repeat exactly the same set of existential class constraints on its existentially quantified type variables as in the supertype; the subtype constructor cannot add or remove any existential class constraints.

Examples:

:- type list(T)
    --->    []
    ;       [T | list(T)].

:- type non_empty_list(T) =< list(T)
    --->    [T | list(T)].

:- type non_empty_list_of_foo =< list(foo)
    --->    [foo | list(foo)].

:- type maybe_foo
    --->    none
    ;       some [T] foo(T) => fooable(T).

:- type foo =< maybe_foo
    --->    some [T] foo(T) => fooable(T).

:- type task
   --->     create(pred(int::in, io::di, io::uo) is det)
   ;        delete(pred(int::in, io::di, io::uo) is det).

:- type create_task =< task
   --->     create(pred(int::in, io::di, io::uo) is det).

A subtype may be exported as an abstract type by declaring only the name of the subtype in the interface section of a module (without the ‘=< supertype’ part). Then the subtype definition must be given in the implementation section of the same module.

Example:

:- interface.

:- type non_empty_list(T).  % abstract type

:- implementation.

:- import list.

:- type non_empty_list(T) =< list(T)
    --->    [T | list(T)].

Subtypes must not have user-defined equality or comparison predicates. The base type of a subtype may have user-defined equality or comparison. In that case, values of the subtype will be tested for equality or compared using those predicates.

There is no special interaction between subtypes and the type class system.


Previous: Abstract types, Up: User-defined types   [Contents]