idris2中的mapM和mapM_相当于什么？

Question

我知道有一个

mapM

函数，它将一元操作应用于列表并返回一个包含列表的一元值。 （参见例如 Haskell中的mapM_和mapM有什么区别？）

但我在 idris2 中找不到任何

mapM

（或

mapM_

或底层

sequence

）函数（截至 0.6.0）。我唯一能找到的是foldM。

我是否期望基于

mapM 

推出我自己的

foldM

版本，还是在 Idris2 的其他地方提供它？

Answer 1

为了回答我自己的问题，我刚刚通过试验发现实际上有一个

sequence

功能（谷歌搜索中没有显示）：

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

它似乎与Haskell的

sequence

函数相同，并且

mapM

可以以相同的方式定义为：

mapM f = sequence . map f

Answer 2

我想你想要

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

注意

sequence = traverse id

。