[mercury-users] Request for comments on this code

[Peter Schachte]

On Tue, Jul 11, 2006 at 08:42:08PM +1000, Ian MacLarty wrote:
> On Tue, Jul 11, 2006 at 06:03:31PM +1000, Peter Schachte wrote:
> > On Tue, Jul 11, 2006 at 01:32:03PM +1000, Ian MacLarty wrote:
> > > On Tue, Jul 11, 2006 at 12:03:55PM +1000, Peter Schachte wrote:
> > > > On Tue, Jul 11, 2006 at 11:15:35AM +1000, Ian MacLarty wrote:
> > > > 
> > > > > For every IO primitive executed in the program the first IO state
> > > > > argument is the state of the universe at the time that IO primitive is
> > > > > executed, while the second IO state argument is the state of the
> > > > > universe at the time the *next* IO primitive is executed.

> > We need to thread the IO state through the code to keep the actions
> > that effect the "state of the universe" in the right order.  So you
> > don't want to consider too many things to be part of the "state of the
> > universe," because you'll have to thread the IO state through
> > everything that effects any of those things, at least if you care
> > about the order they happen in.  You can't get around that by
> > declaring that the state of the world psychically determines
> > everything that's going to happen before the next IO action, including
> > things inside Mercury, because that doesn't distinguish goals that
> > cannot be reordered from goals that can.

> I don't really understand what you're saying.  I think what you're
> saying is that my interprettation of the IO state means you can never
> reorder any goals.

I'm just saying that you need to thread the IO state through all goals
the order of whose effects on the state of the universe you care
about, or else make them impure.  As far as I can see, this is exactly
the given wisdom about IO states and impurity.  For any operation
whose effect on the state of the universe is commutative, such as
making time pass*, the order of execution of that code is immaterial,
so the IO state needn't be threaded through.

But as soon as you provide a way to fetch that part of the state of
the world, such as reading the current clock time, the operations that
effect that part of the state of the world are no longer commutative.
Now you can tell the difference between

	do_something,
	get_time(Time, !IO),

and

	get_time(Time, !IO)
	do_something,

so the IO state needs to be threaded through do_something, and in fact
through everything that could make an observable change to the state
of the world.

It's basically the same problem as tell and ask constraints.  As long
as you only have tell constraints, they can happen in any order, so
you don't need to thread the constraint store through them.  But as
soon as you add an ask constraint, the order matters, and you have to
thread the constraint store through everything.  Or you just make the
ask constraint impure, so that's what we do.

Saying that at the previous IO operation the universe somehow knows
what the state of the universe will be at the next operation doesn't
solve the problem of telling *Mercury* what order to do things in.
The IO state is threaded through to ensure that non-commutative
operations (such as IO operations) happen in the right order.  Making
something observable to Mercury through the IO state means that
changes to that thing are no longer commutative, so everything that
changes that thing must have the IO state threaded through.


------
* I still have real trouble with the idea that executing code makes
time pass; I suspect time would pass even if the code weren't
executed.


-- 
Peter Schachte              If your thesis is utterly vacuous Use
schachte at cs.mu.OZ.AU        first-order predicate calculus. With sufficient
www.cs.mu.oz.au/~schachte/  formality The sheerist banality Will be hailed
Phone: +61 3 8344 1338      by the critics: "Miraculous!" -- Anon. 
--------------------------------------------------------------------------
mercury-users mailing list
post:  mercury-users at csse.unimelb.edu.au
administrative address: owner-mercury-users at csse.unimelb.edu.au
unsubscribe: Address: mercury-users-request at csse.unimelb.edu.au Message: unsubscribe
subscribe:   Address: mercury-users-request at csse.unimelb.edu.au Message: subscribe
--------------------------------------------------------------------------