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 IOError
s 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.