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

[Mark Brown]

On 19-Jan-2007, Peter Schachte <schachte at csse.unimelb.edu.au> wrote:
> Maria Garcia de la Banda <Maria.GarciadelaBanda at infotech.monash.edu.au> wrote:
> > Ralph Becket wrote:
> >> I'm just debugging a change to the compiler to support putting impurity
> >> annotations on clause heads as an alternative to placing them on all
> >> impure goals in the clause bodies.  There's some resistance to the idea
> >> at the Melbourne end (i.e. we're going to have a syntax fight over
> >> this...) and it would be helpful if you could send me any copies of your
> >> Mercury modules that are currently festooned with impurity annotations
> >> so I can use them as ammo in the forthcoming debate.
> > 
> > which I find extremely relevant. Considering how many people are nowdays
> > implementing impure things, it might be easier to convince them now (I bet most
> > of the solvers code is festoned with impure keywords). What do you think?
> 
> If we're going to dredge up old battles, I'll weigh in....
> 
> I agree with Maria that having code festooned with impurity declarations is
> undesirable.  They're a nuisance to write and they obscure the logic of the
> code.

Yes, I agree with this too.

> But more importantly, they are too blunt an instrument:  they say 'all
> bets are off in this chunk of code'.  Putting a single impurity declaration at
> the front of the clause fixes the two smaller problems, but makes the bigger
> one worse, since then there's nothing in the clause whose semantics is simple.

And this.

That is, I agree that the purity annotations currently required are a problem,
but I don't agree that dropping the purity requirements is the solution.

>  If all bets really are off everywhere in the clause, having a single impurity
> declaration at the front is probably an improvement.  But I think in most cases
> it would be far preferable to have a more fine-grained kind of impurity

I think this is in the longer term plans of the Mercury team.  The
"resistance to the idea" that Ralph mentions above, for my part at least,
is not because I don't think that the purity annotations are a problem,
but because I think we can provide a better solution in the longer term.

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.

These are described by "semipure" and "impure" respectively.  It was expected
that code making use of the purity system would have a thin layer of impure
code with a pure interface, so that the number of annotations would remain
fairly small.

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.

	4) Mode specific clauses (similar to 3).

	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.

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

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

	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.

	9) Trace goals.

Situations 3, 5, 6, 7 and 8 come up all the time when constraint programming
in Mercury, which would be the main ones affecting Maria.  Note that 5 is
easy to avoid since a predicate can be used instead of a function, and
the requirement of referential transparency thereby goes away.

The longer term plans are still in discussion, but a summary of the basic
ideas is as follows:

First, situation 3 is not really as harmful as 1 or 2 (IMHO), so a different
annotation (e.g., "ask") may be in order.  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, ...)

Second, 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)'
	->
		...
	;
		...
	)

instead of

	promise_pure
	(
		impure Min = get_min(X),	% Mode of X is `ia'
		Min < NewMin
	->
		...
	;
		...
	)

Furthermore, the requirements on using an annotation could be relaxed for
chains of if-then-elses, so that it would be possible to write:

	promise_pure
	(
		p(X)				% Mode of X is `ia'
	->
		...
	;
		q(X)				% Mode of X is `ia'
	->
		...
	;
		...
	)

and have the one promise apply to all conditions in the chain.  (As with 3,
an annotation other than "impure" could be used.  But I can't think of a good
name at the moment.)

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

Fourth, situation 8 could be obviated by introducing a sequential conjunction
operator.

Finally, note that 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
> 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 don't mean to take anything away from
your resources proposal, but it doesn't address the problems with purity
annotations in constraint programs, IMHO.

Cheers,
Mark.

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