You know, 'when' doesn't need Monad either.
commit4f93ab60140e2414a1e27a340888fc65ede5690a
authorstartling <tdixon51793@gmail.com>
dateThu 13 Dec 2012, 20:41 (14 years ago)
parent376b4b5
lib/Prelude/Applicative.idr+3
@@ -17,3 +17,6 @@ class Applicative f => Alternative (f : Type -> Type) where
1717
1818guard : Alternative f => Bool -> f ()
1919guard a = if a then pure () else empty
20+
21+when : Applicative f => Bool -> f () -> f ()
22+when a f = if a then f else pure ()
lib/Prelude/Monad.idr−4
@@ -18,10 +18,6 @@ class Monad m => MonadPlus (m : Type -> Type) where
1818 mplus : m a -> m a -> m a
1919 mzero : m a
2020
21−when : Monad m => Bool -> m () -> m ()
22−when True f = f
23−when False _ = return ()
24−
2521sequence : Monad m => List (m a) -> m (List a)
2622sequence [] = return []
2723sequence (x :: xs) = [ x' :: xs' | x' <- x, xs' <- sequence xs ]