git.iko.soy/Idris-dev
on master help sign in
Add Functor Monad and Applicative id instances
97a2c74Carter Charbonneau
CONTRIBUTORS+1
compare with master
unifiedsplit
@@ -8,6 +8,7 @@ Michael R. Bernstein
8Nicola Botta
8Nicola Botta
9Edwin Brady
9Edwin Brady
10David Raymond Christiansen
10David Raymond Christiansen
11+Carter Charbonneau
11Jason Dagit
12Jason Dagit
12Simon Fowler
13Simon Fowler
13Google
14Google
libs/prelude/Prelude/Applicative.idr+4
@@ -13,6 +13,10 @@ class Functor f => Applicative (f : Type -> Type) where
13 pure : a -> f a
13 pure : a -> f a
14 (<$>) : f (a -> b) -> f a -> f b
14 (<$>) : f (a -> b) -> f a -> f b
15
15
16+instance Applicative id where
17+ pure a = a
18+ f <$> a = f a
19+
16infixl 2 <$
20infixl 2 <$
17(<$) : Applicative f => f a -> f b -> f a
21(<$) : Applicative f => f a -> f b -> f a
18a <$ b = map const a <$> b
22a <$ b = map const a <$> b
libs/prelude/Prelude/Functor.idr+5
@@ -1,5 +1,7 @@
1module Prelude.Functor
1module Prelude.Functor
2
2
3+import Prelude.Basics
4+
3||| Functors
5||| Functors
4||| @ f the action of the functor on objects
6||| @ f the action of the functor on objects
5class Functor (f : Type -> Type) where
7class Functor (f : Type -> Type) where
@@ -7,3 +9,6 @@ class Functor (f : Type -> Type) where
7 ||| @ f the functor
9 ||| @ f the functor
8 ||| @ m the morphism
10 ||| @ m the morphism
9 map : (m : a -> b) -> f a -> f b
11 map : (m : a -> b) -> f a -> f b
12+
13+instance Functor id where
14+ map f a = f a
libs/prelude/Prelude/Monad.idr+4
@@ -5,6 +5,7 @@ module Prelude.Monad
5import Builtins
5import Builtins
6import Prelude.List
6import Prelude.List
7import Prelude.Applicative
7import Prelude.Applicative
8+import Prelude.Basics
8
9
9%access public
10%access public
10
11
@@ -13,6 +14,9 @@ infixl 5 >>=
13class Applicative m => Monad (m : Type -> Type) where
14class Applicative m => Monad (m : Type -> Type) where
14 (>>=) : m a -> (a -> m b) -> m b
15 (>>=) : m a -> (a -> m b) -> m b
15
16
17+instance Monad id where
18+ a >>= f = f a
19+
16||| Also called `join` or mu
20||| Also called `join` or mu
17flatten : Monad m => m (m a) -> m a
21flatten : Monad m => m (m a) -> m a
18flatten a = a >>= id
22flatten a = a >>= id