[m-dev.] Summary of resources/solvers meeting 23/8/04

[Ralph Becket]

This is a (very) rough outline of the meeting on 23/8/04 concerning
syntactic and semantic issues relating to solver states, resources and
impurity.

Attended:
	Ralph
	Peter Stuckey
	Zoltan
	Vitali
	Kim
	Peter Schachte
	Mark

I'm not confident I followed the latter part of the discussion, so feel
free to add to or correct any part of this summary.

Four issues were discussed.


GLOBAL VARIABLES

Solver types require global variables.

Mercury needs some syntactic support for this.  Any suggestions?

Initialisation of global variables will probably require extending the C
INIT files for modules that define them.

TODO: Ralph to implement this when we agree upon a design.


IMPURITY SYNTAX

It was agreed that the current impurity syntax is too heavy and that
purity annotations should be moved from individual goals to the head of
the clause.

That is, rather than write

	p(...) :-
		impure q(...),
		semipure r(...),
		s(...).

we should just write

	impure p(...) :-
		q(...),
		r(...),
		s(...).

This meets the requirement that clause code contain some warning to the
reader that the usual interpretation does not apply to the definition,
but doesn't obscure the code with excessive purity annotation.

TODO: Decide how to migrate to the new syntax.
TODO: Ralph to add the new syntax at some point.


STATE VARIABLES

Peter Schachte suggested changing state variable syntax to leave the
state variables themselves largely implicit.  That is, rather than
writing

	io.write_string("Hello, World!", !IO)

one would just write

	!io.write_string("Hello, World!")

and, thanks to annotations on the signature of io.write_string, the
!IO state thread would be automatically inserted at the end.

This *may* be an improvement, but before changing anything it would be
worth revisiting the mailing list archives for the exteeeeeeeeensive
discussion on this point that we had about two or three years ago.


SOLVER STATES AND RESOURCES IN GENERAL

Two mutually compatible positions were advanced.

(1) Changes to the language should proceed bottom-up and be motivated by
a sufficient number of example problems.  The current Mercury syntax
(modulo the changes to impurity annotations mentioned above) was
generally deemed to be fine for our current situation.

(2) There is a more general problem here that merits thinking about
top-down.  Specifically that declaratively clean, syntactically
lightweight mechanisms amenable to automatic analysis for describing
resource usage may be a Good Thing to look into.

Following along this line...

We currently have two mechanisms to describe ordering constraints
between goals.

At the crudest level, impure goals cannot be reordered, semipure goals
can be reordered but not across impure goals, and pure goals can go
pretty much anywhere.

e.g.

	p :-
		a,		% Can go anywhere.
		impure b,	% Must go here.
		semipure c,	% Can be reordered between b and f.
		d,		% Can go anywhere.
		semipure e,	% Can be reordered between b and f.
		impure f,	% Must go here.
		impure g.	% Must go here.

A slightly more refined approach is to use a "state" thread (e.g. using
state variables), which preserves the order independance of goals using
different "state" threads.

e.g.
	p(!A, !B) :-
		a(!A),		% Relative order of a, b, c, f
		b(!A),		% must be preserved.
		c(!A),
		d(!B),		% Relative order of d, e, f, g
		e(!B),		% must be preserved.
		f(!A, !B),
		g(!B).

More generally we would like to be able to express the commutativity of
certain goals (e.g. that the order of insertion of items into a set is
irrelevant.) 

(My earlier e-mail regarding resource annotations describes the starting
point of a mechanism to explicitly associate virtual resources with
predicates.)

One well received suggestion was (for solvers) to divide operations into
`tell' and `ask' variants.  Tell goals would need no annotation, but ask
goals would.  Ask goals commute and tell goals commute, but ask goals
cannot be reordered w.r.t. tell goals and vice versa.

It was not clear how this would affect higher order code.

It was not clear *how* this should be implemented, although the
declarative semantics seemed straightforward.

A question was raised about whether supporting multiple states for a
single solver was a good thing (for e.g. copying-based solvers?) and if
so how it might be managed.


OTHER DETAIL

Other things were discussed, but I didn't follow them well enough to say
anything.


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