<div dir="ltr"><div>Hi,</div><div><br></div><div>I went over an old mail, sorry for the late reply. David's law does not hold:</div><div><br></div><div>GHCi, version 8.8.4: <a href="https://www.haskell.org/ghc/">https://www.haskell.org/ghc/</a> :? for help<br>Prelude> :m Control.Monad.Except Control.Monad.Writer<br>Prelude Control.Monad.Except Control.Monad.Writer> let lhs f h m = catchError (m >>= f) h<br>Prelude Control.Monad.Except Control.Monad.Writer> let rhs f h m = catchError (Right <$> m) (pure . Left) >>= either h ((`catchError` h) . f)<br>Prelude Control.Monad.Except Control.Monad.Writer> let f a = WriterT (Left ())<br>Prelude Control.Monad.Except Control.Monad.Writer> let h e = WriterT (Right (True , [()]))<br>Prelude Control.Monad.Except Control.Monad.Writer> let m = WriterT (Right (False , [(), ()]))<br>Prelude Control.Monad.Except Control.Monad.Writer> lhs f h m<br>WriterT (Right (True,[()]))<br>Prelude Control.Monad.Except Control.Monad.Writer> rhs f h m<br>WriterT (Right (True,[(),(),()]))</div><div><br></div><div>Regards,</div><div>Härmel<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">Kontakt David Feuer (<<a href="mailto:david.feuer@gmail.com">david.feuer@gmail.com</a>>) kirjutas kuupäeval L, 10. september 2022 kell 02:57:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="auto"><div>Sorry, I mangled that. I meant<div dir="auto"><br></div><div dir="auto"><div dir="auto">catchError (m >>= f) h = catchError (Right <$> m) (pure . Left) >>=</div><div dir="auto"> either h ((`catchError` h) . f)</div></div><br><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, Sep 9, 2022, 8:49 PM David Feuer <<a href="mailto:david.feuer@gmail.com" target="_blank">david.feuer@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="auto"><div>I agree. These are still insufficient for much reasoning, however. I would intuitively expect that</div><div dir="auto"><br></div><div dir="auto">catchError (m >>= f) h = catchError (Right <$> m) (pure . Left) >>=</div><div dir="auto"> either throwError ((`catchError` h) . f)</div><div dir="auto"><br></div><div dir="auto">But I have no idea whether all "reasonable" instances obey that.</div><div dir="auto"><br></div><div dir="auto">Is there anything useful to say about the case when the argument to mapError is sufficiently nice (a monad morphism with some extra property, for instance?</div><div dir="auto"><br></div><div dir="auto"><div class="gmail_quote" dir="auto"><div dir="ltr" class="gmail_attr">On Fri, Sep 9, 2022, 5:43 PM Alexandre Esteves <<a href="mailto:alexandre.fmp.esteves@gmail.com" rel="noreferrer noreferrer" target="_blank">alexandre.fmp.esteves@gmail.com</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir="ltr">I ran into a scenario where the use of MonadError would only be valid if <div> catchError (pure a) h = pure a<br></div><div>was a law, so I looked up the laws in <a href="https://hackage.haskell.org/package/mtl-2.3/docs/Control-Monad-Error-Class.html#t:MonadError" rel="noreferrer noreferrer noreferrer" target="_blank">https://hackage.haskell.org/package/mtl-2.3/docs/Control-Monad-Error-Class.html#t:MonadError</a> but surprisingly found none.</div><div><br></div><div>One would expect to see</div><div> 1. catchError (pure a) h = pure a<br> 2. catchError (throwError e) h = h e<br></div><div> 3. throwError e >>= f = throwError e</div><div><br></div><div>which would rule out silly instances like</div><div> instance MonadError () Maybe where<br> throwError () = Nothing<br> catchError _ f = f ()<br></div><div><br></div><div>Searching for "monad error laws" gives me no haskell results, only <a href="https://typelevel.org/blog/2018/04/13/rethinking-monaderror.html" rel="noreferrer noreferrer noreferrer" target="_blank">https://typelevel.org/blog/2018/04/13/rethinking-monaderror.html</a> which suggests the same laws.</div><div><br></div><div>I propose adding these 3 laws to MonadError haddocks.</div><div>AFAICT the IO/Maybe/Either/ExceptT instances in <a href="https://hackage.haskell.org/package/mtl-2.3/docs/src/Control.Monad.Error.Class.html%20" rel="noreferrer noreferrer noreferrer" target="_blank">https://hackage.haskell.org/package/mtl-2.3/docs/src/Control.Monad.Error.Class.html%20</a> all obey the laws.</div></div>
_______________________________________________<br>
Libraries mailing list<br>
<a href="mailto:Libraries@haskell.org" rel="noreferrer noreferrer noreferrer" target="_blank">Libraries@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer noreferrer noreferrer noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
</blockquote></div></div></div>
</blockquote></div></div></div>
_______________________________________________<br>
Libraries mailing list<br>
<a href="mailto:Libraries@haskell.org" target="_blank">Libraries@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
</blockquote></div>