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

Perhaps I should have said "as inspired by discussion 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:   ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
> [...]
> 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.  Consider
any_list.det_head:

:- pred any_list.det_head(list(T)::ia, T::oa) is semidet.
any_list.det_head(Xs, X) :-
	( if Xs = [X0 | _] then X = X0 else throw("empty list") ).

Note that the list spine is not a solver type, but the list members are.
The condition features inst any non-locals, but does not further
constrain them.  If, instead, the condition used some auxiliary
predicate instead of a deconstruction then there'd be no way in
general of deciding.

It therefore isn't at all clear whether something impure is really
happening or not, which makes this a legitimate use for purity promises.

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

But the negation/if-then-else may not be impure at all.  Your approach
requires the programmer to say something is impure, regardless of
whether it is or not, and *then* promise otherwise.

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