Next: , Previous: Determinism, Up: Top   [Contents]


7 User-defined equality and comparison

When defining abstract data types, often it is convenient to use a non-canonical representation — that is, one for which a single abstract value may have more than one different possible concrete representation. For example, you may wish to implement an abstract type ‘set’ by representing a set as an (unsorted) list.

:- module set_as_unsorted_list.
:- interface.
:- type set(T).

:- implementation.
:- import_module list.
:- type set(T)
    --->    set(list(T)).

In this example, the concrete representations ‘set([1,2])’ and ‘set([2,1])’ would both represent the same abstract value, namely the set containing the elements 1 and 2.

For types such as this, which do not have a canonical representation, the standard definition of equality is not the desired one; we want equality on sets to mean equality of the abstract values, not equality of their representations. To support such types, Mercury allows programmers to specify a user-defined equality predicate for user-defined types (not including subtypes):

:- type set(T)
    --->    set(list(T))
            where equality is set_equals.

Here ‘set_equals’ is the name of a user-defined predicate that is used for equality on the type ‘set(T)’. It could for example be defined in terms of a ‘subset’ predicate.

:- pred set_equals(set(T)::in, set(T)::in) is semidet.
set_equals(S1, S2) :-
    subset(S1, S2),
    subset(S2, S1).

A comparison predicate can also be supplied.

:- type set(T)
    --->    set(list(T))
            where equality is set_equals, comparison is set_compare.

:- pred set_compare(builtin.comparison_result::uo,
    set(T)::in, set(T)::in) is det.

set_compare(Result, Set1, Set2) :-
    promise_equivalent_solutions [Result] (
        set_compare_2(Set1, Set2, Result)
    ).

:- pred set_compare_2(set(T)::in, set(T)::in,
    builtin.comparison_result::uo) is cc_multi.

set_compare_2(set(List1), set(List2), Result) :-
    builtin.compare(Result, list.sort(List1), list.sort(List2)).

If a comparison predicate is supplied and the unification predicate is omitted, a unification predicate is generated by the compiler in terms of the comparison predicate. For the ‘set’ example, the generated predicate would be:

set_equals(S1, S2) :-
    set_compare((=), S1, S2).

If a unification predicate is supplied without a comparison predicate, the compiler will generate a comparison predicate which throws an exception of type ‘exception.software_error’ when called.

A type declaration for a type ‘foo(T1, …, TN)’ may contain a ‘where equality is equalitypred’ specification only if it declares a discriminated union type or a foreign type (see Using foreign types from Mercury) and the following conditions are satisfied:

Types with user-defined equality can only be used in limited ways. Because there are multiple representations for the same abstract value, any attempt to examine the representation of such a value is a conceptually non-deterministic operation. In Mercury this is modelled using committed choice nondeterminism.

The semantics of specifying ‘where equality is equalitypred’ on the type declaration for a type T are as follows:

A type declaration for a type ‘foo(T1, …, TN)’ may contain a ‘where comparison is comparepred’ specification only if it declares a discriminated union type or a foreign type (see Using foreign types from Mercury) and the following conditions are satisfied:

For each type for which the declaration has a ‘where comparison is comparepred’ specification, any calls to the standard library predicate ‘builtin.compare/3’ with arguments of that type are evaluated as if they were calls to comparepred.

A type declaration may contain a ‘where equality is equalitypred, comparison is comparepred’ specification only if in addition to the conditions above, ‘all [X, Y] (comparepred((=), X, Y) <=> equalitypred(X, Y))’. The compiler is not required to check this.


Footnotes

(3)

If equalitypred is not an equivalence relation, then the program is inconsistent: its declarative semantics contains a contradiction, because the additional axioms for the user-defined equality contradict the standard equality axioms. That implies that the implementation may compute any answer at all (see Semantics), i.e. the behaviour of the program is undefined.


Next: , Previous: Determinism, Up: Top   [Contents]