Prouver quelques lois de monade sur une monade d'erreur J'ai écrit

J'ai donc monté une monade d'erreur personnalisée et je me demandais comment j'allais prouver quelques lois de monade pour cela. Si quelqu'un est prêt à prendre le temps de m'aider, ce serait très apprécié. Merci!Prouver quelques lois de monade sur une monade d'erreur J'ai écrit

Et voici mon code:

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)

Source

2011-03-07 Cody Bonney

Pour quoi avez-vous besoin d'aide? Jusqu'où êtes-vous déjà arrivé? –

À ce stade, je n'ai fait aucun progrès à ce sujet. J'ai besoin d'aide pour démontrer que ces lois sont satisfaites. –

Pendant que vous y êtes, vous pouvez mettre 'fail = Error' dans votre instance' Monad Error'. Cela entraînera des échecs de correspondance de pattern dans la notation 'do' pour être un' Error' comme vous l'avez défini au lieu du 'error' plus dard. – luqui

Commencez par énoncer un côté de l'équation et essayez d'atteindre l'autre côté. Je commence habituellement du côté «plus compliqué» et travaille vers le plus simple. Pour la troisième loi, cela ne fonctionne pas (les deux côtés sont tout aussi complexes), donc je vais habituellement des deux côtés et je les simplifie autant que possible, jusqu'à ce que j'arrive au même endroit. Ensuite, je peux simplement inverser les étapes que j'ai prises d'un des côtés pour obtenir une preuve.

Ainsi, par exemple:

return x >>= g

Ajouter ensuite:

= Ok x >>= g 
= bindError (Ok x) g 
= case Ok x of { Ok v -> g v ; ... } 
= g x

Et ainsi nous avons prouvé

return x >>= g = g x

Le processus pour les deux autres lois est à peu près la même.

Source

2011-03-07 06:26:59 luqui

Merci pour votre explication claire et exemple! Très utile! –

Je viens de réaliser que pour la troisième loi, vous devrez peut-être faire une analyse de cas. Par exemple. Si vous avez quelque chose comme 'bindError x f' et que vous devez le simplifier davantage, vous pouvez dire que' 'x' est soit 'Ok y' soit' Error e'', puis vérifiez que la loi est valide pour chacun de ces cas. – luqui

Votre monade est isomorphe à Either String a (droite = Ok, Gauche = erreur), et je crois que vous avez mis en œuvre correctement. Comme pour prouver que les lois sont satisfaites, je recommande d'examiner ce qui se passe quand g résulte en une erreur, et quand h résulte en une erreur.

Source

2011-03-07 00:57:52

Prouver quelques lois de monade sur une monade d'erreur J'ai écrit

Répondre

Questions connexes