提问人：thor 提问时间：9/18/2023 更新时间：9/20/2023 访问量：36
idris2 中的 mapM 和 mapM_ 的等价物是什么？
What is the equivalent of mapM and mapM_ in idris2?
问：
我知道有一个函数将一元操作应用于列表并返回一个包含列表的一元值。（例如，参见 Haskell 中的 mapM_ 和 mapM 有什么区别？mapM)
但是我在 idris2 中找不到任何（或底层）函数（截至 0.6.0）。我唯一能找到的就是foldM。mapMmapM_sequence
我是否应该基于 foldM 推出我自己的 mapM 版本，还是在 Idris2 的其他地方提供？
答：
0赞
thor
9/18/2023
#1
为了回答我自己的问题，我刚刚通过试验发现实际上有一个功能（没有出现在谷歌搜索中）：sequence
Prelude.sequence : Applicative f => Traversable t => t (f a) -> f (t a)
它似乎与 Haskell 函数相同，可以用相同的方式定义：sequencemapM
mapM f = sequence . map f
3赞
joel
9/20/2023
#2
我想你想要
traverse : Traversable t => Applicative f => (a -> f b) -> t a -> f (t b)
traverse_ : Applicative f => Foldable t => (a -> f b) -> t a -> f ()
注意。sequence = traverse id
下一个：应用组成，单子不组成
评论