Control.Effect.Fail

Definitions

data FailE : Type -> (Type -> Type) -> Type -> Type

Totality: total
Visibility: public export
Constructor: 

Fail : e -> FailE e m a

Hints:

Functor (\e => FailE e m a)

Inj (EitherE e) sig => Inj (FailE e) sig

fail : Inj (FailE e) sig => Algebra sig m => e -> m a

  Fail a computation.

Visibility: public export

fromEither : Inj (FailE e) sig => Algebra sig m => Either e b -> m b

Visibility: public export

glueFail : {0 m : Type -> Type} -> Inj (FailE e) sig => (e' -> e) -> (Inj (FailE e') sig => m a) -> m a

  Given a transformation between two failure types `e'` and `e`,
  run an effectful computation `act` in the context
  with the transformed failure.

Visibility: export