git.iko.soy/Idris-dev
on master help sign in
Add ReaderT.
b92d2a9George Leontiev
lib/Control/Monad/Reader.idrnew file+41
compare with master
unifiedsplit
@@ -0,0 +1,41 @@
1+module Control.Monad.Reader
2+
3+import Builtins
4+import Control.Monad.Identity
5+import Prelude.Monad
6+import Prelude.Applicative
7+import Prelude.Functor
8+
9+%access public
10+
11+class Monad m => MonadReader r (m : Type -> Type) where
12+ ask : m r
13+
14+record ReaderT : Type -> (Type -> Type) -> Type -> Type where
15+ RD : {m : Type -> Type} ->
16+ (runReaderT : r -> m a) -> ReaderT r m a
17+
18+liftReaderT : {m : Type -> Type} -> m a -> ReaderT r m a
19+liftReaderT m = RD $ const m
20+
21+instance Functor f => Functor (ReaderT r f) where
22+ map f (RD g) = RD $ (map f) . g
23+
24+instance Applicative m => Applicative (ReaderT r m) where
25+ pure = liftReaderT . pure
26+ (RD f) <$> (RD v) = RD $ \r => f r <$> v r
27+
28+instance Alternative m => Alternative (ReaderT r m) where
29+ empty = liftReaderT empty
30+ (RD m) <|> (RD n) = RD $ \r => m r <|> n r
31+
32+instance Monad m => Monad (ReaderT r m) where
33+ (RD f) >>= k = RD $ \r => do a <- f r
34+ let RD ka = k a
35+ ka r
36+
37+instance Monad m => MonadReader r (ReaderT r m) where
38+ ask = RD return
39+
40+Reader : Type -> Type -> Type
41+Reader r a = ReaderT r Identity a
lib/base.ipkg+1−1
@@ -29,6 +29,6 @@ modules = Builtins, Prelude, IO, System,
29 Data.Vect, Data.HVect, Data.Vect.Quantifiers,
29 Data.Vect, Data.HVect, Data.Vect.Quantifiers,
30
30
31 Control.Monad.Identity, Control.Monad.State, Control.Category,
31 Control.Monad.Identity, Control.Monad.State, Control.Category,
32− Control.Monad.Writer,
32+ Control.Monad.Writer, Control.Monad.Reader,
33 Control.Arrow,
33 Control.Arrow,
34 Control.Catchable, Control.IOExcept
34 Control.Catchable, Control.IOExcept