[m-dev.] Fw: Re: Impurity annotations on clauses

[Peter Schachte]

Mark Brown wrote:

> When the existing purity system came about, there were really two situations
> in mind:
> 
> 	1) Having outputs that depend on some implicit state.
> 
> 	2) Updating some implicit state.

Actually, the original problem that lead to the purity system was implementing
all-solutions predicates.  Prior to the purity system, they were implemented
with some really painful, subtle C code.  I guess you could call that "implicit
state," but since it's non-backtrackable, I think of it a bit differently.

But I agree the original intention was that only small chunks of code would be
 impure.

[I've reordered your message below to make it easier to reply to.]

> Since then we have identified several new situations which introduce impurity:
> 
> 	3) Having outputs that depend on the instantiation state of a
> 	variable.  We consider this to be different to 1 because we don't
> 	want to interpret the constraint store as implicit state -- doing
> 	so would oblige us to call every constraint impure, even those
> 	with a pure semantics.

> Situation 3 is not really as harmful as 1 or 2 (IMHO), so a different
> annotation (e.g., "ask") may be in order.

So you're saying Prolog's var/1 isn't as harmful as hidden state?  I'm not
convinced.

> The requirements on using this
> annotation may not need to be as strict as those for "impure".  For example,
> it might be reasonable to allow the annotation on a goal to apply to function
> calls inside the goal, so that the following would be allowed:
>
> 	ask p(get_min(X), get_max(X), ...)
>
> where currently you would need to write something like
>
> 	impure Min = get_min(X),
> 	impure Max = get_max(X),
> 	p(Min, Max, ...)

The thing in this example is that p/? must not depend too heavily on it's first
two arguments.  It can only count on get_min(X) =< X =< get_max(X), not on them
having any particular values.

What worries me about this example is that you're using functional notation
without referential transparency.  How about something like this:

	some [Min, Max] (
		Min =< X,
		X <= Max,
		p(Min, Max, ...)
	)

This is almost right.  We just need a pragma to say that for any values of Min
and Max that satisfy the constraints, the outputs of p are the same (I forget
the syntax for this one).  Then we add new cc_multi modes for =<, and use
sequential conjunction on either side of this, to force it to be executed when
you want.  Look, Ma, no impurity!

Another approach, where the values that don't depend on which bounds for X we
choose don't appear until later in the computation, would be to have the
predicate that gets the bounds for X acknowledge that it uses the constraint
store as a resource, which would prevent goals that could modify that resource
(by adding constraints) from being reordered with respect to it.  No impurity
that way, either, though you have to be aware of the resource.

> 	4) Mode specific clauses (similar to 3).

I think of these like foreign code:  they're an opportunity to get the logic
wrong, so you should be obliged to certify that you haven't.  I don't see
what's wrong with promise_pure for these.

> 	5) Referentially opaque functions.  These can occur if a function's
> 	return value has inst `any'.  E.g., a function that returns a new
> 	integer variable with bounds (1, 10) does not always return the
> 	same value, even though the arguments might be the same.

That's not a function; why would you want to use functional notation for it?
If you do, I think you should declare it impure.

> 	6) Negated contexts which *may* constrain solver variables.

> situation 6 could be mitigated by extending the compiler's ability
> to prove that solver variables aren't constrained.  One way to do this
> would be to introduce a new mode which is like `any >> any', but which is
> guaranteed not to constrain the solver variable (cf HAL's `same(old)' mode).
> For example, the very common situation where an "ask" goal appears in the
> condition of an if-then-else could be written
>
> 	(
> 		ask get_min(X) < NewMin		% Mode of X is `same(old)'
> 	->

Again with the referential opacity?  I think you should fix this first.  Then,
as for problems 3 and 4, you acknowledge that getting the bounds of a variable
depends on the solver state.  I agree having a same(old) kind of mode is a good
idea, but it's really not so hard to put the code to fetch the bounds outside
the if->then;else.

> 	7) Lambda expressions which *may* constrain non-local solver
> 	variables.

> Situation 7 could be mitigated by adding a higher-order `any' inst
> to the mode system.  There is nothing intrinsically impure about lambda
> expressions which constrain non-local solver variables, so long as they
> are not called inside a negated context.  The higher-order `any' inst
> would prevent this from happening without a promise of safety, and therefore
> the construction of the lambda expression need not be considered impure.

This sounds good to me.

> 	8) Goals which aren't really impure at all, but for which it is
> 	important to have some control over the operational semantics.
> 	For example, search predicates in constraint programs are often
> 	declared impure even though they are pure, simply to ensure that
> 	calls to them are not scheduled before all constraints are posted.

> Situation 8 could be obviated by introducing a sequential conjunction
> operator.

This too, though getting the semantics exactly right may be tricky.  Rather
than having "A & B" mean "A must always be executed before B," perhaps it
should mean "execute A before B, unless B must be executed first to satisfy the
modes."  I'd hate to see anything make it any harder to have multiple modes for
a predicate.

> 	9) Trace goals.

> Situation 9 is considered less harmful than 1 or 2,
> so we have already opted for relaxing the annotation requirements -- impurity
> from trace goals does not need to be annotated at all.

That still doesn't seem right to me, since trace goals do force an order of
execution.

>> that
>> admits, in a syntactically lightweight way, that a particular goal is impure,
>> but only with respect to certain resources.
> 
> This would seem to relate mainly to 1 and 2, which are not the main part of
> the problem as far as I can see.

I would argue that solvers shouldn't usually have to use impurity at all, and
with resources and some changes to the way solver vars work, they wouldn't have
to.  After all, what they're doing isn't actually impure if you consider the
state of the constraint store.  It's just that we don't want the user of the
constraint predicates to see the constraint store.  So why not think of writing
a CLP program as an ordinary pure Mercury program, with everything threaded
through the code as needed, and then extend Mercury to create an abstraction
barrier that hides the threading of the parts of the state the user shouldn't
know about?  This is just what Mercury already does now, hiding the heap from
the user.

Summing up, resources can handle issues 1-3, I don't think 4-6 are really
problems, I like your solutions for issues 7 and 8, and I think you're asking
for problems with your solution to 9, at least if anybody cares about
commutativity of conjunction.

-- 
Peter Schachte              Don't worry about people stealing your ideas. If
schachte at cs.mu.OZ.AU        your ideas are any good, you'll have to ram them
www.cs.mu.oz.au/~schachte/  down people's throats.
Phone: +61 3 8344 1338          -- Howard Aiken
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at csse.unimelb.edu.au
Administrative Queries: owner-mercury-developers at csse.unimelb.edu.au
Subscriptions:          mercury-developers-request at csse.unimelb.edu.au
--------------------------------------------------------------------------