git.iko.soy/Idris-dev
on master help sign in
More functions for Reader and Writer.
commit9ca5cfa65f7acfc61286045f7a5a4506e06c821c authorGeorge Leontiev <folone@gmail.com> dateThu 31 Oct 2013, 10:16 (13 years ago) parentb92d2a9
2 files changed+20−4
compare with master
unifiedsplit
lib/Control/Monad/Reader.idr+6−2 lib/Control/Monad/Writer.idr+14−2
lib/Control/Monad/Reader.idr+6−2
@@ -9,7 +9,9 @@ import Prelude.Functor
99%access public
1010
1111class 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
1315
1416record ReaderT : Type -> (Type -> Type) -> Type -> Type where
1517 RD : {m : Type -> Type} ->
@@ -35,7 +37,9 @@ instance Monad m => Monad (ReaderT r m) where
3537 ka r
3638
3739instance Monad m => MonadReader r (ReaderT r m) where
38− ask = RD return
40+ ask = RD return
41+ local f (RD m) = RD $ m . f
42+ asks f = RD $ return . f
3943
4044Reader : Type -> Type -> Type
4145Reader r a = ReaderT r Identity a
lib/Control/Monad/Writer.idr+14−2
@@ -9,7 +9,11 @@ import Prelude.Functor
99%access public
1010
1111class (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
1317
1418record WriterT : Type -> (Type -> Type) -> Type -> Type where
1519 WR : {m : Type -> Type} ->
@@ -34,7 +38,15 @@ instance (Monoid w, Monad m) => Monad (WriterT w m) where
3438 return (b, w <+> w')
3539
3640instance (Monoid w, Monad m) => MonadWriter w (WriterT w m) where
37− tell w = WR $ return ((), w)
41+ tell w = WR $ return ((), w)
42+ listen (WR m) = WR $ do (a, w) <- m
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)
3850
3951
4052Writer : Type -> Type -> Type