Proposal: add laws to MonadError

[David Feuer]

No, the error type is fixed by the monad, and there's no way to change it
in general. catchError m throwError = m looks promising.

On Sun, Sep 11, 2022, 7:24 PM Alexandre Esteves <
alexandre.fmp.esteves at gmail.com> wrote:

> 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/20220911/811e02b7/attachment.html>