0 | ||| The Error monad (also called the Exception monad).
  1 | module Control.Monad.Error.Interface
  2 |
  3 | import Control.Monad.Error.Either
  4 | import Control.Monad.Maybe
  5 | import Control.Monad.RWS.CPS
  6 | import Control.Monad.Reader.Reader
  7 | import Control.Monad.State.State
  8 | import Control.Monad.Trans
  9 | import Control.Monad.Writer.CPS
 10 |
 11 | %default total
 12 |
 13 | ||| The strategy of combining computations that can throw exceptions
 14 | ||| by bypassing bound functions
 15 | ||| from the point an exception is thrown to the point that it is handled.
 16 | ||| Is parameterized over the type of error information and
 17 | ||| the monad type constructor.
 18 | ||| It is common to use `Either String` as the monad type constructor
 19 | ||| for an error monad in which error descriptions take the form of strings.
 20 | ||| In that case and many other common cases the resulting monad is already defined
 21 | ||| as an instance of the 'MonadError' class.
 22 | public export
 23 | interface Monad m => MonadError e m | m where
 24 |   ||| Is used within a monadic computation to begin exception processing.
 25 |   throwError : e -> m a
 26 |
 27 |   ||| A handler function to handle previous errors and return to normal execution.
 28 |   ||| A common idiom is:
 29 |   |||
 30 |   ||| ```idris example
 31 |   ||| do { action1; action2; action3 } `catchError` handler
 32 |   ||| ```
 33 |   catchError : m a -> (e -> m a) -> m a
 34 |
 35 | ||| Lifts an `Either e` into any `MonadError e`.
 36 | public export
 37 | liftEither : MonadError e m => Either e a -> m a
 38 | liftEither = either throwError pure
 39 |
 40 | ||| Makes a success or failure of an action visible in
 41 | ||| the return type.
 42 | public export
 43 | tryError : MonadError e m => m a -> m (Either e a)
 44 | tryError action = (map Right action) `catchError` (pure . Left)
 45 |
 46 | ||| `MonadError` analogue to the `withEitherT` function.
 47 | ||| Modify the value (but not the type) of an error.
 48 | ||| If you need to change the type of `e` use `mapError`.
 49 | public export
 50 | withError : MonadError e m => (e -> e) -> m a -> m a
 51 | withError f action = tryError action >>= either (throwError . f) pure
 52 |
 53 | ||| Flipped version of `catchError`.
 54 | public export
 55 | handleError : MonadError e m => (e -> m a) -> m a -> m a
 56 | handleError = flip catchError
 57 |
 58 | ||| `MonadError` analogue of the `mapEitherT` function.  The
 59 | ||| computation is unwrapped, a function is applied to the `Either`, and
 60 | ||| the result is lifted into the second `MonadError` instance.
 61 | public export
 62 | mapError : (MonadError e m, MonadError e' n)
 63 |          => (m (Either e a) -> n (Either e' b)) -> m a -> n b
 64 | mapError f action = f (tryError action) >>= liftEither
 65 |
 66 | --------------------------------------------------------------------------------
 67 | --          Implementations
 68 | --------------------------------------------------------------------------------
 69 |
 70 | public export
 71 | MonadError () Maybe where
 72 |   throwError ()        = Nothing
 73 |   catchError Nothing f = f ()
 74 |   catchError x       _ = x
 75 |
 76 | public export
 77 | Monad m => MonadError () (MaybeT m) where
 78 |   throwError () = MkMaybeT $ pure Nothing
 79 |   catchError (MkMaybeT m) f = MkMaybeT $ m >>= maybe (runMaybeT $ f ()) (pure @{Compose})
 80 |
 81 | public export
 82 | MonadError e (Either e) where
 83 |   throwError             = Left
 84 |   Left  l `catchError` h = h l
 85 |   Right r `catchError` _ = Right r
 86 |
 87 | public export
 88 | Monad m => MonadError e (EitherT e m) where
 89 |   throwError = throwE
 90 |   catchError = catchE
 91 |
 92 | public export
 93 | MonadError e m => MonadError e (MaybeT m) where
 94 |   throwError = lift . throwError
 95 |   catchError (MkMaybeT m) f = MkMaybeT (catchError m (runMaybeT . f))
 96 |
 97 | public export
 98 | MonadError e m => MonadError e (ReaderT r m) where
 99 |   throwError = lift . throwError
100 |   catchError (MkReaderT m) f =
101 |     MkReaderT $ \e => catchError (m e) (runReaderT e . f)
102 |
103 | public export
104 | MonadError e m => MonadError e (StateT r m) where
105 |   throwError = lift . throwError
106 |   catchError (ST m) f =
107 |     ST $ \s => catchError (m s) (runStateT s . f)
108 |
109 | public export
110 | MonadError e m => MonadError e (RWST r w s m) where
111 |   throwError = lift . throwError
112 |   catchError (MkRWST m) f =
113 |     MkRWST $ \r,w,s => catchError (m r w s) (\e => unRWST (f e) r w s)
114 |
115 | public export
116 | MonadError e m => MonadError e (WriterT w m) where
117 |   throwError = lift . throwError
118 |   catchError (MkWriterT m) f =
119 |     MkWriterT $ \w => catchError (m w) (\e => unWriterT (f e) w)
120 |