[m-dev.] proposal: user-defined equality predicates

Fergus Henderson fjh at cs.mu.oz.au
Fri Jun 27 16:47:31 AEST 1997


Peter Schachte, you wrote:
> On Thu, 26 Jun 1997, Fergus Henderson wrote:
> 
> >    For types such as this, which do not have a canonical representation,
> > the standard definition of equality is the desired one; we want
> 
> ... is *not* the desired one...

Oops ;-)

> > To support such types, Mercury allows
> > programmers to specify a user-defined equality predicate for
> > user-defined types:
> > 
> >      :- type set(T) ---> set(list(T))
> >      	where equality is set_equals.
> 
> I have one reservation about this syntax:  it doesn't allow easy later
> extension to support unification of values of different types (but, I
> would hope, of the same type class).

Well, if you have any suggestions for an alternative syntax...

> >    * EQUALITYPRED must be the name of a predicate with type `pred(T,
> >      T)' and mode `(in, in) is semidet'.
> 
> What if there are other declared modes?  Are they currently ignored for
> unification, or are they used where appropriate?

They're ignored.  (Well, the implementation could in theory implement
unification as calls to them, but for purposes of determinism analysis,
etc. they're ignored.)

> >    * 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.
> 
> I guess this answers my last question.  Is this a limitation that can
> later be lifted (to say something like "other than unifications of a mode
> which is a declared mode for the EQUALITYPRED.")?

Yes, this limitation could potentially be lifted later.

> >    * 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'.
> 
> Is there some way to turn this back to det?  I'd like to be able to
> promise that the code I'm writing will compute the same solutions for any
> concrete representation of the abstract type.

Well, you can use the following code.  It's quite inefficient and
not very elegant though, and it is potentially implementation-specific,
so I'd like a better method.

:- func assert_unique(pred(T)) = T.
:- mode assert_unique(pred(out) is cc_nondet) = out is semidet.
:- mode assert_unique(pred(out) is cc_multi) = out is det.

assert_unique(Pred) = OutVal :-
	call(cc_cast(Pred), OutVal).

:- func cc_cast(pred(T)) = pred(T).
:- mode cc_cast(pred(out) is cc_nondet) = out(pred(out) is semidet) is det.
:- mode cc_cast(pred(out) is cc_multi) = out(pred(out) is det) is det.

:- pragma c_code(cc_cast(X::(pred(out) is cc_multi)) =
			(Y::out(pred(out) is det)),
		will_not_call_mercury,
		"Y = X;").
:- pragma c_code(cc_cast(X::(pred(out) is cc_nondet)) =
			(Y::out(pred(out) is semidet)),
		will_not_call_mercury,
		"Y = X;").

-- 
Fergus Henderson <fjh at cs.mu.oz.au>   |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>   |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3         |     -- the last words of T. S. Garp.



More information about the developers mailing list