对一个错误monad证明了一些monad法我写了

所以我掀起了一个自定义错误monad，我想知道如何去证明它的一些monad法则。如果有人愿意花时间帮助我，那将是非常感谢。谢谢！对一个错误monad证明了一些monad法我写了

这里是我的代码：

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)

来源

2011-03-07 Cody Bonney

你需要什么帮助？你已经有多远了？ – 2011-03-07 00:57:53

在这一点上，我还没有取得任何进展。我需要帮助证明这些monad法律得到满足。 – 2011-03-07 01:01:25

当你在它的时候，你可能会把'fail = Error'放到你的'Monad Error'实例中。这会导致'do'符号中的模式匹配失败，因为您已经定义了错误，而不是更为卑鄙的错误。 – luqui 2011-03-07 06:41:31

首先说明方程的一个方面，并试图找到另一方。我通常从“更复杂”的角度出发，朝着更简单的方向努力。对于第三项法律来说，这是行不通的（双方都同样复杂），所以我通常从双方都尽量简化，直到我到达同一个地方。然后，我可以将我从一侧拿走的步骤颠倒过来以获得证明。

因此，例如：

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-07 06:26:59 luqui

谢谢您的明确解释和示例！很有帮助！ – 2011-03-07 06:35:11

我刚刚意识到，对于第三部法律你可能需要做一些案例分析。例如。如果你有类似'bindError x f'的东西，你需要进一步简化它，你可以说''x'或者是'Ok y'或'Error e''，然后检查这些法则适用于每种情况。 – luqui 2011-03-07 06:57:52

你的单子是同构于Either String a（右= OK，左=错误），我相信你已经正确实现它。至于证明法律得到满足，我建议考虑g导致错误时以及h导致错误时会发生什么情况。

来源

2011-03-07 00:57:52

对一个错误monad证明了一些monad法我写了

回答

相关问题