[m-dev.] proposal for promise_pure scope warning

[Ian MacLarty]

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

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