Rewrote 'mapM' and 'mapM_' as 'traverse' and 'traverse_'.
It only requires Applicative, now, too.
This should be generalized eventually to a Traversable class, but I
don't think this is a bad way to start.
commit811a3cd5a6d404d7877a0e7bfc5fa050b9d7ad43
authorstartling <tdixon51793@gmail.com>
dateThu 13 Dec 2012, 21:41 (14 years ago)
parente75227b
lib/Prelude/Applicative.idr+6
@@ -37,3 +37,9 @@ sequence (x :: xs) = fmap (::) x <$> sequence xs
3737sequence_ : Applicative f => List (f a) -> f ()
3838sequence_ [] = pure ()
3939sequence_ (x :: xs) = x $> sequence_ xs
40+
41+traverse : Applicative f => (a -> f b) -> List a -> f (List b)
42+traverse f xs = sequence (map f xs)
43+
44+traverse_ : Applicative f => (a -> f b) -> List a -> f ()
45+traverse_ f (x :: xs) = f x $> traverse_ f xs
lib/Prelude/Monad.idr−6
@@ -14,11 +14,5 @@ class Applicative m => Monad (m : Type -> Type) where
1414 return : a -> m a
1515 (>>=) : m a -> (a -> m b) -> m b
1616
17−mapM : Monad m => (a -> m b) -> List a -> m (List b)
18−mapM f xs = sequence (map f xs)
19−
20−mapM_ : Monad m => (a -> m b) -> List a -> m ()
21−mapM_ f xs = sequence_ (map f xs)
22−
2317flatten : Monad m => m (m a) -> m a
2418flatten a = a >>= id