在我写的错误单子上证明一些单子定律

Question

所以我创建了一个自定义错误单子，我想知道如何为其证明一些单子定律。如果有人愿意花时间帮助我，我将不胜感激。谢谢！

这是我的代码：

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

首先陈述等式的一侧，然后尝试到达另一侧。我通常从“更复杂”的一侧开始，然后朝着更简单的一侧努力。对于第三定律，这是行不通的（双方都一样复杂），所以我通常从双方出发并尽可能地简化它们，直到达到相同的地方。然后我可以反转我从一侧采取的步骤来获得证明。

例如：

return x >>= g

然后展开：

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

因此我们已经证明了

return x >>= g = g x

其他两个定律的过程大致相同。

Answer 2

您的 monad 与 Either String a 同构（Right = Ok，Left = Error），我相信您已经正确实现了它。至于证明满足定律，我建议考虑当 g 导致错误和 h 导致错误时会发生什么。