Re: Proposal: add laws to MonadError

--===============8794242309512341912==
Content-Type: multipart/alternative; boundary="0000000000009c165605e8482391"

--0000000000009c165605e8482391
Content-Type: text/plain; charset="UTF-8"

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

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

<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 &gt;&gt;=3D f) h =
=3D catchError (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]">=
[email protected]</a>&gt; wrote:<br></div><blockquote class=3D"gmail_qu=
ote" 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 insufficient for much rea=
soning, however. I would intuitively expect that</div><div dir=3D"auto"><br=
></div><div dir=3D"auto">catchError (m &gt;&gt;=3D f) h =3D catchError (Rig=
ht &lt;$&gt; m) (pure . Left) &gt;&gt;=3D</div><div dir=3D"auto">=C2=A0 eit=
her throwError ((`catchError` h)=C2=A0 . f)</div><div dir=3D"auto"><br></di=
v><div dir=3D"auto">But I have no idea whether all &quot;reasonable&quot; i=
nstances obey that.</div><div dir=3D"auto"><br></div><div dir=3D"auto">Is t=
here 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_qu=
ote" dir=3D"auto"><div dir=3D"ltr" class=3D"gmail_attr">On Fri, Sep 9, 2022=
, 5:43 PM Alexandre Esteves &lt;<a href=3D"mailto:alexandre.fmp.esteves@gma=
il.com" rel=3D"noreferrer noreferrer" target=3D"_blank">alexandre.fmp.estev=
[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"ltr">I ran into a scenario where the use of MonadError would only be v=
alid 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-Monad-Error-Class.html#t:MonadError" rel=
=3D"noreferrer noreferrer noreferrer" target=3D"_blank">https://hackage.has=
kell.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 t=
o 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 throwError e</div><div><br></div><div>which would rule ou=
t 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>Searchin=
g for &quot;monad error laws&quot; gives me no haskell results, only <a hre=
f=3D"https://typelevel.org/blog/2018/04/13/rethinking-monaderror.html" rel=
=3D"noreferrer noreferrer noreferrer" target=3D"_blank">https://typelevel.o=
rg/blog/2018/04/13/rethinking-monaderror.html</a> which suggests the same l=
aws.</div><div><br></div><div>I propose adding these 3 laws to MonadError h=
addocks.</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.Erro=
r.Class.html%20" rel=3D"noreferrer noreferrer noreferrer" target=3D"_blank"=
>https://hackage.haskell.org/package/mtl-2.3/docs/src/Control.Monad.Error.C=
lass.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" 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" target=3D"_blank">http://m=
ail.haskell.org/cgi-bin/mailman/listinfo/libraries</a><br>
</blockquote></div></div></div>
</blockquote></div></div></div>

--0000000000009c165605e8482391--

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

X19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX18KTGlicmFyaWVz
IG1haWxpbmcgbGlzdApMaWJyYXJpZXNAaGFza2VsbC5vcmcKaHR0cDovL21haWwuaGFza2VsbC5v
cmcvY2dpLWJpbi9tYWlsbWFuL2xpc3RpbmZvL2xpYnJhcmllcwo=

--===============8794242309512341912==--