<div dir="ltr"><div><div dir="auto"><div>Hmm, I can't seem to actually state</div><div> catchError m throwError = m<br></div><div>in terms of the other laws, so maybe it's another candidate. I also don't see how to reduce your law candidate.</div><div><br></div><div dir="auto">About law (1), what I really was going for was "if you don't throw, the catch/handle is useless", but couldn't find out how to express "don't throw". <br></div></div></div><div>Now, if we don't throw, the error can type can be anything, including Void. I wonder if (1) can be replaced with</div><div> catchError m absurd = m<br></div><div><br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sat, Sep 10, 2022 at 7:43 PM Alexandre Esteves <<a href="mailto:alexandre.fmp.esteves@gmail.com">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="auto">Nevermind, AFAICT it's s always the case that<div dir="auto"> catchError m throwError = m</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sat, 10 Sept 2022, 19:41 Alexandre Esteves, <<a href="mailto:alexandre.fmp.esteves@gmail.com" 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="auto">How about instead a distributive law of sorts:<div dir="auto">catchError (m >>= f) h </div><div dir="auto">= catchError (catchError m throwError >>= f) h</div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Sat, 10 Sept 2022, 01:56 David Feuer, <<a href="mailto:david.feuer@gmail.com" rel="noreferrer" 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>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" rel="noreferrer noreferrer" 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 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 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 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 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 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 noreferrer noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
</blockquote></div></div></div>
</blockquote></div></div></div>
</blockquote></div>
</blockquote></div>
</blockquote></div>