[m-dev.] proposal for promise_pure scope warning

[Julien Fischer]

On Tue, 15 Apr 2008, Ian MacLarty wrote:

> On Tue, Apr 15, 2008 at 05:09:43PM +1000, Julien Fischer wrote:
>>
>> On Tue, 15 Apr 2008, Julien Fischer wrote:
>>
>>>
>>> On Tue, 15 Apr 2008, Ian MacLarty wrote:
>>>
>>>> ( promise_pure ( impure p ) ->
>>>>    true
>>>> ;
>>>>    true
>>>> )
>>>> The same applies to the case where there is output, but the output is
>>>> not used.
>>>>> (Which is the "bug" I assume you are trying to address here)
>>>> That is a symptom, but the underlying problem is that purity is being
>>>> promised away in the wrong spot.  A goal like:
>>>>    promise_pure ( impure p )
>>>> just makes no sense (regardless of the determinism), because either the
>>>> goal should be impure, or p itself should be pure.
>>>
>>> The G12 FD solver uses constructs like the above extensively (which
>>> is one reason I don't want any warning to be enabled by default).
>>
>> Actually, calls to the automatically generated solver type casting
>> functions is another case where one may legitimatly have something of
>> the form:
>>
>> 	promise_pure (impure p).
>>
>
> If you say so.
>
> I don't think having a warning that is turned off by default is going to
> be very useful, so scrap the idea.

zs popped into the office before and mentioned a few things:

(1) the whole point of promises is that they are for things that the
compiler cannot check, so trying to insert such check is in general
pointless, ..., however

(2) the specific case you encountered in the benchmarking code may
be worth checking for, e.g. where you have


 	p(..., !IO) :-
 		promise_pure (
 			<top_level_goal>
 		).

i.e, a purity promise around the top-level goal (and only around that)
and the predicate takes an I/O state pair is likely to be an error,
and may be worth warning about.

(3) his preferred fix for the benchmarking code would be to  put
an explicit unification for the I/O state inside the promise_pure scope
rather than use a pragma.  (I guess (2) should be modified so that there
is no warning if there is such a unification.)

Julien.
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at csse.unimelb.edu.au
Administrative Queries: owner-mercury-developers at csse.unimelb.edu.au
Subscriptions:          mercury-developers-request at csse.unimelb.edu.au
--------------------------------------------------------------------------