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

[Mark Brown]

On 14-Dec-2005, Ralph Becket <rafe at cs.mu.OZ.AU> wrote:
> Mark Brown, Wednesday, 14 December 2005:
> > 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:   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
> > [...]
> > 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?
> 
> There is one key difference: we can't know whether a non-local solver
> var is being constrained in a negated context or not.

That's not really a difference.  With the existing impurity you also can't
know whether the impure thing really will happen.  For example, the goal

	impure maybe_do_impure_thing(Bool, ...)

may be known to be pure if Bool is 'no', but you still need to say that it
is impure and then promise otherwise.  So I still don't see that the
non-orthogonality is justified.

If you're really concerned about declaring something impure when it isn't,
then I'd be happy to allow 'promise_pure ( Goal )' as an abbreviation of
'promise_pure ( impure Goal )'.  That is, you can drop the impure annotation
if there is a promise immediately after the introduction of the impurity.
But this should also apply to the other ways of introducing impurity, so
that the purity system remains orthogonal.

If you are going to insist on non-orthogonality, then for the sake of the
sanity of our users it will need to be made much clearer in the reference
manual that the purity system works differently for negations/if-then-elses
than for other impure goals.

On another note, if you want to write an if-then-else which really is impure,
but not because of 'any' insts in the condition, then it appears you have to
put it in a "promise_impure" scope.  I reiterate my view that "promise_impure"
is a misnomer -- a promise is exactly what it ain't -- and point out that
what you really mean here is "impure".  Moreover, the documentation of
promise_impure in the reference manual bears no resemblance to what it
actually means in this case.  Other places where promise_impure is supposedly
required can be equally (or better) served by an "impure_true" goal, similar
in spirit to semidet_succeed, so I don't see that promise_impure is in any
way defensible.  Can we please rid ourselves of promise_impure before anyone
becomes accustomed to it?

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