Control.Monad.MErr

Reexports

Definitions

0 Result : List Type -> Type -> Type

  Generalized result of running a pure computation with
  error handling: Possible error values are wrapped in
  a heterogeneous sum.

Totality: total
Visibility: public export

interface MErr : (List Type -> Type -> Type) -> Type

  A monad with error handling via a generalized bind
  
  Possible errors are given as a `List Type` parameter, and a single
  error is wrapped in an `HSum`.

Parameters: m
Methods:

fail : HSum es -> m es a

succeed : a -> m es a

attempt : m es a -> m fs (Result es a)

bind : m es a -> (a -> m es b) -> m es b

mapImpl : (a -> b) -> m es a -> m es b

appImpl : m es (a -> b) -> m es a -> m es b

Implementation: 

MCancel f -> MErr f

fail : MErr m => HSum es -> m es a

Totality: total
Visibility: public export

succeed : MErr m => a -> m es a

Totality: total
Visibility: public export

attempt : MErr m => m es a -> m fs (Result es a)

Totality: total
Visibility: public export

bind : MErr m => m es a -> (a -> m es b) -> m es b

Totality: total
Visibility: public export

mapImpl : MErr m => (a -> b) -> m es a -> m es b

Totality: total
Visibility: public export

appImpl : MErr m => m es (a -> b) -> m es a -> m es b

Totality: total
Visibility: public export

fromResult : MErr m => Result es a -> m es a

Totality: total
Visibility: export

throw : MErr m => Has x es => x -> m es a

  Throws a single error by injecting it into the sum of possible errors.

Totality: total
Visibility: export

injectEither : MErr m => Has x es => Either x a -> m es a

  Inject an `Either e a` computation into an `Async` monad dealing
  with several possible errors.

Totality: total
Visibility: export

handleErrors : MErr m => (HSum es -> m fs a) -> m es a -> m fs a

  Handle possible errors with the given function

Totality: total
Visibility: export

handleError : MErr m => (0 e : Type) -> Has e es => (e -> m es a) -> m es a -> m es a

  Handles an error of a single type by running it through
  the given effectful computation.

Totality: total
Visibility: export

catch : MErr m => (0 e : Type) -> Has e es => m es a -> m es (Either e a)

  Tries to extract errors of a single type from a computation that
  can fail wrapping it in a `Left`. Other errors will be rethrown.

Totality: total
Visibility: export

extractErr : MErr m => (0 e : Type) -> {auto p : Has e es} -> m es a -> m (es - e) (Either e a)

  Tries to extract errors of a single type from a computation that
  can fail wrapping it in a `Left`. Other errors will be rethrown.
  
  Unlike `catch`, this will decompose the list of possible errors,
  so errors can be handled one type at a time.

Totality: total
Visibility: export

mapErrors : MErr m => (HSum es -> HSum fs) -> m es a -> m fs a

Totality: total
Visibility: export

mapErr : MErr m => {auto h : Has e es} -> (e -> f) -> m es a -> m (Replaced es h f) a

Totality: total
Visibility: export

widenErrors : MErr m => All (\{arg:0} => Elem {arg:0} es) fs => m fs a -> m es a

Totality: total
Visibility: export

weakenErrors : MErr m => m [] a -> m fs a

Totality: total
Visibility: export

dropErrs : MErr m => m es () -> m [] ()

Totality: total
Visibility: export

liftError : MErr m => m [e] a -> m fs (Either e a)

Totality: total
Visibility: export

handle : MErr m => All (\e => e -> m [] a) es -> m es a -> m [] a

Totality: total
Visibility: export

bindResult : MErr m => m es a -> (Result es a -> m fs b) -> m fs b

  Sequencing of computations plus error handling

Totality: total
Visibility: export

onError : MErr m => m es a -> (HSum es -> m [] ()) -> m es a

  Runs the given handler in case of an error but does not
  catch the error in question.

Totality: total
Visibility: export

ifError : MErr m => Has e es => Eq e => e -> Lazy a -> m es a -> m es a

  Handles the given error by replacing it with the provided value.
  
  All other errors will be unaffected.

Totality: total
Visibility: export