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

[Fergus Henderson]

For the most part I agree with almost everything that Ralph wrote
in his long email.

There's just one minor issue...

On 27-Apr-2004, Ralph Becket <rafe at cs.mu.OZ.AU> wrote:
> Let us revisit the Church numerals solver type, but this time I'm going
> to use *two*: an "outer", non-canonical type, and an "inner" canonical
> type.
> 
> Here's how it would look:
> 
> 	% The "outer" type (non-canonical).
> 	%
> :- solver type church ---> church(ch `with_inst` any)
> 	where initialisation is init_church, equality is eq_church.
> 
> 	% The "inner" type (canonical).
> 	%
> :- solver type ch ---> z ; s(church `with_inst` any) ; v(...)
> 	where initialisation is init_ch.
> 
> Now we define equality for church/0 like this:
> 
> :- pred eq_church(church::in(any), church::in(any)) is semidet.
> 
> eq_church(A0, B0) :-
> 	A = promise_only_solution(unwrap(A0)),
> 	B = promise_only_solution(unwrap(B0)),
> 	eq_ch(A, B).

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.

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).

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