[m-dev.] Revisiting `any' and inst casts for solver types

[Ralph Becket]

Discussion in yesterday's HAL group meeting indicated that we may be
able to do away with the need for inst casts with solver types.

As I understand it, `any' *should be* similar to `ground' in the
following sense:

- inst `ground' applied to a variable X of type t with data constructors c1,
  c2, ..., cN means that X will be bound to one of c1, c2, ..., or cN,
  each of whose fields will also be `ground';

- inst `any' applied to a variable X of type t with data constructors c1,
  c2, ..., cN means that X will be bound to one of c1, c2, ..., or cN,
  each of whose fields will also be `any'.

The difference between the two is that the set of values that unify with
a `ground' value form an equivalence class whereas the set unifying with
an `any' value may not.

If the compiler actually did understand `any' this way then there
wouldn't seem to be any need for an inst cast (impure or otherwise) and
the whole slightly sordid business of attaching insts to the fields of
solver type data constructors could be done away with.

Going back to the Church numerals example, here's how things might look
with "real" `any' insts:


:- solver type church ---> church(ch)
	where initialisation is init, equality is eq.

:- type ch ---> z ; s(church) ; v(...).


:- pred eq(church::in(any), church::in(any)) is semidet.

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


:- pred eq_2(church::in(any), church::in(any), bool::out) is cc_multi.

eq_2(A0, B0, Eq) :-
	unwrap(A0, ChA),
	unwrap(B0, ChB),
	Eq = ( if eq_ch(ChA, ChB) then yes else no ).

	% In case anyone is bothered by the sheer tedium of the
	% promise_only_solution bit and eq_2, we can make most of that
	% go away by providing a suitable higher order utility predicate
	% for the job.


:- pred unwrap(church::in(any), ch::out(any)) is cc_multi.

unwrap(church(Ch), Ch).


:- pred eq_ch(ch::in, ch::in) is semidet.
:- pragma promise_pure(eq_ch/2).

eq_ch(z,    z   ).
eq_ch(s(C), s(C)).
eq_ch(v(V), B   ) :- ... impure stuff ...


I can't see where we need (impure) inst casts here - can anyone else see
a problem?

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