Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

instance (MonadError e f, MonadError e g) => MonadError e (Product f g) #84

Open
LightAndLight opened this issue Nov 26, 2020 · 1 comment

Comments

@LightAndLight
Copy link

Is there a technical reason why this instance doesn't exist? It seems well-behaved (some sanity-check proofs are at the bottom of the page).

fstP :: Product f g a -> f a
fstP (Pair a _) = a

sndP :: Product f g a -> g a
sndP (Pair _ a) = a

instance (MonadError e f, MonadError e g) => MonadError e (Product f g) where
  throwError e = Pair (throwError e) (throwError e)
  catchError (Pair ma mb) f = Pair (catchError ma (fstP . f)) (catchError mb (sndP . f))

catchError m throwError = m

catchError (Pair f g) throwError
= { inline catchError }
Pair (catchError f (fstP . throwError)) (catchError g (sndP . throwError))
= { inline throwError }
Pair 
  (catchError f (fstP . (\e -> Pair (throwError e) (throwError e)))
  (catchError g (sndP . (\e -> Pair (throwError e) (throwError e)))
= { inline (.) }
Pair 
  (catchError f (\e -> fstP (Pair (throwError e) (throwError e)))
  (catchError g (\e -> sndP (Pair (throwError e) (throwError e)))
= { eta-reduction }
Pair 
  (catchError f (\e -> throwError e))
  (catchError g (\e -> throwError e))
= { eta-reduction }
Pair 
  (catchError f throwError)
  (catchError g throwError)
= { hypothesis }
Pair f g
catchError (throwError e) pure = pure e

catchError (throwError e) pure
= { inline throwError }
catchError (Pair (throwError e) (throwError e)) pure = pure e
= { inline catchError }
Pair (catchError (throwError e) (fstP . pure)) (catchError (throwError e) (sndP . pure))
= { inline pure, (.) }
Pair 
  (catchError (throwError e) (\x -> fstP (Pair (pure x) (pure x)))) 
  (catchError (throwError e) (\x -> sndP (Pair (pure x) (pure x))))
= { eta-reduction }
Pair 
  (catchError (throwError e) (\x -> pure x)) 
  (catchError (throwError e) (\x -> pure x))
= { eta-reduction }
Pair 
  (catchError (throwError e) pure) 
  (catchError (throwError e) pure)
= { hypothesis }
Pair (pure e) (pure e}
= { pure }
pure e
@despresc
Copy link

despresc commented Apr 9, 2021

Is that instance unnecessarily restrictive? I would have thought that

instance (MonadError e1 f, MonadError e2 g) => MonadError (e1, e2) (Product f g) where

would work as well. Your throwError would then be \e -> throwError (e, e).


EDIT: Never mind. The catchError method can't be defined with this alternate instance.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants