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).

As previously described, the syntax for non-subtype discriminated union types is

:- type type ---> body.

where type is the name of a type constructor applied to zero or more distinct type variables (the parameters of the type constructor), and body is a sequence of constructor definitions separated by semicolons. All universally quantified type variables that occur in body must be among type’s parameters.

The syntax for subtypes is similar but slightly different:

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

Since a subtype is also a discriminated union type, the rules for discriminated union types apply to them as well: subtype must be the name of a type constructor applied to zero or more distinct type variables (its parameters), body must be a sequence of constructor definitions separated by semicolons, and all universally quantified type variables that occur in body must be among subtype’s parameters.

supertype must be a type constructor applied to zero or more argument types, which may be type variables, but they do not have to be, and if they are, do not need to be distinct. After expanding out equivalences, supertype’s principal type 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 the chain of subtype definitions, it must be possible to arrive at a base type, which is a discriminated union type but not a subtype.

The body of the subtype may differ from the body of its supertype in two ways.

• It may omit one or more constructor definitions. The ability to do this is the main motivation for the use of subtypes.

  Since the subtype cannot add definitions of constructors, the set of constructor definitions in the subtype must be a subset of the constructors definitions in the supertype. We recommend that they should appear in the same relative order as in the supertype definition.

• It may change the types of some of the arguments of some of the constructors, provided that each replacement replaces a type with one of its subtypes.

  Formally, this means that if the supertype ‘t’ has a constructor ‘f(T1, ..., Tn)’, and the subtype ‘s =< t’ has a constructor ‘f(S1, ..., Sn)’. then for each Si, the condition ‘Si =< Ti’ must hold.

This is an example of the first kind of difference:

:- type fruit
    --->    apple
    ;       pear
    ;       lemon
    ;       orange.

:- type citrus_fruit =< fruit
    --->    lemon
    ;       orange.

And this is an example of the second:

:- type fruit_basket
    --->    basket(fruit, int).
            % What kind of fruit, and how many.

:- type citrus_fruit_basket =< fruit_basket
    --->    basket(citrus_fruit, int).

(There are more examples below.)

If the subtype retains a constructor from the super type that has one or more existentially quantified type variables, then there must be a one-to-one mapping between the existentially quantified type variables for the 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.

As mentioned above, any universally quantified type variable that occurs in body must occur also in subtype. However, this is the only restriction on the list of parameters in subtype. For example, it need not have any particular relationship with the list of parameters of the principal type constructor of supertype. For example, subtype may have a phantom type parameter (see Discriminated unions) that does not occur in supertype.

(In the following discussion, we assume that all equivalence types have been expanded out.)

Mercury considers it possible for a type ‘S’ to be a subtype of type ‘T’, where ‘S != T’, in two cases: where ‘S’ and ‘T’ are both discriminated union type, and where they are both higher order types. In every other case, ‘S’ is a subtype of ‘T’, denoted ‘S =< T’, if and only if ‘S’ and ‘T’ are syntactically identical, i.e. ‘S = T’.

A discriminated union type ‘S’ can be a subtype of another discriminated union type ‘T’ in two distinct ways:

• If ‘S’ and ‘T’ have the same principal type constructor, say f/n, which implies that ‘S = f(S1, ..., Sn)’ and ‘T = f(T1, ..., Tn)’, then ‘S =< T’ holds if and only if for all i in ‘1..n’, ‘Si =< Ti’.
• If ‘S’ and ‘T’ have different principal type constructors, and if ‘S = f(S1, ..., Sn)’, ‘S =< T’ holds if
  • - there is a visible subtype definition starting with ‘:- type f(R1, ..., Rn) =< U’,
  • - for all i in ‘1..n’, ‘Si = Ri’ (unification), and
  • - ‘U =< T’.

  In other words, if all occurrences of Ri in U are replaced by the corresponding for Si to give Usub, then ‘Usub =< T’ must hold.

A higher order type ‘S’ can be a subtype of another higher order type ‘T’ in only one way. Since subtype definitions do not apply to higher order types, this way is analogous to the first way above.

• ‘P =< Q’ holds for two higher-order types P and Q if and only if all of the following conditions hold:
  • - P and Q are either both ‘pred’ types, or both ‘func’ types,
  • - they have the same arity,
  • - P and Q have the same argument types (the current implementation does not allow subtyping in higher-order arguments), and
  • - if either of P and Q has higher-order inst information, then P and Q must have the same higher order inst information, i.e. their higher order inst information must specify the same argument modes, determinism, and purity.

In every case not covered above, ‘S =< T’ if and only if ‘S = T’.

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.

Some more examples of subtypes:

:- 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).

And one more complex example.

In the case of a set of mutually recursive types, omitting some constructor definitions from a type may not be enough; it may be necessary to replace some argument types with their subtypes as well. Consider this pair of mutually recursive types representing a bipartite graph, i.e. a graph in which there are two kinds of nodes, and edges always connect two nodes of different kinds. In this bipartite graph, the two kinds of nodes are or nodes and and nodes, and each kind of node can be connected to zero, two or more nodes of the other kind.

:- type or_node
    --->    or_source(source_id)
    ;       logical_or(and_node, and_node)
    ;       logical_or_list(and_node, and_node, and_node, list(and_node)).

:- type and_node
    --->    and_source(source_id)
    ;       logical_and(or_node, or_node)
    ;       logical_and_list(or_node, or_node, or_node, list(or_node)).

If we wanted a subtype to represent graphs in which no or node could be connected to more than two and nodes, one might think that it would be enough to delete the logical_or_list constructor from the or_node type, like this:

:- type binary_or_node =< or_node
    --->    or_source(source_id)
    ;       logical_or(and_node, and_node).

However, this would not work, because the and_nodes have constructors whose arguments have type or_node, not binary_or_node. One would have to create a subtype of the and_node type that constructs and nodes from binary_or_nodes, not plain or_nodes, like this:

:- type binary_or_node =< or_node
    --->    or_source(source_id)
    ;       logical_or(binary_or_and_node, binary_or_and_node).

:- type binary_or_and_node =< and_node
    --->    and_source(source_id)
    ;       logical_and(binary_or_node, binary_or_node)
    ;       logical_and_list(binary_or_node, binary_or_node, binary_or_node,
                list(binary_or_node)).