
  0 | module Control.Effect.Exception
  1 | 
  2 | import Data.Contravariant
  3 | 
  4 | import Control.EffectAlgebra
  5 | 
  6 | import public Control.Effect.Fail
  7 | 
  8 | import Control.Monad.Either
  9 | 
 10 | ||| Exception effect.
 11 | public export
 12 | data TryE : Type -> (Type -> Type) -> Type -> Type where
 13 |   Try : m a -> (e -> m a) -> TryE e m a
 14 | 
 15 | public export
 16 | Contravariant (\e => TryE e m r) where
 17 |   contramap f (Try x h) = Try x (h . f)
 18 | 
 19 | public export
 20 | EitherE : Type -> (Type -> Type) -> Type -> Type
 21 | EitherE e = TryE e :+: FailE e
 22 | 
 23 | public export
 24 | Inj (EitherE e) sig => Inj (FailE e) sig where
 25 |   inj = inj {sub = EitherE e, sup = sig} . Inr
 26 | 
 27 | public export
 28 | Inj (EitherE e) sig => Inj (TryE e) sig where
 29 |   inj = inj {sub = EitherE e, sup = sig} . Inl
 30 | 
 31 | ||| Try running a computation. If it fails (via Fail) resort to the supplied callback.
 32 | public export
 33 | try : Inj (TryE e) sig => Algebra sig m => m a -> (e -> m a) -> m a
 34 | try x err = send (Try x err)
 35 | 
 36 | namespace Algebra
 37 |   public export
 38 |   [Either] (al : Algebra sig m) => Algebra (EitherE e :+: sig) (EitherT e m) where
 39 |     alg ctx hdl (Inl (Inr (Fail x))) = left x
 40 |     alg ctx hdl (Inl (Inl (Try t er))) =
 41 |       catchE (hdl (t <$ ctx)) (hdl . (<$ ctx) . er)
 42 |     alg ctxx hdl (Inr other) =
 43 |       let fused = (~<~) {ctx2 = ctx} {m = EitherT e m} f hdl in
 44 |       MkEitherT (alg {f = Functor.Compose} {ctx = Either e . ctx} (Right ctxx) fused other)
 45 |      where
 46 |       f : forall a. Either e (EitherT e m a) -> m (Either e a)
 47 |       f (Left x) = pure (Left x)
 48 |       f (Right x) = runEitherT x
 49 | 
 50 |   %hint public export
 51 |   AlgebraEither : (al : Algebra sig m) => Algebra (EitherE e :+: sig) (EitherT e m)
 52 |   AlgebraEither = Algebra.Either
 53 |