git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1695 from japesinator/verified_monads
ddc2981Edwin Brady
libs/prelude/Prelude/Applicative.idr+11
compare with master
unifiedsplit
@@ -17,6 +17,17 @@ instance Applicative id where
17 pure a = a
17 pure a = a
18 f <$> a = f a
18 f <$> a = f a
19
19
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+
20infixl 2 <$
31infixl 2 <$
21(<$) : Applicative f => f a -> f b -> f a
32(<$) : Applicative f => f a -> f b -> f a
22a <$ b = map const a <$> b
33a <$ b = map const a <$> b
libs/prelude/Prelude/Functor.idr+6
@@ -10,5 +10,11 @@ class Functor (f : Type -> Type) where
10 ||| @ m the morphism
10 ||| @ m the morphism
11 map : (m : a -> b) -> f a -> f b
11 map : (m : a -> b) -> f a -> f b
12
12
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+
13instance Functor id where
19instance Functor id where
14 map f a = f a
20 map f a = f a
libs/prelude/Prelude/Monad.idr+10
@@ -14,6 +14,16 @@ infixl 5 >>=
14class Applicative m => Monad (m : Type -> Type) where
14class Applicative m => Monad (m : Type -> Type) where
15 (>>=) : m a -> (a -> m b) -> m b
15 (>>=) : m a -> (a -> m b) -> m b
16
16
17+class (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) where
18+ monadApplicative : (mf : m (a -> b)) -> (mx : m a) ->
19+ mf <$> mx = mf >>= \f =>
20+ mx >>= \x =>
21+ pure (f x)
22+ monadLeftIdentity : (x : a) -> (f : a -> m b) -> return x >>= f = f x
23+ monadRightIdentity : (mx : m a) -> mx >>= return = mx
24+ monadAssociativity : (mx : m a) -> (f : a -> m b) -> (g : b -> m c) ->
25+ (mx >>= f) >>= g = mx >>= (\x => f x >>= g)
26+
17instance Monad id where
27instance Monad id where
18 a >>= f = f a
28 a >>= f = f a
19
29