Agda.Utils.Except

Wrapper for Control.Monad.Except from the mtl package

Documentation

class Error a where

Minimal complete definition

Nothing

Methods

noMsg :: a

strMsg :: String -> a

Instances

Error String

A string can be thrown as an error.

Error ()

To simulate MaybeT by ExceptT.

Error DeclarationException

Error TCErr

Error UnquoteError

Error SplitError

Error UnifyException

Error (a, b, c)

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)

MonadState s m => MonadState s (ExceptT e m)

MonadReader r m => MonadReader r (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)

(Functor m, Monad m) => Applicative (ExceptT e m)

Foldable f => Foldable (ExceptT e f)

Traversable f => Traversable (ExceptT e f)

(Functor m, Monad m, Monoid e) => Alternative (ExceptT e m)

(Monad m, Monoid e) => MonadPlus (ExceptT e m)

MonadIO m => MonadIO (ExceptT e m)

(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)

PrimMonad m => PrimMonad (ExceptT e m)

(Error err, 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) = PrimState 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

Methods

throwError :: e -> m a

catchError :: m a -> (e -> m a) -> m a

Instances

MonadError IOException IO

MonadError ParseError Parser

MonadError TCErr IM

MonadError TCErr TerM

MonadError e m => MonadError e (MaybeT m)

MonadError e m => MonadError e (ListT m)

MonadError e m => MonadError e (IdentityT m)

MonadError e (Either e)

MonadError TCErr (TCMT IO)

(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 (ReaderT r 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)

(Monoid w, MonadError e m) => MonadError e (RWST r w s m)

(Monoid w, MonadError e m) => MonadError e (RWST r w s m)

MonadError e m => MonadError e (EquivT s c v 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 (mapExceptT f m) = f (runExceptT m)