Re: Proposal: add laws to MonadError
Alexandre Esteves <[email protected]> Sat, 10 Sep 2022 19:43:24 +0100
| Newsgroups | gmane.comp.lang.haskell.libraries |
|---|---|
| Message-ID | <CAFgV2ea9yJuQp955MCz11VtSvxiz03Yb=PwdPsgYEye3OX4ZkQ@mail.gmail.com> |
--===============7349358193327941045== Content-Type: multipart/alternative; boundary="00000000000058888405e8570ad6" --00000000000058888405e8570ad6 Content-Type: text/plain; charset="UTF-8" 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 >>>> >>> --00000000000058888405e8570ad6 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable <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, 1= 9:41 Alexandre Esteves, <<a href=3D"mailto:[email protected]= om">[email protected]</a>> wrote:<br></div><blockquote cla= ss=3D"gmail_quote" style=3D"margin:0 0 0 .8ex;border-left:1px #ccc solid;pa= dding-left:1ex"><div dir=3D"auto">How about instead a distributive law of s= orts:<div dir=3D"auto">catchError (m >>=3D f) h=C2=A0</div><div dir= =3D"auto">=3D catchError (catchError m throwError >>=3D f) h</div></d= iv><br><div class=3D"gmail_quote"><div dir=3D"ltr" class=3D"gmail_attr">On = Sat, 10 Sept 2022, 01:56 David Feuer, <<a href=3D"mailto:david.feuer@gma= il.com" target=3D"_blank" rel=3D"noreferrer">[email protected]</a>> = wrote:<br></div><blockquote class=3D"gmail_quote" style=3D"margin:0 0 0 .8e= x;border-left:1px #ccc solid;padding-left:1ex"><div dir=3D"auto"><div>Sorry= , I mangled 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) (pure . Left) >>=3D</div><div dir=3D"auto">=C2=A0 either h ((`ca= tchError` 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 &= lt;<a href=3D"mailto:[email protected]" rel=3D"noreferrer noreferrer" t= arget=3D"_blank">[email protected]</a>> wrote:<br></div><blockquote = class=3D"gmail_quote" style=3D"margin:0 0 0 .8ex;border-left:1px #ccc solid= ;padding-left:1ex"><div dir=3D"auto"><div>I agree. These are still insuffic= ient for much reasoning, however. I would intuitively expect that</div><div= dir=3D"auto"><br></div><div dir=3D"auto">catchError (m >>=3D f) h = =3D catchError (Right <$> m) (pure . Left) >>=3D</div><div dir= =3D"auto">=C2=A0 either throwError ((`catchError` h)=C2=A0 . f)</div><div d= ir=3D"auto"><br></div><div dir=3D"auto">But I have no idea whether all &quo= t;reasonable" instances obey that.</div><div dir=3D"auto"><br></div><d= iv dir=3D"auto">Is there anything useful to say about the case when the arg= ument to mapError is sufficiently nice (a monad morphism with some extra pr= operty, for instance?</div><div dir=3D"auto"><br></div><div dir=3D"auto"><d= iv 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:alexa= [email protected]" rel=3D"noreferrer noreferrer noreferrer norefer= rer" target=3D"_blank">[email protected]</a>> wrote:<br></= div><blockquote class=3D"gmail_quote" style=3D"margin:0 0 0 .8ex;border-lef= t:1px #ccc solid;padding-left:1ex"><div dir=3D"ltr">I ran into a scenario w= here the use of MonadError would only be valid if=C2=A0<div>=C2=A0 catchErr= or (pure a) h =3D pure a<br></div><div>was a law, so I looked up the laws i= n=C2=A0<a href=3D"https://hackage.haskell.org/package/mtl-2.3/docs/Control-= Monad-Error-Class.html#t:MonadError" rel=3D"noreferrer noreferrer noreferre= r noreferrer noreferrer" target=3D"_blank">https://hackage.haskell.org/pack= age/mtl-2.3/docs/Control-Monad-Error-Class.html#t:MonadError</a> but surpri= singly found none.</div><div><br></div><div>One would expect to see</div><d= iv>=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 insta= nces like</div><div>=C2=A0 instance MonadError () Maybe where<br>=C2=A0 =C2= =A0 throwError () =C2=A0 =C2=A0 =C2=A0 =C2=A0=3D Nothing<br>=C2=A0 =C2=A0 c= atchError _ f =3D f ()<br></div><div><br></div><div>Searching for "mon= ad error laws" gives me no haskell results, only <a href=3D"https://ty= pelevel.org/blog/2018/04/13/rethinking-monaderror.html" rel=3D"noreferrer n= oreferrer noreferrer noreferrer noreferrer" target=3D"_blank">https://typel= evel.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 MonadE= rror haddocks.</div><div>AFAICT the IO/Maybe/Either/ExceptT instances in <a= href=3D"https://hackage.haskell.org/package/mtl-2.3/docs/src/Control.Monad= .Error.Class.html%20" rel=3D"noreferrer noreferrer noreferrer noreferrer no= referrer" target=3D"_blank">https://hackage.haskell.org/package/mtl-2.3/doc= s/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> --00000000000058888405e8570ad6-- --===============7349358193327941045== Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: base64 Content-Disposition: inline X19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX18KTGlicmFyaWVz IG1haWxpbmcgbGlzdApMaWJyYXJpZXNAaGFza2VsbC5vcmcKaHR0cDovL21haWwuaGFza2VsbC5v cmcvY2dpLWJpbi9tYWlsbWFuL2xpc3RpbmZvL2xpYnJhcmllcwo= --===============7349358193327941045==--