Proving some monad laws on an error monad I wrote

Question

So I whipped up a custom error monad and I was wondering how I would go about proving a few monad laws for it. If anyone is willing to take the time to help me out it would be much appreciated. Thanks!

And here's my code:

data Error a = Ok a | Error String

instance Monad Error where
    return = Ok
    (>>=) = bindError

instance Show a => Show (Error a) where
    show = showError

showError :: Show a => Error a -> String
showError x =
    case x of
        (Ok v) -> show v
        (Error msg) -> show msg

bindError :: Error a -> (a -> Error b) -> Error b
bindError x f = case x of
    (Ok v) -> f v
    (Error msg) -> (Error msg)

What do you need help with? How far have you gotten already? — Jeremiah Willcock, Mar 07 '11 at 00:57
At this point, I haven't made any progress on it. I need help demonstrating that those monad laws are satisfied. — Cody Bonney, Mar 07 '11 at 01:01
While you're at it you may as well put `fail = Error` in to your `Monad Error` instance. That will cause pattern match failures in `do` notation to be an `Error` as you have defined instead of the more dastardly `error`. — luqui, Mar 07 '11 at 06:41

score 1 · Answer 1 · answered Mar 07 '11 at 00:57

Your monad is isomorphic to Either String a (Right = Ok, Left = Error), and I believe you have implemented it correctly. As for proving the laws are satisfied, I recommend considering what happens when g results in an error, and when h results in an error.

score 1 · Accepted Answer · answered Mar 07 '11 at 06:26

Start by stating one side of the equation, and try to get to the other side. I usually start from the "more complicated" side and work toward the simpler one. For the third law this doesn't work (both sides are just as complex), so I usually go from both sides and simplify them as much as possible, until I get to the same place. Then I can just reverse the steps I took from one of the sides to get a proof.

So for example:

return x >>= g

Then expand:

= Ok x >>= g
= bindError (Ok x) g
= case Ok x of { Ok v -> g v ; ... }
= g x

And thus we have proved

return x >>= g = g x

The process for the other two laws is approximately the same.

I just realized that for the third law you may need to do some case analysis. Eg. if you have something like `bindError x f` and you need to simplify it further, you can say "`x` is either `Ok y` or `Error e`", and then check that the law holds for each of those cases. — luqui, Mar 07 '11 at 06:57

Proving some monad laws on an error monad I wrote

2 Answers2