[m-rev.] For review: allow unifications to be delayed across impure goals

[Fergus Henderson]

Hi Ralph,

On 19-Oct-2005, Ralph Becket <rafe at cs.mu.OZ.AU> wrote:
> Fergus Henderson, Wednesday, 19 October 2005:
> > Yes.  Some impure calls may affect pure unifications (e.g. consider
> > Prolog's setarg/3, or it's Mercury equivalent in
> > samples/trailed_update/var.m).  Furthermore, even if the pure
> > unification is not affected by the impure goal, that doesn't
> > necessarily mean that the two goals can be safely reordered, because
> > the impure goal might be affected by the pure unification (e.g.
> > consider Prolog's var/1).
> 
> This is all well and good, but the mode system prevents these issues
> from arising.  During normalisation a goal is flattened so that any
> argument unifications are listed before the "top-level" call in the
> goal.  During mode analysis we delay a goal only if it cannot be
> scheduled immediately.  Therefore any argument unifications for an
> impure call that *can* be scheduled before the impure call *will* be
> scheduled before the impure call.  The only argument unifications
> that are *not* scheduled before the call are those that *cannot* be
> scheduled before the call because some of the variables involved
> have yet to become non-free.  There is therefore *no* choice in the
> matter: these unifications must come after the call.

There _is_ a choice: move the unifications after the call,
thus potentially changing the behaviour of the program
from what the programmer intended... or report a mode error.

The current situation is that if you write code using Mercury's impurity
system, and the code passes mode checking, you will get Prolog-like order
of execution for all the parts that depend on the order of execution.

Your proposal would change that.  Programmers could no longer rely on
Prolog-like order of execution for code fragments using impure code.
They would need to look at the mode declarations of called procedures
and do in-their-head mode inference in order to figure out the actual
order of execution.

> One other point: with impure code it is the programmer's responsibility
> to ensure that calls are made in the right sequence.  The situation is,
> I claim, analagous to writing code like `X \= 0, Z = Y / X' to avoid a
> division-by-zero exception.  The *correct* thing to do here is to use an
> if-then-else to ensure the test for X is executed before the division.
> Similarly, if one really really does care about the relative order of
> a unification and an impure call, one should write the unification as a
> separate goal in the right place (and not as an argument to the impure
> call).

You seem to be suggesting that if I have a call such as

	impure p(f(X), X)

and I want the call to f/1 to occur before the call to p/2,
then I should write it as

	Y = f(X),
	impure p(Y, X)

But with your proposal, if I such write a goal, I still couldn't be sure
that Y = f(X) would be executed before the call to p(X, Y).  Whether or
not it gets reordered in that way would depend on the insts of X and Y at
this point, and on the mode(s) of f/1 if f/1 is a function rather than a
constructor, and on the mode(s) of p/2.

I like the current situation where we essentially guarantee Prolog-like
order of execution for code fragments using impure code.  That makes it
easier to reason about the order of execution of such code.  While I
agree that this does lead to more verbose code in some situations,
I don't think that making that code more concise is worth giving up
this guarantee.

Cheers,
	Fergus.

-- 
Fergus Henderson                    |  "I have always known that the pursuit
                                    |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
mercury-reviews mailing list
post:  mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------