# Monad Laws

Every data structure has not just a signature, but some expected behavior. For example, a stack has a push and a pop operation, and we expect those operations to satisfy certain laws:

- for all
`x`

and`s`

, it holds that`peek (push x s) = x`

- for all
`x`

, it holds that`pop (push x empty) = empty`

- etc.

The laws for a given data structure usually follow from the specifications for its operations, as do the two examples laws given above.

A monad, though, is not just a single data structure. It's a design
pattern for data structures. So it's impossible to write specifications
of `return`

and `>>=`

for monads in general: the specifications would need
to discuss the particular monad, like the writer monad or the Lwt monad.

On the other hand, it turns out that we can write down some laws that
ought to hold of any monad. The reason for that goes back to one
of the intuitions we gave about monads, namely, that they represent
computations that have effects. Consider Lwt, for example. We might
register a callback C on promise X with `bind`

. That produces a new
promise Y, on which we could register another callback D. We expect
a sequential ordering on those callbacks: C must run before D, because
Y cannot be resolved before X.

That notion of *sequential order* is part of what the monad laws stipulate.
We will state those laws below. But first, let's pause to consider
sequential order in imperative languages.

## Sequential Order in Imperative Languages

In languages like Java and C, there is a semicolon that imposes a sequential order on statements, e.g.:

```
System.out.println(x);
x++;
System.out.println(x);
```

First `x`

is printed, then incremented, then printed again. The effects that
those statements have must occur in that sequential order.

Let's imagine a hypothetical statement that causes no effect whatsoever.
For example, `assert true`

causes nothing to happen in Java. (Some compilers
will completely ignore it and not even produce bytecode for it.)
In most assembly languages, there is likewise a "no op" instruction whose
mnemonic is usually `NOP`

that also causes nothing to happen. (Technically,
some clock cycles would elapse. But there wouldn't be any changes
to registers or memory.) In the theory of programming languages, statements
like this are usually called `skip`

, as in, "skip over me because I don't
do anything interesting."

Here are two laws that should hold of `skip`

and semicolon:

`skip; s;`

should behave the same as just`s;`

.`s; skip;`

should behave the same as just`s;`

.

In other words, you can remove any occurrences of `skip`

, because it has
no effects. Mathematically, we say that `skip`

is a *left identity* (the first law)
and a *right identity* (the second law) of semicolon.

Imperative languages also usually have a way of grouping statements together into blocks. In Java and C, this is usually done with curly braces. Here is a law that should hold of blocks and semicolon:

`{s1; s2;} s3;`

should behave the same as`s1; {s2; s3;}`

.

In other words, the order is always `s1`

then `s2`

then `s3`

, regardless
of whether you group the first two statements into a block or the second two into
a block. So you could even remove the braces and just write `s1; s2; s3;`

, which
is what we normally do anyway. Mathematically, we say that semicolon is
*associative.*

## Sequential Order with the Monad Laws

The three laws above embody exactly the same intuition as the monad laws, which we will now state. The monad laws are just a bit more abstract hence harder to understand at first.

Suppose that we have any monad, which as usual must have the following signature:

```
module type Monad = sig
type 'a t
val return : 'a -> 'a t
val (>>=) : 'a t -> ('a -> 'b t) -> 'b t
end
```

The three monad laws are as follows:

**Law 1:**`return x >>= f`

behaves the same as`f x`

.**Law 2:**`m >>= return`

behaves the same as`m`

.**Law 3:**`(m >>= f) >>= g`

behaves the same as`m >>= (fun x -> f x >>= g)`

.

Here, "behaves the same as" means that the two expressions will both evaluate to the same value, or they will both go into an infinite loop, or they will both raise the same exception.

These laws are mathematically saying the same things as the laws for
`skip`

, semicolon, and braces that we saw above: `return`

is a left and
right identity of `>>=`

, and `>>=`

is associative.

Let's look at each law in more detail.

*Law 1* says that having the trivial effect on a value, then binding a function on it,
is the same as just calling the function on the value. Consider the maybe monad:
`return x`

would be `Some x`

, and `>>= f`

would extract `x`

and apply `f`

to it.
Or consider the Lwt monad: `return x`

would be a promise that is already resolved
with `x`

, and `>>= f`

would register `f`

as a callback to run on `x`

.

*Law 2* says that binding on the trivial effect is the same as just not having
the effect. Consider the maybe monad: `m >>= return`

would depend upon
whether `m`

is `Some x`

or `None`

. In the former case, binding would extract
`x`

, and `return`

would just re-wrap it with `Some`

. In the latter case,
binding would just return `None`

. Similarly, with Lwt, binding on `m`

would register
`return`

as a callback to be run on the contents of `m`

after it is resolved,
and `return`

would just take those contents and put them back into an already
resolved promise.

*Law 3* says that bind sequences effects correctly, but it's harder to see
it in this law than it was in the version above with semicolon and braces.
Law 3 would be clearer if we could rewrite it as

`(m >>= f) >>= g`

behaves the same as`m >>= (f >>= g)`

.

But the problem is that doesn't type check: `f >>= g`

doesn't have the right
type to be on the right-hand side of `>>=`

. So we have to insert an
extra anonymous function `fun x -> ...`

to make the types correct.

## Composition and Monad Laws

There is another monad operator called `compose`

that can be used to compose
monadic functions. For example, suppose you have a monad with type
`'a t`

, and two functions:

`f : 'a -> 'b t`

`g : 'b -> 'c t`

The composition of those functions would be

`compose f g : 'a -> 'c t`

That is, the composition would take a value of type `'a`

, apply `f`

to it, extract
the `'b`

out of the result, apply `g`

to it, and return that value.

We can code up `compose`

using `>>=`

; we don't need to know anything more about
the inner workings of the monad:

```
let compose f g x =
f x >>= fun y ->
g y
let (>=>) = compose
```

As the last line suggests, `compose`

can be expressed as
infix operator written `>=>`

.

Returning to our example of the maybe monad with a safe division operator, imagine that we have increment and decrement functions:

```
let inc (x:int) : int option = Some (x+1)
let dec (x:int) : int option = Some (x-1)
```

The monadic compose operator would enable us to compose those two into an identity function without having to write any additional code:

```
let id : int -> int option = inc >=> dec
```

Using the compose operator, there is a much cleaner formulation of the monad laws:

**Law 1:**`return >=> f`

behaves the same as`f`

.**Law 2:**`f >=> return`

behaves the same as`f`

.**Law 3:**`(f >=> g) >=> h`

behaves the same as`f >=> (g >=> h)`

.

In that formulation, it becomes immediately clear that `return`

is a left
and right identity, and that composition is associative.