[Haskell-cafe] Yet another IO initializer: Effectful declarations and an ACIO monad

[Ian.Stark at ed.ac.uk]

Way back in this thread, Koen Claessen mentioned the idea of a commutative
version of the IO monad for handling things with identity.  That doesn't quite
do it, but I have a refinement that might.  The thing is to focus on IO
computations that are:

 a) central -- their effect commutes with every other IO action
 b) affine  -- their effect is not directly observable, and can be discarded.

Thus an element u of (IO a) is affine central if for all v::IO b and w::IO c,

  do { x <- u; v } = v                                (affine)
  do { x <- u; y <-v; w } = do { y <- v; x <- u; w }  (central)

where '=' is observational equivalence.

For example, we would expect newMVar x :: IO (MVar a) to be affine central;
similarly newIORef, and newStdGen for random number generators.


If we define an ACIO monad for affine central IO expression, then we can
safely use these in toplevel declarations:

  declare x <- u                 --  x::a, u::ACIO a
  declare count <- newIORef 0    --  count :: IORef Int
  declare flag  <- newMVar True  --  flag  :: MVar Bool

The semantics of such declarations would be to gather them all to the start of
a program, whose meaning is now

  do { declarations; main }

Because all declarations are ACIO: they can appear anywhere in the source; be
executed at any point between the start of the program and the use of their
value; and if there is no such use, need never be executed at all.  In any
event, the right-hand side of each declaration will be evaluated, and perform
its side-effect, at most once.

The declared values (x, count, flag) are pure values and do not have IO types.
However, almost all their uses (bumping the counter, reading the flag) will
live in the IO monad.  Like stdIn and stdOut.  Also, just because these
declarations are toplevel doesn't mean they are globally visible: they are
lexically scoped within standard module namespaces.


I conjecture that when used "safely" the {-# NOINLINE #-} unsafePerformIO
idiom is in fact being applied to IO expressions that are affine central;
which means they could be put in ACIO and used as declarations instead.

--
Ian Stark                               http://www.ed.ac.uk/~stark
LFCS, School of Informatics, The University of Edinburgh, Scotland