git.iko.soy/Idris-dev
on master help sign in
Merge pull request #1695 from japesinator/verified_monads

Added verified monads

commitddc2981f046e41f7f2c7f2f07fed618b75418cb4 authorEdwin Brady <edwin.brady@gmail.com> dateMon 24 Nov 2014, 11:12 (12 years ago) parent52b18cc5eb8dff
3 files changed+27
compare with master
unifiedsplit
libs/prelude/Prelude/Applicative.idr+11 libs/prelude/Prelude/Functor.idr+6 libs/prelude/Prelude/Monad.idr+10
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+10
@@ -14,6 +14,16 @@ infixl 5 >>=
1414class Applicative m => Monad (m : Type -> Type) where
1515 (>>=) : m a -> (a -> m b) -> m b
1616
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+
1727instance Monad id where
1828 a >>= f = f a
1929