
On Sat, 27 Nov 2004, Benjamin Franksen wrote:
I would think that with ACIO we have a nice mathematical characterization for the IO actions that would be "safe" even at the top-level. ("Safe" meaning mainly that we do not open a can-of-worms with regard to execution order.) I don't know how easy or hard it is to prove of a certain IO action that is in fact in ACIO.
Hard, because it depends on observational equivalence of IO effects, and for that you need a semantics for the RealWorld. Maybe a better way to treat it is that whereas doing an IO action puts it in an execution trace at a specific point, doing an ACIO action is simply "perform this some time, maybe, if required". Giving something like newUnique an ACIO type indicates that semantics is sufficient; whereas for readIORef it typically isn't, and you want the stronger guarantee of an IO type.
This breaks down as soon as the IO action does a forkIO.
Isn't sharing global variables the correct semantics for forkIO ? That explicitly creates a 'lightweight' thread, which shares execution context with its invoker. I agree that forkOS, with its own local context, is harder. I suspect that, yes, as soon as you want to have more than one execution context simultaneously, then you need to manage them. For which XIO seems to do the job. Ian -- Ian Stark http://www.ed.ac.uk/~stark LFCS, School of Informatics, The University of Edinburgh, Scotland