IO Monads: GHC Implementation Meaning vs. Mathematical Meaning

Question

Consider

ioFunction :: String -> IO ()
ioFunction str = do putStrLn str
                    putStrLn "2"

Here, ioFunction, from a mathematical point of view, is a function that takes one input and returns a value of type IO (). I presume it means nothing else. That is, from a mathematical point of view, this function returns a value and nothing else; in particular, it doesn't print anything.

So does this mean that the way Haskell uses the IO monad for imperative side-effects (in this case: that running this function will first print str and then print "2", in that order) is purely a GHC implementation detail that has nothing to do with the mathematical (and in some sense even the Haskell) meaning of the term?

EDIT: To make this question clearer, what I mean to ask is, for example, is there any difference from the mathematical point of view between the following two functions:

ioFunction1 :: String -> IO ()
ioFunction1 str = do putStrLn str
                     putStrLn "2"


ioFunction2 :: String -> IO ()
ioFunction2 str = do return ()

It seems the answer is no, for -- from the mathematical point of view -- they both take as input a String and return a value (presumably, the same value) of type IO (). Is this not the case?

Answer 1

For simplicity, let us concentrate on the output aspect of the I/O monad. Mathematically speaking, the output (writer) monad is given by an endofunctor T with T(A) = U* × A, where U is a fixed set of characters, and U* is the set of strings over U. Then ioFunction : U* → T (), i.e. ioFunction : U* → U* × (), and ioFunction(s) = (s++"\n"++"2\n", ()). By contrast, ioFunction2(s) = ("", ()). Any implementation has to respect this difference. The difference is primarily a mathematical one, not an implementation detail.

Answer 2

I always find it helpful to consider a simplified “imperative-language source code” implementation of the IO monad:

data IO :: * -> * where
   PutStr :: String -> IO ()
   GetLine :: IO String
   IOPure :: a -> IO a
   IOSeq :: IO a -> IO b -> IO b
   ...
   LaunchMissiles :: IO ()

Then what ioFunction is quite clearly a proper, sensible function in the mathematical sense:

ioFunction str = do putStrLn str
                    putStrLn "2"
               = putStr (str++"\n") >> putStrLn "2\n"
               = IOSeq (PutStr (str++"\n")) (PutStrLn "2\n")

This is simply a data structure representing effectively some source code of an imperative language. ioFunction places the given argument in a specific spot in the result structure, so it's mathematically very much not just a trivial “return () and nothing else (something may happen but it's a GHC implementation detail)”.

The value is indeed completely different for ioFunction2:

ioFunction2 str = do return ()
                = return ()
                = IOPure ()

---

how do we know they are different in this sense?

That's a good question. Practically speaking, you know it by executing both programs and observing that they cause different effects, hence they must have been different. This is more than a little awkward of course – “observing what happens” isn't maths, it's physics, and the observation would scientifically require that you execute twice under exact the same environment conditions.

Worse, even with pure values that are generally taken to be mathematically the same you can observe different behaviour: print 100000000 will immediately cause the side-effect, whereas print $ last [0..100000000] takes a significant pause (which, if you follow it with a time-printing command, can actually yield different text output).

But these issues are unavoidable in a real-world context. It hence makes only sense that Haskell's does not specify any structure on IO that could with mathematical rigour be checked for equality from within the language. So, in quite some sense you really can't know that putStrLn str >> putStrLn "2" is not the same as return ().

And indeed they might be the same. It is conceivable to make a even simpler toy implementation of IO than the above thus:

data IO :: * -> * where
   IONop :: IO ()
   IOHang :: IO a -> IO a

and simply map any pure output operation to the no-op (and any input to an infinite loop). Then you would have

ioFunction str = do putStrLn str
                    putStrLn "2"
               = IONop >> IONop
               = IONop

and

ioFunction2 str = return ()
                = IONop

This is a bit as if we've imposed an additional axiom on the natural numbers, namely 1 = 0. From that you can then conclude that every number is zero.

Clearly though, that would be a totally useless implementation. But something similar could actually make sense if you're running Haskell code in a sandbox environment and want to be utterly sure nothing bad happens. http://tryhaskell.org/ does something like this.

Answer 3

Here, ioFunction, from a mathematical point of view, is a function that takes one input and returns a value of type IO (). I presume it means nothing else.

Yes. Exactly.

So does this mean that the way Haskell uses the IO monad for imperative side-effects (in this case: that running this function will first print str and then print "2", in that order) is purely a GHC implementation detail that has nothing to do with the mathematical (and in some sense even the Haskell) meaning of the term?

Not quite. From a mathematical (set-theory) standpoint, I would assume "same" means structurally identical. Since I don't know what makes up a value of IO (), I can't say anything about whether two values of that type are the same or not.

In fact, this is by design: by making IO opaque (in the sense that I don't know what constitutes an IO), GHC prevents me from ever being able to say that one value of type IO () is equal to another. The only things I can do with IO is exposed through functions like fmap, (<*>), (>>=), mplus, etc.