| Safe Haskell | Safe |
|---|---|
| Language | Haskell2010 |
Agda.Utils.Except
Description
Wrapper for Control.Monad.Except from the mtl package
Documentation
Instances
| Error String # | A string can be thrown as an error. |
| Error DeclarationException # | |
| Error TCErr # | |
| Error UnquoteError # | |
| Error SplitError # | |
data ExceptT e m a :: * -> (* -> *) -> * -> * #
A monad transformer that adds exceptions to other monads.
ExceptT constructs a monad parameterized over two things:
- e - The exception type.
- m - The inner monad.
The return function yields a computation that produces the given
value, while >>= sequences two subcomputations, exiting on the
first exception.
Instances
| HasOptions NLM # | |
| MonadEquiv c v d m => MonadEquiv c v d (ExceptT e m) | |
| MonadWriter w m => MonadWriter w (ExceptT e m) | |
| MonadReader r m => MonadReader r (ExceptT e m) | |
| MonadState s m => MonadState s (ExceptT e m) | |
| Monad m => MonadError e (ExceptT e m) | |
| MonadTrans (ExceptT e) | |
| Monad m => Monad (ExceptT e m) | |
| Functor m => Functor (ExceptT e m) | |
| MonadFix m => MonadFix (ExceptT e m) | |
| MonadFail m => MonadFail (ExceptT e m) | |
| (Functor m, Monad m) => Applicative (ExceptT e m) | |
| Foldable f => Foldable (ExceptT e f) | |
| Traversable f => Traversable (ExceptT e f) | |
| (Eq e, Eq1 m) => Eq1 (ExceptT e m) | |
| (Ord e, Ord1 m) => Ord1 (ExceptT e m) | |
| (Read e, Read1 m) => Read1 (ExceptT e m) | |
| (Show e, Show1 m) => Show1 (ExceptT e m) | |
| MonadZip m => MonadZip (ExceptT e m) | |
| MonadIO m => MonadIO (ExceptT e m) | |
| (Functor m, Monad m, Monoid e) => Alternative (ExceptT e m) | |
| (Monad m, Monoid e) => MonadPlus (ExceptT e m) | |
| PrimMonad m => PrimMonad (ExceptT e m) | |
| MonadTCM tcm => MonadTCM (ExceptT err tcm) # | |
| (Eq e, Eq1 m, Eq a) => Eq (ExceptT e m a) | |
| (Ord e, Ord1 m, Ord a) => Ord (ExceptT e m a) | |
| (Read e, Read1 m, Read a) => Read (ExceptT e m a) | |
| (Show e, Show1 m, Show a) => Show (ExceptT e m a) | |
| type PrimState (ExceptT e m) | |
mkExceptT :: m (Either e a) -> ExceptT e m a #
We cannot define data constructors synonymous, so we define the
mkExceptT function to be used instead of the data constructor
ExceptT.
class Monad m => MonadError e m | m -> e where #
Minimal complete definition
Instances
| MonadError IOException IO | |
| MonadError ParseError Parser # | |
| MonadError ParseError PM # | |
| MonadError TCErr IM # | |
| MonadError TCErr TerM # | |
| MonadError e m => MonadError e (MaybeT m) | |
| MonadError e m => MonadError e (ListT m) | |
| MonadError e (Either e) | |
| MonadError TCErr (TCMT IO) # | |
| MonadError e m => MonadError e (STT s m) | |
| (Monoid w, MonadError e m) => MonadError e (WriterT w m) | |
| (Monoid w, MonadError e m) => MonadError e (WriterT w m) | |
| MonadError e m => MonadError e (StateT s m) | |
| MonadError e m => MonadError e (StateT s m) | |
| MonadError e m => MonadError e (IdentityT * m) | |
| Monad m => MonadError e (ExceptT e m) | |
| (Monad m, Error e) => MonadError e (ErrorT e m) | |
| (Error err, MonadError err' m) => MonadError err' (ExceptionT err m) # | |
| MonadError e m => MonadError e (ReaderT * r m) | |
| MonadError e m => MonadError e (ParsecT s u m) | |
| MonadError e m => MonadError e (EquivT s c v m) | |
| (Monoid w, MonadError e m) => MonadError e (RWST r w s m) | |
| (Monoid w, MonadError e m) => MonadError e (RWST r w s m) | |
runExceptT :: ExceptT e m a -> m (Either e a) #
The inverse of ExceptT.
mapExceptT :: (m (Either e a) -> n (Either e' b)) -> ExceptT e m a -> ExceptT e' n b #
Map the unwrapped computation using the given function.
runExceptT(mapExceptTf m) = f (runExceptTm)