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

[Ralph Becket]

I didn't receive any responses to the e-mail below which I sent three
weeks ago prior to my hols, so I'm tempted to take that as tacit
agreement :-)

If you have anything to say, please do so soon as otherwise I plan to
start implementing it tomorrow (which means ripping out all the
insts-attached-to-fields-in-type-definitions stuff and the need for
inst casts, impure or otherwise).

Can the HAL group members try to review this before tomorrow's meeting?

Ta,
-- Ralph

----- Forwarded message from Ralph Becket <rafe at cs.mu.OZ.AU> -----

Subject: [HAL-dev] Revisiting `any' and inst casts for solver types
From: Ralph Becket <rafe at cs.mu.OZ.AU>
Date: Fri, 30 Apr 2004 16:04:11 +1000
To: Mercury Developers <mercury-developers at cs.mu.OZ.AU>,
        HAL Developers <hal-developers at bowman.csse.monash.edu.au>

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

----- End forwarded message -----
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------