對一個錯誤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法我寫了

回答

相關問題