git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1485 from gavlegoat/master
f2f050aEdwin Brady
libs/base/Control/Monad/RWS.idr+3
compare with master
unifiedsplit
@@ -7,8 +7,10 @@ import Control.Monad.Reader
7
7
8%access public
8%access public
9
9
10+||| A combination of the Reader, Writer, and State monads
10class (Monoid w, MonadReader r m, MonadWriter w m, MonadState s m) => MonadRWS r w s (m : Type -> Type) where {}
11class (Monoid w, MonadReader r m, MonadWriter w m, MonadState s m) => MonadRWS r w s (m : Type -> Type) where {}
11
12
13+||| The transformer on which the RWS monad is based
12record RWST : Type -> Type -> Type -> (Type -> Type) -> Type -> Type where
14record RWST : Type -> Type -> Type -> (Type -> Type) -> Type -> Type where
13 MkRWST : {m : Type -> Type} ->
15 MkRWST : {m : Type -> Type} ->
14 (runRWST : r -> s -> m (a, s, w)) -> RWST r w s m a
16 (runRWST : r -> s -> m (a, s, w)) -> RWST r w s m a
@@ -46,5 +48,6 @@ instance (Monoid w, Monad m) => MonadState s (RWST r w s m) where
46
48
47instance (Monoid w, Monad m) => MonadRWS r w s (RWST r w s m) where {}
49instance (Monoid w, Monad m) => MonadRWS r w s (RWST r w s m) where {}
48
50
51+||| The RWS monad. See the MonadRWS class
49RWS : Type -> Type -> Type -> Type -> Type
52RWS : Type -> Type -> Type -> Type -> Type
50RWS r w s a = RWST r w s Identity a
53RWS r w s a = RWST r w s Identity a
libs/base/Control/Monad/Reader.idr+7
@@ -5,14 +5,19 @@ import Control.Monad.Identity
5
5
6%access public
6%access public
7
7
8+||| A monad representing a computation that runs in an immutable context
8class Monad m => MonadReader r (m : Type -> Type) where
9class Monad m => MonadReader r (m : Type -> Type) where
10+ ||| Return the context
9 ask : m r
11 ask : m r
12+ ||| Temprorarily modify the input and run an action in the new context
10 local : (r -> r) -> m a -> m a
13 local : (r -> r) -> m a -> m a
11
14
15+||| The transformer on which the Reader monad is based
12record ReaderT : Type -> (Type -> Type) -> Type -> Type where
16record ReaderT : Type -> (Type -> Type) -> Type -> Type where
13 RD : {m : Type -> Type} ->
17 RD : {m : Type -> Type} ->
14 (runReaderT : r -> m a) -> ReaderT r m a
18 (runReaderT : r -> m a) -> ReaderT r m a
15
19
20+||| Create a ReaderT with an empty context
16liftReaderT : {m : Type -> Type} -> m a -> ReaderT r m a
21liftReaderT : {m : Type -> Type} -> m a -> ReaderT r m a
17liftReaderT m = RD $ const m
22liftReaderT m = RD $ const m
18
23
@@ -36,9 +41,11 @@ instance Monad m => MonadReader r (ReaderT r m) where
36 ask = RD return
41 ask = RD return
37 local f (RD m) = RD $ m . f
42 local f (RD m) = RD $ m . f
38
43
44+||| Evaluate a function in the context of a Reader monad
39asks : MonadReader r m => (r -> a) -> m a
45asks : MonadReader r m => (r -> a) -> m a
40asks f = do r <- ask
46asks f = do r <- ask
41 return (f r)
47 return (f r)
42
48
49+||| The reader monad. See MonadReader
43Reader : Type -> Type -> Type
50Reader : Type -> Type -> Type
44Reader r a = ReaderT r Identity a
51Reader r a = ReaderT r Identity a
libs/base/Control/Monad/State.idr+7
@@ -4,10 +4,14 @@ import Control.Monad.Identity
4
4
5%access public
5%access public
6
6
7+||| A computation which runs in a context and produces an output
7class Monad m => MonadState s (m : Type -> Type) where
8class Monad m => MonadState s (m : Type -> Type) where
9+ ||| Get the context
8 get : m s
10 get : m s
11+ ||| Write a new context/output
9 put : s -> m ()
12 put : s -> m ()
10
13
14+||| The transformer on which the State monad is based
11record StateT : Type -> (Type -> Type) -> Type -> Type where
15record StateT : Type -> (Type -> Type) -> Type -> Type where
12 ST : {m : Type -> Type} ->
16 ST : {m : Type -> Type} ->
13 (runStateT : s -> m (a, s)) -> StateT s m a
17 (runStateT : s -> m (a, s)) -> StateT s m a
@@ -33,13 +37,16 @@ instance Monad m => MonadState s (StateT s m) where
33 get = ST (\x => return (x, x))
37 get = ST (\x => return (x, x))
34 put x = ST (\y => return ((), x))
38 put x = ST (\y => return ((), x))
35
39
40+||| Apply a function to modify the context of this computation
36modify : MonadState s m => (s -> s) -> m ()
41modify : MonadState s m => (s -> s) -> m ()
37modify f = do s <- get
42modify f = do s <- get
38 put (f s)
43 put (f s)
39
44
45+||| Evaluate a function in the context held by this computation
40gets : MonadState s m => (s -> a) -> m a
46gets : MonadState s m => (s -> a) -> m a
41gets f = do s <- get
47gets f = do s <- get
42 return (f s)
48 return (f s)
43
49
50+||| The State monad. See the MonadState class
44State : Type -> Type -> Type
51State : Type -> Type -> Type
45State s a = StateT s Identity a
52State s a = StateT s Identity a
libs/base/Control/Monad/Writer.idr+8
@@ -5,11 +5,16 @@ import Control.Monad.Identity
5
5
6%access public
6%access public
7
7
8+||| A monad representing a computation that produces a stream of output
8class (Monoid w, Monad m) => MonadWriter w (m : Type -> Type) where
9class (Monoid w, Monad m) => MonadWriter w (m : Type -> Type) where
10+ ||| tell w produces the output w
9 tell : w -> m ()
11 tell : w -> m ()
12+ ||| Execute an action and add it's output to the value of the computation
10 listen : m a -> m (a, w)
13 listen : m a -> m (a, w)
14+ ||| Execute an action and apply the returned function to the output
11 pass : m (a, w -> w) -> m a
15 pass : m (a, w -> w) -> m a
12
16
17+||| The transformer base of the Writer monad
13record WriterT : Type -> (Type -> Type) -> Type -> Type where
18record WriterT : Type -> (Type -> Type) -> Type -> Type where
14 WR : {m : Type -> Type} ->
19 WR : {m : Type -> Type} ->
15 (runWriterT : m (a, w)) -> WriterT w m a
20 (runWriterT : m (a, w)) -> WriterT w m a
@@ -39,14 +44,17 @@ instance (Monoid w, Monad m) => MonadWriter w (WriterT w m) where
39 pass (WR m) = WR $ do ((a, f), w) <- m
44 pass (WR m) = WR $ do ((a, f), w) <- m
40 return (a, f w)
45 return (a, f w)
41
46
47+||| Run an action in the Writer monad and transform the written output
42listens : MonadWriter w m => (w -> b) -> m a -> m (a, b)
48listens : MonadWriter w m => (w -> b) -> m a -> m (a, b)
43listens f m = listens' f (listen m) where
49listens f m = listens' f (listen m) where
44 listens' f' ma = do (a, w) <- ma
50 listens' f' ma = do (a, w) <- ma
45 return (a, f' w)
51 return (a, f' w)
46
52
53+||| Run an action, apply a function to it's output, and return it's value
47censor : MonadWriter w m => (w -> w) -> m a -> m a
54censor : MonadWriter w m => (w -> w) -> m a -> m a
48censor f m = pass $ do a <- m
55censor f m = pass $ do a <- m
49 return (a, f)
56 return (a, f)
50
57
58+||| The Writer monad itself. See the MonadWriter class
51Writer : Type -> Type -> Type
59Writer : Type -> Type -> Type
52Writer w a = WriterT w Identity a
60Writer w a = WriterT w Identity a