I’ve given in to the unholy urge to write a monad tutorial. Here are some remarks that might help you decide whether it’s worth your time to read on.
My intended readers are programmers interested in functional programming, not mathematicians. No category theory is required.
All the code will be in Clojure. The level of Clojure expertise required is intermediate. The reader should be comfortable defining functions, especially functions that return functions as values, and should understand the comp operator. That said, there is nothing in the code that exploits features unique to Clojure. Everything I’m going to show you could easily be done Scheme or (I suspect) Ruby or Python.
My goal will be to explain what a monad is. That might seem too obvious to mention, but bear with me. Suppose I were writing about regular expressions. I might come up with several very different tutorials. One might discuss the languages recognized by finite state automata. Another might concern the symbolic technology used to describe regexes. Another tutorial might show how to use regexes to solve some particular class of problems. Someone new to regular expressions and looking for the third tutorial might well find the first confusing.
This tutorial will explain what a monad is, with as little mathematical formalism as possible. It does not attempt to show how to use monads to solve a variety of practical problems, nor does it make any use of the clojure.contrib.monads library. I try to keep things as concrete as I can, but a certain level of abstraction is inherent in the topic. I have put much effort into explaining the meaning of the so-called monad laws as clearly and intuitively as the subject and my ability allow.
Here’s the plan. We’ll start by solving a simple but not entirely trivial programming problem, using pure functional programming. We will not use mutable state, nor macros. A fairly natural solution falls out; that solution contains the elements that make up a monad. We’ll discus what those elements are, what the monad laws are, and what those laws mean.
So much for the prelude; let’s get started.
I will take as given that the function is the fundamental unit of modularity in functional programming, and that functions interact via composition. Here is our starting point.
The following two expressions are equivalent; both are examples of the composition of functions. The first example is more idiomatic, but we will be using the comp operator and the latter form extensively.
Our goal will be to build an enhanced composition operator, call it comp*, that traces the flow of data through composed functions. The comp* operator should compute the value one would expect, and also present intermediate results as data flows into and out of the functions that make up the computation. Here’s an example of what I have in mind.
The first problem we have to tackle is that Clojure functions do not have access to their names (they may not even have names), and so cannot provide their names to the proposed comp* operator. One way to get around that is to create enhanced functions that do know their names.
The type signature of (verbose f) is not the same as that of f. We are going to need to keep track of type signatures, so let’s introduce some terminology. I’ll refer to three types of functions, imaginatively called type 0, type 1, or type 2, depending on type signature, as follows:
- type 0 has signature Number->Number
- type 1 has signature Number->[String, Number]
- type 2 has signature [String, Number]->[String, Number]
By using verbose to create type 1 functions we have traded one problem for another. The type 0 functions sq and dbl could be composed with one another, but did not know their own names. The type 1 functions v-sq and v-dbl know their own names but they cannot be composed with one another. Their type signatures don’t allow it.
We seem to be at an impasse, since our goal is precisely to compose type 1 functions. Strictly speaking that is not possible, but let’s see what we can do. The way forward is to define a new function, which we will call bind.
Bind takes a type 1 function as input, and returns a type 2 function. Notice that unlike type 1 functions, type 2 functions can be composed.
The output traces the computation, but the calling syntax is ugly and puts too much burden on the user. We don’t want to have to call bind explicitly, nor to wrap the final argument by hand. And it would be nice to be able to compose an arbitrary number of functions. Not a problem.
That completes the first part of this tutorial. We solved the problem we set out to solve. Notice that we did so without using mutable state, without using macros, and without modifying the source code of the type 1 functions whose compositions we set out to trace. The entire solution was based on the creation of two functions, unit and bind, which we then used to implement some syntactic sugar, comp*.
In solving our toy problem, we built a monad. What is a monad? It is essentially a pair of functions, bind and unit, that satisfy three conditions known as the monad laws. The principal goal of this post is to present the monad laws in the simplest way possible. But we will start with somewhat complicated version of the monad laws. Why?
Clojure has an excellent monad library called clojure.contrib.monads. Its author, Konrad Hinsen, has written some fine monad tutorials which I hope this article will complement. I want this presentation to be useful to someone who might want to use Konrad’s work. That means I need to bridge the gap between my exposition and his. I will start by considering the monad laws as Konrad presents them in part 2 of his Monad Tutorial for Clojure Programmers.
Yow! That is quite something to get your head around. I promised a simple version the monad laws. Here’s my first cut, with a simpler version still to come.
Comparing Konrad’s presentaton and mine, it is evident that we are not using the same terminology. Allow me to translate. The function I call bind, Konrad calls m-bind. What I call unit, Konrad calls m-result. I use f and g, he uses function, function1, and function2. But those are just names, and not terribly important.
The important difference between Konrad’s version of the monad laws and mine stems from the fact that I define bind as a function of a single argument. My bind takes a function as an argument, and returns a function. Konrad’s version of bind takes two arguments, a function f and a value x, and it returns a value computed using f and x. The returned value is generally not a function. The monad laws describe the contracts that bind and unit must fulfill. Not surprisingly, the arity of bind affects the written formulation of the monad laws. By reducing the arity of bind, I get a simpler set of laws.
Why did I choose one way and Konrad the other? Because we had different purposes in mind. Konrad wanted to build a monad library, I wanted to present the monad laws in the simplest manner possible.
I chose to write bind in a point-free style precisely because that style allows a simpler formulation of the monad laws. Konrad chose his version of bind because it is better suited than mine to the business of building a monad library. In particular, his choice to reverse the usual order of arguments and go with (m-bind [x function] …) instead of (m-bind [function x]…) was brilliant. I hope to explore that idea in another posting.
I promised you a simple version of the monad laws. We’re not there yet. To get there, we are going to do two things. One is that we will abandon Clojure’s prefix notation in favor of infix notation. The second amounts to a change of variables. Notice the repetition of the pattern (comp (bind f) g) in my version of the monad laws. This is a sign of a missing abstraction. We’ll write (comp (bind f) g) as f * g, and write (comp f g) as f . g.
Then we can write the monad laws as follows. Here parentheses serve only to indicate operator precedence, and bind has precedence over composition.
Together, the first two monad laws require that unit be an identity element with respect to the * operator. Just as 0 is an identity element with respect to addition and for every x, x+0 = 0+x = x, so unit is an identity element with respect to *, and for every f, f*unit = unit*f = f. Identity elements are sometimes called unit elements, which is why I prefer the name unit over the more commonly used return, or Konrad’s m-result. I think return is an especially unfortunate choice of name, because the word return is already overloaded with other associations.
Take a hard look at that third monad law. Does it seem familiar? You have probably seen that pattern before. Compare the third monad law to the law of logarithms:
Both log and bind follow the general pattern foo(a ⊕ b) = foo(a) ⊗ foo(b). Functions that have this property are called homomorphisms. The logarithm function is typically the first and certainly the most important homomorphism that most of us encounter. But I promised no category theory, and the spirit of that promise demands that I not pursue abstract algebra either. Let’s take a different approach, and think about type signatures.
We invented bind in order to get around the fact that type 1 functions cannot be composed. Recall that if f and g are type 1, then (bind f) and (bind g) are of type 2, and type 2 functions can be composed with one another. Notice that (bind f) can be also be composed with g, resulting in a type 1 function. So there are two ways to use bind, f, and g to create a type 2 function. One is (comp (bind f) (bind g)). The other is (bind (comp (bind f) g)). The third monad law demands that these two ways of building a type 2 function result in exactly the same function.
Okay, we have defined bind and unit. We have contemplated the monad laws. Now it’s time to bite the bullet and show that our particular bind and unit in fact satisfy the monad laws. In each of the cases below, the functions f and g are assumed to be of type 1.
The first monad law states that (= (comp (bind f) unit) f).
Asserting the equality of the functions f and (comp (bind f) unit) is equivalent to asserting that for any and every type-appropriate argument n, (f n) is equal to ((comp (bind f) unit) n). Here’s the proof.
The second monad law asserts that (= (comp (bind unit) f) f). We need to show that for any f and any type appropriate n, (f n) is equal to ((comp (bind unit) f) n). Here we go.
Keep in mind that this sort of gruntwork is not part of the day to day use of monads. Only the monad designer needs to establish that the monad laws hold.
We have just one more law to go. I tried doing the next proof in the style of the first two proofs, but found the prefix notation tough sledding. I’m going to switch to infix notation. I love prefix for programming, but infix seems better suited to doing algebra.
Here are the notational shortcuts I’ll be using:
- Bg denotes (bind g)
- f x denotes that the function f is applied to x
- f . g denotes (comp f g)
- f . g x denotes ((comp f g) x); notice composition has precedence over application.
- Functions are right associative: f g h x denotes f (g (h x)).
- Notice that f g h x is the same as f.g.h x
- x : y denotes the string concatenation (str x y)
- F x denotes (first x)
- S x denotes (second x)
- commas are whitespace
- [a, b] denotes a pair with elements a and b
Let’s describe the action of bind in the infix notation:
Instead of ((bind g) [t x]) we’ll write Bg [t x].
We’ll make heavy use of this identity, which is the definition of bind written in the new notation: Bg [t x] = [t : F.g x, S.g x ]
Make sure that makes sense to you, or just skip the next section entirely.
The third monad law states that (comp (bind f) (bind g)) = (bind (comp (bind f) g)). We’ll write that as Bf . Bg = B(Bf . g).
To show this equality holds, we’ll show that for arbitrary [t x],
Bf . Bg [t x] = (B(Bf .g)) [t x] ;; call this ML3
First consider the left hand side of ML3.
Now consider the right hand side of ML3:
Hold that thought, while we figure out what h x is.
Now we know what h x is, and can substitute for F.h x and S.h x in expression B. In particular,
expression C shows us what h x is, and we see that
F.h x = F.g x : F.f.S.g x
S.h x = S.f.S.g x.
Substituting these into expression B give us
[t : F.h x, S.h x] =
[t : F.g x : F.f.S.g x, S.f.S.g x] ;; Call this D
Notice that expressions A and D are identical, which establishes ML3. We’re done. We showed that bind and unit satisfy the monad laws.
A remark by Donald Knuth comes to mind: “Beware of bugs in the above code; I have only proved it correct, not tried it”. I am not as brave as Professor Knuth, so I wrote some code to test whether the monad laws actually hold. The idea is to randomly generate functions, perform the appropriate compositions, and then test whether the laws hold. It’s actually pretty easy to do; you can get the code here. This post has already run longer than I expected; I’ll say no more about testing.
So what is a monad? It’s a pair of functions, bind and unit, which satisfy the monad laws. Bind and unit do not have fixed definitions like sine and cosine. Instead, they vary from monad to monad. But in all cases they must satisfy the monad laws. There is a bit more to it, in that the monad laws presumably operate on some specific set of functions. Here I waved my hands and called those functions type 1 functions. A more formal treatment would specify those functions more precisely, and consider a monad to be a triple, say bind, unit, and a type constructor, or some such. I chose to omit such considerations in favor of simplicity.
But in the context of programming, what are monads for? It is unfortunate that the term design pattern has been turned into a synonym for meta-boilerplate. Because design pattern might have been a fair description for the methodological role of monads The choice to write or use a monad is the choice to organize one’s code in a coherent, principled, and flexible fashion. My one example is hardly enough to show that. But perhaps it may help a programmer new to monads to better understand what the fuss is about, and to get started reading other material.
Speaking of further reading, most treatments of programming with monads default to the use of Haskell. But the Clojure community is fortunate to have some very good monad tutorials. Check out Konrad Hinsen’s and Jim Duey’s articles.
Credit where credit is due. I stole the use of the name unit, and the idea for my tracing example, from You Could Have Invented Monads, by Dan Piponi. I think this is a fantastic article, but it does require some knowledge of Haskell.
I hope you found this informative; thank you for your attention.