From ea4faec54aee546c935c637d91b7298888be9986 Mon Sep 17 00:00:00 2001
From: Jan Mas Rovira <janmasrovira@gmail.com>
Date: Wed, 31 Jul 2024 16:34:31 +0200
Subject: [PATCH] add liftA2, mapA_, replicateA

---
 Stdlib/Data/Unit.juvix         |  2 +-
 Stdlib/Trait/Applicative.juvix | 21 +++++++++++++++++++--
 2 files changed, 20 insertions(+), 3 deletions(-)

diff --git a/Stdlib/Data/Unit.juvix b/Stdlib/Data/Unit.juvix
index d5c17ba1..624289e7 100644
--- 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
index 54f08164..d556da7c 100644
--- 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;