[m-dev.] Rethink of impurity w.r.t. solver code in negated contexts

[Mark Brown]

On 06-Dec-2005, Ralph Becket <rafe at cs.mu.OZ.AU> wrote:
> My recent change to require impurity annotations on goals with solver
> variables in negated contexts was not a good one.
> 
> The problem is that if X has inst any then in
> ( if p(X), q(X) then ...  else ... ) the compiler has no way of knowing
> in general whether the goal p(X), q(X) constrains X or not (constraining
> a non-local solver variable in a negated context is not logically
> sound).
> 
> My recent change required the programmer to instead write
> 
> 	( if impure p(X), impure q(X) then ... else ... )
> 
> to alert the compiler and other programmers that something odd may be
> going on.
> 
> In virtyually all cases, the goal in the condition will be semantically
> pure, so the programmer will actually have to write
> 
> 	promise_pure ( if impure p(X), impure q(X) then ... else ... )
> 
> which is horrible.

I agree with the conclusion, if not with how you arrived at it.  The
problem with the above goal is that it isn't the calls to p/1 and q/1
in the condition which are impure, but the if-then-else construct itself.
Likewise for negations, it is the negation which is impure rather than
the goal inside the negation.

(Actually, I'm not sure that "impure" is the right word here -- we didn't
consider this usage of purity when we devised the purity system.  But that
is a different story.  I agree that "promise" _is_ the right word, and we
can refine the definition of impure if need be.)

> 
> Worse, say the programmer writes
> 
> 	promise_pure ( if impure p(f(X)), impure q(X) then ... else ... )
> 
> then this will be flattened by the compiler into
> 
> 	promise_pure
> 	    ( if V = f(X), impure p(V), impure q(X) then ... else ... )
> 
> which will lead to a purity error because the introduced unification
> should also be impure!

Yes, this is absurd.  And it illustrates my point because the goal `V = f(X)'
is pure.

> 
> NEW PROPOSAL
> 
> I propose instead that the compiler just insist that the offending goal
> or goals be wrapped in a promise_pure context.  That is,
> 
> 	( if promise_pure(p(f(X)), q(X)) then ... else ... )
> 
> This also has the advantage that the compiler can now reorder p/1 and
> q/1, whereas before it could not because they were labelled impure.
> 
> Object now if you want to e'er I start work on this...

Yes, I object to this proposal.  It doesn't make sense that you should
promise that (p(f(X)), q(X)) is pure when it is already known to the
compiler that it is pure.  Indeed, even if it does constrain some of its
variables it can still be pure, so the execution of the code could be
unsound even though the promise was not a lie.

So here's an alternative proposal.  We can currently annotate some goals
with "impure", namely predicate calls and calls to =/2 where one of the
arguments is a function call.  The proposal is that we should also be
allowed to annotate if-then-else goals and negations, and only check that
no "any" insts are used if the goal doesn't have this annotation.

So, you would write the above example as

	impure ( (p(f(X)), q(X)) -> ... ; ... )

and the compiler would accept this code and just treat it as an impure goal
like any other.  Furthermore, if you know that the condition really doesn't
bind any variables then you can safely put your promise in an appropriate
place.  In particular, you could write

	promise_pure_implicit ( ... -> ... ; ... )

and this would mean that you are promising (amongst other things) that the
condition won't bind any variables.

This alternative meets our language design aim for the purity system: all
impure code is explicitly marked (or at least the fact that there is some
implicit impurity is explicit).  It also has the nice property that even if
there is an unsound negation in a program main/2 must still be pure, so if
the program misbehaves we can deduce that there must be a broken promise
somewhere.

(I have a related idea about predicates with 'any' insts which are known
to not bind their arguments, but I think I'll mention that in a separate
thread.)

Cheers,
Mark.

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