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.