# Critique of the IO monad being viewed as a state monad operating on the world

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.)

-
Is it this article (or this older version of it)? – Joachim Sauer Aug 20 '12 at 7:45
@JoachimSauer Thanks, it's also an interesting article, but it's not the one I'm looking for. That one was focused on the state-of-the-world paradigm. – Petr Pudlák Aug 20 '12 at 8:11
Off the top of my head, the comments here are a good start – Adam Aug 20 '12 at 18:55
What does "world" mean in this context? I presume it does not mean "The Earth." Is it some kind of global scope? The author who penned this is selling himself short. If he wants to simultaneously confuse and crush the egos of his readers, he should call it "The State is the Universe" or "The God State." World. Pah! You young people don't aspire high enough these days! – GlenPeterson Sep 4 '12 at 16:37
– sdcvvc Sep 4 '12 at 18:18

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.

-
Is anyone surprised that a nonterminating program is equivalent to `undefined` in the pure semantics of Haskell? Different ⊥s are supposed to be indistinguishable in Haskell's pure semantics! But when we think operationally about our programs we want to distinguish different kinds of ⊥ too, even when `IO` is not involved; I care whether my program is throwing an exception or entering an infinite loop, even if you can prove that those are equal by proving that they're both ⊥. That's not actually a contradiction though. – Ben Jan 24 '13 at 20:40
The denotations of ⊥ and [0,1..] are distinct even though they are both "non-terminating". The difference is that ⊥ is denotes non-terminating and non-productive computations, while [0,1..] is non-terminating but productive. We expect (forever (putStrLn "Hello")) to have a similar non-terminating but productive denotation. – Russell O'Connor Feb 9 '14 at 17:20
But `forever (putStrLn "Hello")` isn't like `[0,1..]`, surely. Your proof isn't particular to `worldState`, therefore it also applies to the regular state monad. So `forever (someModificationWith "Hello")` is also denotationally equivalent to ⊥. I'm completely unsurprised by that result; it isn't productive in the denotational semantics, and what the computer is doing operationally while we wait forever is irrelevant. Same thing for `forever (putStrLn "Hello")`; it doesn't and shouldn't produce a new world state we can somehow consume lazily. – Ben Feb 9 '14 at 23:31
Are programming languages like Mercury and Clean that use explicit world-state passing to provide a declarative model for IO fundamentally wrong? – Ben Feb 9 '14 at 23:35
@Ben are you referring to how does world passing work with concurrency? Have you seen the rosetta code for Mercury's concurrency? I have wondered what that means semantically too. – CMCDragonkai Feb 20 at 4:27

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

-

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.

-
I believe this is the original article I was looking for, mainly section 3.1. If you had posted it before I edited the question, I'd have accepted your answer, but now I think it'll be more fair to wait until the end, to see all ideas that others will post. – Petr Pudlák Sep 5 '12 at 7:27

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)