feat: binary recursive implementation of List.mapA

[digama0]

Inspired by https://github.com/leanprover/lean4/pull/3867#discussion_r1559543688 . After playing with this function a bit more, I was able to confirm that it's not really possible to implement it tail recursively in most monads (note that tail-recursiveness depends on the monad itself), because seq is not tail recursive in most monads and you have to stack up at least n-1 of them to reduce a list of length n. However, we can do the next best thing which is to use a balanced tree of seq applications. I have confirmed that this will evaluate

#eval List.mapA (m := StateT Nat Id) pure (List.range 10000) |>.run 1

without stack overflow, unlike the original implementation, but it still deserves a !bench because the binary reduction has overhead and it may be worthwhile to switch over to naive recursion below some threshold.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-3877 has successfully built against this PR. (2024-04-11 02:37:20) View Log
• ✅ Mathlib branch lean-pr-testing-3877 has successfully built against this PR. (2024-04-11 04:14:27) View Log
• ✅ Mathlib branch lean-pr-testing-3877 has successfully built against this PR. (2024-04-22 06:21:55) View Log

[david-christiansen]

!bench

[leanprover-bot]

Here are the benchmark results for commit f405eb453f1c236a3943cd136c33cd402e404bf9. There were no significant changes against commit d988849ce31462fe7548a876a0317e8deaaeff6e.

[digama0]

(note: the benchmark is useless because List.mapA is unused in core)

[kim-em]

Could you add a doc-string explaining at least that the complicated implementation is for performance, and ideally explaining why tail-recursiveness is impossible and that this is "the next best thing"?