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, 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 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@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.h... 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.Cla... all obey the laws. _______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

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@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@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, 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 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@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.h... 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.Cla... all obey the laws. _______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

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 () 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 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@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.h... 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.Cla... all obey the laws. _______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries

_______________________________________________ Libraries mailing list Libraries@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/libraries