RFC: Add Array.mapA

I have noticed List has mapA but Array doesnt. Same in batteries - List has traverse but Array doesnt.

I propose adding the following implementation:

def mapA {m : Type u → Type v} [Applicative m] {α : Type w} {β : Type u} (f : α → m β) (as : Array α) : m (Array β) :=
  as.foldl (fun macc x => (fun acc y => acc.push y) <$> macc <*> f x) (pure (Array.emptyWithCapacity as.size))

I suppose it was not added bc of performance worries. But maybe can use @[csimp] to optimize for known monads? Or is there other way?

• User Experience: This provides a standard way to map Applicative effects over Arrays, consistent with the existing List API.
• Beneficiaries: Users working with Array who currently have to convert to List and back to perform effectful operations.
• Maintainability: This reduces boilerplate for users and aligns Array with other traversable collections in the standard library.

Community Feedback

https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/RFC.3A.20Add.20Array.2EmapA

Impact

This would allow for more ergonomic and performant code when working with Array and Applicative functors. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

Start by reading the linked List.mapA implementation in Init/Data/List/Control.lean and the Array/List traversal context in Batteries/Data/List/Basic.lean. Review the linked Zulip discussion and performance question before proposing changes. Done means the API and optimization approach are agreed and the resulting Array.mapA work is accepted.