What is the equivalent of mapM and mapM_ in idris2?

Question

I know there is the mapM function that applies a monadic action to a list and returns one monadic value containing a list. (See e.g. What is the difference between mapM_ and mapM in Haskell?)

But I couldn't find any mapM (or mapM_ or the underlying sequence) function in idris2 (as of 0.6.0). The only thing I could find is a foldM.

Am I expected to roll out my own version of mapM based on foldM, or is it provided elsewhere in Idris2?

Answer 1

I think you want

traverse : Traversable t => Applicative f => (a -> f b) -> t a -> f (t b)

and

traverse_ : Applicative f => Foldable t => (a -> f b) -> t a -> f ()

Note sequence = traverse id.

Answer 2

To answer my own question, I just found by trial that there is actually a sequence function (which didn't show up in a Google search):

Prelude.sequence : Applicative f => Traversable t => t (f a) -> f (t a)

It seems to be the same as Haskell's sequence function, and mapM can be defined the same way as:

mapM f = sequence . map f