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 | export %inline
 94 | mapErr : MErr m => (h : Has e es) => (e -> f) -> m es a -> m (Replaced es h f) a
 95 | mapErr fun = mapErrors (update fun)
 96 |
 97 | widen_ : All (`Elem` es) fs => HSum fs -> HSum es
 98 | widen_ @{_::_} (Here v)  = inject v
 99 | widen_ @{_::_} (There v) = widen_ v
100 |
101 | export %inline
102 | widenErrors : MErr m => All (`Elem` es) fs => m fs a -> m es a
103 | widenErrors = mapErrors widen_
104 |
105 | export %inline
106 | weakenErrors : MErr m => m [] a -> m fs a
107 | weakenErrors = handleErrors absurd
108 |
109 | export %inline
110 | dropErrs : MErr m => m es () -> m [] ()
111 | dropErrs = handleErrors (const $ succeed ())
112 |
113 | export %inline
114 | liftError : MErr m => m [e] a -> m fs (Either e a)
115 | liftError = handleErrors (pure . Left . project1) . map Right
116 |
117 | export %inline
118 | handle : MErr m => All (\e => e -> m [] a) es -> m es a -> m [] a
119 | handle hs = handleErrors (collapse' . hzipWith id hs)
120 |
121 | ||| Sequencing of computations plus error handling
122 | export %inline
123 | bindResult : MErr m => m es a -> (Result es a -> m fs b) -> m fs b
124 | bindResult act f = attempt act >>= f
125 |
126 | ||| Runs the given handler in case of an error but does not
127 | ||| catch the error in question.
128 | export %inline
129 | onError : MErr m => m es a -> (HSum es -> m [] ()) -> m es a
130 | onError act f = handleErrors (\x => weakenErrors (f x) >> fail x) act
131 |
132 | ||| Handles the given error by replacing it with the provided value.
133 | |||
134 | ||| All other errors will be unaffected.
135 | export
136 | ifError : MErr m => Has e es => Eq e => (err : e) -> Lazy a -> m es a -> m es a
137 | ifError err v =
138 |   handleErrors $ \x => case project e x of
139 |     Nothing => fail x
140 |     Just y  => if err == y then pure v else fail x
141 |