verified monads are applicatives
commit5eb8dffe308934d5bc63202aa8864ebd58a27026
authorJP Smith <jp.smith@ilstu.edu>
dateTue 4 Nov 2014, 06:37 (12 years ago)
parentc71826a
libs/prelude/Prelude/Monad.idr+4
@@ -15,6 +15,10 @@ class Applicative m => Monad (m : Type -> Type) where
1515 (>>=) : m a -> (a -> m b) -> m b
1616
1717class (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)
1822 monadLeftIdentity : (x : a) -> (f : a -> m b) -> return x >>= f = f x
1923 monadRightIdentity : (mx : m a) -> mx >>= return = mx
2024 monadAssociativity : (mx : m a) -> (f : a -> m b) -> (g : b -> m c) ->