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

[Ralph Becket]

Mark Brown, Wednesday, 14 December 2005:
> 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.

I think the lack of orthogonality is because we treat promise_<purity>
differently from ordinary purity annotations.  If we changed that, this
would not be an issue.

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

I've been thinking for a while now that
- we should allow optional purity annotations on compound goals as well
- promise_<purity> should be a purity annotation just as `impure' and
  `semipure' are, not a scope.

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

Okay.

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

Yes, we've discussed this wart in the past, but nobody has provided a
better name.

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

I'm inclined to agree.
*plonk* - that's the sound of a job landing in your lap :-)
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------