Re: Proposal: add laws to MonadError
Alexandre Esteves <[email protected]> Mon, 12 Sep 2022 00:24:18 +0100
| Newsgroups | gmane.comp.lang.haskell.libraries |
|---|---|
| Message-ID | <CAFgV2ebGR0JcG8GWY1qdf8tmGP6x3hRR+zgBXE67AMkakLjnww@mail.gmail.com> |
--===============0769112907956356100== Content-Type: multipart/alternative; boundary="000000000000ba9cd205e86f149d" --000000000000ba9cd205e86f149d Content-Type: text/plain; charset="UTF-8" Hmm, I can't seem to actually state catchError m throwError = m in terms of the other laws, so maybe it's another candidate. I also don't see how to reduce your law candidate. 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". Now, if we don't throw, the error can type can be anything, including Void. I wonder if (1) can be replaced with catchError m absurd = m On Sat, Sep 10, 2022 at 7:43 PM Alexandre Esteves < [email protected]> wrote: > Nevermind, AFAICT it's s always the case that > catchError m throwError = m > > On Sat, 10 Sept 2022, 19:41 Alexandre Esteves, < > [email protected]> wrote: > >> How about instead a distributive law of sorts: >> catchError (m >>= f) h >> = catchError (catchError m throwError >>= f) h >> >> On Sat, 10 Sept 2022, 01:56 David Feuer, <[email protected]> wrote: >> >>> Sorry, I mangled that. I meant >>> >>> catchError (m >>= f) h = catchError (Right <$> m) (pure . Left) >>= >>> either h ((`catchError` h) . f) >>> >>> >>> On Fri, Sep 9, 2022, 8:49 PM David Feuer <[email protected]> wrote: >>> >>>> I agree. These are still insufficient for much reasoning, however. I >>>> would intuitively expect that >>>> >>>> catchError (m >>= f) h = catchError (Right <$> m) (pure . Left) >>= >>>> either throwError ((`catchError` h) . f) >>>> >>>> But I have no idea whether all "reasonable" instances obey that. >>>> >>>> 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? >>>> >>>> On Fri, Sep 9, 2022, 5:43 PM Alexandre Esteves < >>>> [email protected]> wrote: >>>> >>>>> I ran into a scenario where the use of MonadError would only be valid >>>>> if >>>>> catchError (pure a) h = pure a >>>>> was a law, so I looked up the laws in >>>>> https://hackage.haskell.org/package/mtl-2.3/docs/Control-Monad-Error-Class.html#t:MonadError >>>>> but surprisingly found none. >>>>> >>>>> One would expect to see >>>>> 1. catchError (pure a) h = pure a >>>>> 2. catchError (throwError e) h = h e >>>>> 3. throwError e >>= f = throwError e >>>>> >>>>> which would rule out silly instances like >>>>> instance MonadError () Maybe where >>>>> throwError () = Nothing >>>>> catchError _ f = f () >>>>> >>>>> Searching for "monad error laws" gives me no haskell results, only >>>>> https://typelevel.org/blog/2018/04/13/rethinking-monaderror.html >>>>> which suggests the same laws. >>>>> >>>>> I propose adding these 3 laws to MonadError haddocks. >>>>> AFAICT the IO/Maybe/Either/ExceptT instances in >>>>> https://hackage.haskell.org/package/mtl-2.3/docs/src/Control.Monad.Error.Class.html%20 >>>>> all obey the laws. >>>>> _______________________________________________ >>>>> Libraries mailing list >>>>> [email protected] >>>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries >>>>> >>>> --000000000000ba9cd205e86f149d Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable <div dir=3D"ltr"><div><div dir=3D"auto"><div>Hmm, I can't seem to actua= lly state</div><div>=C2=A0 catchError m throwError =3D m<br></div><div>in t= erms 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=3D"au= to">About law (1), what I really was going for was "if you don't t= hrow, the catch/handle is useless", but couldn't find out how to e= xpress "don't throw".=C2=A0<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>=C2=A0 catchError m absurd =3D= m<br></div><div><br></div></div><br><div class=3D"gmail_quote"><div dir=3D= "ltr" class=3D"gmail_attr">On Sat, Sep 10, 2022 at 7:43 PM Alexandre Esteve= s <<a href=3D"mailto:[email protected]">alexandre.fmp.este= [email protected]</a>> wrote:<br></div><blockquote class=3D"gmail_quote" sty= le=3D"margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);paddi= ng-left:1ex"><div dir=3D"auto">Nevermind, AFAICT it's s always the case= that<div dir=3D"auto">=C2=A0 catchError m throwError =3D m</div></div><br>= <div class=3D"gmail_quote"><div dir=3D"ltr" class=3D"gmail_attr">On Sat, 10= Sept 2022, 19:41 Alexandre Esteves, <<a href=3D"mailto:alexandre.fmp.es= [email protected]" target=3D"_blank">[email protected]</a>> = wrote:<br></div><blockquote class=3D"gmail_quote" style=3D"margin:0px 0px 0= px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir= =3D"auto">How about instead a distributive law of sorts:<div dir=3D"auto">c= atchError (m >>=3D f) h=C2=A0</div><div dir=3D"auto">=3D catchError (= catchError m throwError >>=3D f) h</div></div><br><div class=3D"gmail= _quote"><div dir=3D"ltr" class=3D"gmail_attr">On Sat, 10 Sept 2022, 01:56 D= avid Feuer, <<a href=3D"mailto:[email protected]" rel=3D"noreferrer"= target=3D"_blank">[email protected]</a>> wrote:<br></div><blockquot= e class=3D"gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;border-left:1px s= olid rgb(204,204,204);padding-left:1ex"><div dir=3D"auto"><div>Sorry, I man= gled that. I meant<div dir=3D"auto"><br></div><div dir=3D"auto"><div dir=3D= "auto">catchError (m >>=3D f) h =3D catchError (Right <$> m) (p= ure . Left) >>=3D</div><div dir=3D"auto">=C2=A0 either h ((`catchErro= r` h)=C2=A0 . f)</div></div><br><br><div class=3D"gmail_quote"><div dir=3D"= ltr" class=3D"gmail_attr">On Fri, Sep 9, 2022, 8:49 PM David Feuer <<a h= ref=3D"mailto:[email protected]" rel=3D"noreferrer noreferrer" target= =3D"_blank">[email protected]</a>> wrote:<br></div><blockquote class= =3D"gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;border-left:1px solid rg= b(204,204,204);padding-left:1ex"><div dir=3D"auto"><div>I agree. These are = still insufficient for much reasoning, however. I would intuitively expect = that</div><div dir=3D"auto"><br></div><div dir=3D"auto">catchError (m >&= gt;=3D f) h =3D catchError (Right <$> m) (pure . Left) >>=3D</d= iv><div dir=3D"auto">=C2=A0 either throwError ((`catchError` h)=C2=A0 . f)<= /div><div dir=3D"auto"><br></div><div dir=3D"auto">But I have no idea wheth= er all "reasonable" instances obey that.</div><div dir=3D"auto"><= br></div><div dir=3D"auto">Is there anything useful to say about the case w= hen the argument to mapError is sufficiently nice (a monad morphism with so= me extra property, for instance?</div><div dir=3D"auto"><br></div><div dir= =3D"auto"><div class=3D"gmail_quote" dir=3D"auto"><div dir=3D"ltr" class=3D= "gmail_attr">On Fri, Sep 9, 2022, 5:43 PM Alexandre Esteves <<a href=3D"= mailto:[email protected]" rel=3D"noreferrer noreferrer norefe= rrer noreferrer" target=3D"_blank">[email protected]</a>> = wrote:<br></div><blockquote class=3D"gmail_quote" style=3D"margin:0px 0px 0= px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir= =3D"ltr">I ran into a scenario where the use of MonadError would only be va= lid if=C2=A0<div>=C2=A0 catchError (pure a) h =3D pure a<br></div><div>was = a law, so I looked up the laws in=C2=A0<a href=3D"https://hackage.haskell.o= rg/package/mtl-2.3/docs/Control-Monad-Error-Class.html#t:MonadError" rel=3D= "noreferrer noreferrer noreferrer noreferrer noreferrer" target=3D"_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>=C2=A0 1.=C2=A0catchError (pure a) h =3D= pure a<br>=C2=A0 2. catchError (throwError e) h =3D h e<br></div><div>=C2= =A0 3. throwError e >>=3D f =3D throwError e</div><div><br></div><div= >which would rule out silly instances like</div><div>=C2=A0 instance MonadE= rror () Maybe where<br>=C2=A0 =C2=A0 throwError () =C2=A0 =C2=A0 =C2=A0 =C2= =A0=3D Nothing<br>=C2=A0 =C2=A0 catchError _ f =3D f ()<br></div><div><br><= /div><div>Searching for "monad error laws" gives me no haskell re= sults, only <a href=3D"https://typelevel.org/blog/2018/04/13/rethinking-mon= aderror.html" rel=3D"noreferrer noreferrer noreferrer noreferrer noreferrer= " target=3D"_blank">https://typelevel.org/blog/2018/04/13/rethinking-monade= rror.html</a> which suggests the same laws.</div><div><br></div><div>I prop= ose adding these 3 laws to MonadError haddocks.</div><div>AFAICT the IO/May= be/Either/ExceptT instances in <a href=3D"https://hackage.haskell.org/packa= ge/mtl-2.3/docs/src/Control.Monad.Error.Class.html%20" rel=3D"noreferrer no= referrer noreferrer noreferrer noreferrer" target=3D"_blank">https://hackag= e.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=3D"mailto:[email protected]" rel=3D"noreferrer noreferrer noref= errer noreferrer noreferrer" target=3D"_blank">[email protected]</a><br= > <a href=3D"http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel= =3D"noreferrer noreferrer noreferrer noreferrer noreferrer noreferrer" targ= et=3D"_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> --000000000000ba9cd205e86f149d-- --===============0769112907956356100== Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: base64 Content-Disposition: inline X19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX18KTGlicmFyaWVz IG1haWxpbmcgbGlzdApMaWJyYXJpZXNAaGFza2VsbC5vcmcKaHR0cDovL21haWwuaGFza2VsbC5v cmcvY2dpLWJpbi9tYWlsbWFuL2xpc3RpbmZvL2xpYnJhcmllcwo= --===============0769112907956356100==--