Control.RIO

Definitions

data RIO : Type -> Type -> Type

  A stack-safe, effectful computation
  producing a value of type `a`, with
  the possibility of an error of type `x`.
  
  We get flexible error handling by using an open union
  over a list of types for `x` (see `Control.RIO.App`),
  and we get flexible, mockable effects by providing the
  corresponding implementations (typically mere records)
  via the envirionment.
  
  About the name: This stems originally from Haskell, where
  `RIO` is an abbreviation for `ReaderT IO`. In Idris, we need
  to add exceptions to the stack, which will not be handled
  automatically in `IO` itself. On the other hand, we can just
  use implicit arguments for our effects, so there is no
  need for an envirionment in the monad itself.

Totality: total
Visibility: public export
Constructors:

Lift : PrimIO (Either x a) -> RIO x a

Chain : RIO x1 a -> (Either x1 a -> RIO x2 b) -> RIO x2 b

Hints:

Applicative (RIO x)

Bifunctor RIO

Functor (RIO x)

HasIO (RIO x)

Monad (RIO x)

eval : RIO x a -> IO (Either x a)

  Tail-recursively evaluate a `RIO` computation.

Totality: total
Visibility: export

run : Uninhabited x => RIO x a -> IO a

  Tail-recursively evaluate a `RIO` computation,
  which cannot fail with an exception.

Totality: total
Visibility: export

liftEither : Either x a -> RIO x a

  Wrap an `Either x a` in a `RIO` computation.

Totality: total
Visibility: export

liftEitherIO : IO (Either x a) -> RIO x a

  Wrap an `IO (Either x a)` in a `RIO` computation.

Totality: total
Visibility: export

mapApp : (Either x a -> Either y b) -> RIO x a -> RIO y b

  Map a function over the result over a `RIO` computation.

Totality: total
Visibility: export

fail : x -> RIO x a

  Fail with an error.

Totality: total
Visibility: export

catch : (x -> RIO y a) -> RIO x a -> RIO y a

  Catch an exception with the given handler.

Totality: total
Visibility: export

finally : RIO x () -> RIO x a -> RIO x a

  Makes sure the given (cleanup) action is run at the end
  of a computation even in case of an error.

Totality: total
Visibility: export

lift : Uninhabited x => RIO x a -> RIO y a

Totality: total
Visibility: export