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 on every element in the list, left-to-right, and returns the list of results.

See List.forM for the variant that discards the results. See List.mapA for 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.

NB: 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.

Warning: this function is not tail-recursive, meaning that it may fail with a stack overflow on long lists.

Equations

• List.mapA f [] = pure []
• List.mapA f (a :: as) = Seq.seq (List.cons <$> f a) fun (x : Unit) => 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 on every element in the list, left-to-right.

See List.mapM for the variant that collects results. See List.forA for the variant that works with 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 on every element in the list, left-to-right.

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

See List.mapA for the variant that collects results. See List.forM for the variant that works with Monad.

Equations

• [].forA f = pure PUnit.unit
• (a :: as_1).forA f = SeqRight.seqRight (f a) fun (x : Unit) => 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 on every element in the list, left-to-right, and returns those elements x for which p x returns true.

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, right-to-left, and returns those elements x for which p x returns true.

Equations

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

@[inline]

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

Applies the monadic function f on every element x in the list, left-to-right, and returns those results y for which f x returns some y.

Equations

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

@[specialize #[]]

def List.filterMapM.loop {m : Type u → Type v} [Monad m] {α : Type u} {β : 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)

@[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 left to right:

foldlM f x₀ [a, b, c] = do
  let x₁ ← f x₀ a
  let x₂ ← f x₁ b
  let x₃ ← f x₂ c
  pure x₃

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 : β) : List.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 α) : List.foldlM f b (a :: l) = do let init ← f b a List.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 right to left:

foldrM f x₀ [a, b, c] = do
  let x₁ ← f c x₀
  let x₂ ← f b x₁
  let x₃ ← f a x₂
  pure x₃

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 : β) : List.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 <|>.

firstM f [a, b, c] = f a <|> f b <|> f c <|> failure

Equations

• List.firstM f [] = failure
• List.firstM f (a :: as) = HOrElse.hOrElse (f a) fun (x : Unit) => List.firstM f as

@[specialize #[]]

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

Equations

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

@[specialize #[]]

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

Equations

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

@[specialize #[]]

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

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

@[specialize #[]]

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

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

@[inline]

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

Equations

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

@[specialize #[]]

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

Equations

• List.forIn.loop f [] x = pure x
• List.forIn.loop f (a :: as) x = do let __do_lift ← f a x match __do_lift with | ForInStep.done b => pure b | ForInStep.yield b => List.forIn.loop f as b

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

Equations

• List.instForIn = { forIn := fun {β : Type ?u.20} [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 : α → β → m (ForInStep β)) (b : β) : forIn [] b f = pure b

@[simp]

theorem List.forIn_cons {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → β → m (ForInStep β)) (a : α) (as : List α) (b : β) : forIn (a :: as) b f = do let x ← f a b match x with | ForInStep.done b => pure b | ForInStep.yield b => forIn as b f

@[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.20} [Monad m] => List.forIn' }

@[simp]

theorem List.forIn'_eq_forIn {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : List α) (init : β) (f : α → β → m (ForInStep β)) : (forIn' as init fun (a : α) (x : a ∈ as) (b : β) => f a b) = forIn as init f

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_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.10} => List.map, mapConst := fun {α β : Type ?u.10} => List.map ∘ Function.const β }