@@ -0,0 +1,41 @@
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+
14+record WriterT : Type -> (Type -> Type) -> Type -> Type where
15+ WR : {m : Type -> Type} ->
16+ (runWriterT : m (a, w)) -> WriterT w m a
17+
18+instance Functor f => Functor (WriterT w f) where
19+ map f (WR g) = WR $ map (\w => (f . fst $ w, snd w)) g
20+
21+instance (Monoid w, Applicative m) => Applicative (WriterT w m) where
22+ pure a = WR $ pure (a, neutral)
23+ (WR f) <$> (WR v) = WR $ liftA2 merge f v where
24+ merge (fn, w) (a, w') = (fn a, w <+> w')
25+
26+instance (Monoid w, Alternative m) => Alternative (WriterT w m) where
27+ empty = WR empty
28+ (WR m) <|> (WR n) = WR $ m <|> n
29+
30+instance (Monoid w, Monad m) => Monad (WriterT w m) where
31+ (WR m) >>= k = WR $ do (a, w) <- m
32+ let WR ka = k a
33+ (b, w') <- ka
34+ return (b, w <+> w')
35+
36+instance (Monoid w, Monad m) => MonadWriter w (WriterT w m) where
37+ tell w = WR $ return ((), w)
38+
39+
40+Writer : Type -> Type -> Type
41+Writer w a = WriterT w Identity a