Addendum: Deriving the Third Monad Law From Nested Comprehensions
The third monad law declares that the following identity must hold for a monad M
, where a:M<A>
, f: A -> M<B>
, and g: B -> M<C>
:
(a >>=- f) >>=- g == a >>=- { b in f(x) >>=- g }
To motivate this, we first want to show that the snippet below is a form of the left-hand-side of the identity:
// Form 1
let val = for {
b <- for {
ignore <- doSomething()
b1 <- doSomething()
} yield {
b1
}
c <- process(b) // process(val:Int?) -> Int?
} yield {
c
}
Then we want to show that Form 2 below is a form of the right-hand-side:
// Form 2
let val = for {
ignore <- doSomething()
b <- doSomething()
c <- process(b) // process(val:Int?) -> Int?
} yield {
c
}
Intuitively, these two snippets should do the same thing, which is the impetus for enshrining the behavior in a law.
• • • • •
Remembering that the right-hand side of a <-
assignment is monadic, we can write Form 1 as:
// Form 1
let optB = doSomething() >>=- { ignore in
doSomething() >>=- { b in
lift(b)
}
let val = optB >>=- { b in
process(b) >>= { c in {
lift( c)
}
}
Clearly, we can rewrite the snippet like this:
// Form 1
let val = doSomething() >>=- { ignore in
doSomething() >>=- lift
} >>=- { b in
process(b) >>=- lift
}
Notice, incidentally, that nested for-comprehensions are the equivalent of chained >>=-
calls. Using the second monad law (see, it’s useful), we can simplify it as:
// Form 1
let val = doSomething() >>=- { ignore in
doSomething()
} >>=- { b in
process(b)
}
Now let’s simplify by introducing the definition of
doSomethingWhileIgnoring
:
func doSomethingWhileIgnoring(ignored:Int) -> Int? {
return doSomething()
}
This takes us to the final form, with added parentheses to emphasize that >>=-
is a left-associative operator.
// Form 1
let val = (doSomething() >>=- doSomethingWhileIgnoring) >>=- process
• • • • •
For the second snippet, we’re going to work backwards. This means I’m going to start with what I already know I’m trying to get to, and I’m going to show you that it’s equivalent to Form 2. This is just as valid as going from Form 2 to the final result, but it’s easier to follow. What I want to show is that this snippet is the same as Form 2:
// Form 2 candidate
let val = doSomething() >>=- { ignore in
doSomethingWhileIgnoring(ignore) >>=- process
}
So let’s get to substituting:
// Form 2 candidate
let val = doSomething() >>=- { ignore in
{ _ in doSomething() }(ignore) >>=- { b in
process(b)
}
}
And now, using the second law, but in reverse, we have:
// Form 2 candidate
let val = doSomething() >>=- { ignore in
{ _ in doSomething() }(ignore) >>=- { b in
process(b) >>=- { c in
lift(c)
}
}
}
Finally, it’s pretty clear that the second line is an unnecessary wrapper, and that we can write it as:
// Form 2 candidate
let val =
doSomething() >>=- { ignore in
doSomething() >>=- { b in
process(b) >>=- { c in
lift(c)
}
}
}
But this is precisely the >>=-
version of Form 2.
• • • • •
Again, remember that this appendix is not proving the law, but instead showing how it naturally comes out of expecting intuitive semantics from for-comprehensions. In the context of monads, “law” doesn’t mean something observed to be true, but rather a prescribed rule that a type must follow in order to be called a monad.