bdef7ec · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

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

commitbdef7ec7296679434909bc0d8d8306b9689debe1 authorstartling <tdixon51793@gmail.com> dateThu 13 Dec 2012, 21:18 (14 years ago) parent112f92a

2 files changed+8−8

unifiedsplit

lib/Prelude/Applicative.idr+8

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

2828

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

3030when 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

1818 mplus : m a -> m a -> m a

1919 mzero : m a

2020

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−

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

3022mapM f xs = sequence (map f xs)

3123