[m-dev.] proposal for promise_pure scope warning

[Julien Fischer]

On Tue, 15 Apr 2008, Ian MacLarty wrote:

> On Tue, Apr 15, 2008 at 06:19:28PM +1000, Julien Fischer wrote:
>>
>> 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.
>>
>
> Such a check doesn't make any sense to me and I don't think it is
> particularly likely to be an error.
>
> The case that it is likely to be an error is when there is only one
> goal in the promise_pure scope.

The example above covers that case.

> This is likely an error, because in
> effect it is adding a pragma promise_pure to the called predicate.  If
> the called predicate is in fact pure, then why isn't it declared pure?

I don't follow you there - the called predicate is impure, isn't that
what we have been discussing?

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