Take the 2-minute tour ×
Programmers Stack Exchange is a question and answer site for professional programmers interested in conceptual questions about software development. It's 100% free, no registration required.

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

share|improve this question
1  
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
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 Sep 4 '12 at 16:37
2  
See stackoverflow.com/a/7072217/100020 –  sdcvvc Sep 4 '12 at 18:18
show 1 more comment

5 Answers

up vote 19 down vote accepted
+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.

share|improve this answer
5  
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 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 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 at 23:35
add comment

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

share|improve this answer
add comment

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.

share|improve this answer
    
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
add comment

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

share|improve this answer
add comment

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

share|improve this answer
5  
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 Sep 4 '12 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 –  Jimmy Hoffa Sep 4 '12 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 Sep 4 '12 at 17:07
    
@JimmyHoffa: You can carry around the rule store in state though. –  sclv Sep 4 '12 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 Sep 5 '12 at 14:42
show 5 more comments

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

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