[mercury-users] Request for comments on this code

Ian MacLarty maclarty at csse.unimelb.edu.au
Thu Jul 13 12:18:08 AEST 2006


On Thu, Jul 13, 2006 at 09:52:54AM +1000, Peter Schachte wrote:
> On Wed, Jul 12, 2006 at 02:50:56PM +1000, Ralph Becket wrote:
> > by labelling IO
> > operations as det we are quietly assuming a deterministic universe,
> > whereas I believe it has been proved that the universe is fundamentally
> > probabilistic.
> 
> I always thought of the determinism of a predicate as describing
> *that* predicate's behavior.  So
> 
> 	write("Hello World!", !IO)
> 
> being det should just mean that write/3 behaves deterministically, it
> shouldn't have to promise anything about the universe, any more than
> it should have to promise that you won't run out of memory or suffer a
> power failure while executing it.  It really should just describe the
> success set of the predicate given the mode.
> 
> Of course, Ian's right that for any operation that effects with the
> universe, the state of the universe after it depends on the operation,
> the state of the universe before it, *plus* whatever else the universe
> happens to do concurrently.  So the whole "threading the state of the
> world" idea is a pretty crude approximation.  It doesn't even work if
> we just take the state of the world to include only the files we're
> manipulating, because someone can alway write to the same file we are
> concurrently.

But this is exactly what I'm trying to address with my proposed
interpretation of IO primitives!  In my interpretation the output IO
state argument is not the state of the universe when the IO primitive
finishes executing, but the state of the world when the *next* IO
primitive starts executing, so any subsequence writes by concurrent
processes would be taken into account.

> 
> The only model I know that really has a chance of working is to think
> of an IO state pair as difference list of messages we send to the
> universe.

But my interpretation works fine.  Granted, you can't use it for
modelling benchmarking declaratively; that's a limitation I'm okay with;
but as a completely accurate way to model IO declaratively I see no
problem with it.  I certainly wouldn't call it a crude approximation.

> So main/2 simply describes the IO commands the program
> executes while it's running; nothing more.  This doesn't require us to
> say anything about what the universe actually does with those
> messages.  

I think that's basically equivalent to what I'm proposing.  You can only
interact with the universe by executing an IO primitive, so describing
them as a list of messages or a sequence of state transformation doesn't
really make any difference.  When you request some information from the
universe (like reading a character from a stream) you have no idea what
it'll return really.  I take that into account by saying the input
state-of-the-universe argument already contains everything that's
happened up to the point we read the character, while you do it by
saying it's a message we send to a black box that could return anything.
Am I right, or have I misunderstood your messages idea?

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



More information about the users mailing list