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

[Ralph Becket]

Mark Brown, Wednesday, 12 October 2005:
> On 12-Oct-2005, Ralph Becket <rafe at cs.mu.OZ.AU> wrote:
> > Estimated hours taken: 1
> > Branches: main
> > 
> > Allow unifications to be delayed across impure goals.  Previously this
> > was disallowed which made it impossible to have deconstruction unifications
> > in impure pred calls, which was unnecessarily awkward.
> > 
> > It is safe to reorder unifications across an impure goal because they cannot
> > be affected by the impure goal (unifications are pure).
> 
> That doesn't follow!  In general pure goals cannot be reordered across
> impure goals.  If it really is safe then please be clearer about your proof
> in the log message, since I don't immediately see how it is safe.

Yes, I thought I might be picked up on that one :-)  Part of the
difficulty here is that we haven't really defined what an impure call is
and what one is allowed to do.

I propose that an impure call is one with the following properties:

(1) it's semantics depends upon hidden state (i.e., something other than
its arguments)

AND

(2) it can be used to violate referential transparency (which in our
case also means not respecting the commutativity of conjunction and
disjunction).

Pure solver calls have property (1), but not (2) (except when used in a
negated context).

What is an impure call allowed to do?  I think the side effects of
impure calls should be restricted to the hidden state.  An impure call
should not be allowed to, say, change the inst of a variable that is not
one of its arguments.

It follows that any call that does not refer to hidden state cannot be
affected by an impure call.  We can't decide this for most calls, but we
know it that assignments, constructions, and deconstructions do not
refer to any hidden state.  That leaves equality tests (so called
complex unifications) which, if they mention arguments to the impure
call, can only appear as implied modes which necessarily happen
after the call.

> Also, you
> will need to update the reference manual (section 15.3) to match what is
> actually allowed.

I'll do that if my argument above is accepted.

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