[SOLVED] Proving some monad laws on an error monad I wrote

Proving some monad laws on an error monad I wrote

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)

Solution

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.