git.iko.soy/Idris-dev
on master help sign in
Merge pull request #571 from folone/topic/writer

RWST

commitc78d8d22bf5fe0d5a095d7d6a7899a13b7f546af authorEdwin Brady <edwin.brady@gmail.com> dateFri 1 Nov 2013, 05:26 (13 years ago) parent572db40a54b9fd
6 files changed+176−3
compare with master
unifiedsplit
lib/Control/Monad/RWS.idr+53 lib/Control/Monad/Reader.idr+47 lib/Control/Monad/State.idr+8−1 lib/Control/Monad/Writer.idr+55 lib/Prelude/Applicative.idr+9 lib/base.ipkg+4−2
lib/Control/Monad/RWS.idrnew file+53
@@ -0,0 +1,53 @@
1+module Control.Monad.RWS
2+
3+import Builtins
4+import Control.Monad.Identity
5+import Control.Monad.State
6+import Control.Monad.Writer
7+import Control.Monad.Reader
8+import Prelude.Monad
9+import Prelude.Functor
10+
11+%access public
12+
13+class (Monoid w, MonadReader r m, MonadWriter w m, MonadState s m) => MonadRWS r w s (m : Type -> Type) where {}
14+
15+record RWST : Type -> Type -> Type -> (Type -> Type) -> Type -> Type where
16+ MkRWST : {m : Type -> Type} ->
17+ (runRWST : r -> s -> m (a, s, w)) -> RWST r w s m a
18+
19+instance Monad m => Functor (RWST r w s m) where
20+ map f (MkRWST m) = MkRWST $ \r => \s => do (a, s', w) <- m r s
21+ return (f a, s', w)
22+
23+instance (Monoid w, Monad m) => Applicative (RWST r w s m) where
24+ pure a = MkRWST $ \_ => \s => return (a, s, neutral)
25+ (MkRWST f) <$> (MkRWST v) = MkRWST $ \r => \s => do (a, s', w) <- v r s
26+ (fn, ss, w') <- f r s
27+ return (fn a, ss, w <+> w)
28+
29+instance (Monoid w, Monad m) => Monad (RWST r w s m) where
30+ (MkRWST m) >>= k = MkRWST $ \r => \s => do (a, s', w) <- m r s
31+ let MkRWST ka = k a
32+ (b, ss, w') <- ka r s'
33+ return (b, ss, w <+> w')
34+
35+instance (Monoid w, Monad m) => MonadReader r (RWST r w s m) where
36+ ask = MkRWST $ \r => \s => return (r, s, neutral)
37+ local f (MkRWST m) = MkRWST $ \r => \s => m (f r) s
38+
39+instance (Monoid w, Monad m) => MonadWriter w (RWST r w s m) where
40+ tell w = MkRWST $ \_ => \s => return ((), s, w)
41+ listen (MkRWST m) = MkRWST $ \r => \s => do (a, s', w) <- m r s
42+ return ((a, w), s', w)
43+ pass (MkRWST m) = MkRWST $ \r => \s => do ((a, f), s', w) <- m r s
44+ return (a, s', f w)
45+
46+instance (Monoid w, Monad m) => MonadState s (RWST r w s m) where
47+ get = MkRWST $ \_ => \s => return (s, s, neutral)
48+ put s = MkRWST $ \_ => \_ => return ((), s, neutral)
49+
50+instance (Monoid w, Monad m) => MonadRWS r w s (RWST r w s m) where {}
51+
52+RWS : Type -> Type -> Type -> Type -> Type
53+RWS r w s a = RWST r w s Identity a
lib/Control/Monad/Reader.idrnew file+47
@@ -0,0 +1,47 @@
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+ local : (r -> r) -> m a -> m a
14+
15+record ReaderT : Type -> (Type -> Type) -> Type -> Type where
16+ RD : {m : Type -> Type} ->
17+ (runReaderT : r -> m a) -> ReaderT r m a
18+
19+liftReaderT : {m : Type -> Type} -> m a -> ReaderT r m a
20+liftReaderT m = RD $ const m
21+
22+instance Functor f => Functor (ReaderT r f) where
23+ map f (RD g) = RD $ (map f) . g
24+
25+instance Applicative m => Applicative (ReaderT r m) where
26+ pure = liftReaderT . pure
27+ (RD f) <$> (RD v) = RD $ \r => f r <$> v r
28+
29+instance Alternative m => Alternative (ReaderT r m) where
30+ empty = liftReaderT empty
31+ (RD m) <|> (RD n) = RD $ \r => m r <|> n r
32+
33+instance Monad m => Monad (ReaderT r m) where
34+ (RD f) >>= k = RD $ \r => do a <- f r
35+ let RD ka = k a
36+ ka r
37+
38+instance Monad m => MonadReader r (ReaderT r m) where
39+ ask = RD return
40+ local f (RD m) = RD $ m . f
41+
42+asks : MonadReader r m => (r -> a) -> m a
43+asks f = do r <- ask
44+ return (f r)
45+
46+Reader : Type -> Type -> Type
47+Reader r a = ReaderT r Identity a
lib/Control/Monad/State.idr+8−1
@@ -35,6 +35,13 @@ instance Monad m => MonadState s (StateT s m) where
3535 get = ST (\x => return (x, x))
3636 put x = ST (\y => return ((), x))
3737
38+modify : MonadState s m => (s -> s) -> m ()
39+modify f = do s <- get
40+ put (f s)
41+
42+gets : MonadState s m => (s -> a) -> m a
43+gets f = do s <- get
44+ return (f s)
45+
3846State : Type -> Type -> Type
3947State s a = StateT s Identity a
40−
lib/Control/Monad/Writer.idrnew file+55
@@ -0,0 +1,55 @@
1+module Control.Monad.Writer
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 (Monoid w, Monad m) => MonadWriter w (m : Type -> Type) where
12+ tell : w -> m ()
13+ listen : m a -> m (a, w)
14+ pass : m (a, w -> w) -> m a
15+
16+record WriterT : Type -> (Type -> Type) -> Type -> Type where
17+ WR : {m : Type -> Type} ->
18+ (runWriterT : m (a, w)) -> WriterT w m a
19+
20+instance Functor f => Functor (WriterT w f) where
21+ map f (WR g) = WR $ map (\w => (f . fst $ w, snd w)) g
22+
23+instance (Monoid w, Applicative m) => Applicative (WriterT w m) where
24+ pure a = WR $ pure (a, neutral)
25+ (WR f) <$> (WR v) = WR $ liftA2 merge f v where
26+ merge (fn, w) (a, w') = (fn a, w <+> w')
27+
28+instance (Monoid w, Alternative m) => Alternative (WriterT w m) where
29+ empty = WR empty
30+ (WR m) <|> (WR n) = WR $ m <|> n
31+
32+instance (Monoid w, Monad m) => Monad (WriterT w m) where
33+ (WR m) >>= k = WR $ do (a, w) <- m
34+ let WR ka = k a
35+ (b, w') <- ka
36+ return (b, w <+> w')
37+
38+instance (Monoid w, Monad m) => MonadWriter w (WriterT w m) where
39+ tell w = WR $ return ((), w)
40+ listen (WR m) = WR $ do (a, w) <- m
41+ return ((a, w), w)
42+ pass (WR m) = WR $ do ((a, f), w) <- m
43+ return (a, f w)
44+
45+listens : MonadWriter w m => (w -> b) -> m a -> m (a, b)
46+listens f m = listens' f (listen m) where
47+ listens' f' ma = do (a, w) <- ma
48+ return (a, f' w)
49+
50+censor : MonadWriter w m => (w -> w) -> m a -> m a
51+censor f m = pass $ do a <- m
52+ return (a, f)
53+
54+Writer : Type -> Type -> Type
55+Writer w a = WriterT w Identity a
lib/Prelude/Applicative.idr+9
@@ -19,6 +19,15 @@ infixl 2 $>
1919($>) : Applicative f => f a -> f b -> f b
2020a $> b = map (const id) a <$> b
2121
22+liftA : Applicative f => (a -> b) -> f a -> f b
23+liftA f a = pure f <$> a
24+
25+liftA2 : Applicative f => (a -> b -> c) -> f a -> f b -> f c
26+liftA2 f a b = (map f a) <$> b
27+
28+liftA3 : Applicative f => (a -> b -> c -> d) -> f a -> f b -> f c -> f d
29+liftA3 f a b c = (map f a) <$> b <$> c
30+
2231infixl 3 <|>
2332class Applicative f => Alternative (f : Type -> Type) where
2433 empty : f a
lib/base.ipkg+4−2
@@ -28,6 +28,8 @@ modules = Builtins, Prelude, IO, System,
2828 Data.SortedMap, Data.SortedSet, Data.BoundedList,
2929 Data.Vect, Data.HVect, Data.Vect.Quantifiers,
3030
31− Control.Monad.Identity, Control.Monad.State, Control.Category,
32− Control.Arrow,
31+ Control.Monad.Identity,
32+ Control.Monad.RWS,
33+ Control.Monad.State, Control.Monad.Writer, Control.Monad.Reader,
34+ Control.Category, Control.Arrow,
3335 Control.Catchable, Control.IOExcept