Add Functor, Applicative and Monad traits

Stdlib/Data/Applicative.juvix

@@ -0,0 +1,22 @@
+module Stdlib.Data.Applicative;
+
+import Stdlib.Data.Fixity open;
+import Stdlib.Data.Functor open;
+
+trait
+type Applicative (f : Type -> Type) :=
+  mkApplicative {
+    functor : Functor f;
+    pure : {A : Type} -> A -> f A;
+    apply : {A B : Type} -> f (A -> B) -> f A -> f B
+  };
+
+open Applicative public;
+
+syntax operator <*> lapp;
+syntax alias <*> := apply;
+
+syntax operator >> seq;
+>> {f : Type -> Type} {{I : Applicative
+  f}} {A B : Type} (fa : f A) (fb : f B) : f B :=
+  map {{functor}} λ {_ b := b} fa <*> fb;

Stdlib/Data/Functor.juvix

@@ -0,0 +1,23 @@
+module Stdlib.Data.Functor;
+
+import Stdlib.Data.Fixity open;
+import Stdlib.Data.Unit open;
+
+trait
+type Functor (f : Type -> Type) :=
+  mkFunctor {
+  -- TODO what about calling it map? (like in Lean)
+  -- YES
+    map : {A B : Type} -> (A -> B) -> f A -> f B
+  };
+
+open Functor public;
+
+syntax operator <$> lapp;
+syntax alias <$> := map;
+
+syntax operator $> lapp;
+$> {f : Type → Type} {A B : Type} {{Functor f}} (fa : f A) (b : B) : f B :=
+  λ {_ := b} <$> fa;
+
+void {f : Type → Type} {A : Type} {{Functor f}} (fa : f A) : f Unit := fa $> unit;

Stdlib/Data/Maybe.juvix

@@ -8,6 +8,10 @@ import Stdlib.Trait.Show open;
 
 import Stdlib.Data.Bool.Base open;
 import Stdlib.Data.String.Base open;
+import Stdlib.Data.Functor open;
+import Stdlib.Data.Applicative open;
+import Stdlib.Data.Monad open;
+import Stdlib.Function open;
 
 instance
 eqMaybeI {A} {{Eq A}} : Eq (Maybe A) :=
@@ -35,3 +39,32 @@ ordMaybeI {A} {{Ord A}} : Ord (Maybe A) :=
       | nothing (just _) := LT
       | (just _) nothing := GT
     };
+
+instance
+Functor-Maybe : Functor Maybe :=
+  mkFunctor@{
+    map {A B} (f : A -> B) : Maybe A -> Maybe B
+      | nothing := nothing
+      | (just a) := just (f a)
+  };
+
+instance
+Applicative-Maybe : Applicative Maybe :=
+  mkApplicative@{
+    functor := Functor-Maybe;
+    pure {A} (a : A) : Maybe A := just a;
+    apply {A B} : Maybe (A -> B) -> Maybe A -> Maybe B
+      | (just f) := map f
+      | nothing := const nothing
+  };
+
+instance
+Monad-Maybe : Monad Maybe :=
+  mkMonad@{
+    applicative := Applicative-Maybe;
+    bind {A B} (ma : Maybe A) (f : A -> Maybe B) : Maybe B :=
+      case ma of {
+        | just a := f a
+        | nothing := nothing
+      }
+  };

Stdlib/Data/Monad.juvix

@@ -0,0 +1,17 @@
+module Stdlib.Data.Monad;
+
+import Stdlib.Data.Fixity open;
+import Stdlib.Data.Functor open;
+import Stdlib.Data.Applicative open;
+
+trait
+type Monad (f : Type -> Type) :=
+  mkMonad {
+    applicative : Applicative f;
+    bind : {A B : Type} -> f A -> (A -> f B) -> f B;
+  };
+
+open Monad public;
+
+syntax operator >>= seq;
+syntax alias >>= := bind;