0 | module Control.Monad.Reader.Reader
 1 |
 2 | import Control.Monad.Identity
 3 | import Control.Monad.Trans
 4 |
 5 | %default total
 6 |
 7 | ||| A monad transformer extending an inner monad with access to an environment.
 8 | |||
 9 | ||| The environment is the same for all actions in a sequence, but may be
10 | ||| changed within scopes created by `Control.Monad.Reader.local`.
11 | public export
12 | record ReaderT (stateType : Type) (m : Type -> Type) (a : Type) where
13 |   constructor MkReaderT
14 |   1 runReaderT' : stateType -> m a
15 |
16 | ||| Transform the computation inside a @ReaderT@.
17 | public export %inline
18 | mapReaderT : (m a -> n b) -> ReaderT r m a -> ReaderT r n b
19 | mapReaderT f m = MkReaderT $ \st => f (runReaderT' m st)
20 |
21 | ||| Unwrap and apply a ReaderT monad computation
22 | public export
23 | %inline
24 | runReaderT : stateType -> ReaderT stateType m a -> m a
25 | runReaderT s action = runReaderT' action s
26 |
27 | --------------------------------------------------------------------------------
28 | --          Reader
29 | --------------------------------------------------------------------------------
30 |
31 | ||| A monad that can access an environment.
32 | |||
33 | ||| This is `ReaderT` applied to `Identity`.
34 | public export
35 | Reader : (stateType : Type) -> (a : Type) -> Type
36 | Reader s = ReaderT s Identity
37 |
38 | ||| Unwrap and apply a Reader monad computation
39 | public export %inline
40 | runReader : stateType -> Reader stateType a -> a
41 | runReader s = runIdentity . runReaderT s
42 |
43 | --------------------------------------------------------------------------------
44 | --          Implementations
45 | --------------------------------------------------------------------------------
46 |
47 | public export
48 | implementation Functor f => Functor (ReaderT stateType f) where
49 |   map f (MkReaderT g) = MkReaderT $ \st => f <$> g st
50 |
51 | public export
52 | implementation Applicative f => Applicative (ReaderT stateType f) where
53 |   pure x = MkReaderT $ \_ => pure x
54 |
55 |   MkReaderT f <*> MkReaderT a =
56 |     MkReaderT $ \st =>
57 |       let f' = f st in
58 |       let a' = a st in
59 |       f' <*> a'
60 |
61 | public export
62 | implementation Monad m => Monad (ReaderT stateType m) where
63 |   MkReaderT f >>= k =
64 |     MkReaderT $ \st => f st >>= runReaderT st . k
65 |
66 | public export
67 | implementation MonadTrans (ReaderT stateType) where
68 |   lift x = MkReaderT $ \_ => x
69 |
70 | public export
71 | implementation HasIO m => HasIO (ReaderT stateType m) where
72 |   liftIO f = MkReaderT $ \_ => liftIO f
73 |
74 | public export
75 | implementation Alternative f => Alternative (ReaderT stateType f) where
76 |   empty = MkReaderT $ const empty
77 |
78 |   MkReaderT f <|> mg = MkReaderT $ \st => f st <|> runReaderT' mg st
79 |