git.iko.soy/Idris-dev
on master help sign in
Functor and Applicative instances for Identity.
d13c4bastartling
lib/Control/Monad/Identity.idr+10
compare with master
unifiedsplit
@@ -1,10 +1,20 @@
1module Control.Monad.Identity
1module Control.Monad.Identity
2
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