0 | module Control.RIO
  1 |
  2 | %default total
  3 |
  4 | ||| A stack-safe, effectful computation
  5 | ||| producing a value of type `a`, with
  6 | ||| the possibility of an error of type `x`.
  7 | |||
  8 | ||| We get flexible error handling by using an open union
  9 | ||| over a list of types for `x` (see `Control.RIO.App`),
 10 | ||| and we get flexible, mockable effects by providing the
 11 | ||| corresponding implementations (typically mere records)
 12 | ||| via the envirionment.
 13 | |||
 14 | ||| About the name: This stems originally from Haskell, where
 15 | ||| `RIO` is an abbreviation for `ReaderT IO`. In Idris, we need
 16 | ||| to add exceptions to the stack, which will not be handled
 17 | ||| automatically in `IO` itself. On the other hand, we can just
 18 | ||| use implicit arguments for our effects, so there is no
 19 | ||| need for an envirionment in the monad itself.
 20 | public export
 21 | data RIO : (x : Type) -> (a : Type) -> Type where
 22 |   Lift  : (run : PrimIO (Either x a)) -> RIO x a
 23 |   Chain : RIO x1 a -> (Either x1 a -> RIO x2 b) -> RIO x2 b
 24 |
 25 | -- Computation stack for evaluating `RIO` actions.
 26 | data Stack : (x1,x2,a,b : Type) -> Type where
 27 |   Nil  : Stack x x a a
 28 |   (::) : (Either x1 a -> RIO y v) -> Stack y  x2 v b -> Stack x1 x2 a b
 29 |
 30 | ||| Tail-recursively evaluate a `RIO` computation.
 31 | export
 32 | eval : RIO x a -> IO (Either x a)
 33 | eval app = fromPrim $ go app []
 34 |
 35 |   where
 36 |     go : RIO x1 v -> Stack x1 x2 v w -> PrimIO (Either x2 w)
 37 |     go (Chain z f) st       w = go z (f :: st) w
 38 |     go (Lift run) []        w = run w
 39 |     go (Lift run) (f :: fs) w =
 40 |       let MkIORes ei w2 = run w
 41 |        in assert_total $ go (f ei) fs w2
 42 |
 43 | ||| Tail-recursively evaluate a `RIO` computation,
 44 | ||| which cannot fail with an exception.
 45 | export
 46 | run : Uninhabited x => RIO x a -> IO a
 47 | run app = either absurd id <$> eval app
 48 |
 49 | ||| Wrap an `Either x a` in a `RIO` computation.
 50 | export
 51 | liftEither : Either x a -> RIO x a
 52 | liftEither v = Lift $ \w => MkIORes v w
 53 |
 54 | ||| Wrap an `IO (Either x a)` in a `RIO` computation.
 55 | export
 56 | liftEitherIO : IO (Either x a) -> RIO x a
 57 | liftEitherIO io = Lift $ toPrim io
 58 |
 59 | ||| Map a function over the result over a `RIO` computation.
 60 | export
 61 | mapApp : (Either x a -> Either y b) -> RIO x a -> RIO y b
 62 | mapApp f app = Chain app (liftEither . f)
 63 |
 64 | ||| Fail with an error.
 65 | export
 66 | fail : x -> RIO x a
 67 | fail err = liftEither (Left err)
 68 |
 69 | %inline
 70 | bindApp : RIO x a -> (a -> RIO x b) -> RIO x b
 71 | bindApp app f = Chain app (either fail f)
 72 |
 73 | export
 74 | Functor (RIO x) where
 75 |   map = mapApp . map
 76 |
 77 | export
 78 | Bifunctor RIO where
 79 |   bimap f g = mapApp (bimap f g)
 80 |
 81 | export
 82 | Applicative (RIO x) where
 83 |   pure v    = liftEither (Right v)
 84 |   af <*> aa = bindApp af (\f => map f aa)
 85 |
 86 | export
 87 | Monad (RIO x) where
 88 |   (>>=) = bindApp
 89 |
 90 | export
 91 | HasIO (RIO x) where
 92 |   liftIO io = Lift $ toPrim (map Right io)
 93 |
 94 | ||| Catch an exception with the given handler.
 95 | export
 96 | catch : (x -> RIO y a) -> RIO x a -> RIO y a
 97 | catch f app = Chain app (either f pure)
 98 |
 99 | ||| Makes sure the given (cleanup) action is run at the end
100 | ||| of a computation even in case of an error.
101 | export
102 | finally : RIO x () -> RIO x a -> RIO x a
103 | finally cleanup app =
104 |   Chain app (either (\e => cleanup >> fail e) (\v => cleanup $> v))
105 |
106 | export
107 | lift : Uninhabited x => RIO x a -> RIO y a
108 | lift io = catch (\v => absurd v) io
109 |