feat: binary recursive implementation of List.mapA

Author: digama0

src/Init/Data/List/Control.lean

@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 prelude
 import Init.Control.Basic
 import Init.Data.List.Basic
+import Init.Data.Nat.Log2
 
 namespace List
 universe u v w u₁ u₂
@@ -48,9 +49,15 @@ def mapM {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α 
   loop as []
 
 @[specialize]
-def mapA {m : Type u → Type v} [Applicative m] {α : Type w} {β : Type u} (f : α → m β) : List α → m (List β)
-  | []    => pure []
-  | a::as => List.cons <$> f a <*> mapA f as
+def mapA {m : Type u → Type v} [Applicative m] {α : Type w} {β : Type u} (f : α → m β) (as : List α) : m (List β) :=
+  let rec @[specialize] go : Nat → List α → List α × m (List β → List β)
+    | 0,   []    => ([], pure id)
+    | 0,   a::as => (as, List.cons <$> f a)
+    | n+1, as    =>
+      let (as, f₁) := go n as
+      let (as, f₂) := go n as
+      (as, Function.comp <$> f₁ <*> f₂)
+  (· []) <$> (go as.length.log2 as).2
 
 @[specialize]
 protected def forM {m : Type u → Type v} [Monad m] {α : Type w} (as : List α) (f : α → m PUnit) : m PUnit :=