Proposal: add laws to MonadError

[Alexandre Esteves]

Hmm, I can't seem to actually state
  catchError m throwError = m
in terms of the other laws, so maybe it's another candidate. I also don't
see how to reduce your law candidate.

About law (1), what I really was going for was "if you don't throw, the
catch/handle is useless", but couldn't find out how to express "don't
throw".
Now, if we don't throw, the error can type can be anything, including Void.
I wonder if (1) can be replaced with
  catchError m absurd = m


On Sat, Sep 10, 2022 at 7:43 PM Alexandre Esteves <
alexandre.fmp.esteves at gmail.com> wrote:

> Nevermind, AFAICT it's s always the case that
>   catchError m throwError = m
>
> On Sat, 10 Sept 2022, 19:41 Alexandre Esteves, <
> alexandre.fmp.esteves at gmail.com> wrote:
>
>> 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, <david.feuer at gmail.com> 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 <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
>>>>>
>>>>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/libraries/attachments/20220912/14d8fb28/attachment.html>