0 | ||| Note: The difference to a 'strict' RWST implementation is
  1 | ||| that accumulation of values does not happen in the
  2 | ||| Applicative and Monad instances but when invoking `Writer`-specific
  3 | ||| functions like `writer` or `listen`.
  4 | module Control.Monad.RWS.CPS
  5 |
  6 | import Control.Monad.Identity
  7 | import Control.Monad.Trans
  8 |
  9 | %default total
 10 |
 11 | ||| A monad transformer extending an inner monad `m` with the ability to read
 12 | ||| an environment of type `r`, collect an output of type `w` and update a
 13 | ||| state of type `s`.
 14 | |||
 15 | ||| This is equivalent to `ReaderT r (WriterT w (StateT s m)) a`, but fuses the
 16 | ||| three layers.
 17 | public export
 18 | record RWST (r : Type) (w : Type) (s : Type) (m : Type -> Type) (a : Type) where
 19 |   constructor MkRWST
 20 |   unRWST : r -> s -> w -> m (a, s, w)
 21 |
 22 | ||| Unwrap an RWST computation as a function.
 23 | |||
 24 | ||| This is the inverse of `rwsT`.
 25 | public export %inline
 26 | runRWST : Monoid w => r -> s -> RWST r w s m a -> m (a, s, w)
 27 | runRWST r s m = unRWST m r s neutral
 28 |
 29 | ||| Construct an RWST computation from a function.
 30 | |||
 31 | ||| This is the inverse of `runRWST`.
 32 | public export %inline
 33 | rwsT : Semigroup w => Functor m => (r -> s -> m (a, s, w)) -> RWST r w s m a
 34 | rwsT f = MkRWST $ \r,s,w => (\(a,s',w') => (a,s',w <+> w')) <$> f r s
 35 |
 36 | ||| Evaluate a computation with the given initial state and environment,
 37 | ||| returning the final value and output, discarding the final state.
 38 | public export %inline
 39 | evalRWST : Monoid w => Functor m => r -> s -> RWST r w s m a -> m (a,w)
 40 | evalRWST r s m = (\(a,_,w) => (a,w)) <$> runRWST r s m
 41 |
 42 | ||| Evaluate a computation with the given initial state and environment,
 43 | ||| returning the final state and output, discarding the final value.
 44 | public export %inline
 45 | execRWST : Monoid w => Functor m => r -> s -> RWST r w s m a -> m (s,w)
 46 | execRWST r s m = (\(_,s',w) => (s',w)) <$> runRWST r s m
 47 |
 48 | ||| Map over the inner computation.
 49 | public export %inline
 50 | mapRWST : (Functor n, Monoid w, Semigroup w')
 51 |         => (m (a, s, w) -> n (b, s, w')) -> RWST r w s m a -> RWST r w' s n b
 52 | mapRWST f m = MkRWST $ \r,s,w =>
 53 |                 (\(a,s',w') => (a,s',w <+> w')) <$> f (runRWST r s m)
 54 |
 55 | ||| `withRWST f m` executes action `m` with an initial environment
 56 | ||| and state modified by applying `f`.
 57 | public export %inline
 58 | withRWST : (r' -> s -> (r, s)) -> RWST r w s m a -> RWST r' w s m a
 59 | withRWST f m = MkRWST $ \r,s => uncurry (unRWST m) (f r s)
 60 |
 61 | --------------------------------------------------------------------------------
 62 | --          RWS Functions
 63 | --------------------------------------------------------------------------------
 64 |
 65 | ||| A monad containing an environment of type `r`, output of type `w`
 66 | ||| and an updatable state of type `s`.
 67 | |||
 68 | ||| This is `RWST` applied to `Identity`.
 69 | public export
 70 | RWS : (r : Type) -> (w : Type) -> (s : Type) -> (a : Type) -> Type
 71 | RWS r w s = RWST r w s Identity
 72 |
 73 | ||| Unwrap an RWS computation as a function.
 74 | |||
 75 | ||| This is the inverse of `rws`.
 76 | public export %inline
 77 | runRWS : Monoid w => r -> s -> RWS r w s a -> (a, s, w)
 78 | runRWS r s = runIdentity . runRWST r s
 79 |
 80 | ||| Construct an RWS computation from a function.
 81 | |||
 82 | ||| This is the inverse of `runRWS`.
 83 | public export %inline
 84 | rws : Semigroup w => (r -> s -> (a, s, w)) -> RWS r w s a
 85 | rws f = MkRWST $ \r,s,w => let (a, s', w') = f r s
 86 |                            in Id (a, s', w <+> w')
 87 |
 88 | ||| Evaluate a computation with the given initial state and environment,
 89 | ||| returning the final value and output, discarding the final state.
 90 | public export %inline
 91 | evalRWS : Monoid w => r -> s -> RWS r w s a -> (a,w)
 92 | evalRWS r s m = let (a,_,w) = runRWS r s m
 93 |                  in (a,w)
 94 |
 95 | ||| Evaluate a computation with the given initial state and environment,
 96 | ||| returning the final state and output, discarding the final value.
 97 | public export %inline
 98 | execRWS : Monoid w => r -> s -> RWS r w s a -> (s,w)
 99 | execRWS r s m = let (_,s1,w) = runRWS r s m
100 |                  in (s1,w)
101 |
102 | ||| Map the return value, final state and output of a computation using
103 | ||| the given function.
104 | public export %inline
105 | mapRWS :  (Monoid w, Semigroup w')
106 |        => ((a, s, w) -> (b, s, w')) -> RWS r w s a -> RWS r w' s b
107 | mapRWS f = mapRWST $ \(Id p) => Id (f p)
108 |
109 | ||| `withRWS f m` executes action `m` with an initial environment
110 | ||| and state modified by applying `f`.
111 | public export %inline
112 | withRWS : (r' -> s -> (r, s)) -> RWS r w s a -> RWS r' w s a
113 | withRWS = withRWST
114 |
115 | --------------------------------------------------------------------------------
116 | --          Implementations
117 | --------------------------------------------------------------------------------
118 |
119 | public export %inline
120 | Functor m => Functor (RWST r w s m) where
121 |   map f m = MkRWST $ \r,s,w => (\(a,s',w') => (f a,s',w')) <$> unRWST m r s w
122 |
123 | public export %inline
124 | Monad m => Applicative (RWST r w s m) where
125 |   pure a = MkRWST $ \_,s,w => pure (a,s,w)
126 |   MkRWST mf <*> MkRWST mx =
127 |     MkRWST $ \r,s,w => do (f,s1,w1) <- mf r s w
128 |                           (a,s2,w2) <- mx r s1 w1
129 |                           pure (f a,s2,w2)
130 |
131 | public export %inline
132 | (Monad m, Alternative m) => Alternative (RWST r w s m) where
133 |   empty = MkRWST $ \_,_,_ => empty
134 |   MkRWST m <|> mn = MkRWST $ \r,s,w => m r s w <|> unRWST mn r s w
135 |
136 | public export %inline
137 | Monad m => Monad (RWST r w s m) where
138 |   m >>= k = MkRWST $ \r,s,w => do (a,s1,w1) <- unRWST m r s w
139 |                                   unRWST (k a) r s1 w1
140 |
141 | public export %inline
142 | MonadTrans (RWST r w s) where
143 |   lift m = MkRWST $ \_,s,w => map (\a => (a,s,w)) m
144 |
145 | public export %inline
146 | HasIO m => HasIO (RWST r w s m) where
147 |   liftIO = lift . liftIO
148 |