Re: Proposal: add laws to MonadError

--===============4883651179759013014==
Content-Type: multipart/alternative; boundary="00000000000020628605e85703a0"

--00000000000020628605e85703a0
Content-Type: text/plain; charset="UTF-8"

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
>>>
>>

--00000000000020628605e85703a0
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

<div dir=3D"auto">How about instead a distributive law of sorts:<div dir=3D=
"auto">catchError (m &gt;&gt;=3D f) h=C2=A0</div><div dir=3D"auto">=3D catc=
hError (catchError m throwError &gt;&gt;=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 David Feuer, &lt;<a href=3D"mailto:[email protected]">david.feu=
[email protected]</a>&gt; wrote:<br></div><blockquote class=3D"gmail_quote" styl=
e=3D"margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div di=
r=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 &gt;&gt;=3D f) h =3D catch=
Error (Right &lt;$&gt; m) (pure . Left) &gt;&gt;=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 &lt;<a href=3D"mailto:[email protected]" target=3D=
"_blank" rel=3D"noreferrer">[email protected]</a>&gt; 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 sti=
ll insufficient for much reasoning, however. I would intuitively expect tha=
t</div><div dir=3D"auto"><br></div><div dir=3D"auto">catchError (m &gt;&gt;=
=3D f) h =3D catchError (Right &lt;$&gt; m) (pure . Left) &gt;&gt;=3D</div>=
<div dir=3D"auto">=C2=A0 either throwError ((`catchError` h)=C2=A0 . f)</di=
v><div dir=3D"auto"><br></div><div dir=3D"auto">But I have no idea whether =
all &quot;reasonable&quot; instances obey that.</div><div dir=3D"auto"><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 with some =
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"gma=
il_attr">On Fri, Sep 9, 2022, 5:43 PM Alexandre Esteves &lt;<a href=3D"mail=
to:[email protected]" rel=3D"noreferrer noreferrer noreferrer=
" target=3D"_blank">[email protected]</a>&gt; wrote:<br></div=
><blockquote class=3D"gmail_quote" style=3D"margin:0 0 0 .8ex;border-left:1=
px #ccc solid;padding-left:1ex"><div dir=3D"ltr">I ran into a scenario wher=
e the use of MonadError would 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://hackage.haskell.org/package/mtl-2.3/docs/Control-M=
onad-Error-Class.html#t:MonadError" rel=3D"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 &gt;&gt;=3D f =3D throwEr=
ror e</div><div><br></div><div>which would rule out silly instances like</d=
iv><div>=C2=A0 instance MonadError () Maybe where<br>=C2=A0 =C2=A0 throwErr=
or () =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 &quot;monad error law=
s&quot; gives me no haskell results, only <a href=3D"https://typelevel.org/=
blog/2018/04/13/rethinking-monaderror.html" rel=3D"noreferrer noreferrer no=
referrer noreferrer" target=3D"_blank">https://typelevel.org/blog/2018/04/1=
3/rethinking-monaderror.html</a> which suggests the same laws.</div><div><b=
r></div><div>I propose adding these 3 laws to MonadError haddocks.</div><di=
v>AFAICT the IO/Maybe/Either/ExceptT instances in <a href=3D"https://hackag=
e.haskell.org/package/mtl-2.3/docs/src/Control.Monad.Error.Class.html%20" r=
el=3D"noreferrer noreferrer noreferrer noreferrer" target=3D"_blank">https:=
//hackage.haskell.org/package/mtl-2.3/docs/src/Control.Monad.Error.Class.ht=
ml%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" 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" target=3D"_blan=
k">http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
</blockquote></div></div></div>
</blockquote></div></div></div>
</blockquote></div>

--00000000000020628605e85703a0--

--===============4883651179759013014==
Content-Type: text/plain; charset="utf-8"
MIME-Version: 1.0
Content-Transfer-Encoding: base64
Content-Disposition: inline

X19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX18KTGlicmFyaWVz
IG1haWxpbmcgbGlzdApMaWJyYXJpZXNAaGFza2VsbC5vcmcKaHR0cDovL21haWwuaGFza2VsbC5v
cmcvY2dpLWJpbi9tYWlsbWFuL2xpc3RpbmZvL2xpYnJhcmllcwo=

--===============4883651179759013014==--