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.

 
25
Kudos
 
25
Kudos

Now read this

Types as Units

A few years ago, Steve Yegge wrote a great piece arguing that software developers can be divided into conservatives and liberals, and moreover that, like in politics, there are some issues where the dividing lines are very clear. The... Continue →