3.2.1 Discriminated unions

These encompass both enumeration and record types in other languages. A derived type is defined using ‘:- type type ---> body’. (Note there are three dashes in that arrow. It should not be confused with the two-dash arrow used for DCGs or the one-dash arrow used for if-then-else.) If the type term is a functor of arity zero (i.e. one having zero arguments), it names a monomorphic type. Otherwise, it names a polymorphic type; the arguments of the functor must be distinct type variables. The body term is defined as a sequence of constructor definitions separated by semicolons.

Ordinarily, each constructor definition must be a functor whose arguments (if any) are types. Ordinary discriminated union definitions must be transparent: all type variables occurring in the body must also occur in the type. (The reverse is not the case: a variable occurring in the type need not also occur in the body. Such variables are called ‘phantom type parameters’, and their use is explained below.)

However, constructor definitions can optionally be existentially typed. In that case, the functor will be preceded by an existential type quantifier and can optionally be followed by an existential type class constraint. For details, see Existential types. Existentially typed discriminated union definitions need not be transparent.

The arguments of constructor definitions may be labelled. These labels cause the compiler to generate functions which can be used to conveniently select and update fields of a term in a manner independent of the definition of the type (see Field access functions). A labelled argument has the form fieldname :: Type. It is an error for two fields in the same type to have the same label.

Here are some examples of discriminated union definitions:

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

:- type strange
        --->    foo(int)
        ;       bar(string).

:- type employee
        --->    employee(
                       name        :: string,
                       age         :: int,
                       department  :: string
                ).

:- type tree
        --->    empty
        ;       leaf(int)
        ;       branch(tree, tree).

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

:- type pair(T1, T2)
        --->    T1 - T2.

If the body of a discriminated union type definition contains a term whose top-level functor is ';'/2, the semicolon is normally assumed to be a separator. This makes it difficult to define a type whose constructors include ';'/2. To allow this, curly braces can be used to quote the semicolon. It is then also necessary to quote curly braces. The following example illustrates this:

:- type tricky
        --->    { int ; int }
        ;       { { int } }.

This defines a type with two constructors, ';'/2 and '{}'/1, whose argument types are all int. We recommend against using constructors named '{}' because of the possibility of confusion with the builtin tuple types.

Each discriminated union type definition introduces a distinct type. Mercury considers two discriminated union types that have the same bodies to be distinct types (name equivalence). Having two different definitions of a type with the same name and arity in the same module is an error.

Constructors may be overloaded among different types: there may be any number of constructors with a given name and arity, so long as they all have different types. However, there must not be more than one constructor with the same name, arity, and result type in the same module. (There is no particularly good reason for this restriction; in the future we may allow several such functors as long as they have different argument types.) Note that excessive overloading of constructors can slow down type checking and can make the program confusing for human readers, so overloading should not be over-used.

Note that user defined types may not have names that have meanings in Mercury. (Most of these are documented in later sections.)

The list of reserved type names is

int
int8
int16
int32
int64
uint
uint8
uint16
uint32
uint64
float
character
string
{}
=
=<
pred
func
pure
semipure
impure
''

Phantom type parameters are useful when you have two distinct concepts that you want to keep separate, but for which nevertheless you want to use the representation. This is an example of their use, taken from the Mercury compiler:

:- type var(T)
        --->    ...

:- type prog_var == var(prog_var_type).
:- type type_var == var(type_var_type).

:- type prog_var_type
    --->    prog_var_type.
:- type type_var_type
    --->    type_var_type.

The var type represents the generic notion of a variable. It has a phantom type parameter, T, which does not occur in the body of its type definition. The prog_var and type_var types represent two different specific kinds of variables: program variables, which occur in code (clauses), and type variables, which occur in types, respectively. They each bind a different type to the type parameter T. These types, prog_var_type and type_var_type, each have a single function symbol of arity zero. This means that each type has only one value, which in turn means that values of these types contain no information at all. But containing information is not the purpose of these types. Their purpose is to ensure that if ever a computation that expects program variables is ever accidentally given type variables, or vice versa, this mismatch is detected and reported by the compiler. Two variables can be unified only if they have the same type. While two prog_vars have the same type, and two type_vars have the same type, a prog_var and type_var have different types, due to having different types (prog_var_type and type_var_type) being bound to the phantom type parameter T.