7ee208c · Idris-dev · git.iko.soy

lib/Control/Monad/Identity.idr+10

compare with master

unifiedsplit

@@ -1,10 +1,20 @@

1module Control.Monad.Identity

2

3+import Prelude.Functor

4+import Prelude.Applicative

3import Prelude.Monad

5import Prelude.Monad

4

6

5public record Identity : Set -> Set where

7public record Identity : Set -> Set where

6 Id : (runIdentity : a) -> Identity a

8 Id : (runIdentity : a) -> Identity a

7

9

10+instance Functor Identity where

11+ fmap fn (Id a) = Id (fn a)

12+

13+instance Applicative Identity where

14+ pure x = Id x

15+

16+ (Id f) <$> (Id g) = Id (f g)

17+

8instance Monad Identity where

18instance Monad Identity where

9 return x = Id x

19 return x = Id x

10 (Id x) >>= k = k x

20 (Id x) >>= k = k x

lib/Control/Monad/State.idr+13

@@ -2,6 +2,7 @@ module Control.Monad.State

2

3import Control.Monad.Identity

4import Prelude.Monad

5+import Prelude.Functor

5

6

6%access public

7%access public

7

8

@@ -13,6 +14,18 @@ record StateT : Set -> (Set -> Set) -> Set -> Set where

13 ST : {m : Set -> Set} ->

14 ST : {m : Set -> Set} ->

14 (runStateT : s -> m (a, s)) -> StateT s m a

15 (runStateT : s -> m (a, s)) -> StateT s m a

15

16

17+instance Functor f => Functor (StateT s f) where

18+ fmap f (ST g) = ST (\st => fmap (mapFst f) (g st)) where

19+ mapFst : (a -> x) -> (a, b) -> (x, b)

20+ mapFst fn (a, b) = (fn a, b)

21+

22+instance Monad f => Applicative (StateT s f) where

23+ pure x = ST (\st => pure (x, st))

24+

25+ (ST f) <$> (ST a) = ST (\st => do (g, r) <- f st

26+ (b, t) <- a r

27+ return (g b, t))

28+

16instance Monad m => Monad (StateT s m) where

29instance Monad m => Monad (StateT s m) where

17 return x = ST (\st => return (x, st))

30 return x = ST (\st => return (x, st))

18

31

lib/Data/Morphisms.idr+6−3

@@ -22,14 +22,17 @@ applyHomo (Homo f) a = f a

22applyEndo : Endomorphism a -> a -> a

23applyEndo (Endo f) a = f a

24

25−instance Monad (Homomorphism r) where

25+instance Functor (Homomorphism r) where

26− return a = Homo $ const a

27− (Homo h) >>= f = Homo $ \r => applyHomo (f $ h r) r

26+ fmap f (Homo a) = Homo (f . a)

28

27

29instance Applicative (Homomorphism r) where

28instance Applicative (Homomorphism r) where

30 pure a = Homo $ const a

29 pure a = Homo $ const a

31 (Homo f) <$> (Homo a) = Homo $ \r => f r $ a r

30 (Homo f) <$> (Homo a) = Homo $ \r => f r $ a r

32

31

32+instance Monad (Homomorphism r) where

33+ return a = Homo $ const a

34+ (Homo h) >>= f = Homo $ \r => applyHomo (f $ h r) r

35+

33instance Semigroup (Endomorphism a) where

36instance Semigroup (Endomorphism a) where

34 (Endo f) <+> (Endo g) = Endo $ g . f

37 (Endo f) <+> (Endo g) = Endo $ g . f

35

38

lib/Network/Cgi.idr+11

@@ -27,6 +27,17 @@ data CGI : Set -> Set where

27getAction : CGI a -> CGIInfo -> IO (a, CGIInfo)

28getAction (MkCGI act) = act

29

30+instance Functor CGI where

31+ fmap f (MkCGI c) = MkCGI (\s => do (a, i) <- c s

32+ return (f a, i))

33+

34+instance Applicative CGI where

35+ pure v = MkCGI (\s => return (v, s))

36+

37+ (MkCGI a) <$> (MkCGI b) = MkCGI (\s => do (f, i) <- a s

38+ (c, j) <- b i

39+ return (f c, j))

40+

30instance Monad CGI where {

41instance Monad CGI where {

31 (>>=) (MkCGI f) k = MkCGI (\s => do v <- f s

42 (>>=) (MkCGI f) k = MkCGI (\s => do v <- f s

32 getAction (k (fst v)) (snd v))

43 getAction (k (fst v)) (snd v))

lib/Prelude.idr+42−33

@@ -10,6 +10,7 @@ import Prelude.List

10import Prelude.Maybe

11import Prelude.Monad

12import Prelude.Applicative

13+import Prelude.Functor

13import Prelude.Either

14import Prelude.Either

14import Prelude.Vect

15import Prelude.Vect

15import Prelude.Strings

16import Prelude.Strings

@@ -67,41 +68,11 @@ instance Show a => Show (Maybe a) where

67 show Nothing = "Nothing"

68 show Nothing = "Nothing"

68 show (Just x) = "Just " ++ show x

69 show (Just x) = "Just " ++ show x

69

70

70−---- Monad instances

71−

72−instance Monad IO where

73− return t = io_return t

74− b >>= k = io_bind b k

75−

76−instance Monad Maybe where

77− return t = Just t

78−

79− Nothing >>= k = Nothing

80− (Just x) >>= k = k x

81−

82−instance MonadPlus Maybe where

83− mzero = Nothing

84−

85− mplus (Just x) _ = Just x

86− mplus Nothing (Just y) = Just y

87− mplus Nothing Nothing = Nothing

88−

89−instance Monad (Either e) where

90− return = Right

91−

92− (Left n) >>= _ = Left n

93− (Right r) >>= f = f r

94−

95−instance Monad List where

96− return x = [x]

97− m >>= f = concatMap f m

98−

99−instance MonadPlus List where

100− mzero = []

101− mplus = (++)

102−

103---- Functor instances

71---- Functor instances

104

72

73+instance Functor IO where

74+ fmap f io = io_bind io (io_return . f)

75+

105instance Functor Maybe where

76instance Functor Maybe where

106 fmap f (Just x) = Just (f x)

77 fmap f (Just x) = Just (f x)

107 fmap f Nothing = Nothing

78 fmap f Nothing = Nothing

@@ -115,6 +86,11 @@ instance Functor List where

115

86

116---- Applicative instances

87---- Applicative instances

117

88

89+instance Applicative IO where

90+ pure = io_return

91+

92+ am <$> bm = io_bind am (\f => io_bind bm (io_return . f))

93+

118instance Applicative Maybe where

94instance Applicative Maybe where

119 pure = Just

95 pure = Just

120

96

@@ -133,6 +109,39 @@ instance Applicative List where

133

109

134 fs <$> vs = concatMap (\f => map f vs) fs

110 fs <$> vs = concatMap (\f => map f vs) fs

135

111

112+---- Monad instances

113+

114+instance Monad IO where

115+ return t = io_return t

116+ b >>= k = io_bind b k

117+

118+instance Monad Maybe where

119+ return t = Just t

120+

121+ Nothing >>= k = Nothing

122+ (Just x) >>= k = k x

123+

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+

131+instance Monad (Either e) where

132+ return = Right

133+

134+ (Left n) >>= _ = Left n

135+ (Right r) >>= f = f r

136+

137+instance Monad List where

138+ return x = [x]

139+ m >>= f = concatMap f m

140+

141+instance MonadPlus List where

142+ mzero = []

143+ mplus = (++)

144+

136---- some mathematical operations

145---- some mathematical operations

137

146

138%include "math.h"

147%include "math.h"

lib/Prelude/Applicative.idr+2−1

@@ -1,12 +1,13 @@

1module Prelude.Applicative

2

3import Builtins

4+import Prelude.Functor

4

5

5---- Applicative functors/Idioms

6---- Applicative functors/Idioms

6

7

7infixl 2 <$>

8infixl 2 <$>

8

9

9−class Applicative (f : Set -> Set) where

10+class Functor f => Applicative (f : Set -> Set) where

10 pure : a -> f a

11 pure : a -> f a

11 (<$>) : f (a -> b) -> f a -> f b

12 (<$>) : f (a -> b) -> f a -> f b

12

13

lib/Prelude/Functor.idrnew file+4

@@ -0,0 +1,4 @@

1+module Prelude.Functor

2+

3+class Functor (f : Set -> Set) where

4+ fmap : (a -> b) -> f a -> f b

lib/Prelude/Monad.idr+2−4

@@ -4,18 +4,16 @@ module Prelude.Monad

4

5import Builtins

6import Prelude.List

7+import Prelude.Applicative

7

8

8%access public

9%access public

9

10

10infixl 5 >>=

11infixl 5 >>=

11

12

12−class Monad (m : Set -> Set) where

13+class Applicative m => Monad (m : Set -> Set) where

13 return : a -> m a

14 return : a -> m a

14 (>>=) : m a -> (a -> m b) -> m b

15 (>>=) : m a -> (a -> m b) -> m b

15

16

16−class Functor (f : Set -> Set) where

17− fmap : (a -> b) -> f a -> f b

18−

19class Monad m => MonadPlus (m : Set -> Set) where

17class Monad m => MonadPlus (m : Set -> Set) where

20 mplus : m a -> m a -> m a

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

21 mzero : m a

19 mzero : m a

lib/System/Concurrency/Process.idr+7

@@ -15,6 +15,13 @@ data ProcID msg = MkPID Ptr

15data Process : (msgType : Set) -> Set -> Set where

16 lift : IO a -> Process msg a

17

18+instance Functor (Process msg) where

19+ fmap f (lift a) = lift (fmap f a)

20+

21+instance Applicative (Process msg) where

22+ pure = lift . return

23+ (lift f) <$> (lift a) = lift (f <$> a)

24+

18instance Monad (Process msg) where

25instance Monad (Process msg) where

19 return = lift . return

26 return = lift . return

20 (lift io) >>= k = lift (do x <- io

27 (lift io) >>= k = lift (do x <- io