[m-rev.] For review: change the way we handle inst any non-locals in negated contexts (again)

[Mark Brown]

On 13-Dec-2005, Ralph Becket <rafe at cs.mu.OZ.AU> wrote:
> Undo my recent changes to purity error checking in the context of inst any
> non-locals in negated contexts.
> 
> Implement a better way of handling the problem, as discussed on the mailing
> list.  The new solution is to require that any goals featuring inst any 
> non-locals in a negated context must appear in a
> promise_{pure,semipure,impure} context.

This isn't quite the solution that was discussed on the mailing list.  The
solution we discussed is that negations/if-then-elses which may bind inst
'any' non-locals in a negated context should be inferred to be impure, and
must be explicitly marked as such (unless in a promise_pure_implicit scope).

For example, if Cond binds a non-local variable then we can do one of the
following:

1) Mark it impure and wrap it in a promise_pure scope:

	promise_pure ( impure ( Cond -> Then ; Else ) )

2) Mark it impure but leave the impurity to be resolved elsewhere:

	impure ( Cond -> Then ; Else )

3) Use promise_pure_implicit to save us the hassle of marking it impure:

	promise_pure_implicit (
		...,
		( Cond -> Then ; Else ),
		...
	).

The rationale is orthogonality: goals which introduce impurity should be
treated the same way regardless of whether they are calls to impure
predicates, unifications containing a call to an impure function, or impure
negations/if-then-elses.  The three options we have above are the same
three options that we have for dealing with the already existing ways of
introducing impurity.  Is there any reason why the new way should be
different?

> This is something of a compromise:
> on the one hand it does require that the condition be explicitly recognised
> by the programmer; on the other, it does not require that the "offending" goals
> be individually identified

I don't think you need to say this.  Bear in mind that when we say "inst 'any'
non-locals" we mean those that are non-local to the negation/if-then-else.
The offending goal is the negation or if-then-else, and according to the
solution we had settled on it _is_ the one which is identified.

(And not to put too fine a point on it, "impure" is what we use to explicitly
recognise that impurity has been introduced.  The solution you have here
leads to programs that have a promise_pure scope, with no apparent (that is,
explicit) impurity introduced inside.)

> (this is partly for pragmatic reasons: the earlier
> approach required a plethora of awkward impurity declarations on goals that
> would otherwise be considered completely pure).

I totally agree with the reason, but I wouldn't describe it as pragmatic.
Requiring an impurity annotation on a goal that would, in another context,
not require one is Just Plain Wrong.

Cheers,
Mark.

--------------------------------------------------------------------------
mercury-reviews mailing list
post:  mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------