add liftA2, mapA_, replicateA

anoma · Aug 5, 2024 · ea4faec · ea4faec
1 parent 51dc4d6
commit ea4faec
Show file tree

Hide file tree

Showing 2 changed files with 20 additions and 3 deletions.
diff --git a/Stdlib/Data/Unit.juvix b/Stdlib/Data/Unit.juvix
@@ -1,7 +1,7 @@
 --- The unit type.
 module Stdlib.Data.Unit;
 
-import Stdlib.Data.Unit.Base open;
+import Stdlib.Data.Unit.Base open public;
 import Stdlib.Data.Bool.Base open;
 
 import Stdlib.Trait.Eq open;

diff --git a/Stdlib/Trait/Applicative.juvix b/Stdlib/Trait/Applicative.juvix
@@ -1,6 +1,11 @@
 module Stdlib.Trait.Applicative;
 
 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.Foldable.Polymorphic open;
 import Stdlib.Data.Unit.Base open;
@@ -20,8 +25,12 @@ open Applicative public;
 applicativeSeq {f : Type -> Type} {{Applicative f}} {A B : Type} (fa : f A) (fb : f B) : f B :=
   ap (map λ {_ b := b} fa) fb;
 
-syntax iterator mapM_ {init := 0; range := 1};
-mapM_
+--- lifts a binary function to ;Applicative;
+liftA2 {f : Type -> Type} {{Applicative f}} {A B C} (fun : A -> B -> C) : f A -> f B -> f C :=
+  map fun >> ap;
+
+syntax iterator mapA_ {init := 0; range := 1};
+mapA_
   {t : Type -> Type}
   {f : Type -> Type}
   {A B}
@@ -30,3 +39,11 @@ mapM_
   (fun : A -> f B)
   (l : t A)
   : f Unit := rfor (acc := pure unit) (x in l) {applicativeSeq (fun x) acc};
+
+replicateA {f : Type -> Type} {A} {{Applicative f}} : Nat -> f A -> f (List A)
+  | zero _ := pure []
+  | (suc n) x := liftA2 (::) x (replicateA n x);
+
+when {f : Type -> Type} {{Applicative f}} : Bool -> f Unit -> f Unit
+  | false _ := pure unit
+  | true a := a;