Agda-2.5.1: A dependently typed functional programming language and proof assistant

Safe HaskellSafe
LanguageHaskell98

Agda.Utils.Except

Description

Wrapper for Control.Monad.Except from the mtl package

Synopsis

Documentation

class Error a where Source

Minimal complete definition

Nothing

Methods

noMsg :: a Source

strMsg :: String -> a Source

Instances

Error String Source

A string can be thrown as an error.

Error () Source

To simulate MaybeT by ExceptT.

Error DeclarationException Source 
Error TCErr Source 
Error UnquoteError Source 
Error SplitError Source 
Error (a, b, c) Source 

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 Source 
MonadEquiv c v d m => MonadEquiv c v d (ExceptT e m) 
Monad m => MonadError e (ExceptT e m) 
MonadReader r m => MonadReader r (ExceptT e m) 
MonadState s m => MonadState s (ExceptT e m) 
MonadWriter w m => MonadWriter w (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) 
MonadTCM tcm => MonadTCM (ExceptT err tcm) Source 
(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 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 | m -> e where

The strategy of combining computations that can throw exceptions by bypassing bound functions from the point an exception is thrown to the point that it is handled.

Is parameterized over the type of error information and the monad type constructor. It is common to use Either String as the monad type constructor for an error monad in which error descriptions take the form of strings. In that case and many other common cases the resulting monad is already defined as an instance of the MonadError class. You can also define your own error type and/or use a monad type constructor other than Either String or Either IOError. In these cases you will have to explicitly define instances of the Error and/or MonadError classes.

Methods

throwError :: e -> m a

Is used within a monadic computation to begin exception processing.

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

A handler function to handle previous errors and return to normal execution. A common idiom is:

do { action1; action2; action3 } `catchError` handler

where the action functions can call throwError. Note that handler and the do-block must have the same return type.

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.