Proposal: add laws to MonadError
David Feuer
david.feuer at gmail.com
Mon Sep 12 00:38:15 UTC 2022
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>
More information about the Libraries
mailing list