47

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

Improve this question
6
  • 1
    Is it this article (or this older version of it)?
    – Joachim Sauer
    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
    – Adam
    Commented Aug 20, 2012 at 18:55
  • 1
    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
    Commented Sep 4, 2012 at 16:37
  • 2
    See stackoverflow.com/a/7072217/100020
    – sdcvvc
    Commented Sep 4, 2012 at 18:18

5 Answers 5

Reset to default
34
+50

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.

Improve this answer
6
  • 8
    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
  • 4
    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
    Commented Feb 9, 2014 at 17:20
  • 2
    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.
    – CMCDragonkai
    Commented Feb 20, 2015 at 4:27
12

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

Improve this answer
14
  • 8
    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
  • 1
    @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
    – Jimmy Hoffa
    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.
    – Thomas Eding
    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
  • 1
    @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
12

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

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

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.

Improve this answer
1
  • 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
5

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

Improve this answer

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.