[m-dev.] Solver types: non-canonical types, `any' insts, equality

[Zoltan Somogyi]

On 28-Apr-2004, Fergus Henderson <fjh at cs.mu.OZ.AU> wrote:
> This code telling a lie to the compiler; you're promising that
> there is only one possible representation for A0, but there might be
> more than one.

Being on a very slow link, I have looked at Ralph's proposal only
superficially, but so far, I agree with Fergus's assessment: good,
but don't lie to the compiler.

> To avoid lying to the compiler, you should only promise that the result
> of the predicate as a whole is unaffected by the representations,
> so it should be something like
> 
> 	eq_church(A0, B0) :-
> 		yes = promise_only_solution(pred(
> 			if eq_ch(unwrap(A0), unwrap(B0)) then yes else no
> 		)::out is cc_multi).

However, his proposed solution is cumbersome and inefficient. I have bumped
into this problem before, when I tried to turn set/1 into a non-canonical type,
so it is not a problem unique to solver types. Fergus and I agreed then that
the right way to solve the problem is to add to Mercury a new syntactic
construct that effectively does what the promise_only_solution wrapper does
in Fergus's code above, but with a much more lightweight syntax (similar to
quantification) and implemented as a compiler builtin (the implementation is
after all trivial: a noop). This wasn't my first order of business, so it is
still in my mental in-tray. Any volunteers? :-)

Zoltan.
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------