Monadology

Looking through the GHC source code, it seems that the IO Monad is defined in ghc-prim/GHC/Types.hs line 233:

{- |
A value of type @'IO' a@ is a computation which, when performed,
does some I\/O before returning a value of type @a@.
There is really only one way to \"perform\" an I\/O action: bind it to
@Main.main@ in your program.  When your program is run, the I\/O will
be performed.  It isn't possible to perform I\/O from an arbitrary
function, unless that function is itself in the 'IO' monad and called
at some point, directly or indirectly, from @Main.main@.
'IO' is a monad, so 'IO' actions can be combined using either the do-notation
or the 'Prelude.>>' and 'Prelude.>>=' operations from the 'Prelude.Monad'
class.
-}
newtype IO a = IO (State# RealWorld -> (# State# RealWorld, a #))

But it's used all over the place:

• GHC.IO asserts IO is just an ST monad, "The IO Monad is just an instance of the ST monad, where the state thread is the real world."
• Its monadic structure is defined in GHC.Base, Lines 1561–1565 (it seems that bindIO does the heavy lifting).
  • Note: State# and RealWorld are defined in GHC.Builtin.primops lines 2759–2769. They are pseudo-operations.

Note that bindIO is defined as:

--  ghc/libraries/base/GHC/Base.hs
bindIO :: IO a -> (a -> IO b) -> IO b
bindIO (IO m) k = IO (\ s -> case m s of (# new_s, a #) -> unIO (k a) new_s)

unIO :: IO a -> (State# RealWorld -> (# State# RealWorld, a #))
unIO (IO a) = a

Peyton Jones and Wadler write in their paper, "Imperative Functional Programming", (page 4):

If m :: IO a and k :: a -> IO b, then m `bindIO` k denotes the action that, when performed, behaves as follows: first perform action m, yielding a value x of type a, then perform action k x, yielding a value y of type b, then return value y.

This only makes sense if IO a is a wrapper around (State# RealWorld -> (# State# RealWorld, a #)), or (less exciting and probably more accurate): things have changed since January 1993…

Printing a string in Haskell is done in System.IO, line 277, for example:

putStr          :: String -> IO ()
putStr s        =  hPutStr stdout s

This delegates the heavy lifting to GHC.IO.Handle.Text defining hPutStr (lines 613 et seq.):

hPutStr :: Handle -> String -> IO ()
hPutStr handle str = hPutStr' handle str False

-- | The same as 'hPutStr', but adds a newline character.
hPutStrLn :: Handle -> String -> IO ()
hPutStrLn handle str = hPutStr' handle str True
  -- An optimisation: we treat hPutStrLn specially, to avoid the
  -- overhead of a single putChar '\n', which is quite high now that we
  -- have to encode eagerly.

{-# NOINLINE hPutStr' #-}
hPutStr' :: Handle -> String -> Bool -> IO ()
hPutStr' handle str add_nl =
  do
    (buffer_mode, nl) <-
         wantWritableHandle "hPutStr" handle $ \h_ -> do
                       bmode <- getSpareBuffer h_
                       return (bmode, haOutputNL h_)

    case buffer_mode of
       (NoBuffering, _) -> do
            hPutChars handle str        -- v. slow, but we don't care
            when add_nl $ hPutChar handle '\n'
       (LineBuffering, buf) ->
            writeBlocks handle True  add_nl nl buf str
       (BlockBuffering _, buf) ->
            writeBlocks handle False add_nl nl buf str

If I try to do something similar with Standard ML, then I'd guess:

datatype 'a IO = IO of (unit -> 'a);

fun putStr (s : string) : unit IO = IO (fn () => print s);

This typechecks fine, but it doesn't produce what we'd expect. For example, in Hamlet:

- putStr "foo";
val it = IO _fn : unit IO
- print "foo\n";
foo
val it = () : unit

Arguably, the only state which is discussed in the Standard ML definition is mutable references. (Perhaps the case could be made that environments managing bindings is another form of state, but it is one which we all accept.) How can we bundle "mutable references" up in a monadic way?

Recall, the type signature for mutable references in Standard ML:

ref : 'a -> 'a ref            (* "data constructor" *)
(op !) : 'a ref -> 'a         (* dereferencing *)
(op :=) : 'a ref * 'a -> unit (* updating *)

• Compilation of IORef and STRef
• What does 'MutVar#' mean?
• Andrew Butterfield and Glenn Strong,
  "Proving Correctness of Programs with IO—A Paradigm Comparison".
  In Proceedings of IFL2001.
• Wouter Swierstra and Thorsten Altenkirch,
  "Beauty in the Beast: A Functional Semantics for the Awkward Squad".
  PDF (2007)
• Simon Peyton Jones,
  "Tackling the Awkward Squad: monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell".
  EPrint (2010)
• Jeremy Gibbons and Ralf Hinze,
  "Just do It:Simple Monadic Equational Reasoning".
  Eprint (2011)
• John Launchbury and Simon Peyton Jones,
  "Lazy Functional State Threads".
  1994 (discusses IO as a ST instance) Citeseerx
• Edsko de Vries,
  Understanding the RealWorld
• Unraveling the mystery of the IO monad

• Philip Wadler,
  "Monads for Functional Programming".
  Eprint (1995)
• Philip Wadler,
  "How to declare an imperative".
  PS (1997). Gives an example of reasoning with IO monad.
• Philip Wadler and Simon Peyton Jones,
  "Imperative Functional Programming".
  PS Eprint (1993)
• R. Affeldt, D. Nowak, T. Saikawa,
  "A Hierarchy of Monadic Effects for Program Verification using Equational Reasoning".
  Eprint discusses using Coq to verify Monadic effects.