git.iko.soy/Idris-dev
on master help sign in
added verified functors/applicatives
commitc71826a6fb244b06c1b8bfa53134a66c77488e54 authorJP Smith <jp.smith@ilstu.edu> dateMon 3 Nov 2014, 21:21 (12 years ago) parent0a4c35d
3 files changed+22−5
compare with master
unifiedsplit
libs/prelude/Prelude/Applicative.idr+11 libs/prelude/Prelude/Functor.idr+6 libs/prelude/Prelude/Monad.idr+5−5
libs/prelude/Prelude/Applicative.idr+11
@@ -17,6 +17,17 @@ instance Applicative id where
1717 pure a = a
1818 f <$> a = f a
1919
20+class (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type -> Type) where
21+ applicativeMap : (x : f a) -> (g : a -> b) ->
22+ map g x = pure g <$> x
23+ applicativeIdentity : (x : f a) -> pure id <$> x = x
24+ applicativeComposition : (x : f a) -> (g1 : f (a -> b)) -> (g2 : f (b -> c)) ->
25+ ((pure (.) <$> g2) <$> g1) <$> x = g2 <$> (g1 <$> x)
26+ applicativeHomomorphism : (x : a) -> (g : a -> b) ->
27+ (<$>) {f} (pure g) (pure x) = pure {f} (g x)
28+ applicativeInterchange : (x : a) -> (g : f (a -> b)) ->
29+ g <$> pure x = pure (\g' : a -> b => g' x) <$> g
30+
2031infixl 2 <$
2132(<$) : Applicative f => f a -> f b -> f a
2233a <$ b = map const a <$> b
libs/prelude/Prelude/Functor.idr+6
@@ -10,5 +10,11 @@ class Functor (f : Type -> Type) where
1010 ||| @ m the morphism
1111 map : (m : a -> b) -> f a -> f b
1212
13+class Functor f => VerifiedFunctor (f : Type -> Type) where
14+ functorIdentity : {a : Type} -> (x : f a) -> map id x = id x
15+ functorComposition : {a : Type} -> {b : Type} -> (x : f a) ->
16+ (g1 : a -> b) -> (g2 : b -> c) ->
17+ map (g2 . g1) x = (map g2 . map g1) x
18+
1319instance Functor id where
1420 map f a = f a
libs/prelude/Prelude/Monad.idr+5−5
@@ -14,11 +14,11 @@ infixl 5 >>=
1414class Applicative m => Monad (m : Type -> Type) where
1515 (>>=) : m a -> (a -> m b) -> m b
1616
17−class Monad m => VerifiedMonad (m : Type -> Type) where
18− total lIdentity : (f : a -> m b) -> (x : a) -> return x >>= f = f x
19− total rIdentity : (ma : m a) -> ma >>= return = ma
20− total associativity : (ma : m a) -> (f : a -> m b) -> (g : b -> m c) ->
21− (ma >>= f) >>= g = ma >>= (\x => f x >>= g)
17+class (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) where
18+ monadLeftIdentity : (x : a) -> (f : a -> m b) -> return x >>= f = f x
19+ monadRightIdentity : (mx : m a) -> mx >>= return = mx
20+ monadAssociativity : (mx : m a) -> (f : a -> m b) -> (g : b -> m c) ->
21+ (mx >>= f) >>= g = mx >>= (\x => f x >>= g)
2222
2323instance Monad id where
2424 a >>= f = f a