Conal asked me to write some thoughts on the
He has not seen a proof that
IO is a monad and was wondering if it really is.
I do not think I can prove that
IO is a monad, since I do not know exactly what
IO is, but I think I can provide some evidence that
IO is a monad by giving a partial model of
IO that is a monad.
Wait a minute! Look up at the title. Doesn’t the title say that I/O is not a monad?
Well, I want to distinguish between I/O that is model of input and output, and the abstract data type constructor
The story you are about to read is a fib, but it is short. The names are made up, but the problems are real. It starts on Sunday, March 1st 1992. The Haskell 1.2 report was released. Back then, Haskell had the following mechanism for I/O
type Dialogue = [Response] -> [Request] main :: Dialogue
main program would create a lazy list of system requests.
Request was an algebraic data type that had a series of constructors such
data Request = ReadChan String | AppendChan String String | GetArgs ... stdin, stdout :: String stdin = "stdin" stdout = "stdout"
For each request made, the run time system would preform some I/O effect and return a
main function could access this response by reading it from the lazy list parameter. The possible responses were also an algebraic data type.
data Response = Success | Str String | StrList String | Bn Bin | Failure IOError
There are some advantages of this model of I/O. Because the type of
a concrete data type, it is easier to understand what the model of I/O is in Haskell 1.2.
However this model of I/O is actually pretty bad.
When writing your code in Haskell 1.2, you need to make sure that you always consume
Response for each
Request you make.
If you ever become out of sync, problems arise.
If you do not consume a
Response after you make
Request you will end up
reading the wrong response for the next
If you consume a
Response before making your
Request, I expect your code
By most accounts, this was a pretty awful way of interacting with I/O.
The problem is that nothing in the type of
Dialogue enforces that the first n + 1 elements of the
Requests list should depend on exactly the first n elements of the
Response list. Fortunately, we can make a new data type that captures this invariant.
data Dialogue1 = Stop | Go Request (Response -> Dialogue1)
Dialogue1 type now exactly captures the notion of a stream transformer
[Request] that satisfies our invariant. Notice that
the data structure for
Dialogue is a tree holding a
Request at each node
and has branch for each
We can write an interpreter from
intepret1 :: Dialogue1 -> Dialogue intepret1 Stop _ =  intepret1 (Go req cont) resps = req:rest resps where rest (hresp:tresp) = intepret1 (cont hresp) tresp
We can do even better.
Certain requests only produce certain responses, so we can refine our
data type to only respond appropriately to requests by adding a constructor for each
data Dialogue2 = Stop2 | ReadChan2 String (Either IOError String -> Dialogue2) | AppendChan2 String String (Either IOError () -> Dialogue2) | GetArgs2 ( [String] -> Dialogue2) ...
IOErrors could even be refined if you desired.
We have the obvious interpretation from
intepret2 :: Dialogue2 -> Dialogue1 intperet2 Stop2 = Stop intperet2 (ReadChan2 s cont) = Go (ReadChan s) rest where rest (Str resp) = cont (Right resp) rest (Failure err) = cont (Left err) intperet2 (AppendChan2 s1 s2 cont) = Go (AppendChan s1 s2) rest where rest Success = cont (Right ()) rest (Failure err) = cont (Left err) intperet2 (GetArgs2 cont) = Go (GetArgs) rest where rest (StrList sl) = cont sl
After this was developed Haskell 1.2.5 was released (not really) with this new
Dialogue2 type for
main and things were much better. It was now impossible
for one’s requests and responses to become out of sync, and you only needed to handle
responses that were possible for your requests.
Notice that there is no monad anywhere. There are not even any type constructors around. This is why I/O is not a monad. A model of I/O is a data type, not a data type constructor.
What we can do is write a data type constructor along with some combinators to make
it easier to build this
Let us call this new type constructor
data IO a = StopIO a | ReadChanIO String (Either IOError String -> IO a) | AppendChanIO String String (Either IOError () -> IO a) | GetArgsIO ( [String] -> IO a) ...
All we have done is add a parameter to
Stop to hold a polymorphic value.
The resulting data type
IO (), the type of
main in Haskell 1.3, is isomorphic to
Dialogue2 (I will not even bother writing out the isomorphism).
We can write combinators to build
IO a out of smaller pieces, with the ultimate
goal of building an
IO () value.
instance Monad IO where return a = StopIO a (StopIO a) >>= f = f a (ReadChanIO s cont) >>= f = ReadChanIO s (\resp -> cont resp >>= f) (AppendChanIO s1 s2 cont) >>= f = AppendChanIO s1 s2 (\resp -> cont resp >>= f) (GetArgsIO cont) >>= f = GetArgsIO (\resp -> cont resp >>= f)
These combinators satisfy the monad laws, so this data type constructor
IO is a
monad, even though the type modeling input and output, which is
IO (), is not. In fact, this monad is a free monad. That is why I call this the free monad model of
One might want to identify different values of
IO () (or
Dialogue2) as representing equivalent I/O. Such an equivalence relation should lift (naturally?) to an
equivalence relation on
IO a and that would produce a non-free monad model of
IO would still be a monad.
This idea of generalizing data types into monads is useful in general. I have used it in the past when writing an assembler.
newtype AssemblyCodeMonad a = AssemblyCodeMonad (RWS () [Instruction Register] Location a) deriving (Monad, MonadFix) type AssemblyCode = AssemblyCodeMonad ()
Exercise for the reader: Extend
Dialogue2 to support concurrency.
Then check to see if this can still be generalized to a monad in the same way that we
have done for sequential I/O.