f1ba88c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Make Applicative derive from Functor

f1ba88cEdwin Brady15 years ago

lib/prelude.idr+1−1

@@ -127,7 +127,7 @@ instance Functor List where {

127

128infixl 2 <$>;

129

130−class Applicative (f : Set -> Set) where {

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

131 pure : a -> f a;

132 (<$>) : f (a -> b) -> f a -> f b;

133}

test/test007/test007.idr+4

@@ -22,6 +22,10 @@ fetch x = MkEval (\e => fetchVal e) where {

22 fetchVal ((v, val) :: xs) = if (x == v) then (Just val) else (fetchVal xs);

23}

25+instance Functor Eval where {

26+ fmap f (MkEval g) = MkEval (\e => fmap f (g e));

27+}

28+

25instance Applicative Eval where {

29instance Applicative Eval where {

26 pure x = MkEval (\e => Just x);

30 pure x = MkEval (\e => Just x);