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)

Answer 1

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.

Answer 2

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.