git.iko.soy/Idris-dev
on master help sign in
Rewrote 'mapM' and 'mapM_' as 'traverse' and 'traverse_'.
811a3cdstartling
lib/Prelude/Applicative.idr+6
compare with master
unifiedsplit
@@ -37,3 +37,9 @@ sequence (x :: xs) = fmap (::) x <$> sequence xs
37sequence_ : Applicative f => List (f a) -> f ()
37sequence_ : Applicative f => List (f a) -> f ()
38sequence_ [] = pure ()
38sequence_ [] = pure ()
39sequence_ (x :: xs) = x $> sequence_ xs
39sequence_ (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
14 return : a -> m a
14 return : a -> m a
15 (>>=) : m a -> (a -> m b) -> m b
15 (>>=) : m a -> (a -> m b) -> m b
16
16
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−
23flatten : Monad m => m (m a) -> m a
17flatten : Monad m => m (m a) -> m a
24flatten a = a >>= id
18flatten a = a >>= id