Applicative variants of Monadic functions

Stream: mathlib4

[Arien Malec]

In the data.list.defs there are functions that are analogues of List.mapIdxM but are defined in terms of Applicative (from a type signature perspective, the only difference is replacing Monad m with Applicative m

I could either:

1. #align the difference away, betting that zero code in mathlib cares about the difference & it's covariant anyway.
2. Create List.mapIdxA variants with the Applicative constraint (with the con that the monadic variants are going to be better maintained over time b/c they are in Std4.

In the Haskell community, people Care Deeply about constraining to the minimum set of laws; I don't get the sense than the Lean community does as much?

[Scott Morrison]

My guess is that in the long run we may end up with none of the "Haskell category theory" in mathlib itself, and that it will all move out to std or a separate library.

[Mario Carneiro]

Note that the monadic functions actually perform better than the applicative ones even when both are applicable, because applicative functors require lots of mapping over closures to do anything with the value. It is a conscious design choice of lean 4 to stick to Monad functions

[Arien Malec]

Cool -- I'll #align away these to the Monad-flavored ones in Std