git.iko.soy/Idris-dev
on bf4e535 help sign in
Idris-dev/libs/base/Control/Monad/Writer.idr
66 lines 2.4 kB history raw
1module Control.Monad.Writer
3import Builtins
4import Control.Monad.Identity
5import Control.Monad.Trans
7%access public
9||| A monad representing a computation that produces a stream of output
10class (Monoid w, Monad m) => MonadWriter w (m : Type -> Type) where
11 ||| tell w produces the output w
12 tell : w -> m ()
13 ||| Execute an action and add it's output to the value of the computation
14 listen : m a -> m (a, w)
15 ||| Execute an action and apply the returned function to the output
16 pass : m (a, w -> w) -> m a
18||| The transformer base of the Writer monad
19record WriterT : Type -> (Type -> Type) -> Type -> Type where
20 WR : {m : Type -> Type} ->
21 (runWriterT : m (a, w)) -> WriterT w m a
23instance Functor f => Functor (WriterT w f) where
24 map f (WR g) = WR $ map (\w => (f . fst $ w, snd w)) g
26instance (Monoid w, Applicative m) => Applicative (WriterT w m) where
27 pure a = WR $ pure (a, neutral)
28 (WR f) <*> (WR v) = WR $ liftA2 merge f v where
29 merge (fn, w) (a, w') = (fn a, w <+> w')
31instance (Monoid w, Alternative m) => Alternative (WriterT w m) where
32 empty = WR empty
33 (WR m) <|> (WR n) = WR $ m <|> n
35instance (Monoid w, Monad m) => Monad (WriterT w m) where
36 (WR m) >>= k = WR $ do (a, w) <- m
37 let WR ka = k a
38 (b, w') <- ka
39 return (b, w <+> w')
41instance (Monoid w, Monad m) => MonadWriter w (WriterT w m) where
42 tell w = WR $ return ((), w)
43 listen (WR m) = WR $ do (a, w) <- m
44 return ((a, w), w)
45 pass (WR m) = WR $ do ((a, f), w) <- m
46 return (a, f w)
48instance Monoid w => MonadTrans (WriterT w) where
49 lift x = WR $ do r <- x
50 return (r, neutral)
52||| Run an action in the Writer monad and transform the written output
53listens : MonadWriter w m => (w -> b) -> m a -> m (a, b)
54listens {m} f act = listens' f (listen act) where
55 listens' : (w -> b) -> m (a, w) -> m (a, b)
56 listens' f' ma = do (a, w) <- ma
57 return (a, f' w)
59||| Run an action, apply a function to it's output, and return it's value
60censor : MonadWriter w m => (w -> w) -> m a -> m a
61censor f m = pass $ do a <- m
62 return (a, f)
64||| The Writer monad itself. See the MonadWriter class
65Writer : Type -> Type -> Type
66Writer w a = WriterT w Identity a