Merge pull request #1422 from fread2281/master
Add Functor Monad and Applicative id instances
commit313340e285bae81650e2d517cebbf3784d935fee
authorDavid Christiansen <david@davidchristiansen.dk>
dateThu 24 Jul 2014, 10:15 (12 years ago)
parentabc99c697a2c74
CONTRIBUTORS+1
@@ -8,6 +8,7 @@ Michael R. Bernstein
88Nicola Botta
99Edwin Brady
1010David Raymond Christiansen
11+Carter Charbonneau
1112Jason Dagit
1213Simon Fowler
1314Google
libs/prelude/Prelude/Applicative.idr+4
@@ -13,6 +13,10 @@ class Functor f => Applicative (f : Type -> Type) where
1313 pure : a -> f a
1414 (<$>) : f (a -> b) -> f a -> f b
1515
16+instance Applicative id where
17+ pure a = a
18+ f <$> a = f a
19+
1620infixl 2 <$
1721(<$) : Applicative f => f a -> f b -> f a
1822a <$ b = map const a <$> b
libs/prelude/Prelude/Functor.idr+5
@@ -1,5 +1,7 @@
11module Prelude.Functor
22
3+import Prelude.Basics
4+
35||| Functors
46||| @ f the action of the functor on objects
57class Functor (f : Type -> Type) where
@@ -7,3 +9,6 @@ class Functor (f : Type -> Type) where
79 ||| @ f the functor
810 ||| @ m the morphism
911 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
55import Builtins
66import Prelude.List
77import Prelude.Applicative
8+import Prelude.Basics
89
910%access public
1011
@@ -13,6 +14,9 @@ infixl 5 >>=
1314class Applicative m => Monad (m : Type -> Type) where
1415 (>>=) : m a -> (a -> m b) -> m b
1516
17+instance Monad id where
18+ a >>= f = f a
19+
1620||| Also called `join` or mu
1721flatten : Monad m => m (m a) -> m a
1822flatten a = a >>= id