Proposal: add laws to MonadError

[Härmel Nestra]

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 =
catchError (m >>= f) h
Prelude Control.Monad.Except Control.Monad.Writer> let rhs f h m =
catchError (Right <$> m) (pure . Left) >>= either h ((`catchError` h) . f)
Prelude Control.Monad.Except Control.Monad.Writer> let f a = WriterT (Left
())
Prelude Control.Monad.Except Control.Monad.Writer> let h e = WriterT (Right
(True , [()]))
Prelude Control.Monad.Except Control.Monad.Writer> let m = 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ärmel

Kontakt David Feuer (<david.feuer at gmail.com>) kirjutas kuupäeval L, 10.
september 2022 kell 02:57:

> 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 <david.feuer at gmail.com> 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 <
>> alexandre.fmp.esteves at gmail.com> 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
>>> Libraries at haskell.org
>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>>>
>> _______________________________________________
> Libraries mailing list
> Libraries at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20230706/63ea4194/attachment.html>