git.iko.soy/Idris-dev
on master help sign in
Add WriterT.
7e8466fGeorge Leontiev
lib/Control/Monad/Writer.idrnew file+41
compare with master
unifiedsplit
@@ -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
lib/Prelude/Applicative.idr+9
@@ -19,6 +19,15 @@ infixl 2 $>
19($>) : Applicative f => f a -> f b -> f b
19($>) : Applicative f => f a -> f b -> f b
20a $> b = map (const id) a <$> b
20a $> b = map (const id) a <$> b
21
21
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+
22infixl 3 <|>
31infixl 3 <|>
23class Applicative f => Alternative (f : Type -> Type) where
32class Applicative f => Alternative (f : Type -> Type) where
24 empty : f a
33 empty : f a
lib/base.ipkg+1
@@ -29,5 +29,6 @@ modules = Builtins, Prelude, IO, System,
29 Data.Vect, Data.HVect, Data.Vect.Quantifiers,
29 Data.Vect, Data.HVect, Data.Vect.Quantifiers,
30
30
31 Control.Monad.Identity, Control.Monad.State, Control.Category,
31 Control.Monad.Identity, Control.Monad.State, Control.Category,
32+ Control.Monad.Writer,
32 Control.Arrow,
33 Control.Arrow,
33 Control.Catchable, Control.IOExcept
34 Control.Catchable, Control.IOExcept