Control.RIO.App

Reexports

Definitions

0 App : List Type -> Type -> Type

  A `RIO` computation, which can fail with one of several errors.

Totality: total
Visibility: public export

throw : Has x xs => x -> App xs a

  Throw an exception to be caught in the `App` monad.
  
  The error type has to be in the list of accepted errors.

Totality: total
Visibility: export

injectRIO : Has x xs => RIO x a -> App xs a

  Inject a `RIO` computation into one dealing with several
  possible errors.

Totality: total
Visibility: export

injectEither : Has x xs => Either x a -> App xs a

  Inject an `Either x a` computation into a `RIO` monad dealing
  with several possible errors.

Totality: total
Visibility: export

injectIO : Has x xs => IO (Either x a) -> App xs a

  Inject an `IO (Either x a)` computation into a `RIO` monad dealing
  with several possible errors.

Totality: total
Visibility: export

0 Handler : Type -> Type -> Type

  An error handler.

Totality: total
Visibility: public export

handle : {auto prf : Has x xs} -> Handler a x -> App xs a -> App (xs - x) a

  Handle a single error type in an application.
  
  This removes the error type from the list of possible errors
  in the resulting `App` type.

Totality: total
Visibility: export

handleAll : All (Handler a) xs => App xs a -> RIO Void a

  Handle all errors, converting the computation to one that cannot fail.

Totality: total
Visibility: export

handleAllDflt : All (Handler ()) xs => a -> App xs a -> RIO Void a

  Handle all errors, converting the computation to one that cannot fail.
  
  This yields the provided default value in case of an error.

Totality: total
Visibility: export

runApp : All (Handler ()) xs -> App xs () -> IO ()

  Run an application handling all errors. This can be invoked
  directly from  an applcation's `main` function. It invokes
  `exitFailure` in case of an error.

Totality: total
Visibility: export