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

[Ralph Becket]

Peter Stuckey, Wednesday, 28 April 2004:
> 
>   > For the most part I agree with almost everything that Ralph wrote
>   > in his long email.
>   > 
>   > There's just one minor issue...
>   > 
>   > 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).
> 
> There is only "one" representation of the term. Its not a lie!

No, no, no!  Fergus is right.

When we deconstruct the `church' *value* to get a `ch', the `ch' value
is one possible *representation* of the `church' value (minus its
wrapper).

Taking the more familiar idea of representing sets as unordered lists:

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


:- pred eq(set(T)::in, set(T)::in) is semidet.

eq(A, B) :-
	promise_only_solution(eq_2(A, B)) = yes.

:- pred eq_2(set(T)::in, set(T)::in, bool::out) is cc_multi.

eq_2(A0, B0, Eq) :-
	A0 = set(A),  % A is one possible internal representation of A0
	B0 = set(B),  % B is one possible internal representation of B0
	Eq = ( if   sort_and_remove_dups(A) = sort_and_remove_dups(B)
	       then yes
	       else no
	     ).

Now, set([1, 2]) = set([1, 1, 2]) = set([2, 1]) = ...
but [1, 2] \= [1, 1, 2] \= [2, 1] \= ...

If the deconstructions of A0 and B0 weren't cc_multi then referential
transparency would require that [1, 2] = [1, 1, 2] = [2, 1] = ...

Or, to put it another way, if the deconstructions *weren't* cc_multi
then it would be possible to tell that set([1, 2]) and set([2, 1]) are
different, even though they compare equal.

-- Ralph
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------