[mercury-users] Request for comments on this code

[Ian MacLarty]

On Tue, Jul 11, 2006 at 03:46:35PM +1000, Ralph Becket wrote:
> Here's my two worms' worth:
> 
> I've always assumed that the IO state corresponded to a representation
> of part of the world, including parts of the state of the computer
> running the computation.
> 
> When an IO operation is invoked, the universe gets to manipulate the IO
> state just before and just after the IO operation is carried out.
> 
> That is, when I write
> 
> 	io.print(..., !IO),
> 
> what really happens is
> 
> 	universe_gets_a_turn(!IO),
> 	io.print(..., !IO),
> 	universe_gets_a_turn(!IO),
> 
> What the universe does, however, is cc_multi (i.e., for any IO state
> there are many possible successor IO states, but we only get one of
> them and we can't backtrack.)
> 

Does the one that gets chosen happen to be the IO state that's fed as
input to the next IO primitive?  If so then I think your understanding
is quite similar to mine, except you view it as cc_multi and I view it as
deterministic.

If the chosen IO state doesn't correspond to the IO state at the next IO
primitive then how do you account for the fact that the time has
changed?

> Under that interpretation, IO operations should be cc_multi.
> 
> However, there is a strong pragmatic argument that allows us to mark IO
> operations to be det, namely that it allows us to distinguish between
> the cc-ness of our program vs the cc-ness of the universe.
> 
> (As far as I'm aware, (di/uo + det) and (cc_multi) both place identical
> constraints on my code.)
> 
> Is there a problem with this view (i.e., IO is really cc_multi, but we
> actually lose something if we don't pretend it's det)?
> 

I don't think so, since a particular IO state exists only once, so you
can always only get one resulting IO state from calling an IO primitive,
effectively making the operation det.

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