[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