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

[Julien Fischer]

On Wed, 12 Oct 2005, Ralph Becket wrote:

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

I would intepret the reference manual as currently allowing that:

	Impure predicates may perform I/O or modify hidden state,
	even if these side effects alter the operational semantics
	of other code.

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