Make Applicative derive from Functor
commitf1ba88c0b9b9a59254915a8b078f98256d71a300
authorEdwin Brady <eb@cs.st-andrews.ac.uk>
dateWed 4 Jan 2012, 11:08 (15 years ago)
parent1a12cc3
lib/prelude.idr+1−1
@@ -127,7 +127,7 @@ instance Functor List where {
127127
128128infixl 2 <$>;
129129
130−class Applicative (f : Set -> Set) where {
130+class Functor f => Applicative (f : Set -> Set) where {
131131 pure : a -> f a;
132132 (<$>) : f (a -> b) -> f a -> f b;
133133}
test/test007/test007.idr+4
@@ -22,6 +22,10 @@ fetch x = MkEval (\e => fetchVal e) where {
2222 fetchVal ((v, val) :: xs) = if (x == v) then (Just val) else (fetchVal xs);
2323}
2424
25+instance Functor Eval where {
26+ fmap f (MkEval g) = MkEval (\e => fmap f (g e));
27+}
28+
2529instance Applicative Eval where {
2630 pure x = MkEval (\e => Just x);
2731