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

[Julien Fischer]

On Mon, 22 Jan 2007, Mark Brown wrote:

...

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

I like this idea, however I'm not sure that with the current mode
analyser that implementing it is going to be feasible (at least not
without a lot of work).  The same goes for number 6 as well.

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

Impurity from trace goals is not really a user-level purity though -
it's more akin to the various types of impurity that are introduced by
compiler transformations, e.g. that for dependent parallel conjunction.

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