2

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

这是我的代码：

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)
4

2 回答 2

1

您的 monad 与 (Right = Ok, Left = Error) 同构Either String a，我相信您已经正确实现了它。至于证明法律是否满足，我建议考虑导致错误时会发生什么g，以及h导致错误时会发生什么。

于 2011-03-07T00:57:52.923 回答
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

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

于 2011-03-07T06:26:59.057 回答