bdef7ec · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

'sequence' and 'sequence_' don't need Monad, either.

bdef7ecstartling14 years ago

lib/Prelude/Applicative.idr+8

@@ -28,3 +28,11 @@ guard a = if a then pure () else empty

29when : Applicative f => Bool -> f () -> f ()

30when a f = if a then f else pure ()

31+

32+sequence : Applicative f => List (f a) -> f (List a)

33+sequence [] = pure []

34+sequence (x :: xs) = fmap (::) x <$> sequence xs

35+

36+sequence_ : Applicative f => List (f a) -> f ()

37+sequence_ [] = pure ()

38+sequence_ (x :: xs) = x $> sequence_ xs

lib/Prelude/Monad.idr−8

@@ -18,14 +18,6 @@ class Monad m => MonadPlus (m : Type -> Type) where

18 mplus : m a -> m a -> m a

19 mzero : m a

21−sequence : Monad m => List (m a) -> m (List a)

22−sequence [] = return []

23−sequence (x :: xs) = [ x' :: xs' | x' <- x, xs' <- sequence xs ]

24−

25−sequence_ : Monad m => List (m a) -> m ()

26−sequence_ [] = return ()

27−sequence_ (x :: xs) = do x; sequence_ xs

28−

29mapM : Monad m => (a -> m b) -> List a -> m (List b)

21mapM : Monad m => (a -> m b) -> List a -> m (List b)

30mapM f xs = sequence (map f xs)

22mapM f xs = sequence (map f xs)