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

方程式の一方の側を示すことから始めて、反対側にたどり着くようにしてください。私は通常、「より複雑な」側から始めて、より単純な側に向かって作業します。3 番目の法則では、これは機能しません (両側が同じように複雑です)。そのため、通常、同じ場所に到達するまで、両側から可能な限り単純化します。次に、一方の側から行った手順を逆にして、証明を取得できます。

たとえば、次のようになります。

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

他の 2 つの法則のプロセスはほぼ同じです。

于 2011-03-07T06:26:59.057 に答える
1

あなたのモナドはEither String a(Right = OK, Left = Error) に同形であり、正しく実装されていると思います。g法則が満たされていることの証明に関しては、結果がエラーになったときにどうなるか、結果がエラーになったときにどうなるかを検討することをお勧めhします。

于 2011-03-07T00:57:52.923 に答える