Nottingham FP Lab Blog

Comprehending the IO monad

by Thorsten on January 29, 2006.
Tagged as: Lunches.

After I failed to typeset some fancy lhs2tex for the blog (it says the latex is too complicated) here is just a short summary what I talked about last Friday.

In his very readable tutorial Tackling the awkward squad Simon explains and discusses Haskell’s IO features which are encapsulated in the IO monad. He uses a simple process calculus, inspired by he pi calculus, to give an operational semantics to Haskell’s IO. I have been looking at an alternative: defining the meaning of IO within Haskell itself. This has the advantage that we already know Haskell and how to reason about Haskell programs. I also hope that following this line we can add IO to Epigram.

Following Simon’s example I introduce IO in several steps:

First I introduce stream IO. Interestingly the type myIO is a variant of the food processor we have seen recently, introduced by Hank and Conor. See myIOStr.hs
Next we turn our attention to IORefs, see myIORef.hs. Note that I only do IORef Int, doing it more polymorphically involves some standard generic programming technology, not relevant here. How do we combine IORefs and streams? It is the coproduct of the two monads (see Neil’s paper), which in this case has a particularly simple form.
Finally, we implement Concurrent Haskell with forkIO and MVars, see myIOMVar.hs. Here runIO gets an additional parameter a scheduler represented as a stream of Booleans. Also the return type of runIO has to take account of the possibility that the process becomes deadlocked.

The scheduler can also be used to introduce the simulation preorder, given p,q::MyIO a we say that p < q (p can simulate q), iff there is a function f::[Bool] -> [Bool] s.t. for any scheduler s we have that runIO s p = runIO (f s) q. The symmetric closure of < is called bisimulation and is a useful congruence when reasoning about IO, i.e. we consider IO as the quotient of MyIO wrt to bisimulation.