Safe Haskell | Safe |
---|---|
Language | Haskell2010 |
Agda.Utils.Except
Description
Wrapper for Control.Monad.Except from the mtl library (>= 2.2.1)
Synopsis
- class Error a where
- data ExceptT e (m :: Type -> Type) a
- mapExceptT :: (m (Either e a) -> n (Either e' b)) -> ExceptT e m a -> ExceptT e' n b
- mkExceptT :: m (Either e a) -> ExceptT e m a
- class Monad m => MonadError e (m :: Type -> Type) | m -> e where
- throwError :: e -> m a
- catchError :: m a -> (e -> m a) -> m a
- runExceptT :: ExceptT e m a -> m (Either e a)
Documentation
Error class for backward compatibility (from Control.Monad.Trans.Error in transformers 0.3.0.0).
Minimal complete definition
Nothing
data ExceptT e (m :: Type -> Type) a #
Instances
MonadEquiv c v d m => MonadEquiv c v d (ExceptT e m) | |
Defined in Data.Equivalence.Monad Methods equivalent :: v -> v -> ExceptT e m Bool classDesc :: v -> ExceptT e m d equateAll :: [v] -> ExceptT e m () equate :: v -> v -> ExceptT e m () removeClass :: v -> ExceptT e m Bool getClass :: v -> ExceptT e m c combineAll :: [c] -> ExceptT e m () combine :: c -> c -> ExceptT e m c | |
MonadRWS r w s m => MonadRWS r w s (ExceptT e m) | |
Defined in Control.Monad.RWS.Class | |
Conversion MOT (Exp O) Type Source # | |
Conversion MOT (Exp O) Term Source # | |
Conversion MOT a b => Conversion MOT (Abs a) (Abs b) Source # | |
Monad m => MonadError e (ExceptT e m) | |
Defined in Control.Monad.Error.Class Methods throwError :: e -> ExceptT e m a # catchError :: ExceptT e m a -> (e -> ExceptT e m a) -> ExceptT e m a # | |
MonadWriter w m => MonadWriter w (ExceptT e m) | |
MonadState s m => MonadState s (ExceptT e m) | |
MonadReader r m => MonadReader r (ExceptT e m) | |
Conversion MOT a b => Conversion MOT (MM a (RefInfo O)) b Source # | |
MonadTrans (ExceptT e) | |
Defined in Control.Monad.Trans.Except | |
Monad m => Monad (ExceptT e m) | |
Functor m => Functor (ExceptT e m) | |
MonadFix m => MonadFix (ExceptT e m) | |
Defined in Control.Monad.Trans.Except | |
MonadFail m => MonadFail (ExceptT e m) | |
Defined in Control.Monad.Trans.Except | |
(Functor m, Monad m) => Applicative (ExceptT e m) | |
Defined in Control.Monad.Trans.Except | |
Foldable f => Foldable (ExceptT e f) | |
Defined in Control.Monad.Trans.Except Methods fold :: Monoid m => ExceptT e f m -> m foldMap :: Monoid m => (a -> m) -> ExceptT e f a -> m foldr :: (a -> b -> b) -> b -> ExceptT e f a -> b foldr' :: (a -> b -> b) -> b -> ExceptT e f a -> b foldl :: (b -> a -> b) -> b -> ExceptT e f a -> b foldl' :: (b -> a -> b) -> b -> ExceptT e f a -> b foldr1 :: (a -> a -> a) -> ExceptT e f a -> a foldl1 :: (a -> a -> a) -> ExceptT e f a -> a toList :: ExceptT e f a -> [a] length :: ExceptT e f a -> Int elem :: Eq a => a -> ExceptT e f a -> Bool maximum :: Ord a => ExceptT e f a -> a minimum :: Ord a => ExceptT e f a -> a | |
Traversable f => Traversable (ExceptT e f) | |
Defined in Control.Monad.Trans.Except | |
(Functor m, Monad m, Monoid e) => Alternative (ExceptT e m) | |
(Monad m, Monoid e) => MonadPlus (ExceptT e m) | |
(Eq e, Eq1 m) => Eq1 (ExceptT e m) | |
Defined in Control.Monad.Trans.Except | |
(Ord e, Ord1 m) => Ord1 (ExceptT e m) | |
Defined in Control.Monad.Trans.Except Methods liftCompare :: (a -> b -> Ordering) -> ExceptT e m a -> ExceptT e m b -> Ordering | |
(Read e, Read1 m) => Read1 (ExceptT e m) | |
Defined in Control.Monad.Trans.Except Methods liftReadsPrec :: (Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (ExceptT e m a) liftReadList :: (Int -> ReadS a) -> ReadS [a] -> ReadS [ExceptT e m a] liftReadPrec :: ReadPrec a -> ReadPrec [a] -> ReadPrec (ExceptT e m a) liftReadListPrec :: ReadPrec a -> ReadPrec [a] -> ReadPrec [ExceptT e m a] | |
(Show e, Show1 m) => Show1 (ExceptT e m) | |
Defined in Control.Monad.Trans.Except Methods liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> ExceptT e m a -> ShowS liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [ExceptT e m a] -> ShowS | |
MonadIO m => MonadIO (ExceptT e m) | |
Defined in Control.Monad.Trans.Except | |
Contravariant m => Contravariant (ExceptT e m) | |
MonadZip m => MonadZip (ExceptT e m) | |
PrimMonad m => PrimMonad (ExceptT e m) | |
MonadTCM tcm => MonadTCM (ExceptT err tcm) Source # | |
MonadTCState m => MonadTCState (ExceptT err m) Source # | |
MonadTCEnv m => MonadTCEnv (ExceptT err m) Source # | |
MonadReduce m => MonadReduce (ExceptT err m) Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods liftReduce :: ReduceM a -> ExceptT err m a Source # | |
HasOptions m => HasOptions (ExceptT e m) Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods pragmaOptions :: ExceptT e m PragmaOptions Source # commandLineOptions :: ExceptT e m CommandLineOptions Source # | |
ReadTCState m => ReadTCState (ExceptT err m) Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
MonadCatch m => MonadCatch (ExceptT e m) | |
Defined in Control.Monad.Catch | |
MonadMask m => MonadMask (ExceptT e m) | |
Defined in Control.Monad.Catch Methods mask :: ((forall a. ExceptT e m a -> ExceptT e m a) -> ExceptT e m b) -> ExceptT e m b uninterruptibleMask :: ((forall a. ExceptT e m a -> ExceptT e m a) -> ExceptT e m b) -> ExceptT e m b generalBracket :: ExceptT e m a -> (a -> ExitCase b -> ExceptT e m c) -> (a -> ExceptT e m b) -> ExceptT e m (b, c) | |
MonadThrow m => MonadThrow (ExceptT e m) | |
Defined in Control.Monad.Catch | |
MonadDebug m => MonadDebug (ExceptT e m) Source # | |
Defined in Agda.TypeChecking.Monad.Debug Methods displayDebugMessage :: Int -> String -> ExceptT e m () Source # traceDebugMessage :: Int -> String -> ExceptT e m a -> ExceptT e m a Source # formatDebugMessage :: VerboseKey -> Int -> TCM Doc -> ExceptT e m String Source # | |
HasConstInfo m => HasConstInfo (ExceptT err m) Source # | |
Defined in Agda.TypeChecking.Monad.Signature Methods getConstInfo :: QName -> ExceptT err m Definition Source # getConstInfo' :: QName -> ExceptT err m (Either SigError Definition) Source # getRewriteRulesFor :: QName -> ExceptT err m RewriteRules Source # | |
HasBuiltins m => HasBuiltins (ExceptT e m) Source # | |
Defined in Agda.TypeChecking.Monad.Builtin | |
(Eq e, Eq1 m, Eq a) => Eq (ExceptT e m a) | |
(Ord e, Ord1 m, Ord a) => Ord (ExceptT e m a) | |
Defined in Control.Monad.Trans.Except | |
(Read e, Read1 m, Read a) => Read (ExceptT e m a) | |
Defined in Control.Monad.Trans.Except | |
(Show e, Show1 m, Show a) => Show (ExceptT e m a) | |
type PrimState (ExceptT e m) | |
Defined in Control.Monad.Primitive type PrimState (ExceptT e m) = PrimState m |
mapExceptT :: (m (Either e a) -> n (Either e' b)) -> ExceptT e m a -> ExceptT e' n b #
mkExceptT :: m (Either e a) -> ExceptT e m a Source #
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 :: Type -> Type) | m -> e where #
Instances
MonadError () Maybe | |
Defined in Control.Monad.Error.Class | |
MonadError IOException IO | |
Defined in Control.Monad.Error.Class | |
MonadError ParseError Parser Source # | |
Defined in Agda.Syntax.Parser.Monad Methods throwError :: ParseError -> Parser a # catchError :: Parser a -> (ParseError -> Parser a) -> Parser a # | |
MonadError ParseError PM Source # | |
Defined in Agda.Syntax.Parser | |
MonadError DeclarationException Nice Source # | |
Defined in Agda.Syntax.Concrete.Definitions Methods throwError :: DeclarationException -> Nice a # catchError :: Nice a -> (DeclarationException -> Nice a) -> Nice a # | |
MonadError TCErr IM Source # | |
Defined in Agda.TypeChecking.Monad.Base | |
MonadError TCErr TerM Source # | |
Defined in Agda.Termination.Monad | |
MonadError e m => MonadError e (MaybeT m) | |
Defined in Control.Monad.Error.Class | |
MonadError e m => MonadError e (ListT m) | |
Defined in Control.Monad.Error.Class | |
MonadError e (Either e) | |
Defined in Control.Monad.Error.Class | |
MonadError TCErr (TCMT IO) Source # | |
Defined in Agda.TypeChecking.Monad.Base Methods throwError :: TCErr -> TCMT IO a # catchError :: TCMT IO a -> (TCErr -> TCMT IO a) -> TCMT IO a # | |
(Monoid w, MonadError e m) => MonadError e (WriterT w m) | |
Defined in Control.Monad.Error.Class Methods throwError :: e -> WriterT w m a # catchError :: WriterT w m a -> (e -> WriterT w m a) -> WriterT w m a # | |
(Monoid w, MonadError e m) => MonadError e (WriterT w m) | |
Defined in Control.Monad.Error.Class Methods throwError :: e -> WriterT w m a # catchError :: WriterT w m a -> (e -> WriterT w m a) -> WriterT w m a # | |
MonadError e m => MonadError e (StateT s m) | |
Defined in Control.Monad.Error.Class Methods throwError :: e -> StateT s m a # catchError :: StateT s m a -> (e -> StateT s m a) -> StateT s m a # | |
MonadError e m => MonadError e (StateT s m) | |
Defined in Control.Monad.Error.Class Methods throwError :: e -> StateT s m a # catchError :: StateT s m a -> (e -> StateT s m a) -> StateT s m a # | |
MonadError e m => MonadError e (ReaderT r m) | |
Defined in Control.Monad.Error.Class Methods throwError :: e -> ReaderT r m a # catchError :: ReaderT r m a -> (e -> ReaderT r m a) -> ReaderT r m a # | |
MonadError e m => MonadError e (IdentityT m) | |
Defined in Control.Monad.Error.Class Methods throwError :: e -> IdentityT m a # catchError :: IdentityT m a -> (e -> IdentityT m a) -> IdentityT m a # | |
Monad m => MonadError e (ExceptT e m) | |
Defined in Control.Monad.Error.Class Methods throwError :: e -> ExceptT e m a # catchError :: ExceptT e m a -> (e -> ExceptT e m a) -> ExceptT e m a # | |
(Monad m, Error e) => MonadError e (ErrorT e m) | |
Defined in Control.Monad.Error.Class Methods throwError :: e -> ErrorT e m a # catchError :: ErrorT e m a -> (e -> ErrorT e m a) -> ErrorT e m a # | |
MonadError e m => MonadError e (EquivT s c v m) | |
Defined in Data.Equivalence.Monad Methods throwError :: e -> EquivT s c v m a # catchError :: EquivT s c v m a -> (e -> EquivT s c v m a) -> EquivT s c v m a # | |
(Monoid w, MonadError e m) => MonadError e (RWST r w s m) | |
Defined in Control.Monad.Error.Class Methods throwError :: e -> RWST r w s m a # catchError :: RWST r w s m a -> (e -> RWST r w s m a) -> RWST r w s m a # | |
(Monoid w, MonadError e m) => MonadError e (RWST r w s m) | |
Defined in Control.Monad.Error.Class Methods throwError :: e -> RWST r w s m a # catchError :: RWST r w s m a -> (e -> RWST r w s m a) -> RWST r w s m a # |
runExceptT :: ExceptT e m a -> m (Either e a) #