add Applicative instances

anoma · Jul 31, 2024 · e28df3f · e28df3f
1 parent 1dd3cbd
commit e28df3f
Show file tree

Hide file tree

Showing 5 changed files with 34 additions and 7 deletions.
diff --git a/Stdlib/Data/List.juvix b/Stdlib/Data/List.juvix
@@ -8,7 +8,7 @@ import Stdlib.Function open;
 import Stdlib.Trait.Eq open;
 import Stdlib.Trait.Ord open;
 import Stdlib.Trait.Show open;
-import Stdlib.Trait.Functor open;
+import Stdlib.Trait open;
 import Stdlib.Trait.Partial open;
 import Stdlib.Trait.Foldable open using {Foldable; module Polymorphic; fromPolymorphicFoldable};
 
@@ -71,3 +71,12 @@ polymorphicFoldableListI : Polymorphic.Foldable List :=
 
 instance
 foldableListI {A} : Foldable (List A) A := fromPolymorphicFoldable;
+
+instance
+applicativeListI : Applicative List :=
+  mkApplicative@{
+    pure {A} (a : A) : List A := [a];
+    ap {A B} : List (A -> B) -> List A -> List B
+      | [] _ := []
+      | (f :: fs) l := map f l ++ ap fs l
+  };
diff --git a/Stdlib/Data/Maybe.juvix b/Stdlib/Data/Maybe.juvix
@@ -6,6 +6,7 @@ import Stdlib.Trait.Eq open;
 import Stdlib.Trait.Ord open;
 import Stdlib.Trait.Show open;
 import Stdlib.Trait.Functor open;
+import Stdlib.Trait.Applicative open;
 
 import Stdlib.Data.Bool.Base open;
 import Stdlib.Data.String.Base open;
@@ -47,3 +48,12 @@ functorMaybeI : Functor Maybe :=
 
 instance
 monomorphicFunctorMaybeI {A} : Monomorphic.Functor (Maybe A) A := fromPolymorphicFunctor;
+
+instance
+applicativeMaybeI : Applicative Maybe :=
+  mkApplicative@{
+    pure := just;
+    ap {A B} : Maybe (A -> B) -> Maybe A -> Maybe B
+      | (just f) (just x) := just (f x)
+      | _ _ := nothing;
+  };
diff --git a/Stdlib/Data/Result.juvix b/Stdlib/Data/Result.juvix
@@ -5,7 +5,7 @@ import Stdlib.Data.Bool.Base open;
 
 import Stdlib.Trait.Eq open;
 import Stdlib.Trait.Ord open;
-import Stdlib.Trait.Functor open;
+import Stdlib.Trait open;
 
 instance
 ordResultI {A B} {{Ord A}} {{Ord B}} : Ord (Result A B) :=
@@ -35,3 +35,13 @@ functorResultI {err} : Functor (Result err) :=
 instance
 monomorphicFunctorResultI {err res} : Monomorphic.Functor (Result err res) res :=
   fromPolymorphicFunctor;
+
+instance
+applicativeResultI {err} : Applicative (Result err) :=
+  mkApplicative@{
+    pure := ok;
+    ap {A B} : Result err (A -> B) -> Result err A -> Result err B
+      | (ok f) (ok x) := ok (f x)
+      | (ok _) (error e) := error e
+      | (error e) _ := error e
+  };
diff --git a/Stdlib/Trait.juvix b/Stdlib/Trait.juvix
@@ -4,6 +4,7 @@ import Stdlib.Trait.Eq as Eq open using {Eq; module Eq} public;
 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.Foldable open public;
 import Stdlib.Trait.Partial open public;
 import Stdlib.Trait.Natural open public;

diff --git a/Stdlib/Trait/Applicative.juvix b/Stdlib/Trait/Applicative.juvix
@@ -6,16 +6,13 @@ import Stdlib.Trait.Functor open;
 trait
 type Applicative (f : Type -> Type) :=
   mkApplicative {
-    functor : Functor f;
+    {{functor}} : Functor f;
     pure : {A : Type} -> A -> f A;
     ap : {A B : Type} -> f (A -> B) -> f A -> f B
   };
 
 open Applicative public;
 
-syntax operator <*> lapp;
-syntax alias <*> := ap;
-
 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;
+  ap (map λ {_ b := b} fa) fb;