@@ -14,6 +14,12 @@ 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
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)
17instance Monad id where
23instance Monad id where
18 a >>= f = f a
24 a >>= f = f a