Re: Proposal: add laws to MonadError

--===============0351428024342935006==
Content-Type: multipart/alternative; boundary="000000000000a53fb105e848095b"

--000000000000a53fb105e848095b
Content-Type: text/plain; charset="UTF-8"

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
>

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

<div dir=3D"auto"><div>I agree. These are still insufficient for much reaso=
ning, 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 (Right=
 &lt;$&gt; m) (pure . Left) &gt;&gt;=3D</div><div dir=3D"auto">=C2=A0 eithe=
r throwError ((`catchError` h)=C2=A0 . f)</div><div dir=3D"auto"><br></div>=
<div dir=3D"auto">But I have no idea whether all &quot;reasonable&quot; ins=
tances obey that.</div><div dir=3D"auto"><br></div><div dir=3D"auto">Is the=
re anything useful to say about the case when the argument to mapError is s=
ufficiently 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_quot=
e" 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@gmail=
.com" 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"ltr">I r=
an into a scenario where 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/m=
tl-2.3/docs/Control-Monad-Error-Class.html#t:MonadError" rel=3D"noreferrer =
noreferrer" target=3D"_blank">https://hackage.haskell.org/package/mtl-2.3/d=
ocs/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" t=
arget=3D"_blank">https://typelevel.org/blog/2018/04/13/rethinking-monaderro=
r.html</a> which suggests the same laws.</div><div><br></div><div>I propose=
 adding these 3 laws to MonadError 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 noref=
errer" target=3D"_blank">https://hackage.haskell.org/package/mtl-2.3/docs/s=
rc/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" targ=
et=3D"_blank">[email protected]</a><br>
<a href=3D"http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel=
=3D"noreferrer noreferrer noreferrer" target=3D"_blank">http://mail.haskell=
.org/cgi-bin/mailman/listinfo/libraries</a><br>
</blockquote></div></div></div>

--000000000000a53fb105e848095b--

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

X19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX18KTGlicmFyaWVz
IG1haWxpbmcgbGlzdApMaWJyYXJpZXNAaGFza2VsbC5vcmcKaHR0cDovL21haWwuaGFza2VsbC5v
cmcvY2dpLWJpbi9tYWlsbWFuL2xpc3RpbmZvL2xpYnJhcmllcwo=

--===============0351428024342935006==--