[m-dev.] Impurity syntax

[Ralph Becket]

In yesterday's meeting, Maria said that the Mercury versions of the HAL
solver code were drowning under the weight of all the impurity
annotations.  At least with the current solver types design, the
interface code between the solver type and the representation has to be
littered with impurity annotations.

A lighter weight syntax was proposed to get around the problem (see the
end of this e-mail for a description of the proposal).

But it occurrs to me that we could simply get rid of impurity
annotations on calls and instead just keep them on the declarations (and
maybe add them as a requirement to clause heads if a big impurity sign
is still desirable; I'd be inclined to this approach.)

Any takers?

-- Ralph


LIGHTER WEIGHT SYNTAX TO REPLACE IMPURITY
(PROBABLY NOT REALLY NEEDED)

(1) Persistent imaginary "state items" can be introduced with a
declaration

	:- state foo.
	:- state bar.

(2) Predicates must declare it if they "change" a particular state item

	:- pred p(...) changes foo.
	:- pred q(...) changes foo, bar.
	:- pred r(...).

(3) Unless accompanied by a `promise_pure' pragma, predicate calls
in a definition can only change a subset of the state items listed in
the `pred' declaration for the predicate being defined

	% Okay.
	%
	:- pred a(...) changes foo, bar.
	a(...) :-
		p(...),
		q(...),
		r(...).

	% Forbidden (unless b is promised pure).
	%
	:- pred b(...) changes foo.
	b(...) :-
		p(...),
		q(...),		% ERROR: q changes bar as well.
		r(...).

(4) Two calls that change the same state item cannot be reordered with
respect to one another.

(5) The state items have no physical realisation; they exist purely as
an ordering mechanism.  The `changes foo' annotation is tantamount to
adding an implicit (in, out) pair of arguments to a predicate and
threading a state variable throughout the body of the predicate to calls
to predicates that change `foo'.

This is much, much lighter syntax than impurity annotations and has a
somewhat declarative feel.  The `changes foo' annotation indicates to
the reader that the corresponding definition cannot be given a
declarative interpretation without some minor syntactic transformation,
along that lines of what is required to handle 

[Observation: this approach could even be used to do away with IO
states...]

Comments welcome.

-- Ralph
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------