## Comprehending the IO monad

January 29th, 2006 by ThorstenAfter 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.

February 3rd, 2006 at 1:15 pm

Sounds like the record of a session that i definitively would have liked to attend.

Out of his monadic series i always liked best the part where Philip Wadler in his ‘How to declare …’ (p. 14-) demonstrates how to erase causality from streams (of cons… famous Irishman to chime in here) and recover it by means of convergence, but showing how to have this orthogonality and glue right from the start when you keep your inner and outer worlds monadwise connected.

Since the underlying functor of the IO Monad is a stream, can’t we then have η defined by fold[(l|r)] to gain a more typeful insight?

The mixed co/data representation of your Stream (that not is of alternating least/greatest fixpoint) to me foregrounds the Altenkirch/Hutton question of when a function is a fold or an unfold.