Control.Eff.Internal

Reexports

Definitions

Eff : List (Type -> Type) -> Type -> Type

  An effectful computation yielding a value
  of type `t` and supporting the effects listed
  in `fs`.

Totality: total
Visibility: public export

send : Has f fs => f t -> Eff fs t

  Lift a an effectful comutation into the `Eff` monad.

Totality: total
Visibility: export

toFree : Eff fs t -> Handler fs m -> Free m t

  Handle all effectful computations in `m`,
  returning the underlying free monad.

Totality: total
Visibility: export

runEff : MonadRec m => Eff fs t -> Handler fs m -> m t

  Run an effectful computation without overflowing
  the stack by handling all computations in monad `m`.

Totality: total
Visibility: export

extract : Eff [] a -> a

  Extract the (pure) result of an effectful computation
  where all effects have been handled.

Totality: total
Visibility: export

handleRelay : {auto prf : Has f fs} -> (a -> Eff (fs - f) b) -> (f v -> (v -> Eff (fs - f) b) -> Eff (fs - f) b) -> Eff fs a -> Eff (fs - f) b

Totality: total
Visibility: export

handle : {auto prf : Has f fs} -> (f v -> (v -> Eff (fs - f) b) -> Eff (fs - f) b) -> Eff fs b -> Eff (fs - f) b

Totality: total
Visibility: export

handleRelayS : {auto prf : Has f fs} -> s -> (s -> a -> Eff (fs - f) b) -> (s -> f v -> (s -> v -> Eff (fs - f) b) -> Eff (fs - f) b) -> Eff fs a -> Eff (fs - f) b

Totality: total
Visibility: export

lift : Subset fs fs' => Eff fs a -> Eff fs' a

  Turn effect monad into a more relaxed one. Can be used to reorder effects as well. See src/Test/Ordering.idr for usage.

Totality: total
Visibility: export