0 | module Control.Monad.Reader.Interface
 1 |
 2 | import Control.Monad.Maybe
 3 | import Control.Monad.Error.Either
 4 | import Control.Monad.Reader.Reader
 5 | import Control.Monad.State.State
 6 | import Control.Monad.RWS.CPS
 7 | import Control.Monad.Trans
 8 | import Control.Monad.Writer.CPS
 9 |
10 | %default total
11 |
12 | ||| A computation which runs in a static context and produces an output
13 | public export
14 | interface Monad m => MonadReader stateType m | m where
15 |   ||| Get the context
16 |   ask : m stateType
17 |
18 |   ||| `local f c` runs the computation `c` in an environment modified by `f`.
19 |   local : (stateType -> stateType) -> m a -> m a
20 |
21 |
22 | ||| Evaluate a function in the context held by this computation
23 | public export
24 | asks : MonadReader stateType m => (stateType -> a) -> m a
25 | asks f = map f ask
26 |
27 | --------------------------------------------------------------------------------
28 | --          Implementations
29 | --------------------------------------------------------------------------------
30 |
31 | public export %inline
32 | Monad m => MonadReader stateType (ReaderT stateType m) where
33 |   ask = MkReaderT (\st => pure st)
34 |
35 |   local f (MkReaderT action) = MkReaderT (action . f)
36 |
37 | public export %inline
38 | Monad m => MonadReader r (RWST r w s m) where
39 |   ask       = MkRWST $ \r,s,w => pure (r,s,w)
40 |   local f m = MkRWST $ \r,s,w => unRWST m (f r) s w
41 |
42 | public export %inline
43 | MonadReader r m => MonadReader r (EitherT e m) where
44 |   ask = lift ask
45 |   local = mapEitherT . local
46 |
47 | public export %inline
48 | MonadReader r m => MonadReader r (MaybeT m) where
49 |   ask = lift ask
50 |   local = mapMaybeT . local
51 |
52 | public export %inline
53 | MonadReader r m => MonadReader r (StateT s m) where
54 |   ask = lift ask
55 |   local = mapStateT . local
56 |
57 | public export %inline
58 | MonadReader r m => MonadReader r (WriterT w m) where
59 |   ask   = lift ask
60 |
61 |   -- this differs from the implementation in the mtl package
62 |   -- which uses mapWriterT. However, it seems strange that
63 |   -- this should require a Monoid instance to further
64 |   -- accumulate values, while the implementation of
65 |   -- MonadReader for RWST does no such thing.
66 |   local f (MkWriterT m) = MkWriterT $ \w => local f (m w)
67 |