Agda.Utils.Except

Wrapper for Control.Monad.Except from the mtl package

Documentation

class Error a where

Methods

noMsg :: a

strMsg :: String -> a

Instances

Error ()

To simulate MaybeT by ExceptT.

Methods

noMsg :: ()

strMsg :: String -> ()

Error String

A string can be thrown as an error.

Methods

noMsg :: String

strMsg :: String -> String

Error DeclarationException

Methods

noMsg :: DeclarationException

strMsg :: String -> DeclarationException

Error TCErr

Methods

noMsg :: TCErr

strMsg :: String -> TCErr

Error UnquoteError

Methods

noMsg :: UnquoteError

strMsg :: String -> UnquoteError

Error SplitError

Methods

noMsg :: SplitError

strMsg :: String -> SplitError

Error (a, b, c)

Methods

noMsg :: (a, b, c)

strMsg :: String -> (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

Methods

pragmaOptions :: NLM PragmaOptions

commandLineOptions :: NLM CommandLineOptions

MonadEquiv c v d m => MonadEquiv c v d (ExceptT e m)

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

(===) :: c -> c -> ExceptT e m Bool

desc :: c -> ExceptT e m d

remove :: c -> ExceptT e m Bool

Monad m => MonadError e (ExceptT e m)

Methods

throwError :: e -> ExceptT e m a

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

MonadReader r m => MonadReader r (ExceptT e m)

Methods

ask :: ExceptT e m r

local :: (r -> r) -> ExceptT e m a -> ExceptT e m a

reader :: (r -> a) -> ExceptT e m a

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

Methods

get :: ExceptT e m s

put :: s -> ExceptT e m ()

state :: (s -> (a, s)) -> ExceptT e m a

MonadWriter w m => MonadWriter w (ExceptT e m)

Methods

writer :: (a, w) -> ExceptT e m a

tell :: w -> ExceptT e m ()

listen :: ExceptT e m a -> ExceptT e m (a, w)

pass :: ExceptT e m (a, w -> w) -> ExceptT e m a

MonadTrans (ExceptT e)

Methods

lift :: Monad m => m a -> ExceptT e m a

Monad m => Monad (ExceptT e m)

Methods

(>>=) :: ExceptT e m a -> (a -> ExceptT e m b) -> ExceptT e m b

(>>) :: ExceptT e m a -> ExceptT e m b -> ExceptT e m b

return :: a -> ExceptT e m a

fail :: String -> ExceptT e m a

Functor m => Functor (ExceptT e m)

Methods

fmap :: (a -> b) -> ExceptT e m a -> ExceptT e m b

(<$) :: a -> ExceptT e m b -> ExceptT e m a

MonadFix m => MonadFix (ExceptT e m)

Methods

mfix :: (a -> ExceptT e m a) -> ExceptT e m a

MonadFail m => MonadFail (ExceptT e m)

Methods

fail :: String -> ExceptT e m a

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

Methods

pure :: a -> ExceptT e m a

(<*>) :: ExceptT e m (a -> b) -> ExceptT e m a -> ExceptT e m b

(*>) :: ExceptT e m a -> ExceptT e m b -> ExceptT e m b

(<*) :: ExceptT e m a -> ExceptT e m b -> ExceptT e m a

Foldable f => Foldable (ExceptT e f)

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]

null :: ExceptT e f a -> Bool

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

sum :: Num a => ExceptT e f a -> a

product :: Num a => ExceptT e f a -> a

Traversable f => Traversable (ExceptT e f)

Methods

traverse :: Applicative f => (a -> f b) -> ExceptT e f a -> f (ExceptT e f b)

sequenceA :: Applicative f => ExceptT e f (f a) -> f (ExceptT e f a)

mapM :: Monad m => (a -> m b) -> ExceptT e f a -> m (ExceptT e f b)

sequence :: Monad m => ExceptT e f (m a) -> m (ExceptT e f a)

(Eq e, Eq1 m) => Eq1 (ExceptT e m)

Methods

liftEq :: (a -> b -> Bool) -> ExceptT e m a -> ExceptT e m b -> Bool

(Ord e, Ord1 m) => Ord1 (ExceptT e m)

Methods

liftCompare :: (a -> b -> Ordering) -> ExceptT e m a -> ExceptT e m b -> Ordering

(Read e, Read1 m) => Read1 (ExceptT e m)

Methods

liftReadsPrec :: (Int -> ReadS a) -> ReadS [a] -> Int -> ReadS (ExceptT e m a)

liftReadList :: (Int -> ReadS a) -> ReadS [a] -> ReadS [ExceptT e m a]

(Show e, Show1 m) => Show1 (ExceptT e m)

Methods

liftShowsPrec :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> Int -> ExceptT e m a -> ShowS

liftShowList :: (Int -> a -> ShowS) -> ([a] -> ShowS) -> [ExceptT e m a] -> ShowS

MonadZip m => MonadZip (ExceptT e m)

Methods

mzip :: ExceptT e m a -> ExceptT e m b -> ExceptT e m (a, b)

mzipWith :: (a -> b -> c) -> ExceptT e m a -> ExceptT e m b -> ExceptT e m c

munzip :: ExceptT e m (a, b) -> (ExceptT e m a, ExceptT e m b)

MonadIO m => MonadIO (ExceptT e m)

Methods

liftIO :: IO a -> ExceptT e m a

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

Methods

empty :: ExceptT e m a

(<|>) :: ExceptT e m a -> ExceptT e m a -> ExceptT e m a

some :: ExceptT e m a -> ExceptT e m [a]

many :: ExceptT e m a -> ExceptT e m [a]

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

Methods

mzero :: ExceptT e m a

mplus :: ExceptT e m a -> ExceptT e m a -> ExceptT e m a

PrimMonad m => PrimMonad (ExceptT e m)

Associated Types

type PrimState (ExceptT e m :: * -> *) :: *

Methods

primitive :: (State# (PrimState (ExceptT e m)) -> (#VoidRep, PtrRepLifted, State# (PrimState (ExceptT e m)), a#)) -> ExceptT e m a

MonadTCM tcm => MonadTCM (ExceptT err tcm)

Methods

liftTCM :: TCM a -> ExceptT err tcm a

(Eq e, Eq1 m, Eq a) => Eq (ExceptT e m a)

Methods

(==) :: ExceptT e m a -> ExceptT e m a -> Bool

(/=) :: ExceptT e m a -> ExceptT e m a -> Bool

(Ord e, Ord1 m, Ord a) => Ord (ExceptT e m a)

Methods

compare :: ExceptT e m a -> ExceptT e m a -> Ordering

(<) :: ExceptT e m a -> ExceptT e m a -> Bool

(<=) :: ExceptT e m a -> ExceptT e m a -> Bool

(>) :: ExceptT e m a -> ExceptT e m a -> Bool

(>=) :: ExceptT e m a -> ExceptT e m a -> Bool

max :: ExceptT e m a -> ExceptT e m a -> ExceptT e m a

min :: ExceptT e m a -> ExceptT e m a -> ExceptT e m a

(Read e, Read1 m, Read a) => Read (ExceptT e m a)

Methods

readsPrec :: Int -> ReadS (ExceptT e m a)

readList :: ReadS [ExceptT e m a]

readPrec :: ReadPrec (ExceptT e m a)

readListPrec :: ReadPrec [ExceptT e m a]

(Show e, Show1 m, Show a) => Show (ExceptT e m a)

Methods

showsPrec :: Int -> ExceptT e m a -> ShowS

show :: ExceptT e m a -> String

showList :: [ExceptT e m a] -> ShowS

type PrimState (ExceptT e m)

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

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.

Instances

MonadError IOException IO

Methods

throwError :: IOException -> IO a

catchError :: IO a -> (IOException -> IO a) -> IO a

MonadError ParseError Parser

Methods

throwError :: ParseError -> Parser a

catchError :: Parser a -> (ParseError -> Parser a) -> Parser a

MonadError TCErr IM

Methods

throwError :: TCErr -> IM a

catchError :: IM a -> (TCErr -> IM a) -> IM a

MonadError TCErr TerM

Methods

throwError :: TCErr -> TerM a

catchError :: TerM a -> (TCErr -> TerM a) -> TerM a

MonadError e m => MonadError e (MaybeT m)

Methods

throwError :: e -> MaybeT m a

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

MonadError e m => MonadError e (ListT m)

Methods

throwError :: e -> ListT m a

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

MonadError e (Either e)

Methods

throwError :: e -> Either e a

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

MonadError TCErr (TCMT IO)

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)

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)

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)

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)

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 (IdentityT * m)

Methods

throwError :: e -> IdentityT * m a

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

Monad m => MonadError e (ExceptT e m)

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)

Methods

throwError :: e -> ErrorT e m a

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

(Error err, MonadError err' m) => MonadError err' (ExceptionT err m)

Methods

throwError :: err' -> ExceptionT err m a

catchError :: ExceptionT err m a -> (err' -> ExceptionT err m a) -> ExceptionT err m a

MonadError e m => MonadError e (ReaderT * r m)

Methods

throwError :: e -> ReaderT * r m a

catchError :: ReaderT * r m a -> (e -> ReaderT * r m a) -> ReaderT * r m a

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

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)

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

MonadError e m => MonadError e (EquivT s c v m)

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

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)