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)? Commented Aug 20, 2012 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
Commented Aug 20, 2012 at 8:11
• Off the top of my head, the comments here are a good start
Commented Aug 20, 2012 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! Commented Sep 4, 2012 at 16:37
• Commented Sep 4, 2012 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
Commented Jan 24, 2013 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. Commented Feb 9, 2014 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
Commented Feb 9, 2014 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
Commented Feb 9, 2014 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. Commented Feb 20, 2015 at 4:27

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

• that's actually not a problem. you can model the bind operation as performing a modification to the world state derived from some fixed-but-unknowable rule store.
– sclv
Commented Sep 4, 2012 at 15:51
• @sclv: yes, but this fixed-but-unknowable rule store is the differentiating factor that makes the IO not the state monad, this inconsistency is not found in the state monad Commented Sep 4, 2012 at 16:43
• An argument I've heard against the WorldState state is related to concurrency, though I cannot remember the exact argument. But even still, I hypothesize that WorldState could encode the future into it as well, so I still don't really see the problem. Of course, I suppose I'm missing something. Commented Sep 4, 2012 at 17:07
• @JimmyHoffa: You can carry around the rule store in state though.
– sclv
Commented Sep 4, 2012 at 18:22
• @JimmyHoffa: this is the purpose of abstraction. Also, to follow up on my initial comment, Clean models IO as world-passing explicitly and happily, using uniqueness types to ensure that you don't cheat and "duplicate" the world. This is one way of enforcing the abstraction.
– sclv
Commented Sep 5, 2012 at 14:42

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)

That post covers a bit of why it is awkward to reason about the semantics of 'world-passing'.

• +1 - especially interesting, as I have long planned on implementing the IO of the language I'm designing in a similar manner to this! :) Commented Jun 18, 2016 at 11:40

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
Commented Sep 5, 2012 at 7: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