Доказывая некоторые законы монады на монаду ошибки, которую я написал

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

Ваша монада изоморфна Either String a (справа = нормально, слева = ошибка), и я считаю, что вы правильно ее реализовали.Что касается доказательства соблюдения законов, я рекомендую рассмотреть, что происходит, когда g приводит к ошибке, а когда h приводит к ошибке.