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

Safe Haskell | None
Language | Haskell2010

Agda.Utils.IO

Description

Auxiliary functions for the IO monad.

Synopsis

- class CatchIO (m :: Type -> Type) where
  - catchIO :: Exception e => m a -> (e -> m a) -> m a
- showIOException :: Exception e => e -> String

# Documentation

class CatchIO (m :: Type -> Type) where Source #

Catch `Exception`s in an extension of the `IO` monad.

Methods

catchIO :: Exception e => m a -> (e -> m a) -> m a Source #

#### Instances

Instances details

CatchIO IO Source # | Alias of `catch` for the IO monad.
Instance details Defined in Agda.Utils.IO Methods catchIO :: Exception e => IO a -> (e -> IO a) -> IO a Source #
CatchIO m => CatchIO (ExceptT e m) Source # | Upon exception, the error is lost.
Instance details Defined in Agda.Utils.IO Methods catchIO :: Exception e0 => ExceptT e m a -> (e0 -> ExceptT e m a) -> ExceptT e m a Source #
CatchIO m => CatchIO (StateT s m) Source # | Upon exception, the state is reset.
Instance details Defined in Agda.Utils.IO Methods catchIO :: Exception e => StateT s m a -> (e -> StateT s m a) -> StateT s m a Source #
CatchIO m => CatchIO (WriterT w m) Source # | Upon exception, the written output is lost.
Instance details Defined in Agda.Utils.IO Methods catchIO :: Exception e => WriterT w m a -> (e -> WriterT w m a) -> WriterT w m a Source #

showIOException :: Exception e => e -> String Source #

Print an `IOException` without the call stack.