The IO monad in Haskell is often explained as a state monad where the state is the world. So a value of type IO a monad is viewed as something like worldState -> (a, worldState).
Some time ago I read an article (or a blog/mailing list post) that criticized this view and gave several reasons why it’s not correct. But I cannot remember neither the article nor the reasons. Anybody knows?
Edit: The article seems lost, so let’s start gathering various arguments here.
I’m starting a bounty to make things more interesting.
Edit: The article I was looking for is Tackling the awkward squad: monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell by Simon Peyton Jones. (Thanks to TacTics’s answer.)
6
The problem with IO a = worldState -> (a, worldState) is that if this were true then we could prove that forever (putStrLn "Hello") :: IO a and undefined :: IO a are equal. Here is the proof courtesy of dolio (2010, irc):
forever m
=
m >> forever m
=
fix (r -> m >> r)
= {definition of >> for worldState -> (a, worldState)}
fix (r -> w -> r (snd $ m w))
Lemma: (r w -> r (snd $ m w)) ⊥ = ⊥
(r w -> r (snd $ m w)) ⊥
=
w -> ⊥ (snd $ m w))
=
⊥ . snd . m
=
⊥
Therefore forever m = fix (r -> w -> r (snd $ m w)) = ⊥
In particular forever (putStrLn "Hello") = ⊥ and hence forever (putStrLn "Hello") and undefined are equivalent programs. However, clearly they are not supposed to be considered equivalent programs, in theory or in practice.
Notice that this model is wrong even without invoking concurrency.
6
Here’s a trivial answer: any change to the state monad’s state is due to any actions ran in the monad. If indeed the “WorldState -> (a, WorldState)” explanation claims the same property, with WorldState being a pure value that only the IO monad changes, it’s wrong. Time changes, the content of files, the state of handles, etc. can change independently of what happens in the IO monad. That’s the point of the IO monad. The fact that GHC passes around a RealWorld value (or w/e it was) underneath is to guarantee things are ran in order, as far as I know, if that (may just be something to put in the ST value).
14
I wrote a blog post on the topic of how to model IO as a form of asymmetric coroutine communicating with the runtime system for your language. (It is admittedly the third part of a series)
http://comonad.com/reader/2011/free-monads-for-less-3/
That post covers a bit of why it is awkward to reason about the semantics of ‘world-passing’.
1
See Tackling the Awkward Squad.
The big reason is RealWorld state models of the IO monad don’t work well with concurrency. SPJ in this readable classic favors using an operational semantics to understand it.
1
The main complaint about RealWorld state models is that, as TacTics says, world-passing doesn’t necessarily work with concurrency. But Wouter Swierstra and Thorsten Altenkirch showed how to reason about concurrency as “world-passing” effect, with a fixed-but-arbitrary sequence of interleaving threads in their paper “Beauty in the Beast: A Functional Sematics for the Awkward Squad”: http://www.staff.science.uu.nl/~swier004/Publications/BeautyInTheBeast.pdf
The code corresponding to this is on Hackage as IOSpec: http://hackage.haskell.org/package/IOSpec
I think Wouter’s thesis goes into more detail: http://www.staff.science.uu.nl/~swier004/Publications/Thesis.pdf