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

[Mark Brown]

On 22-Jan-2007, Mark Brown <mark at csse.unimelb.edu.au> 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.
> 
> 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.

Another similar situation is

	10) Existentially quantified solver variables.

For this one we don't (yet) have any requirement to annotate the impurity,
or to promise that the code is pure.  Without this the implementation of
existential quantification can be unsound.  Consider three boolean
variables B1 .. B3 with the following constraints:

	B1 = not(B2),
	B2 = not(B3),
	B3 = not(B1)

An FD-style solver would typically succeed, albeit with an unsatisfiable
constraint store.  Failure wouldn't occur until one of the variables becomes
ground.  However, the goal:

	some [B1, B2, B3] (
		new_bool01(B1),
		new_bool01(B2),
		new_bool01(B3),
		B1 = not(B2),
		B2 = not(B3),
		B3 = not(B1)
	)

would succeed even though no values for Bn which satisfy the constraints
exist.  The compiler neither checks that one of the variables becomes
ground, nor does it require the user to promise that values exist.

A while back I proposed something along the lines of groundness analysis
to reduce the need for purity annotations on existential quantifications.

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