mapM'

Stream: mathlib4

[Ruben Van de Velde]

The following are #aligned in Mathlib/Init/Control/Combinators.lean - is that right?

def list.mmap' {m : Type → Type v} [monad m] {α : Type u} {β : Type} (f : α → m β) : list α → m unit
def mapM' [Monad m] (f : α → m β) : List α → m (List β)

[Yakov Pechersky]

I might have slipped in an extra apostrophe somewhere

[Scott Morrison]

Yes, usually the primed versions are the "return nothing" versions.

[Arien Malec]

really? not the Haskell convention of lazy vs strict?

[Scott Morrison]

Nope. There's no such distinction here.

[Mario Carneiro]

The naming convention for "return nothing" map functions is forM

[Mario Carneiro]

e.g docs4#List.forM

[Eric Wieser]

Is there a "return nothing" version of docs4#List.foldrM / docs#list.foldrm?

[Mario Carneiro]

No, I don't think there is a more efficient implementation than l.reverse.forM ... anyway

[Mario Carneiro]

actually I guess foldrM is a bit more different than that

[Mario Carneiro]

Unlike discard <| mapM, I don't really see the advantage of having a separate function for discard <| foldrM since you have to construct the final state s anyway because you have to pass it through the list

[Trebor Huang]

Haskell uses underlines for the "return nothing" version, iirc.