git.iko.soy/Idris-dev
on master help sign in
Merge pull request #130 from startling/alternative
2b30118Edwin Brady
lib/Prelude.idr+13−11
compare with master
unifiedsplit
@@ -109,6 +109,19 @@ instance Applicative List where
109
109
110 fs <$> vs = concatMap (\f => map f vs) fs
110 fs <$> vs = concatMap (\f => map f vs) fs
111
111
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+
112---- Monad instances
125---- Monad instances
113
126
114instance Monad IO where
127instance Monad IO where
@@ -121,13 +134,6 @@ instance Monad Maybe where
121 Nothing >>= k = Nothing
134 Nothing >>= k = Nothing
122 (Just x) >>= k = k x
135 (Just x) >>= k = k x
123
136
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−
131instance Monad (Either e) where
137instance Monad (Either e) where
132 return = Right
138 return = Right
133
139
@@ -138,10 +144,6 @@ instance Monad List where
138 return x = [x]
144 return x = [x]
139 m >>= f = concatMap f m
145 m >>= f = concatMap f m
140
146
141−instance MonadPlus List where
142− mzero = []
143− mplus = (++)
144−
145---- some mathematical operations
147---- some mathematical operations
146
148
147%include "math.h"
149%include "math.h"
lib/Prelude/Applicative.idr+32−1
@@ -9,6 +9,37 @@ infixl 2 <$>
9
9
10class Functor f => Applicative (f : Type -> Type) where
10class Functor f => Applicative (f : Type -> Type) where
11 pure : a -> f a
11 pure : a -> f a
12− (<$>) : f (a -> b) -> f a -> f b
12+ (<$>) : f (a -> b) -> f a -> f b
13
13
14+infixl 2 <$
15+(<$) : Applicative f => f a -> f b -> f a
16+a <$ b = fmap const a <$> b
14
17
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
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−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−
43flatten : Monad m => m (m a) -> m a
17flatten : Monad m => m (m a) -> m a
44flatten a = a >>= id
18flatten a = a >>= id