내가 쓴 오류 모나드에 대한 모나드 법칙을 증명하는 법

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

방정식의 한 쪽을 말하고 다른쪽에 가려고합니다. 나는 보통 더 복잡한 측면에서 시작하여보다 단순한쪽으로 나아갑니다. 제 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 

과정은 거의 동일 증명했다.

Answer 2

귀하의 모나드는 Either String a (오른쪽 = 좋아, 왼쪽 = 오류) 동형이며, 나는 당신이 그것을 정확하게 구현 생각합니다. 법이 입증되면, g은 오류가 발생하고 h은 오류가 발생할 때 어떤 일이 발생하는지 고려하는 것이 좋습니다.