monadsidrisidris2

What is the equivalent of mapM and mapM_ in idris2?

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?

Solution

  • 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.