Yet Another Monad Tutorial (part 3: The Monad Laws)
In the previous article I talked about the two fundamental monadic operations in the Monad type class: the bind operator (>>=) and the return function. In this article I'll complete the definition of the Monad type class and talk about monad laws.
The full Monad type class
Let's look at the entire definition of the Monad constructor class:
class Monad m where (>>=) :: m a -> (a -> m b) -> m b return :: a -> m a (>>) :: m a -> m b -> m b fail :: String -> m a
We see the familiar >>= operator and the return function, with the expected types, but there is also one other operator called >> and one other function called fail. What do they mean?
The fail function is basically a very primitive kind of error reporting function. It is called when the >>= operator can't bind the value of type a to the input of the function of type a -> m b because of a pattern match error. I don't want to go into the details of this here because it's boring; see the documentation on the Haskell web site for more on this if you care. Most of the time you don't need to concern yourself with fail.
The >> operator is a bit more interesting. It has the type:
(>>) :: m a -> m b -> m b
What this operator does is act as a monadic sequencing operator. Specifically, it's a version of monadic apply (>>= or "bind") which throws away the unpacked value of type a before executing the "action" of type m b. It's defined as follows:
mv1 >> mv2 = mv >>= (\_ -> mv2)
From this we can see that whatever value is unpacked from the monadic value mv1, it is discarded and then the final monadic value mv2 is returned. This turns out to be useful when the unpacked value has type () i.e. the unit type. A good example is the putStrLn function:
putStrLn :: String -> IO ()
Imagine if you wanted to print two strings, one after another, with newlines at the end of each string. You can write this as follows:
(putStrLn "This is string 1.") >> (putStrLn "This is string 2.")
It turns out that the >> operator has lower precedence than normal function application (via juxtaposition of the arguments to the function), so we can leave off the parentheses:
putStrLn "This is string 1." >> putStrLn "This is string 2."
Regardless, why does this work? Let's look at the types:
(putStrLn "This is string 1.") :: IO () (putStrLn "This is string 2.") :: IO ()
So what the >> operator is doing is combining two monadic values of type IO () to generate one resulting monadic value of type IO (). Let's take the >> operator and specialize it for this case:
(>>) :: m a -> m b -> m b
Here, m is IO and a and b are both (), so here,
(>>) :: IO () -> IO () -> IO ()
This makes it at least plausible that what >> is doing is to run the two string printing "actions" one after another.
Here's a more complicated example. We want to read a line of text from the terminal and print it back out twice. We can do it as follows:
readAndPrintLineTwice :: IO () readAndPrintLineTwice = getLine >>= (\s -> (putStrLn s >> putStrLn s))
Because of operator precedences, we can write this without parentheses as:
readAndPrintLineTwice :: IO () readAndPrintLineTwice = getLine >>= \s -> putStrLn s >> putStrLn s
Let's figure out what this means. getLine is a monadic value ("action") which reads a line of text from the terminal. The >>= operator "unpacks" this line of text from the monadic value and binds it to the name s (because \s -> putStrLn s >> putStrLn s is the monadic function that is the second argument to >>=). Then the string called s is used by the monadic value putStrLn s >> putStrLn s, which prints out the string twice in sequence.
If this still seems mysterious to you, it's not your fault. There is something odd going on under the covers here, but I won't be able to explain exactly what until I talk about state monads later. But at least you should be able to follow what is happening, even if you aren't clear on exactly how it all happens.
Right now, I want to take a step back and look at monad laws, which have a big impact on what the definitions of the >>= operator and the return function are going to be for any given monad. After this, we'll get back to more practical matters.
The Three Laws of Monadics
Lots of important laws come in groups of three: Newton's three laws of motion, the three laws of thermodynamics, Asimov's Three Laws of Robotics, Kepler's three laws of planetary motion, etc. etc. Monads are no different, except that the "Three Laws of Monadics" are, of course, far more important than the others ;-)
In order for the >>= operator and the return function to be a valid definition of these operators/functions for a particular monad, they have to have the correct types for that monad. So, for instance, the definitions of >>= and return for the Maybe monad will have the types:
(>>=) :: Maybe a -> (a -> Maybe b) -> Maybe b return :: a -> Maybe a
and for the IO monad they would have the types:
(>>=) :: IO a -> (a -> IO b) -> IO b return :: a -> IO b
However, this isn't enough. These operators/functions are also required to satisfy three "monad laws". The monad laws are actually very simple; they simply guarantee that monadic function composition behaves in a reasonable way. I'll give you the "nice" version of the monad laws first and then show you the (ugly) way in which they are usually described. (You'll thank me - the nice way is really much easier to understand.)
The nice version
Here is the nice definition of the three monad laws, in terms of monadic function composition (recall that the (>=>) operator is the monadic function composition operator):
1. return >=> f == f 2. f >=> return == f 3. (f >=> g) >=> h == f >=> (g >=> h)
What do these laws tell us?
Laws 1 and 2 tell us what return is supposed to be: it's an identity for monadic function composition (rule 1 says that return is a left identity, and rule 2 says that return is a right identity). In other words, composing a monadic function f with return (on either side) just gives you f back. This is analogous to the fact that 0 is an identity under addition of integers or 1 is an identity under multiplication of integers; in each case, the identity element combined with an arbitrary value using the appropriate operation just gives you the value back.
Law 3 tells us that monadic function composition is associative: when we want to compose together three monadic functions (f, g, and h), it doesn't matter which one we compose first. This is analogous to the fact that addition or multiplication are associative when applied to integers.
Why are these laws plausible? Let's look at the corresponding "laws" that regular function composition obeys:
1. id . f == f 2. f . id == f 3. (f . g) . h == f . (g . h)
where id is the identity function. Notice the similarity? Composing a function with the identity function on either the right or left side gives the original function back, and function composition is associative. Similarly, monadic function composition should be associative, and return should be the monadic equivalent of the identity function, in order for monadic function composition to be as well-behaved as regular function composition.
What's the significance of these laws from the programmer's standpoint? Since we want our monads to behave in a sensible way, we want our definitions of return and >>= for each monad to obey these laws. This often can help us figure out what the correct definitions of return and >>= have to be for a given monad, and we'll see this later. [Note that the monad laws as I've defined them are in terms of the >=> operator and not the >>= operator, but we'll see a version using the >>= operator below that is equivalent.]
However, there is a catch: Haskell does not enforce the monad laws! The only thing Haskell cares about is that the definitions of return and >>= for a particular monad have the correct types. Whether they also obey the monad laws or not is up to the programmer.
Many people have thus asked "Why can't Haskell enforce the monad laws?" And the answer is simple: Haskell isn't powerful enough! To get a programming language and environment powerful enough to allow you to state and enforce monad laws from within the language, you would need to have something like a theorem prover. Theorem provers are fascinating, and for all I know they may represent the future of programming, but they are much more complicated than conventional programming languages. If you're interested in this, there is a well-respected theorem prover called Coq, and it's available here. But in Haskell, it's up to the programmer who writes the definition of any particular monad to make sure that the monad laws are upheld in that definition.
The ugly version
The problem with the nice version of the monad laws is that we don't define the >=> operator directly when defining a monad as an instance of the Monad type class; instead we define the >>= operator and then >=> follows from that as I've shown above. So if we want to constrain our definitions of return and >>= for any particular monad, we should have a version of the monad laws that only involve return and >>=. And this is what most Haskell textbooks and online documentation usually refer to when they discuss monad laws, even though it's far less intuitive than the definitions I gave in the last section.
In terms of the >>= operator and the return function, the three monad laws are:
1. return x >>= f == f x 2. mv >>= return == mv 3. (mv >>= f) >>= g == mv >>= (\x -> (f x >>= g))
where the types of the various values are:
mv :: m a f :: a -> m b g :: b -> m c
for some types a, b, and c and some monad m.
Deriving the ugly version of the monad laws from the nice version
For fun, let's see how we can take the nice version of the monad laws and derive the ugly version from it. We will use this definition in the derivations:
f >=> g = \x -> (f x >>= g)
which I discussed above.
Law 1:
return >=> f == f \x -> (return x >>= f) == \x -> f x return x >>= f == f x -- Q.E.D.
Note that \x -> f x is identical to f as described above.
Law 2:
f >=> return == f \x -> (f x >>= return) == \x -> f x f x >>= return == f x let mv == f x mv >>= return == mv -- Q.E.D.
Law 3:
(f >=> g) >=> h == f >=> (g >=> h) \x -> ((f >=> g) x >>= h) == \x -> (f x >>= (g >=> h)) (f >=> g) x >>= h == f x >>= (g >=> h) (\y -> (f y >>= g)) x >>= h == f x >>= (\y -> (g y >>= h)) evaluate (\y -> (f y >>= g)) x on LHS to: (f x >>= g) (f x >>= g) >>= h == f x >>= (\y -> (g y >>= h)) let mv == f x (mv >>= g) >>= h == mv >>= (\y -> (g y >>= h)) substitute f for g, g for h (mv >>= f) >>= g == mv >>= (\y -> (f y >>= g)) substitute x for y in RHS (mv >>= f) >>= g == mv >>= (\x -> (f x >>= g)) -- Q.E.D.
The evaluate (\y -> ...) x step just applies the (\y -> ...) function to x to get the result. This works by substituting x for y in the body of (\y -> ...) (the body is the part marked ...) to give the result. In functional programming lingo, this is called beta-reduction, which is the basic way functions get evaluated. The last step, where x is substituted for the bound variable y, is correct in the same way that these two functions:
\x -> f x \y -> f y
are the same (the name of the formal argument is irrelevant). In functional programming lingo, we say that the two functions are alpha-equivalent. The other steps should be straightforward.
What's the point?
The monad laws can occasionally be useful when writing code; you can always take the longer form of an expression and rewrite it as the shorter form (for instance, replace all expressions of the form return x >>= f with just f x). However, the main utility of monad laws is in deriving the definitions of return and >>= for particular monads, which we'll see later in this series.
To wrap up this article, I want to show you a neat syntactic shorthand that can make writing monadic code a whole lot more pleasant.
The "do-notation"
Recall the readAndPrintLineTwice function we defined above:
readAndPrintLineTwice :: IO () readAndPrintLineTwice = getLine >>= \s -> putStrLn s >> putStrLn s
The good thing about this function is that it can be defined on a single line. The bad thing is that it's not exactly the most readable line in the world. The Haskell language designers noticed that monadic definitions were often hard to read and thought up a really nice bit of syntactic sugar to make these kinds of definitions more readable.
The basis of this syntactic sugar is the observation that a large number of operations in monadic code have one of the following two forms:
-- Form 1. -- mv :: m a -- f :: a -> m b mv >>= \x -> f x -- Form 2. -- mv :: m a -- mv2 :: m b mv >> mv2
Therefore, a notation was figured out that made both of these forms very readable. It starts with the keyword do followed by some monadic operations. Here are our two examples in the do notation:
-- Form 1, do-notation. do v <- mv f v -- Form 2, do-notation. do mv mv2
In form 1, the first line says that we take the monadic value mv and "unpack" it into a regular value called v. The second line just says that we then compute f v. The result of f v is the result of the entire expression.
In form 2, the first line says that we "perform" the monadic value ("action") mv. The second line says that we "perform" the monadic value ("action") mv2. So this is just a notation to describe the sequencing of mv and mv2 using the >> operator.
What the Haskell compiler does is convert the do-notation versions of Form 1 and Form 2 into the versions without do. This is just a syntactic transformation, and the meaning is identical. Furthermore, you can mix the two forms, and have multiple forms of each types. For instance:
-- mv :: m a -- v1 :: a -- f :: a -> m b -- v2 :: b -- mv3 :: m c do v1 <- mv v2 <- f v1 mv3 return v2
This means exactly the same thing as:
mv >>= (\v1 -> (f v1 >>= (\v2 -> (mv3 >> (return v2)))))
Or, without the parentheses, as:
mv >>= \v1 -> f v1 >>= \v2 -> mv3 >> return v2
You can imagine that as the monadic expressions get larger, the do form will continue to be easy to read, while the form without do (called the "desugared" form) will often be very hard to read. That's why this notation exists. What's cool is that this notation works for all monads, not just for any particular one.
You're also allowed to mix do-notation with the desugared notation, like this:
do v1 <- mv v2 <- f v1 mv3 >> return v2
Sometimes this is useful, but it can also often lead to ugly hard-to-read code.
Let's look at what our earlier examples would look like with the do-notation.
-- Read a line, then print it. readAndPrintLine :: IO () readAndPrintLine = do line <- getLine putStrLn line -- Print two lines, one after another. -- Not a function. do putStrLn "This is string 1." putStrLn "This is string 2." -- Read a line and print it twice. readAndPrintLineTwice :: IO () readAndPrintLineTwice = do line <- getLine putStrLn line putStrLn line
In all three cases, the do-notation makes the code significantly easier to read. Interestingly, it has the added benefit (or drawback, depending on your perspective) of making Haskell code look like imperative code! If we read a do-expression top to bottom, it looks like it was written in an imperative language that uses <- as an assignment statement. For instance, readAndPrintLine can be described as: "use getLine to read a line, which you put into the variable line; then use putStrLn to print out that variable." This is emphatically not what's actually happening (for instance, line is not a variable), but you can read the code as if it is. When you're dealing with code that does a lot of input and output, it can be very convenient to be able to write it this way.
The do-notation includes other features as well. For instance, you can incorporate let statements and case statements into the body of a do expression, and this is often handy. I won't go into this here, though, because it's pretty routine - see any Haskell tutorial for more details.
Next time
In the next installment I'll start deriving monads, starting with the Maybe monad (for computations that can fail) and continuing with the list monad (for computations that can return multiple results).