add Monad

Stdlib/Trait.juvix

@@ -5,6 +5,7 @@ import Stdlib.Trait.Show as Show open using {Show; module Show} public;
 import Stdlib.Trait.Ord as Ord open using {Ord; module Ord} public;
 import Stdlib.Trait.Functor open public;
 import Stdlib.Trait.Applicative open public;
+import Stdlib.Trait.Monad open public;
 import Stdlib.Trait.Foldable open public;
 import Stdlib.Trait.Partial open public;
 import Stdlib.Trait.Natural open public;

Stdlib/Trait/Monad.juvix

@@ -0,0 +1,24 @@
+module Stdlib.Trait.Monad;
+
+import Stdlib.Data.Fixity open;
+import Stdlib.Function open;
+import Stdlib.Data.Bool.Base open;
+import Stdlib.Data.Nat.Base open;
+import Stdlib.Data.List.Base open;
+import Stdlib.Data.Unit.Base open;
+import Stdlib.Trait.Functor open;
+import Stdlib.Trait.Applicative open;
+import Stdlib.Trait.Foldable.Polymorphic open;
+import Stdlib.Data.Unit.Base open;
+
+trait
+type Monad (m : Type -> Type) :=
+  mkMonad {
+    {{applicative}} : Applicative m;
+    bind : {A B : Type} -> m A -> (A -> m B) -> m B
+  };
+
+open Monad public;
+
+syntax operator >>= seq;
+>>= {A B} {f : Type -> Type} {{Monad f}} (x : f A) (g : A -> f B) : f B := bind x g;