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

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 (Right = Ok, Left = Error), и я полагаю, что вы реализовали это правильно. Что касается доказательства соблюдения законов, я рекомендую рассмотреть, что произойдет, когда g приводит к ошибке, и когда h приводит к ошибке.