The type system is based on many-sorted logic, and supports polymorphism, type classes (see Type classes), and existentially quantified types (see Existential types).
This section describes the special types that are built into the Mercury implementation, or are defined in the standard library.
There is a special syntax
for constants of all primitive types except char.
(For char, the standard syntax suffixes.)
There are five primitive signed integer types:
int, int8, int16, int32 and int64.
Except for int,
the width in bits of each of these is given by the numeric suffix in its name.
The width in bits of int is implementation defined,
but must be at least 32-bits.
All signed integer types use two’s-complement representation. Their width must be equal to the width of the corresponding unsigned type.
Values of the type int8 must be in the range
-128 (-(2^{8 - 1})) to 127 (2^{8 - 1} - 1),
both inclusive.
Values of the type int16 must be in the range
-32768 (-(2^{16 - 1})) to 32767 (2^{16 - 1} - 1),
both inclusive.
Values of the type int32 must be in the range
-2147483648 (-(2^{32 - 1}))
to 2147483647 (2^{32 - 1} - 1),
both inclusive.
Values of the type int64 must be in the range
-9223372036854775808 (-(2^{64 - 1}))
to 9223372036854775807 (2^{64 - 1} - 1),
both inclusive.
Values of the type int must be in the range
to -(2^{N - 1}) to 2^{N - 1} - 1,
both inclusive;
N being the width of int in bits.
There are five primitive unsigned integer types:
uint, uint8, uint16, uint32 and uint64.
Except for uint,
the width in bits of each of these is given by the numeric suffix in its name.
The width in bits of uint is implementation defined,
but must be at least 32-bits.
It must be equal to the width of the type int.
Values of the type uint8 must be in the range
0 (2^0 - 1) to 255 (2^8 - 1),
both inclusive.
Values of the type uint16 must be in the range
0 (2^0- 1) to 65535 (2^16 - 1),
both inclusive.
Values of the type uint32 must be in the range
0 (2^0 - 1) to 4294967295 (2^32 - 1),
both inclusive.
Values of the type uint64 must be in the range
0 (2^0 - 1) to 18446744073709551615 (2^64 - 1),
both inclusive.
Values of the type uint must be in the range
0 (2^0 - 1) to 2^N - 1,
both inclusive;
N being the width of uint in bits.
There is one floating-point type: float.
It is represented using either the 32-bit single-precision IEEE 754 format or the 64-bit double-precision IEEE 754 format.
The choice between the two formats is implementation dependent.
In the Melbourne Mercury implementation,
floats are represented
using the 32-bit single-precision IEEE 754 format
in grades that have .spf grade component,
and using the 64-bit double-precision IEEE 754 format in every other grade.
There is one character type: char.
Values of this type represent Unicode code points.
There is one string type: string.
A string is a sequence of characters encoded using either the UTF-8 or UTF-16 encoding of Unicode.
The choice between the two encodings is implementation dependent.
In the Melbourne Mercury implementation,
strings are represented
using UTF-8 when generating code for C,
and using UTF-16 when generating code for C# or Java.
The predicate types are
pred, pred(T), pred(T1, T2), …
The function types are
(func) = T, func(T1) = T, func(T1, T2) = T, …
Higher-order predicate and function types are used to pass closures to other predicates and functions. See Higher-order.
The tuple types are {}, {T}, {T1, T2}, …
A tuple type is equivalent to a discriminated union type (see Discriminated unions) with declaration
:- type {Arg1, Arg2, …, ArgN}
---> { {Arg1, Arg2, …, ArgN} }.
The type univ is defined in the standard library module univ,
along with the predicates type_to_univ/2 and univ_to_type/2.
With those predicates,
values of any type can be converted to the universal type, and back again.
The conversion from univ to the original type
will check that the value inside the univ has the expected type.
The universal type is useful for situations
where you need heterogeneous collections.
The type io.state is defined in the standard library module io,
and represents the state of the world.
Predicates which perform I/O
are passed the only reference to the current state of the world,
and produce a unique reference to the new state of the world.
In this way, we can give a declarative semantics to code that performs I/O.
New types can be introduced with ‘:- type’ declarations. There are several categories of derived types:
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.
These are type abbreviations. They are defined using ‘==’ as follows. They may be polymorphic.
:- type money == int.
:- type assoc_list(KeyType, ValueType)
== list(pair(KeyType, ValueType)).
Equivalence type definitions must be transparent. Unlike discriminated union type definitions, equivalence type definitions must not be cyclic; that is, the type on the left hand side of the ‘==’ (‘assoc_list’ and ‘money’ in the examples above) must not occur on the right hand side of the ‘==’.
Mercury treats an equivalence type as an abbreviation for the type on the right hand side of the definition; the two are equivalent in all respects in scopes where the equivalence type is visible.
These are types whose implementation is hidden. The type declarations
:- type t1. :- type t2(T1, T2).
declare types t1/0 and t2/2 to be abstract types.
Such declarations are only useful in the interface section of a module.
This means that the type names will be exported,
but the constructors (functors) for these types will not be exported.
The implementation section of a module
must give a definition for all of the abstract types
named in the interface section of the module.
Abstract types may be defined as either discriminated union types
or as equivalence types.
(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.
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.
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, where ‘=<’ is the subtype relation below.
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 supertype that has one or more existentially quantified type variables, then the subtype constructor must repeat the list of existentially quantified type variables from the supertype constructor, and all existential class constraints, with no additions, removals, or reordering. (The type variables do not need to have the same names in the subtype as the supertype, but, stylistically, it makes more sense if they do.)
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.)
The subtype relation ‘S =< T’ has four cases to consider: when ‘S’ and ‘T’ are both discriminated union types, when they are both tuple types, when they are both higher-order types, and all other types.
1. For discriminated union types ‘S’ and ‘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.
2. For two tuple types ‘S = {S1, ..., Sn}’ and ‘T = {T1, ..., Tn}’, ‘S =< T’ holds if and only if ‘Si =< Ti’ for all ‘i’ in ‘1..n’. This is analogous to the case for discriminated union types with the same principal type constructor.
3. 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 case for discriminated union types with the same principal type constructor.
4. For all other types, ‘S =< T’ if and only if ‘S = T’, i.e. they are syntactically identical.
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)).
The argument types of each predicate must be explicitly declared with a ‘:- pred’ declaration. The argument types and return type of each function must be explicitly declared with a ‘:- func’ declaration. For example:
:- pred is_all_uppercase(string). :- func strlen(string) = int.
Predicates and functions can be polymorphic; that is, their declarations can include type variables. For example:
:- pred member(T, list(T)). :- func length(list(T)) = int.
A predicate or function can be declared to have a given higher-order type (see Higher-order) by using an explicit type qualification in the type declaration. This is useful where several predicates or functions need to have the same type signature, which often occurs for type class method implementations (see Type classes), and for predicates to be passed as higher-order terms.
For example,
:- type foldl_pred(T, U) == pred(T, U, U). :- type foldl_func(T, U) == (func(T, U) = U). :- pred p(int) : foldl_pred(T, U). :- func f(int) : foldl_func(T, U).
is equivalent to
:- pred p(int, T, U, U). :- pred f(int, T, U) = U.
Type variables in predicate and function declarations are implicitly universally quantified by default; that is, the predicate or function may be called with arguments and (in the case of functions) return value whose actual types are any instance of the types specified in the declaration. For example, the function ‘length/1’ declared above could be called with the argument having type ‘list(int)’, or ‘list(float)’, or ‘list(list(int))’, etc.
Type variables in predicate and function declarations can also be existentially quantified; this is discussed in Existential types.
There must only be one predicate with a given name and arity in each module, and only one function with a given name and arity in each module. It is an error to declare the same predicate or function twice.
There must be at least one clause defined for each declared predicate or function, except for those defined using the foreign language interface (see Foreign language interface). However, Mercury implementations are permitted to provide a method of processing Mercury programs in which such errors are not reported until and unless the predicate or function is actually called. (The Melbourne Mercury implementation provides this with its ‘--allow-stubs’ option. This can be useful during program development, since it allows you to execute parts of a program while the program’s implementation is still incomplete.)
Note that a predicate defined using DCG notation (see Items) will appear to be defined with two fewer arguments than it is declared with. It will also appear to be called with two fewer arguments when called from predicates defined using DCG notation. However, when called from an ordinary predicate or function, it must have all the arguments it was declared with.
The compiler infers the types of expressions, and in particular the types of variables and overloaded constructors, functions, and predicates. A type assignment is an assignment of a type to every variable, and of a particular constructor, function, or predicate to every name in a clause. A type assignment is valid if it satisfies the following conditions.
Each constructor in a clause must have been declared in at least one visible type declaration. The type assigned to each constructor term must match one of the type declarations for that constructor, and the types assigned to the arguments of that constructor must match the argument types specified in that type declaration.
The type assigned to each function call term must match the return type of one of the ‘:- func’ declarations for that function, and the types assigned to the arguments of that function must match the argument types specified in that type declaration.
The type assigned to each predicate argument must match the type specified in one of the ‘:- pred’ declarations for that predicate. The type assigned to each head argument in a predicate clause must exactly match the argument type specified in the corresponding ‘:- pred’ declaration.
The type assigned to each head argument in a function clause must exactly match the argument type specified in the corresponding ‘:- func’ declaration, and the type assigned to the result term in a function clause must exactly match the result type specified in the corresponding ‘:- func’ declaration.
The type assigned to each expression with an explicit type qualification (see Expressions) must match the type specified by the type qualification expression1.
(Here “match” means to be an instance of, i.e. to be identical to for some substitution of the type parameters, and “exactly match” means to be identical up to renaming of type parameters.)
One type assignment A is said to be more general than another type assignment B if there is a binding of the type parameters in A that makes it identical (up to renaming of parameters) to B. If there is more than one valid type assignment, the compiler must choose the most general one. If there are two valid type assignments which are not identical up to renaming and neither of which is more general than the other, then there is a type ambiguity, and compiler must report an error. A clause is type-correct if there is a unique (up to renaming) most general valid type assignment. Every clause in a Mercury program must be type-correct.
Fields of constructors of discriminated union types may be labelled (see Discriminated unions). These labels cause the compiler to generate functions which can be used to select and update fields of a term in a manner independent of the definition of the type.
The Mercury language includes syntactic sugar to make it more convenient to select and update fields inside nested terms (see Field access expressions) and to select and update fields of the DCG arguments of a clause (see Definite clause grammars).
field(Term)
Each field label ‘field’ in a constructor causes generation of a field selection function ‘field/1’, which takes an expression of the same type as the constructor and returns the value of the labelled field, failing if the top-level constructor of the argument is not the constructor containing the field.
If the declaration of the field is in the interface section of the module, the corresponding field selection function is also exported from the module.
By default, this function has no declared modes—the modes are inferred at each call to the function. However, the type and modes of this function may be explicitly declared, in which case it will have only the declared modes.
To create a higher-order value from a field selection function, an explicit lambda expression must be used, unless a single mode declaration is supplied for the field selection function. The reason for this is that normally, field access functions are implemented directly as unifications, without the code of a function being generated for them. The declaration acts as the request for the generation of that code.
'field :='(Term, ValueTerm)
Each field label ‘field’ in a constructor causes generation of a field update function ‘'field :='/2’. The first argument of this function is an expression of the same type as the constructor. The second argument is an expression of the same type as the labelled field. The return value is a copy of the first argument with the value of the labelled field replaced by the second argument. ‘'field :='/2’ fails if the top-level constructor of the first argument is not the constructor containing the labelled field.
If the declaration of the field is in the interface section of the module, the corresponding field update function is also exported from the module.
By default, this function has no declared modes—the modes are inferred at each call to the function. However, the type and modes of this function may be explicitly declared, in which case it will have only the declared modes.
To create a higher-order value from a field update function, an explicit lambda expression must be used, unless a single mode declaration is supplied for the field update function. The reason for this is that normally, as with field selection functions, field update functions are implemented directly as unifications, without the code of a function being generated for them. The declaration acts as the request for the generation of that code.
Some fields cannot be updated using field update functions. For the constructor ‘unsettable/2’ below, neither field may be updated because the resulting term would not be well-typed. A future release may allow multiple fields to be updated by a single expression to avoid this problem.
:- type unsettable
---> some [T] unsettable(
unsettable1 :: T,
unsettable2 :: T
).
Type and mode declarations for compiler-generated field access functions for fields of constructors local to a module may be placed in the interface section of the module. The user-supplied declarations will be used instead of any automatically generated declarations. This allows the implementation of a type to be hidden while still allowing client modules to use record syntax to manipulate values of the type. Supplying a type declaration and a single mode declaration also allows higher-order terms to be created from a field access function without using explicit lambda expressions.
If a field occurs in the interface section of a module, then any declaration for a field access function for that field must also occur in the interface section.
If there are multiple fields with the same label in the same module, only one of those fields can have user-supplied declarations for its selection function. Similarly, only one of those fields can have user-supplied declarations for its update function.
Declarations and clauses for field access functions can also be supplied for fields which are not a part of any type. This is useful when the data structures of a program change so that a value which was previously stored as part of a type is now computed each time it is requested. It also allows record syntax to be used for type class methods.
User-declared field access functions may take extra arguments.
For example, the Mercury standard library module map
contains the following functions:
:- func elem(K, map(K, V)) = V is semidet. :- func 'elem :='(K, map(K, V), V) = map(K, V).
Field access syntax may be used
at the top-level of func and mode declarations
and in the head of clauses.
For instance:
:- func map(K, V) ^ elem(K) = V. :- mode in ^ in = out is semidet. Map ^ elem(Key) = map.lookup(Map, Key). :- func (map(K, V) ^ elem(K) := V) = V. :- mode (in ^ in := in) = out is semidet. (Map ^ elem(Key) := Value) = map.set(Map, Key, Value).
The Mercury standard library modules array and bt_array
define similar functions.
The examples make use of the following type declarations:
:- type type1
---> type1(
field1 :: type2,
field2 :: string
).
:- type type2
---> type2(
field3 :: int,
field4 :: int
).
The compiler generates some field access functions for ‘field1’. The functions generated for the other fields are similar.
:- func type1 ^ field1 = type2. type1(Field1, _) ^ field1 = Field1. :- func (type1 ^ field1 := type2) = type1. (type1(_, Field2) ^ field1 := Field1) = type1(Field1, Field2).
Using these functions and the syntactic sugar described in Field access expressions, programmers can write code such as
:- func type1 ^ increment_field3 = type1.
Term0 ^ increment_field3 =
Term0 ^ field1 ^ field3 := Term0 ^ field1 ^ field3 + 1.
The compiler expands this into
increment_field3(Term0) = Term :-
OldField3 = field3(field1(Term0)),
OldField1 = field1(Term0),
NewField1 = 'field3 :='(OldField1, OldField3 + 1),
Term = 'field1 :='(Term0, NewField1).
The field access functions defined in the Mercury standard library module ‘map’ can be used as follows:
:- func update_field_in_map(map(int, type1), int, string)
= map(int, type1) is semidet.
update_field_in_map(Map, Index, Value) =
Map ^ elem(Index) ^ field2 := Value.
For (almost) every Mercury type there exists a standard ordering;
any two values of the same type can be compared under this ordering
by using the builtin.compare/3 predicate.
The ordering is total, meaning that the corresponding binary relations
are reflexive, transitive and anti-symmetric.
The one exception is higher-order types,
which cannot be unified or compared;
any attempt to do so will raise an exception.
The existence of this ordering makes it possible to implement generic data structures such as sets and maps, without needing to know the specifics of the ordering. Furthermore, different platforms often have their own natural orderings which are not necessarily consistent with each other. As such, the standard ordering for most types is not fully defined.
For the primitive integer types, the standard ordering is the usual numerical ordering. Implementations should reject code containing overflowing integer literals.
For the primitive type float,
the standard ordering approximates the usual numerical ordering.
If the result of builtin.compare/3 is (<) or (>)
then this relation holds in the numerical ordering,
but this is not necessarily the case for (=) due to lack of precision.
In the standard ordering, “negative” and “positive” zero values are equal.
Implementations should replace overflowing literals
with the infinity of the same sign;
in the standard ordering positive infinity is greater than all finite values
and negative infinity is less than all finite values.
Implementations must throw an exception when comparing
a “not a number” (NaN) value.
For the primitive type char,
the standard ordering is
the numerical ordering of the Unicode code point values.
For the primitive type string,
the standard ordering is implementation dependent.
The current implementation performs string comparison using
the C strcmp() function,
the Java String.compareTo() method, and
the C# System.String.CompareOrdinal() method,
when compiling to C, Java and C# respectively.
For tuple types, corresponding arguments are compared, with the first argument being the most significant, then the second, and so on.
For discriminated union types (other than subtypes),
if both values have the same principal constructor
then corresponding arguments are compared in order,
with the first argument being the most significant,
then the second, and so on.
If the values have different principal constructors,
then the value whose principal constructor
is listed first in the definition of the type
will compare as less than the other value.
There is one exception from this rule:
in types that are subject to a foreign_enum pragma,
the outcomes of comparisons are decided
by user’s chosen foreign language representations,
using the rules of the foreign language.
For subtypes, the two values compare as though converted to the base type. The ordering of constructors in a subtype definition does not affect the standard ordering.
The type of an explicitly type qualified term may be an instance of the type specified by the qualifier. This allows explicit type qualifications to constrain the types of two expressions to be identical, without knowing the exact types of the expressions. It also allows type qualifications to refer to the types of the results of existentially typed predicates or functions.
Previous: Field access functions, Up: Types [Contents]