git.iko.soy/Idris-dev
on 4e34dfd help sign in
Idris-dev/libs/base/Control/Monad/Reader.idr
55 lines 1.7 kB history raw
1module Control.Monad.Reader
3import Builtins
4import Control.Monad.Identity
5import Control.Monad.Trans
7%access public
9||| A monad representing a computation that runs in an immutable context
10class Monad m => MonadReader r (m : Type -> Type) where
11 ||| Return the context
12 ask : m r
13 ||| Temprorarily modify the input and run an action in the new context
14 local : (r -> r) -> m a -> m a
16||| The transformer on which the Reader monad is based
17record ReaderT : Type -> (Type -> Type) -> Type -> Type where
18 RD : {m : Type -> Type} ->
19 (runReaderT : r -> m a) -> ReaderT r m a
21||| Create a ReaderT with an empty context
22liftReaderT : {m : Type -> Type} -> m a -> ReaderT r m a
23liftReaderT m = RD $ const m
25instance Functor f => Functor (ReaderT r f) where
26 map f (RD g) = RD $ (map f) . g
28instance Applicative m => Applicative (ReaderT r m) where
29 pure = liftReaderT . pure
30 (RD f) <*> (RD v) = RD $ \r => f r <*> v r
32instance Alternative m => Alternative (ReaderT r m) where
33 empty = liftReaderT empty
34 (RD m) <|> (RD n) = RD $ \r => m r <|> n r
36instance Monad m => Monad (ReaderT r m) where
37 (RD f) >>= k = RD $ \r => do a <- f r
38 let RD ka = k a
39 ka r
41instance Monad m => MonadReader r (ReaderT r m) where
42 ask = RD return
43 local f (RD m) = RD $ m . f
45instance MonadTrans (ReaderT r) where
46 lift x = RD (const x)
48||| Evaluate a function in the context of a Reader monad
49asks : MonadReader r m => (r -> a) -> m a
50asks f = do r <- ask
51 return (f r)
53||| The reader monad. See MonadReader
54Reader : Type -> Type -> Type
55Reader r a = ReaderT r Identity a