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 | parameters {auto merr : MErr m}
 48 |
 49 |   ||| Throws a single error by injecting it into the sum of possible errors.
 50 |   export %inline
 51 |   throw : Has x es => x -> m es a
 52 |   throw = fail . inject
 53 |
 54 |   ||| Inject an `Either e a` computation into an `Async` monad dealing
 55 |   ||| with several possible errors.
 56 |   export
 57 |   injectEither : Has x es => Either x a -> m es a
 58 |   injectEither (Left v)  = throw v
 59 |   injectEither (Right v) = succeed v
 60 |
 61 |   ||| Handle possible errors with the given function
 62 |   export
 63 |   handleErrors : (HSum es -> m fs a) -> m es a -> m fs a
 64 |   handleErrors f act = attempt act >>= either f pure
 65 |
 66 |   ||| Handles an error of a single type by running it through
 67 |   ||| the given effectful computation.
 68 |   export
 69 |   handleError : (0 e : Type) -> Has e es => (e -> m es a) -> m es a -> m es a
 70 |   handleError e f =
 71 |     handleErrors $ \x => case project e x of
 72 |       Nothing => fail x
 73 |       Just v  => f v
 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 |   export
 78 |   catch : (0 e : Type) -> Has e es => m es a -> m es (Either e a)
 79 |   catch e m =
 80 |     attempt m >>= \case
 81 |       Right v   => pure $ Right v
 82 |       Left errs => case project e errs of
 83 |         Nothing  => fail errs
 84 |         Just err => pure $ Left err
 85 |
 86 |   ||| Tries to extract errors of a single type from a computation that
 87 |   ||| can fail wrapping it in a `Left`. Other errors will be rethrown.
 88 |   |||
 89 |   ||| Unlike `catch`, this will decompose the list of possible errors,
 90 |   ||| so errors can be handled one type at a time.
 91 |   export
 92 |   extractErr : (0 e : Type) -> (p : Has e es) => m es a -> m (es - e) (Either e a)
 93 |   extractErr e m =
 94 |     attempt {fs = es - e} m >>= \case
 95 |       Right v   => pure $ Right v
 96 |       Left errs => case decomp @{p} errs of
 97 |         Left x   => fail x
 98 |         Right x  => pure $ Left x
 99 |
100 |   export %inline
101 |   mapErrors : (HSum es -> HSum fs) -> m es a -> m fs a
102 |   mapErrors f = handleErrors (fail . f)
103 |
104 |   export %inline
105 |   mapErr : (h : Has e es) => (e -> f) -> m es a -> m (Replaced es h f) a
106 |   mapErr fun = mapErrors (update fun)
107 |
108 |   widen_ : All (`Elem` es) fs => HSum fs -> HSum es
109 |   widen_ @{_::_} (Here v)  = inject v
110 |   widen_ @{_::_} (There v) = widen_ v
111 |
112 |   export %inline
113 |   widenErrors : All (`Elem` es) fs => m fs a -> m es a
114 |   widenErrors = mapErrors widen_
115 |
116 |   export %inline
117 |   weakenErrors : m [] a -> m fs a
118 |   weakenErrors = handleErrors absurd
119 |
120 |   export %inline
121 |   dropErrs : m es () -> m [] ()
122 |   dropErrs = handleErrors (const $ succeed ())
123 |
124 |   export %inline
125 |   liftError : m [e] a -> m fs (Either e a)
126 |   liftError = handleErrors (pure . Left . project1) . map Right
127 |
128 |   export %inline
129 |   handle : All (\e => e -> m [] a) es -> m es a -> m [] a
130 |   handle hs = handleErrors (collapse' . hzipWith id hs)
131 |
132 |   ||| Sequencing of computations plus error handling
133 |   export %inline
134 |   bindResult : m es a -> (Result es a -> m fs b) -> m fs b
135 |   bindResult act f = attempt act >>= f
136 |
137 |   ||| Runs the given handler in case of an error but does not
138 |   ||| catch the error in question.
139 |   export %inline
140 |   onError : m es a -> (HSum es -> m [] ()) -> m es a
141 |   onError act f = handleErrors (\x => weakenErrors (f x) >> fail x) act
142 |
143 |   ||| Handles the given error by replacing it with the provided value.
144 |   |||
145 |   ||| All other errors will be unaffected.
146 |   export
147 |   ifError : Has e es => Eq e => (err : e) -> Lazy a -> m es a -> m es a
148 |   ifError err v =
149 |     handleErrors $ \x => case project e x of
150 |       Nothing => fail x
151 |       Just y  => if err == y then pure v else fail x
152 |