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:

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.

comments powered by Disqus