[m-dev.] proposal for promise_pure scope warning

[Peter Schachte]

Ian MacLarty wrote:
> The problems I've seen are when the user wants to make something pure by
> adding the IO state.  They usually do:
> 
> :- pred pure_p(..., io::di, io::uo) is det.
> 
> pure_p(..., !IO) :-
>     promise_pure ( impure impure_p(...) ).
> 
> Which is wrong.  It should be:
> 
> :- pragma promise_pure(pure_p).
> 
> pure_p(..., !IO) :-
>     impure impure_p(...).

Ouch.  That's a subtle one.  OK, I can imagine this kind of error would be 
much more common than my example, so maybe the warning is worth the 
occasional inconvenience.  But is the singleton purity promise really the 
right criterion?  Isn't the real danger to be warned about a purity promise 
that covers a whole clause body?  That would catch your example, as well as 
this one, which your warning wouldn't catch:

:- pred pure_p(..., io::di, io::uo) is det.

pure_p(..., !IO) :-
      promise_pure ( impure impure_p(...), impure impure q(...) ).

Or maybe it would be better to just thread the IO state from the beginning 
and not use impurity at all?

>> I hope it's not 
>> to conjoin it with a 'true' goal so it won't be a single goal....
> 
> As a last resort you could do that.

Yuck.  But OK, I guess, until someone accidentally changes the compiler to 
eliminate true goals too early during compilation.

> Or put
> --no-warn-singleton-promise-pure-goals in your Mercury.options.

It's not a good idea to globally change compiler options to avoid a local 
problem.  Then you'll miss all the warnings you really do want.

> But
> really when would you actually have a legitimate single impure atomic
> goal in a promise_pure?  You mentioned the case where it could be pure
> with some args and impure with others, but then why wouldn't you move
> the promise_pure up to where you test whether the inputs imply a pure or
> impure call,

Because I don't have to test, I know statically.

> or use a pragma promise_pure instead?

You could do that, but that makes the body of the predicate impure.  Eg, 
think of a function to take a position term and return its equivalent polar 
coordinate.  But the position term has space to store a pointer to a polar 
coordinate term, and if it's non-null, the call should return that.  I've 
also got a nasty, impure predicate to poke a value into a word of memory.  In 
this case I can promise the poke goal to store the pointer to the polar term 
to be pure, even though poke itself is anything but pure.  The body of the 
function is actually pure:  the goals can be executed in any order that 
satisfies the modes.

-- 
Peter Schachte              It is the function of the citizen to keep the
schachte at cs.mu.OZ.AU        Government from falling into error.
www.cs.mu.oz.au/~schachte/      -- Robert H. Jackson
Phone: +61 3 8344 1338
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------