I/O is not a monad

2011-05-20T22:02:01Z

Conal asked me to write some thoughts on the IO monad. 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 IO.

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

One’s main program would create a lazy list of system requests. Request was an algebraic data type that had a series of constructors such as

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 Response. The 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 main is 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 a 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 Request. If you consume a Response before making your Request, I expect your code would deadlock.

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)

Our new Dialogue1 type now exactly captures the notion of a stream transformer from [Response] to [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 Response.

We can write an interpreter from Dialogue1 to Dialogue

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 Dialogue1 data type to only respond appropriately to requests by adding a constructor for each Request.

data Dialogue2 = Stop2
               | ReadChan2   String        (Either IOError String   -> Dialogue2)
               | AppendChan2 String String (Either IOError ()       -> Dialogue2)
               | GetArgs2                  (               [String] -> Dialogue2)
               ...

The IOErrors could even be refined if you desired. We have the obvious interpretation from Dialogue2 to Dialogue1.

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 Dialogue2 type. Let us call this new type constructor IO.

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

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. However, 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.

Tags

,

Responses


Russell O’Connor: contact me