Remark: we can define mapM, mapM₂ and forM using Applicative instead of Monad. Example:

def mapM {m : Type u → Type v} [Applicative m] {α : Type w} {β : Type u} (f : α → m β) : List α → m (List β)
  | []    => pure []
  | a::as => List.cons <$> (f a) <*> mapM as

However, we consider f <$> a <*> b an anti-idiom because the generated code may produce unnecessary closure allocations. Suppose m is a Monad, and it uses the default implementation for Applicative.seq. Then, the compiler expands f <$> a <*> b <*> c into something equivalent to

(Functor.map f a >>= fun g_1 => Functor.map g_1 b) >>= fun g_2 => Functor.map g_2 c

In an ideal world, the compiler may eliminate the temporary closures g_1 and g_2 after it inlines Functor.map and Monad.bind. However, this can easily fail. For example, suppose Functor.map f a >>= fun g_1 => Functor.map g_1 b expanded into a match-expression. This is not unreasonable and can happen in many different ways, e.g., we are using a monad that may throw exceptions. Then, the compiler has to decide whether it will create a join-point for the continuation of the match or float it. If the compiler decides to float, then it will be able to eliminate the closures, but it may not be feasible since floating match expressions may produce exponential blowup in the code size.

Finally, we rarely use mapM with something that is not a Monad.

Users that want to use mapM with Applicative should use mapA instead.

@[inline]

def List.mapM {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m β) (as : List α) : m (List β)

Applies the monadic action f to every element in the list, left-to-right, and returns the list of results.

This implementation is tail recursive. List.mapM' is a a non-tail-recursive variant that may be more convenient to reason about. List.forM is the variant that discards the results and List.mapA is the variant that works with Applicative.

Equations

• List.mapM f as = List.mapM.loop f as []

@[specialize #[]]

def List.mapM.loop {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m β) : List α → List β → m (List β)

Equations

• List.mapM.loop f [] x✝ = pure x✝.reverse
• List.mapM.loop f (a :: as) x✝ = do let __do_lift ← f a List.mapM.loop f as (__do_lift :: x✝)

@[specialize #[]]

def List.mapA {m : Type u → Type v} [Applicative m] {α : Type w} {β : Type u} (f : α → m β) : List α → m (List β)

Applies the applicative action f on every element in the list, left-to-right, and returns the list of results.

If m is also a Monad, then using mapM can be more efficient.

See List.forA for the variant that discards the results. See List.mapM for the variant that works with Monad.

This function is not tail-recursive, so it may fail with a stack overflow on long lists.

Equations

• List.mapA f [] = pure []
• List.mapA f (a :: as) = List.cons <$> f a <*> List.mapA f as

@[specialize #[]]

def List.forM {m : Type u → Type v} [Monad m] {α : Type w} (as : List α) (f : α → m PUnit) : m PUnit

Applies the monadic action f to every element in the list, in order.

List.mapM is a variant that collects results. List.forA is a variant that works on any Applicative.

Equations

• [].forM f = pure PUnit.unit
• (a :: as_1).forM f = do f a as_1.forM f

@[specialize #[]]

def List.forA {m : Type u → Type v} [Applicative m] {α : Type w} (as : List α) (f : α → m PUnit) : m PUnit

Applies the applicative action f to every element in the list, in order.

If m is also a Monad, then using List.forM can be more efficient.

List.mapA is a variant that collects results.

Equations

• [].forA f = pure PUnit.unit
• (a :: as_1).forA f = f a *> as_1.forA f

@[specialize #[]]

def List.filterAuxM {m : Type → Type v} [Monad m] {α : Type} (f : α → m Bool) : List α → List α → m (List α)

Equations

• List.filterAuxM f [] x✝ = pure x✝
• List.filterAuxM f (h :: t) x✝ = do let b ← f h List.filterAuxM f t (bif b then h :: x✝ else x✝)

@[inline]

def List.filterM {m : Type → Type v} [Monad m] {α : Type} (p : α → m Bool) (as : List α) : m (List α)

Applies the monadic predicate p to every element in the list, in order from left to right, and returns the list of elements for which p returns true.

O(|l|).

Example:

#eval [1, 2, 5, 2, 7, 7].filterM fun x => do
  IO.println s!"Checking {x}"
  return x < 3

Checking 1
Checking 2
Checking 5
Checking 2
Checking 7
Checking 7

[1, 2, 2]

Equations

• List.filterM p as = do let as ← List.filterAuxM p as [] pure as.reverse

@[inline]

def List.filterRevM {m : Type → Type v} [Monad m] {α : Type} (p : α → m Bool) (as : List α) : m (List α)

Applies the monadic predicate p on every element in the list in reverse order, from right to left, and returns those elements for which p returns true. The elements of the returned list are in the same order as in the input list.

Example:

#eval [1, 2, 5, 2, 7, 7].filterRevM fun x => do
  IO.println s!"Checking {x}"
  return x < 3

Checking 7
Checking 7
Checking 2
Checking 5
Checking 2
Checking 1

[1, 2, 2]

Equations

• List.filterRevM p as = List.filterAuxM p as.reverse []

@[inline]

def List.filterMapM {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m (Option β)) (as : List α) : m (List β)

Applies a monadic function that returns an Option to each element of a list, collecting the non-none values.

O(|l|).

Example:

#eval [1, 2, 5, 2, 7, 7].filterMapM fun x => do
  IO.println s!"Examining {x}"
  if x > 2 then return some (2 * x)
  else return none

Examining 1
Examining 2
Examining 5
Examining 2
Examining 7
Examining 7

[10, 14, 14]

Equations

• List.filterMapM f as = List.filterMapM.loop f as []

@[specialize #[]]

def List.filterMapM.loop {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m (Option β)) : List α → List β → m (List β)

Equations

• List.filterMapM.loop f [] x✝ = pure x✝.reverse
• List.filterMapM.loop f (a :: as) x✝ = do let __do_lift ← f a match __do_lift with | none => List.filterMapM.loop f as x✝ | some b => List.filterMapM.loop f as (b :: x✝)

@[inline]

def List.flatMapM {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m (List β)) (as : List α) : m (List β)

Applies a monadic function that returns a list to each element of a list, from left to right, and concatenates the resulting lists.

Equations

• List.flatMapM f as = List.flatMapM.loop f as []

@[specialize #[]]

def List.flatMapM.loop {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m (List β)) : List α → List (List β) → m (List β)

Equations

• List.flatMapM.loop f [] x✝ = pure x✝.reverse.flatten
• List.flatMapM.loop f (a :: as) x✝ = do let bs' ← f a List.flatMapM.loop f as (bs' :: x✝)

@[specialize #[]]

def List.foldlM {m : Type u → Type v} [Monad m] {s : Type u} {α : Type w} (f : s → α → m s) (init : s) : List α → m s

Folds a monadic function over a list from the left, accumulating a value starting with init. The accumulated value is combined with the each element of the list in order, using f.

Example:

example [Monad m] (f : α → β → m α) :
    List.foldlM (m := m) f x₀ [a, b, c] = (do
      let x₁ ← f x₀ a
      let x₂ ← f x₁ b
      let x₃ ← f x₂ c
      pure x₃)
  := by rfl

Equations

• List.foldlM x✝¹ x✝ [] = pure x✝
• List.foldlM x✝¹ x✝ (a :: as) = do let s' ← x✝¹ x✝ a List.foldlM x✝¹ s' as

@[simp]

theorem List.foldlM_nil {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [Monad m] {f : β → α → m β} {b : β} : foldlM f b [] = pure b

@[simp]

theorem List.foldlM_cons {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [Monad m] {f : β → α → m β} {b : β} {a : α} {l : List α} : foldlM f b (a :: l) = do let init ← f b a foldlM f init l

@[inline]

def List.foldrM {m : Type u → Type v} [Monad m] {s : Type u} {α : Type w} (f : α → s → m s) (init : s) (l : List α) : m s

Folds a monadic function over a list from the right, accumulating a value starting with init. The accumulated value is combined with the each element of the list in reverse order, using f.

Example:

example [Monad m] (f : α → β → m β) :
  List.foldrM (m := m) f x₀ [a, b, c] = (do
    let x₁ ← f c x₀
    let x₂ ← f b x₁
    let x₃ ← f a x₂
    pure x₃)
  := by rfl

Equations

• List.foldrM f init l = List.foldlM (fun (s : s) (a : α) => f a s) init l.reverse

@[simp]

theorem List.foldrM_nil {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] {f : α → β → m β} {b : β} : foldrM f b [] = pure b

@[specialize #[]]

def List.firstM {m : Type u → Type v} [Alternative m] {α : Type w} {β : Type u} (f : α → m β) : List α → m β

Maps f over the list and collects the results with <|>. The result for the end of the list is failure.

Examples:

• [[], [1, 2], [], [2]].firstM List.head? = some 1
• [[], [], []].firstM List.head? = none
• [].firstM List.head? = none

Equations

• List.firstM f [] = failure
• List.firstM f (a :: as) = (f a <|> List.firstM f as)

@[specialize #[]]

def List.anyM {m : Type → Type u} [Monad m] {α : Type v} (p : α → m Bool) (l : List α) : m Bool

Returns true if the monadic predicate p returns true for any element of l.

O(|l|). Short-circuits upon encountering the first true. The elements in l are examined in order from left to right.

Equations

• List.anyM p [] = pure false
• List.anyM p (a :: as) = do let __do_lift ← p a match __do_lift with | true => pure true | false => List.anyM p as

@[specialize #[]]

def List.allM {m : Type → Type u} [Monad m] {α : Type v} (p : α → m Bool) (l : List α) : m Bool

Returns true if the monadic predicate p returns true for every element of l.

O(|l|). Short-circuits upon encountering the first false. The elements in l are examined in order from left to right.

Equations

• List.allM p [] = pure true
• List.allM p (a :: as) = do let __do_lift ← p a match __do_lift with | true => List.allM p as | false => pure false

@[specialize #[]]

def List.findM? {m : Type → Type u} [Monad m] {α : Type} (p : α → m Bool) : List α → m (Option α)

Returns the first element of the list for which the monadic predicate p returns true, or none if no such element is found. Elements of the list are checked in order.

O(|l|).

Example:

#eval [7, 6, 5, 8, 1, 2, 6].findM? fun i => do
  if i < 5 then
    return true
  if i ≤ 6 then
    IO.println s!"Almost! {i}"
  return false

Almost! 6
Almost! 5

some 1

Equations

• List.findM? p [] = pure none
• List.findM? p (a :: as) = do let __do_lift ← p a match __do_lift with | true => pure (some a) | false => List.findM? p as

@[simp]

theorem List.findM?_pure {α : Type} {m : Type → Type u_1} [Monad m] [LawfulMonad m] (p : α → Bool) (as : List α) : findM? (fun (x : α) => pure (p x)) as = pure (find? p as)

@[simp]

theorem List.findM?_id {α : Type} (p : α → Bool) (as : List α) : findM? p as = find? p as

@[specialize #[]]

def List.findSomeM? {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m (Option β)) : List α → m (Option β)

Returns the first non-none result of applying the monadic function f to each element of the list, in order. Returns none if f returns none for all elements.

O(|l|).

Example:

#eval [7, 6, 5, 8, 1, 2, 6].findSomeM? fun i => do
  if i < 5 then
    return some (i * 10)
  if i ≤ 6 then
    IO.println s!"Almost! {i}"
  return none

Almost! 6
Almost! 5

some 10

Equations

• List.findSomeM? f [] = pure none
• List.findSomeM? f (a :: as) = do let __do_lift ← f a match __do_lift with | some b => pure (some b) | none => List.findSomeM? f as

@[simp]

theorem List.findSomeM?_pure {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] [LawfulMonad m] {f : α → Option β} {as : List α} : findSomeM? (fun (x : α) => pure (f x)) as = pure (findSome? f as)

@[simp]

theorem List.findSomeM?_id {α : Type u_1} {β : Type u_2} {f : α → Option β} {as : List α} : findSomeM? f as = findSome? f as

theorem List.findM?_eq_findSomeM? {m : Type → Type u_1} {α : Type} [Monad m] [LawfulMonad m] {p : α → m Bool} {as : List α} : findM? p as = findSomeM? (fun (a : α) => do let __do_lift ← p a pure (if __do_lift = true then some a else none)) as

@[inline]

def List.forIn' {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : List α) (init : β) (f : (a : α) → a ∈ as → β → m (ForInStep β)) : m β

Equations

• as.forIn' init f = List.forIn'.loop as f as init ⋯

@[specialize #[]]

def List.forIn'.loop {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : List α) (f : (a : α) → a ∈ as → β → m (ForInStep β)) (as' : List α) (b : β) : (∃ (bs : List α), bs ++ as' = as) → m β

Equations

• One or more equations did not get rendered due to their size.
• List.forIn'.loop as f [] x x_3 = pure x

instance List.instForIn'InferInstanceMembership {m : Type u_1 → Type u_2} {α : Type u_3} : ForIn' m (List α) α inferInstance

Equations

• List.instForIn'InferInstanceMembership = { forIn' := fun {β : Type ?u.15} [Monad m] => List.forIn' }

@[simp]

theorem List.forIn'_eq_forIn' {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] : List.forIn' = forIn'

@[simp]

theorem List.forIn'_nil {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] {f : (a : α) → a ∈ [] → β → m (ForInStep β)} {b : β} : forIn' [] b f = pure b

@[simp]

theorem List.forIn_nil {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] {f : α → β → m (ForInStep β)} {b : β} : forIn [] b f = pure b

instance List.instForM {m : Type u_1 → Type u_2} {α : Type u_3} : ForM m (List α) α

Equations

• List.instForM = { forM := fun [Monad m] => List.forM }

@[simp]

theorem List.forM_eq_forM {m : Type u_1 → Type u_2} {α : Type u_3} [Monad m] : List.forM = forM

@[simp]

theorem List.forM_nil {m : Type u_1 → Type u_2} {α : Type u_3} [Monad m] {f : α → m PUnit} : forM [] f = pure PUnit.unit

@[simp]

theorem List.forM_cons {m : Type u_1 → Type u_2} {α : Type u_3} [Monad m] {f : α → m PUnit} {a : α} {as : List α} : forM (a :: as) f = do f a forM as f

instance List.instFunctor : Functor List

Equations

• List.instFunctor = { map := fun {α β : Type ?u.9} => List.map }