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:

• equalitypred must be the name of a predicate with signature

  :- pred equalitypred(foo(T1, …, TN)::in,
                  foo(T1, …, TN)::in) is semidet.
  

  It is legal for the type, mode and determinism to be more permissive: the type or the mode’s initial insts may be more general (e.g. the type of the equality predicate could be just the polymorphic type ‘pred(T, T)’) and the mode’s final insts or the determinism may be more specific (e.g. the determinism of the equality predicate could be any of det, failure or erroneous).

• If the type is a discriminated union then its definition cannot be a single zero-arity constructor.
• The equality predicate must be “pure” (see Impurity).
• The equality predicate must be defined in the same module as the type.
• If the type is exported the equality predicate must also be exported.
• equalitypred should be an equivalence relation; that is, it must be symmetric, reflexive, and transitive. However, the compiler is not required to check this ³.

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:

• If the program contains any deconstruction unification or switch on a variable of type T that could fail, other than unifications with mode ‘(in, in)’, then it is a compile-time error.
• If the program contains any deconstruction unification or switch on a variable of type T that cannot fail, then that operation has determinism cc_multi.
• Any attempts to examine the representation of a variable of type T using facilities of the standard library (e.g. ‘argument’/3 and ‘functor/3’ in ‘deconstruct’) that do not have determinism cc_multi or cc_nondet will result in a run-time error.
• In addition to the usual equality axioms, the declarative semantics of the program will contain the axiom ‘X = Y <=> equalitypred(X, Y)’ for all X and Y of type ‘T’.
• Any ‘(in, in)’ unifications for type T are computed using the specified predicate equalitypred.

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:

• comparepred must be the name of a predicate with signature

  :- pred comparepred(builtin.comparison_result::uo,
                  foo(T1, …, TN)::in, foo(T1, …, TN)::in) is det.
  

  As with equality predicates, it is legal for the type, mode and determinism to be more permissive.

• If the type is a discriminated union then its definition cannot be a single zero-arity constructor.
• The comparison predicate must also be “pure” (see Impurity).
• The comparison predicate must be defined in the same module as the type.
• If the type is exported the comparison predicate must also be exported.
• The relation

  compare_eq(X, Y) :- comparepred((=), X, Y).
  

  must be an equivalence relation; that is, it must be symmetric, reflexive, and transitive. The compiler is not required to check this.

• The relations

  compare_leq(X, Y) :- comparepred(R, X, Y), (R = (=) ; R = (<)).
  compare_geq(X, Y) :- comparepred(R, X, Y), (R = (=) ; R = (>)).
  

  must be total order relations: that is they must be antisymmetric, reflexive and transitive. The compiler is not required to check this.

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.