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

git.iko.soy/Idris-dev

Merge pull request #89 from startling/class-hierarchy

Created the Functor ⊃ Applicative ⊃ Monad hierarchy.

commit7ee208caf7fbd69870d68dc87996652917918e17 authorEdwin Brady <edwin.brady@gmail.com> dateTue 20 Nov 2012, 16:27 (14 years ago) parent809c283 77e407e

9 files changed+97−41

compare with master

unifiedsplit

lib/Control/Monad/Identity.idr+10 lib/Control/Monad/State.idr+13 lib/Data/Morphisms.idr+6−3 lib/Network/Cgi.idr+11 lib/Prelude.idr+42−33 lib/Prelude/Applicative.idr+2−1 lib/Prelude/Functor.idr+4 lib/Prelude/Monad.idr+2−4 lib/System/Concurrency/Process.idr+7

lib/Control/Monad/Identity.idr+10

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

11module Control.Monad.Identity

3+import Prelude.Functor

4+import Prelude.Applicative

35import Prelude.Monad

57public record Identity : Set -> Set where

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

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+

818instance Monad Identity where

919 return x = Id x

1020 (Id x) >>= k = k x

lib/Control/Monad/State.idr+13

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

33import Control.Monad.Identity

44import Prelude.Monad

5+import Prelude.Functor

67%access public

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

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

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

1516

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+

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

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

1831

lib/Data/Morphisms.idr+6−3

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

2222applyEndo : Endomorphism a -> a -> a

2323applyEndo (Endo f) a = f a

2424

25−instance Monad (Homomorphism r) where

26− return a = Homo $ const a

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

25+instance Functor (Homomorphism r) where

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

2827

2928instance Applicative (Homomorphism r) where

3029 pure a = Homo $ const a

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

3231

32+instance Monad (Homomorphism r) where

33+ return a = Homo $ const a

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

35+

3336instance Semigroup (Endomorphism a) where

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

3538

lib/Network/Cgi.idr+11

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

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

2828getAction (MkCGI act) = act

2929

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+

3041instance Monad CGI where {

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

3243 getAction (k (fst v)) (snd v))

lib/Prelude.idr+42−33

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

1010import Prelude.Maybe

1111import Prelude.Monad

1212import Prelude.Applicative

13+import Prelude.Functor

1314import Prelude.Either

1415import Prelude.Vect

1516import Prelude.Strings

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

6768 show Nothing = "Nothing"

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

6970

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−

10371---- Functor instances

10472

73+instance Functor IO where

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

75+

10576instance Functor Maybe where

10677 fmap f (Just x) = Just (f x)

10778 fmap f Nothing = Nothing

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

11586

11687---- Applicative instances

11788

89+instance Applicative IO where

90+ pure = io_return

91+

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

93+

11894instance Applicative Maybe where

11995 pure = Just

12096

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

133109

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

135111

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+

136145---- some mathematical operations

137146

138147%include "math.h"

lib/Prelude/Applicative.idr+2−1

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

11module Prelude.Applicative

33import Builtins

4+import Prelude.Functor

56---- Applicative functors/Idioms

78infixl 2 <$>

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

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

1011 pure : a -> f a

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

1213

lib/Prelude/Functor.idrnew file+4

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

1+module Prelude.Functor

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

55import Builtins

66import Prelude.List

7+import Prelude.Applicative

89%access public

910

1011infixl 5 >>=

1112

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

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

1314 return : a -> m a

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

1516

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

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

18−

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

2018 mplus : m a -> m a -> m a

2119 mzero : m a

lib/System/Concurrency/Process.idr+7

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

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

1616 lift : IO a -> Process msg a

1717

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+

1825instance Monad (Process msg) where

1926 return = lift . return

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