Re: Proposal: add laws to MonadError
David Feuer <[email protected]> Sun, 11 Sep 2022 20:38:15 -0400
| Newsgroups | gmane.comp.lang.haskell.libraries |
|---|---|
| Message-ID | <CAMgWh9vA98PysPT=07+7ZehcZGdKJWE_mG2+dh3jEcDxJm-Lgg@mail.gmail.com> |
--===============1619379040367219484== Content-Type: multipart/alternative; boundary="0000000000004843ad05e8701d5a" --0000000000004843ad05e8701d5a Content-Type: text/plain; charset="UTF-8" No, the error type is fixed by the monad, and there's no way to change it in general. catchError m throwError = m looks promising. On Sun, Sep 11, 2022, 7:24 PM Alexandre Esteves < [email protected]> wrote: > 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 >>>>>> >>>>> --0000000000004843ad05e8701d5a Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable <div dir=3D"auto"><div>No, the error type is fixed by the monad, and there&= #39;s no way to change it in general. catchError m throwError =3D m looks p= romising.</div><div dir=3D"auto"><br><div class=3D"gmail_quote" dir=3D"auto= "><div dir=3D"ltr" class=3D"gmail_attr">On Sun, Sep 11, 2022, 7:24 PM Alexa= ndre Esteves <<a href=3D"mailto:[email protected]">alexand= [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"ltr"><div><div dir=3D"auto"><div>Hmm, I can't seem to = actually state</div><div>=C2=A0 catchError m throwError =3D m<br></div><div= >in terms of the other laws, so maybe it's another candidate. I also do= n't see how to reduce your law candidate.</div><div><br></div><div dir= =3D"auto">About law (1), what I really was going for was "if you don&#= 39;t throw, the catch/handle is useless", but couldn't find out ho= w to express "don't throw".=C2=A0<br></div></div></div><div>N= ow, if we don't throw, the error can type can be anything, including Vo= id. I wonder if (1) can be replaced with</div><div>=C2=A0 catchError m absu= rd =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 = Esteves <<a href=3D"mailto:[email protected]" target=3D"_b= lank" rel=3D"noreferrer">[email protected]</a>> wrote:<br>= </div><blockquote class=3D"gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;b= order-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir=3D"auto">N= evermind, AFAICT it's s always the case that<div dir=3D"auto">=C2=A0 ca= tchError 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 Este= ves, <<a href=3D"mailto:[email protected]" target=3D"_blan= k" rel=3D"noreferrer">[email protected]</a>> wrote:<br></d= iv><blockquote class=3D"gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;bord= er-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">catchError (m &= gt;>=3D f) h=C2=A0</div><div dir=3D"auto">=3D catchError (catchError m t= hrowError >>=3D f) h</div></div><br><div class=3D"gmail_quote"><div d= ir=3D"ltr" class=3D"gmail_attr">On Sat, 10 Sept 2022, 01:56 David Feuer, &l= t;<a href=3D"mailto:[email protected]" rel=3D"noreferrer noreferrer" ta= rget=3D"_blank">[email protected]</a>> wrote:<br></div><blockquote c= lass=3D"gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;border-left:1px soli= d rgb(204,204,204);padding-left:1ex"><div dir=3D"auto"><div>Sorry, I mangle= d that. I meant<div dir=3D"auto"><br></div><div dir=3D"auto"><div dir=3D"au= to">catchError (m >>=3D f) h =3D catchError (Right <$> m) (pure= . Left) >>=3D</div><div dir=3D"auto">=C2=A0 either h ((`catchError` = 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 href= =3D"mailto:[email protected]" rel=3D"noreferrer 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 so= lid rgb(204,204,204);padding-left:1ex"><div dir=3D"auto"><div>I agree. Thes= e are still insufficient for much reasoning, however. I would intuitively e= xpect 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 dir=3D"auto"><br></div><div dir=3D"auto">But I have no idea= whether all "reasonable" instances obey that.</div><div dir=3D"a= uto"><br></div><div dir=3D"auto">Is there anything useful to say about the = case when the argument to mapError is sufficiently nice (a monad morphism w= ith some extra property, for instance?</div><div dir=3D"auto"><br></div><di= v dir=3D"auto"><div class=3D"gmail_quote" dir=3D"auto"><div dir=3D"ltr" cla= ss=3D"gmail_attr">On Fri, Sep 9, 2022, 5:43 PM Alexandre Esteves <<a hre= f=3D"mailto:[email protected]" rel=3D"noreferrer noreferrer n= oreferrer noreferrer noreferrer" target=3D"_blank">alexandre.fmp.esteves@gm= ail.com</a>> wrote:<br></div><blockquote class=3D"gmail_quote" style=3D"= margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-lef= t:1ex"><div dir=3D"ltr">I ran into a scenario where the use of MonadError w= ould only be valid 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://ha= ckage.haskell.org/package/mtl-2.3/docs/Control-Monad-Error-Class.html#t:Mon= adError" rel=3D"noreferrer noreferrer noreferrer noreferrer noreferrer nore= ferrer" 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 MonadError () 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&= quot; gives me no haskell results, only <a href=3D"https://typelevel.org/bl= og/2018/04/13/rethinking-monaderror.html" rel=3D"noreferrer noreferrer nore= ferrer noreferrer noreferrer noreferrer" target=3D"_blank">https://typeleve= l.org/blog/2018/04/13/rethinking-monaderror.html</a> which suggests the sam= e laws.</div><div><br></div><div>I propose adding these 3 laws to MonadErro= r haddocks.</div><div>AFAICT the IO/Maybe/Either/ExceptT instances in <a hr= ef=3D"https://hackage.haskell.org/package/mtl-2.3/docs/src/Control.Monad.Er= ror.Class.html%20" rel=3D"noreferrer noreferrer noreferrer noreferrer noref= errer noreferrer" target=3D"_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=3D"mailto:[email protected]" rel=3D"noreferrer noreferrer noref= errer noreferrer noreferrer noreferrer" target=3D"_blank">Libraries@haskell= .org</a><br> <a href=3D"http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel= =3D"noreferrer noreferrer noreferrer noreferrer noreferrer noreferrer noref= errer" target=3D"_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/l= ibraries</a><br> </blockquote></div></div></div> </blockquote></div></div></div> </blockquote></div> </blockquote></div> </blockquote></div> </blockquote></div></div></div> --0000000000004843ad05e8701d5a-- --===============1619379040367219484== Content-Type: text/plain; charset="utf-8" MIME-Version: 1.0 Content-Transfer-Encoding: base64 Content-Disposition: inline X19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX18KTGlicmFyaWVz IG1haWxpbmcgbGlzdApMaWJyYXJpZXNAaGFza2VsbC5vcmcKaHR0cDovL21haWwuaGFza2VsbC5v cmcvY2dpLWJpbi9tYWlsbWFuL2xpc3RpbmZvL2xpYnJhcmllcwo= --===============1619379040367219484==--