
  0 | module Control.Effect.Fail
  1 | 
  2 | import Control.EffectAlgebra
  3 | import Control.Monad.Maybe
  4 | import Control.Monad.Either
  5 | 
  6 | public export
  7 | data FailE : Type -> (Type -> Type) -> (Type -> Type) where
  8 |   Fail : e -> FailE e m a
  9 | 
 10 | export
 11 | Functor (\e => FailE e m a) where
 12 |   map f (Fail x) = Fail (f x)
 13 | 
 14 | ||| Fail a computation.
 15 | public export
 16 | fail : Inj (FailE e) sig => Algebra sig m => e -> m a
 17 | fail x = send (Fail x)
 18 | 
 19 | public export
 20 | fromEither : Inj (FailE e) sig => Algebra sig m => Either e b -> m b
 21 | fromEither (Left err) = fail err
 22 | fromEither (Right x) = pure x
 23 | 
 24 | ||| Given a transformation between two failure types `e'` and `e`,
 25 | ||| run an effectful computation `act` in the context
 26 | ||| with the transformed failure.
 27 | export
 28 | glueFail : {0 m : Type -> Type}
 29 |         -> {0 e : Type}
 30 |         -> (fail : Inj (FailE e) sig)
 31 |         => (e' -> e)
 32 |         -> ((err : Inj (FailE e') sig) => m a)
 33 |         -> m a
 34 | glueFail morph act = act @{f}
 35 |  where
 36 |   f : Inj (FailE e') sig
 37 |   f = MkInj $ \case Fail x => inj (Fail (morph x))
 38 | 
 39 | namespace Algebra
 40 |   public export
 41 |   [Maybe] Algebra sig m => Algebra (FailE e :+: sig) (MaybeT m) where
 42 |     alg ctx hdl (Inl (Fail x)) = nothing
 43 |     alg ctxx hdl (Inr other) =
 44 |       let fused = (~<~) {ctx2 = ctx} {m = MaybeT m} f hdl in
 45 |       MkMaybeT (alg {f = Functor.Compose} {ctx = Maybe . ctx} (Just ctxx) fused other)
 46 |      where
 47 |       f : forall a. Maybe (MaybeT m a) -> m (Maybe a)
 48 |       f Nothing = pure Nothing
 49 |       f (Just x) = runMaybeT x
 50 | 
 51 |   public export
 52 |   [Either] Algebra sig m => Algebra (FailE e :+: sig) (EitherT e m) where
 53 |     alg ctx hdl (Inl (Fail x)) = left x
 54 |     alg ctxx hdl (Inr other) =
 55 |       let fused = (~<~) {ctx2 = ctx} {m = EitherT e m} f hdl in
 56 |       MkEitherT (alg {f = Functor.Compose} {ctx = Either e . ctx} (Right ctxx) fused other)
 57 |      where
 58 |       f : forall a. Either e (EitherT e m a) -> m (Either e a)
 59 |       f (Left x) = pure (Left x)
 60 |       f (Right x) = runEitherT x
 61 |