Is the IO monad technically incorrect?

Question

On the haskell wiki there is the following example of conditional usage of the IO monad (see here).

when :: Bool -> IO () -> IO ()
when condition action world =
    if condition
      then action world
      else ((), world)

Note that in this example, the definition of IO a is taken to be RealWorld -> (a, RealWorld) to make everything more understandable.

This snippet conditionally executes an action in the IO monad. Now, assuming that condition is False, the action action should never be executed. Using lazy semantics this would indeed be the case. However, it is noted here that Haskell is technically speaking non-strict. This means that the compiler is allowed to, for example, preemptively run action world on a different thread, and later throw away that computation when it discovers it doesn't need it. However, by that point the side-effects will already have happened.

Now, one might implement the IO monad in such a way that side-effects are only propagated when the whole program has finished, and we know exactly which side-effects should be executed. This is not the case, however, because it is possible to write infinite programs in Haskell, that clearly have intermediate side-effects.

Does this mean that the IO monad is technically wrong, or is there something else preventing this from happening?

Answer 1

This is a suggested "interpretation" of the IO monad. If you want to take this "interpretation" seriously, then you need to take "RealWorld" seriously. It's irrelevant whether action world gets speculatively evaluated or not, action doesn't have any side-effects, its effects, if any, are handled by returning a new state of the universe where those effects have occurred, e.g. a network packet has been sent. However, the result of the function is ((),world) and therefore the new state of the universe is world. We don't use the new universe that we may have speculatively evaluated on the side. The state of the universe is world.

You probably have a hard time taking that seriously. There are many ways this is at best superficially paradoxical and nonsensical. Concurrency is especially either non-obvious or crazy with this perspective.

"Wait, wait," you say. "RealWorld is just a 'token'. It's not actually the state of the entire universe." Okay, then this "interpretation" explains nothing. Nevertheless, as an implementation detail, this is how GHC models IO.¹ However, this means that we do have magical "functions" that actually do have side-effects and this model provides no guidance to their meaning. And, since these functions actually have side-effects, the concern you raise is completely on point. GHC does have to go out of its way to make sure RealWorld and these special functions are not optimized in ways that change the intended behavior of the program.

Personally (as is probably evident by now), I think this "world-passing" model of IO is just useless and confusing as a pedagogical tool. (Whether it's useful for implementation, I don't know. For GHC, I think it is more of a historical artifact.)

One alternative approach is to view IO as a describing requests with response handlers. There are several ways of doing this. Probably the most accessible is to use a free monad construction, specifically we can use:

data IO a = Return a | Request OSRequest (OSResponse -> IO a)

There are many ways to make this more sophisticated and have somewhat better properties, but this is already an improvement. It doesn't require deep philosophical assumptions about the nature of reality to understand. All it states is that IO is either a trivial program Return that does nothing but return a value, or it's a request to the operating system with a handler for the response. OSRequest can be something like:

data OSRequest = OpenFile FilePath | PutStr String | ...

Similarly, OSResponse might be something like:

data OSResponse = Errno Int | OpenSucceeded Handle | ...

(One of the improvements that can be made is to make things more type safe so that you know you won't get OpenSucceeded from a PutStr request.) This models IO as describing requests that get interpreted by some system (for the "real" IO monad this is the Haskell runtime itself), and then, perhaps, that system will call the handler we've provided with a response. This, of course, also doesn't give any indication of how a request like PutStr "hello world" should be handled, but it also doesn't pretend to. It makes explicit that this is being delegated to some other system. This model is also pretty accurate. All user programs in modern OSes need to make requests to the OS to do anything.

This model provides the right intuitions. For example, many beginners view things like the <- operator as "unwrapping" IO, or have (unfortunately reinforced) views that an IO String, say, is a "container" that "contains" Strings (and then <- gets them out). This request-response view makes this perspective clearly wrong. There is no file handle inside of OpenFile "foo" (\r -> ...). A common analogy to emphasize this is that there is no cake inside of a recipe for cake (or maybe "invoice" would be better in this case).

This model also works readily with concurrency. We can easily have a constructor for OSRequest like Fork :: (OSResponse -> IO ()) -> OSRequest and then the runtime can interleave the requests produced by this extra handler with the normal handler however it likes. With some cleverness you can use this (or related techniques) to actually model things like concurrency more directly rather than just saying "we make a request to the OS and things happen." This is how the IOSpec library works.

¹ Hugs used a continuation-based implementation of IO which is roughly similar to what I describe albeit with opaque functions instead of an explicit data type. HBC also used a continuation-based implementation layered over the old request-response stream-based IO. NHC (and thus YHC) used thunks, i.e. roughly IO a = () -> a though the () was called World, but it isn't doing state-passing. JHC and UHC used basically the same approach as GHC.