git.iko.soy/Idris-dev
on master help sign in
More functions for Reader and Writer.
9ca5cfaGeorge Leontiev
lib/Control/Monad/Reader.idr+6−2
compare with master
unifiedsplit
@@ -9,7 +9,9 @@ import Prelude.Functor
9%access public
9%access public
10
10
11class Monad m => MonadReader r (m : Type -> Type) where
11class Monad m => MonadReader r (m : Type -> Type) where
12− ask : m r
12+ ask : m r
13+ local : (r -> r) -> m a -> m a
14+ asks : (r -> a) -> m a
13
15
14record ReaderT : Type -> (Type -> Type) -> Type -> Type where
16record ReaderT : Type -> (Type -> Type) -> Type -> Type where
15 RD : {m : Type -> Type} ->
17 RD : {m : Type -> Type} ->
@@ -35,7 +37,9 @@ instance Monad m => Monad (ReaderT r m) where
35 ka r
37 ka r
36
38
37instance Monad m => MonadReader r (ReaderT r m) where
39instance Monad m => MonadReader r (ReaderT r m) where
40+ ask = RD return
41+ local f (RD m) = RD $ m . f
38− ask = RD return
42+ asks f = RD $ return . f
39
43
40Reader : Type -> Type -> Type
44Reader : Type -> Type -> Type
41Reader r a = ReaderT r Identity a
45Reader r a = ReaderT r Identity a
lib/Control/Monad/Writer.idr+14−2
@@ -9,7 +9,11 @@ import Prelude.Functor
9%access public
9%access public
10
10
11class (Monoid w, Monad m) => MonadWriter w (m : Type -> Type) where
11class (Monoid w, Monad m) => MonadWriter w (m : Type -> Type) where
12− tell : w -> m ()
12+ tell : w -> m ()
13+ listen : m a -> m (a, w)
14+ listens : (w -> b) -> m a -> m (a, b)
15+ pass : m (a, w -> w) -> m a
16+ censor : (w -> w) -> m a -> m a
13
17
14record WriterT : Type -> (Type -> Type) -> Type -> Type where
18record WriterT : Type -> (Type -> Type) -> Type -> Type where
15 WR : {m : Type -> Type} ->
19 WR : {m : Type -> Type} ->
@@ -34,7 +38,15 @@ instance (Monoid w, Monad m) => Monad (WriterT w m) where
34 return (b, w <+> w')
38 return (b, w <+> w')
35
39
36instance (Monoid w, Monad m) => MonadWriter w (WriterT w m) where
40instance (Monoid w, Monad m) => MonadWriter w (WriterT w m) where
41+ tell w = WR $ return ((), w)
42+ listen (WR m) = WR $ do (a, w) <- m
37− tell w = WR $ return ((), w)
43+ return ((a, w), w)
44+ listens f (WR m) = WR $ do (a, w) <- m
45+ return ((a, f w), w)
46+ pass (WR m) = WR $ do ((a, f), w) <- m
47+ return (a, f w)
48+ censor f (WR m) = WR $ do (a, w) <- m
49+ return (a, f w)
38
50
39
51
40Writer : Type -> Type -> Type
52Writer : Type -> Type -> Type