defined mcompose

Author: vzaliva

theories/Structures/Monad.v

@@ -52,6 +52,15 @@ Section monadic.
               {M : Monad m}
               {A B : Type@{d}} (fM:m (A -> B)) (aM:m A) : m B :=
     bind fM (fun f => liftM f aM).
+
+  (* Left-to-right composition of Kleisli arrows. *)
+  Definition mcompose@{c d}
+             {m:Type@{d}->Type@{c}}
+             {M: Monad m}
+             {T U V:Type@{d}}
+             (f: T -> m U) (g: U -> m V): (T -> m V) :=
+    fun x => bind (f x) g.
+
 End monadic.
 
 Module MonadNotation.
@@ -60,9 +69,7 @@ Module MonadNotation.
 
   Notation "c >>= f" := (@pbind _ _ _ _ _ c f) (at level 50, left associativity) : monad_scope.
   Notation "f =<< c" := (@pbind _ _ _ _ _ c f) (at level 51, right associativity) : monad_scope.
-
-  (* Left-to-right composition of Kleisli arrows. *)
-  Notation "f >=> g" := (fun x => @pbind _ _ _ _ _ (f x) g) (at level 50, left associativity) : monad_scope.
+  Notation "f >=> g" := (@mcompose _ _ _ _ _ f g) (at level 50, left associativity) : monad_scope.
 
   Notation "x <- c1 ;; c2" := (@pbind _ _ _ _ _ c1 (fun x => c2))
     (at level 100, c1 at next level, right associativity) : monad_scope.