Re: Proposal: add laws to MonadError

--===============6325292379821643484==
Content-Type: multipart/alternative; boundary="000000000000ad7c7c05ffcd8782"

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

Hi,

I went over an old mail, sorry for the late reply. David's law does not
hold:

GHCi, version 8.8.4: https://www.haskell.org/ghc/  :? for help
Prelude> :m Control.Monad.Except Control.Monad.Writer
Prelude Control.Monad.Except Control.Monad.Writer> let lhs f h m =3D
catchError (m >>=3D f) h
Prelude Control.Monad.Except Control.Monad.Writer> let rhs f h m =3D
catchError (Right <$> m) (pure . Left) >>=3D either h ((`catchError` h) . f=
)
Prelude Control.Monad.Except Control.Monad.Writer> let f a =3D WriterT (Lef=
t
())
Prelude Control.Monad.Except Control.Monad.Writer> let h e =3D WriterT (Rig=
ht
(True , [()]))
Prelude Control.Monad.Except Control.Monad.Writer> let m =3D WriterT (Right
(False , [(), ()]))
Prelude Control.Monad.Except Control.Monad.Writer> lhs f h m
WriterT (Right (True,[()]))
Prelude Control.Monad.Except Control.Monad.Writer> rhs f h m
WriterT (Right (True,[(),(),()]))

Regards,
H=C3=A4rmel

Kontakt David Feuer (<[email protected]>) kirjutas kuup=C3=A4eval L, 10=
.
september 2022 kell 02:57:

> Sorry, I mangled that. I meant
>
> catchError (m >>=3D f) h =3D catchError (Right <$> m) (pure . Left) >>=3D
>   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 >>=3D f) h =3D catchError (Right <$> m) (pure . Left) >>=
=3D
>>   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 i=
f
>>>   catchError (pure a) h =3D pure a
>>> was a law, so I looked up the laws in
>>> https://hackage.haskell.org/package/mtl-2.3/docs/Control-Monad-Error-Cl=
ass.html#t:MonadError
>>> but surprisingly found none.
>>>
>>> One would expect to see
>>>   1. catchError (pure a) h =3D pure a
>>>   2. catchError (throwError e) h =3D h e
>>>   3. throwError e >>=3D f =3D throwError e
>>>
>>> which would rule out silly instances like
>>>   instance MonadError () Maybe where
>>>     throwError ()        =3D Nothing
>>>     catchError _ f =3D 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.Erro=
r.Class.html%20
>>> all obey the laws.
>>> _______________________________________________
>>> Libraries mailing list
>>> [email protected]
>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>>>
>> _______________________________________________
> Libraries mailing list
> [email protected]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>

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

<div dir=3D"ltr"><div>Hi,</div><div><br></div><div>I went over an old mail,=
 sorry for the late reply. David&#39;s law does not hold:</div><div><br></d=
iv><div>GHCi, version 8.8.4: <a href=3D"https://www.haskell.org/ghc/">https=
://www.haskell.org/ghc/</a> =C2=A0:? for help<br>Prelude&gt; :m Control.Mon=
ad.Except Control.Monad.Writer<br>Prelude Control.Monad.Except Control.Mona=
d.Writer&gt; let lhs f h m =3D catchError (m &gt;&gt;=3D f) h<br>Prelude Co=
ntrol.Monad.Except Control.Monad.Writer&gt; let rhs f h m =3D catchError (R=
ight &lt;$&gt; m) (pure . Left) &gt;&gt;=3D either h ((`catchError` h) . f)=
<br>Prelude Control.Monad.Except Control.Monad.Writer&gt; let f a =3D Write=
rT (Left ())<br>Prelude Control.Monad.Except Control.Monad.Writer&gt; let h=
 e =3D WriterT (Right (True , [()]))<br>Prelude Control.Monad.Except Contro=
l.Monad.Writer&gt; let m =3D WriterT (Right (False , [(), ()]))<br>Prelude =
Control.Monad.Except Control.Monad.Writer&gt; lhs f h m<br>WriterT (Right (=
True,[()]))<br>Prelude Control.Monad.Except Control.Monad.Writer&gt; rhs f =
h m<br>WriterT (Right (True,[(),(),()]))</div><div><br></div><div>Regards,<=
/div><div>H=C3=A4rmel<br></div></div><br><div class=3D"gmail_quote"><div di=
r=3D"ltr" class=3D"gmail_attr">Kontakt David Feuer (&lt;<a href=3D"mailto:d=
[email protected]">[email protected]</a>&gt;) kirjutas kuup=C3=A4eva=
l L, 10. september 2022 kell 02:57:<br></div><blockquote class=3D"gmail_quo=
te" style=3D"margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204=
);padding-left:1ex"><div dir=3D"auto"><div>Sorry, I mangled that. I meant<d=
iv 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)</di=
v></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:david.=
[email protected]" target=3D"_blank">[email protected]</a>&gt; 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"><=
div>I agree. These are still insufficient for much reasoning, however. I wo=
uld intuitively expect that</div><div dir=3D"auto"><br></div><div dir=3D"au=
to">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 ((`cat=
chError` h)=C2=A0 . f)</div><div dir=3D"auto"><br></div><div dir=3D"auto">B=
ut 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"au=
to"><br></div><div dir=3D"auto"><div class=3D"gmail_quote" dir=3D"auto"><di=
v dir=3D"ltr" class=3D"gmail_attr">On Fri, Sep 9, 2022, 5:43 PM Alexandre E=
steves &lt;<a href=3D"mailto:[email protected]" rel=3D"norefe=
rrer noreferrer" target=3D"_blank">[email protected]</a>&gt; =
wrote:<br></div><blockquote class=3D"gmail_quote" style=3D"margin:0px 0px 0=
px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><div dir=
=3D"ltr">I ran into a scenario where the use of MonadError would only be va=
lid 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.o=
rg/package/mtl-2.3/docs/Control-Monad-Error-Class.html#t:MonadError" rel=3D=
"noreferrer noreferrer noreferrer" target=3D"_blank">https://hackage.haskel=
l.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 s=
ee</div><div>=C2=A0 1.=C2=A0catchError (pure a) h =3D pure a<br>=C2=A0 2. c=
atchError (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 out s=
illy 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 f=
or &quot;monad error laws&quot; gives me no haskell results, only <a href=
=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>
_______________________________________________<br>
Libraries mailing list<br>
<a href=3D"mailto:[email protected]" target=3D"_blank">Libraries@haskel=
l.org</a><br>
<a href=3D"http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries" rel=
=3D"noreferrer" target=3D"_blank">http://mail.haskell.org/cgi-bin/mailman/l=
istinfo/libraries</a><br>
</blockquote></div>

--000000000000ad7c7c05ffcd8782--

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

X19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX19fX18KTGlicmFyaWVz
IG1haWxpbmcgbGlzdApMaWJyYXJpZXNAaGFza2VsbC5vcmcKaHR0cDovL21haWwuaGFza2VsbC5v
cmcvY2dpLWJpbi9tYWlsbWFuL2xpc3RpbmZvL2xpYnJhcmllcwo=

--===============6325292379821643484==--