feat: binary recursive implementation of List.mapA

[digama0]

Inspired by #3867 (comment) . 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.

[ghost]

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 f405eb4.
There were no significant changes against commit d988849.

[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"?

[srghma]

@digama0

not really possible to implement it tail recursively in most monads

what are these monads? maybe for these monads possible to create

class CanImplementTailRecursivenessFor m where
  proof_x : ...

and then write in docstring for List.mapA - "hey, if You want List.mapA to work faster for Your monad then proove/add class CanImplementTailRecursivenessFor for it"

and if monad has CanImplementTailRecursivenessFor then we enable optimization using @[csimp]

[kim-em]

This hasn't been touched in over a year, and has a merge conflict. I'm closing now; please re-open if you think appropriate.