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

[Ralph Becket]

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.

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!



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

-- Ralph

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