git.iko.soy/Idris-dev
on master help sign in
Merge pull request #130 from startling/alternative

Some changes for `Applicative`

commit2b301183c707c1057f7ecd63b41ac613c53a92cc authorEdwin Brady <edwin.brady@gmail.com> dateSun 16 Dec 2012, 03:44 (14 years ago) parentb88e7f2811a3cd
3 files changed+45−38
compare with master
unifiedsplit
lib/Prelude.idr+13−11 lib/Prelude/Applicative.idr+32−1 lib/Prelude/Monad.idr−26
lib/Prelude.idr+13−11
@@ -109,6 +109,19 @@ instance Applicative List where
109109
110110 fs <$> vs = concatMap (\f => map f vs) fs
111111
112+---- Alternative instances
113+
114+instance Alternative Maybe where
115+ empty = Nothing
116+
117+ (Just x) <|> _ = Just x
118+ Nothing <|> v = v
119+
120+instance Alternative List where
121+ empty = []
122+
123+ (<|>) = (++)
124+
112125---- Monad instances
113126
114127instance Monad IO where
@@ -121,13 +134,6 @@ instance Monad Maybe where
121134 Nothing >>= k = Nothing
122135 (Just x) >>= k = k x
123136
124−instance MonadPlus Maybe where
125− mzero = Nothing
126−
127− mplus (Just x) _ = Just x
128− mplus Nothing (Just y) = Just y
129− mplus Nothing Nothing = Nothing
130−
131137instance Monad (Either e) where
132138 return = Right
133139
@@ -138,10 +144,6 @@ instance Monad List where
138144 return x = [x]
139145 m >>= f = concatMap f m
140146
141−instance MonadPlus List where
142− mzero = []
143− mplus = (++)
144−
145147---- some mathematical operations
146148
147149%include "math.h"
lib/Prelude/Applicative.idr+32−1
@@ -9,6 +9,37 @@ infixl 2 <$>
99
1010class Functor f => Applicative (f : Type -> Type) where
1111 pure : a -> f a
12− (<$>) : f (a -> b) -> f a -> f b
12+ (<$>) : f (a -> b) -> f a -> f b
1313
14+infixl 2 <$
15+(<$) : Applicative f => f a -> f b -> f a
16+a <$ b = fmap const a <$> b
1417
18+infixl 2 $>
19+($>) : Applicative f => f a -> f b -> f b
20+a $> b = fmap (const id) a <$> b
21+
22+infixl 3 <|>
23+class Applicative f => Alternative (f : Type -> Type) where
24+ empty : f a
25+ (<|>) : f a -> f a -> f a
26+
27+guard : Alternative f => Bool -> f ()
28+guard a = if a then pure () else empty
29+
30+when : Applicative f => Bool -> f () -> f ()
31+when a f = if a then f else pure ()
32+
33+sequence : Applicative f => List (f a) -> f (List a)
34+sequence [] = pure []
35+sequence (x :: xs) = fmap (::) x <$> sequence xs
36+
37+sequence_ : Applicative f => List (f a) -> f ()
38+sequence_ [] = pure ()
39+sequence_ (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−26
@@ -14,31 +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−class Monad m => MonadPlus (m : Type -> Type) where
18− mplus : m a -> m a -> m a
19− mzero : m a
20−
21−guard : MonadPlus m => Bool -> m ()
22−guard True = return ()
23−guard False = mzero
24−
25−when : Monad m => Bool -> m () -> m ()
26−when True f = f
27−when False _ = return ()
28−
29−sequence : Monad m => List (m a) -> m (List a)
30−sequence [] = return []
31−sequence (x :: xs) = [ x' :: xs' | x' <- x, xs' <- sequence xs ]
32−
33−sequence_ : Monad m => List (m a) -> m ()
34−sequence_ [] = return ()
35−sequence_ (x :: xs) = do x; sequence_ xs
36−
37−mapM : Monad m => (a -> m b) -> List a -> m (List b)
38−mapM f xs = sequence (map f xs)
39−
40−mapM_ : Monad m => (a -> m b) -> List a -> m ()
41−mapM_ f xs = sequence_ (map f xs)
42−
4317flatten : Monad m => m (m a) -> m a
4418flatten a = a >>= id