0 | module Control.Monad.MErr
  1 |
  2 | import public Data.List.Quantifiers.Extra
  3 |
  4 | %default total
  5 |
  6 | ||| Generalized result of running a pure computation with
  7 | ||| error handling: Possible error values are wrapped in
  8 | ||| a heterogeneous sum.
  9 | public export
 10 | 0 Result : List Type -> Type -> Type
 11 | Result es a = Either (HSum es) a
 12 |
 13 | ||| A monad with error handling via a generalized bind
 14 | |||
 15 | ||| Possible errors are given as a `List Type` parameter, and a single
 16 | ||| error is wrapped in an `HSum`.
 17 | public export
 18 | interface MErr (0 m : List Type -> Type -> Type) where
 19 |   fail    : HSum es -> m es a
 20 |   succeed : a -> m es a
 21 |   attempt : m es a -> m fs (Result es a)
 22 |   bind    : m es a -> (a -> m es b) -> m es b
 23 |   mapImpl : (a -> b) -> m es a -> m es b
 24 |   appImpl : m es (a -> b) -> m es a -> m es b
 25 |
 26 | public export %inline
 27 | MErr m => Functor (m es) where
 28 |   map = mapImpl
 29 |
 30 | public export %inline
 31 | MErr m => Applicative (m es) where
 32 |   pure  = succeed
 33 |   (<*>) = appImpl
 34 |
 35 | public export %inline
 36 | MErr m => Monad (m es) where
 37 |   (>>=) = bind
 38 |
 39 | export %inline
 40 | fromResult : MErr m => Result es a -> m es a
 41 | fromResult = either fail succeed
 42 |
 43 | --------------------------------------------------------------------------------
 44 | -- Error handling
 45 | --------------------------------------------------------------------------------
 46 |
 47 | ||| Throws a single error by injecting it into the sum of possible errors.
 48 | export %inline
 49 | throw : MErr m => Has x es => x -> m es a
 50 | throw = fail . inject
 51 |
 52 | ||| Inject an `Either e a` computation into an `Async` monad dealing
 53 | ||| with several possible errors.
 54 | export
 55 | injectEither : MErr m => Has x es => Either x a -> m es a
 56 | injectEither (Left v)  = throw v
 57 | injectEither (Right v) = succeed v
 58 |
 59 | ||| Handle possible errors with the given function
 60 | export
 61 | handleErrors : MErr m => (HSum es -> m fs a) -> m es a -> m fs a
 62 | handleErrors f act = attempt act >>= either f pure
 63 |
 64 | ||| Tries to extract errors of a single type from a computation that
 65 | ||| can fail wrapping it in a `Left`. Other errors will be rethrown.
 66 | export
 67 | catch : MErr m => (0 e : Type) -> Has e es => m es a -> m es (Either e a)
 68 | catch e m =
 69 |   attempt m >>= \case
 70 |     Right v   => pure $ Right v
 71 |     Left errs => case project e errs of
 72 |       Nothing  => fail errs
 73 |       Just err => pure $ Left err
 74 |
 75 | ||| Tries to extract errors of a single type from a computation that
 76 | ||| can fail wrapping it in a `Left`. Other errors will be rethrown.
 77 | |||
 78 | ||| Unlike `catch`, this will decompose the list of possible errors,
 79 | ||| so errors can be handled one type at a time.
 80 | export
 81 | extractErr : MErr m => (0 e : Type) -> (p : Has e es) => m es a -> m (es - e) (Either e a)
 82 | extractErr e m =
 83 |   attempt {fs = es - e} m >>= \case
 84 |     Right v   => pure $ Right v
 85 |     Left errs => case decomp @{p} errs of
 86 |       Left x   => fail x
 87 |       Right x  => pure $ Left x
 88 |
 89 | export %inline
 90 | mapErrors : MErr m => (HSum es -> HSum fs) -> m es a -> m fs a
 91 | mapErrors f = handleErrors (fail . f)
 92 |
 93 | widen_ : All (`Elem` es) fs => HSum fs -> HSum es
 94 | widen_ @{_::_} (Here v)  = inject v
 95 | widen_ @{_::_} (There v) = widen_ v
 96 |
 97 | export %inline
 98 | widenErrors : MErr m => All (`Elem` es) fs => m fs a -> m es a
 99 | widenErrors = mapErrors widen_
100 |
101 | export %inline
102 | weakenErrors : MErr m => m [] a -> m fs a
103 | weakenErrors = handleErrors absurd
104 |
105 | export %inline
106 | dropErrs : MErr m => m es () -> m [] ()
107 | dropErrs = handleErrors (const $ succeed ())
108 |
109 | export %inline
110 | liftError : MErr m => m [e] a -> m fs (Either e a)
111 | liftError = handleErrors (pure . Left . project1) . map Right
112 |
113 | export %inline
114 | handle : MErr m => All (\e => e -> m [] a) es -> m es a -> m [] a
115 | handle hs = handleErrors (collapse' . hzipWith id hs)
116 |
117 | ||| Sequencing of computations plus error handling
118 | export %inline
119 | bindResult : MErr m => m es a -> (Result es a -> m fs b) -> m fs b
120 | bindResult act f = attempt act >>= f
121 |
122 | ||| Runs the given handler in case of an error but does not
123 | ||| catch the error in question.
124 | export %inline
125 | onError : MErr m => m es a -> (HSum es -> m [] ()) -> m es a
126 | onError act f = handleErrors (\x => weakenErrors (f x) >> fail x) act
127 |
128 | ||| Handles the given error by replacing it with the provided value.
129 | |||
130 | ||| All other errors will be unaffected.
131 | export
132 | ifError : MErr m => Has e es => Eq e => (err : e) -> Lazy a -> m es a -> m es a
133 | ifError err v =
134 |   handleErrors $ \x => case project e x of
135 |     Nothing => fail x
136 |     Just y  => if err == y then pure v else fail x
137 |