Idris2中mapM与mapM_的等效函数是什么？

首先，这些函数无需自行实现，它们存在于Idris2标准库的Control.Monad模块中，只需显式导入即可使用：

import Control.Monad

如果需要手动基于foldM实现，以下是直观的实现方式：

• sequence：将单子值列表转换为包含列表的单子值

  sequence : Monad m => List (m a) -> m (List a)
  sequence = foldM (\acc, ma => ma >>= \a => pure (acc ++ [a])) []
  

• mapM：先对列表元素映射单子函数，再执行sequence

  mapM : Monad m => (a -> m b) -> List a -> m (List b)
  mapM f = sequence . map f
  

• mapM_：执行所有单子作用，忽略最终结果

  mapM_ : Monad m => (a -> m b) -> List a -> m ()
  mapM_ f = foldM (\(), ma => f ma >> pure ()) ()
  

内容的提问来源于stack exchange，提问作者thor