Correct by construction

I like a good research paper that really changes the way that I think about programming. One paper that did this for me, several years ago, is Deriving Backtracking Monad Transformers by Ralf Hinze. In it, he describes a technique for deriving monads (and monad transformers) from the specification.

I'm not going to go through the whole paper (read it for yourself!) but I'd like to talk a bit about how it made me understand what the "laws" of an abstraction actually are.

Let's suppose we want to implement the Identity monad. That is, we want a data type that only obeys the monad laws, and nothing else. How do we go about that, assuming nothing about the implementation?

If we really do assume nothing, then Identity is an abstract type, that you can only interact with through its observer. An observer is a function associated with the type which doesn't return a value of that type. In our case, the observer is runIdentity.

So let's try defining runIdentity, doing case analysis on the monad expression. A monad expression is either return o (>>=) (we're ignoring fail):

Trying the cases in turn:

runIdentity (return a) = a

Simple enough.

runIdentity (m >>= k) = ?

We're not sure what to do about this yet.

The left-hand-side of a bind is itself a monad expression, so let's try expanding that.

First, return. It turns out that we can just invoke a monad law:

runIdentity (return x >>= k) = k x

And similarly for bind, we can use the associative law:

runIdentity ((m >>= k1) >>= k) = runIdentity (m >>= (\x -> k1 x >>= k))

And, interestingly, that's it. We've now got an implementation that we can actually run, by implementing the monad expressions with data constructors:

> data Identity a where
>     ReturnId :: a -> Identity a
>     BindId :: Identity a -> (a -> Identity b) -> Identity b

> instance Monad Identity where

>     return = ReturnId

>     (>>=) = BindId

> runIdentity :: Identity a -> a

> runIdentity (ReturnId a) = a

> runIdentity (Bind (ReturnId x) k) = runIdentity (k x)

> runIdentity (Bind (Bind m k1) k) = runIdentity (Bind m (\x -> Bind (k1 x) k))

It's not a terribly efficient implementation, but it works as a prototype.

However, there's one other monad law that we didn't use, namely, this one:

m >>= return = m

The fact that we didn't use it raises an intriguing question: Is it important?

Stepping into category theory for the moment: Denoting the functor as T, the "return" operation as η and the "join" operation as μ (as is customary), the law states that:

μ o Tη = 1

which is, indeed, part of the definition of a monad. It's not a direct consequence of η or μ being natural transformations, so it's unlikely to be a consequence of a free theorem.

Hinze's paper points out that the law can be proven by induction on m. That's true in the case of Identity (or the other monads that he develops in the paper), but in the absence of a general proof, it's hard to see whether or not it would automatically hold true in general.

Certainly, the law turns out to be useful in developing the fancier monads, such as the backtracking one. But in a deep sense, you don't need the law to implement the monad, so it's not an axiom.

When developing his backtracking transformer, he does a similar thing. He asserts that a backtracking monad should, in modern notation, satisfy the following laws, amongst others:

mzero `mplus` m = m
m `mplus` mzero = m

Because the implementation is derived in a manner similar to Identity above (i.e. by expanding the leftmost monad expression if there's no obvious law that applies), the first law is used, but the second one isn't. It may well still be true (and it is), but it's not used and hence isn't an axiom.

This isn't a hypothetical, by the way. Until a couple of years ago, it was generally believed that MonadPlus instances should obey a right-zero law:

m >> mzero = mzero

The problem is that this law can't be obeyed by a monad transformer:

lift m >> mzero /= mzero

(I think I was the first person to explicitly point this out. Phil Wadler had previously noted that it's disobeyed if m is bottom. By the way, the Haddock documentation still gets this wrong.)

Of course, if you're deriving a monad using the Hughes/Hinze method, this "law" turns out not to be used. (Unsurprising in retrospect, since it's incorrect!)

It's after midnight and I really need to wrap this up. The point that I guess I want to make is that the best set of "laws" that an abstraction should define is both useful and minimal. Useful, in the sense that they give you an obvious way to implement something that conforms. Minimal, in the sense that "laws" that aren't needed aren't defined.

But I could be wrong. That other monad law is quite handy to have.

Update: Some dude on IRC (yes, he really asked to be credited as this) who goes by the nick of "phobes" pointed out the following non-monad:

> data Foo a = Foo a Bool
> instance Monad Foo where
>     return a = Foo a False
>     (Foo a1 b1) (>>=) k = let Foo a2 b2 = k a1 in Foo a2 (b1 && b2)

This satisfies every Monad law except the right-identity law. It also, of course, disobeys the Functor laws should you try to implement a Functor instance. The Haskell language report requires that if a Monad and Functor instance are both defined, then:

fmap f m = m >>= return . f

And using this as a definition, clearly fmap id is not the same as id. In other words, the right-identity law is required for the monad to be a Functor, which is a precondition for any three theorems about monad types to apply.

The question remains as to whether or not the right-identity law is correct by virtue of using the Hughes/Hinze derivation process. The answer is "no", because we can derive Foo from the following specification:

observe (return a) b = (a,False)
observe (weird a) b = (a,True)
observe (return a >>= k) b = observe (k a) False
observe (weird a >>= k) b = observe (k a) True
observe ((m >>= k1) >>= k) b = observe (m >>= (\x -> k1 x >>= k)) b

And it's clear that weird a >>= return and weird a are not the same under observation, but the other two monad laws are correct by construction.

So it looks like you do have to prove the right-identity law correct after all.