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.

source
@[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 []

Instances For

source
@[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✝)

Instances For

source
@[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

Instances For

source
@[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_2).forM f = do f a as_2.forM f

Instances For

source
@[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

Instances For

source
@[inline]
def List.zipWithM {m : Type u → Type v} [Monad m] {α : Type w} {β : Type x} {γ : Type u} (f : α → β → m γ) (as : List α) (bs : List β) :
m (List γ)

Applies the monadic action `f` to the corresponding elements of two lists, left-to-right, stopping at the end of the shorter list. `zipWithM f as bs` is equivalent to `mapM id (zipWith f as bs)` for lawful `Monad` instances.

This implementation is tail recursive. `List.zipWithM'` is a a non-tail-recursive variant that may be more convenient to reason about.

Equations

- List.zipWithM f as bs = List.zipWithM.loop f as bs #[]

Instances For

source
@[specialize #[]]
def List.zipWithM.loop {m : Type u → Type v} [Monad m] {α : Type w} {β : Type x} {γ : Type u} (f : α → β → m γ) :
List α → List β → Array γ → m (List γ)
Equations

- List.zipWithM.loop f (a :: as) (b :: bs) x✝ = do let __do_lift ← f a b List.zipWithM.loop f as bs (x✝.push __do_lift)
- List.zipWithM.loop f x✝² x✝¹ x✝ = pure x✝.toList

Instances For

source
@[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✝)

Instances For

source
@[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

Instances For

source
@[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 []

Instances For

source
@[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 []

Instances For

source
@[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✝)

Instances For

source
@[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 []

Instances For

source
@[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✝)

Instances For

source
@[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

Instances For

source
@[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
source
@[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
source
@[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

Instances For

source
@[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
source
@[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)

Instances For

source
@[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

Instances For

source
@[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

Instances For

source
@[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

Instances For

source
@[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)
source
@[simp]
theorem List.idRun_findM? {α : Type} (p : α → Id Bool) (as : List α) :
(findM? p as).run = find? (fun (x : α) => (p x).run) as
source
@[deprecated List.idRun_findM? (since := "2025-05-21")]
theorem List.findM?_id {α : Type} (p : α → Id Bool) (as : List α) :
findM? p as = find? p as
source
@[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

Instances For

source
@[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)
source
@[simp]
theorem List.idRun_findSomeM? {α : Type u_1} {β : Type u_2} (f : α → Id (Option β)) (as : List α) :
(findSomeM? f as).run = findSome? (fun (x : α) => (f x).run) as
source
@[deprecated List.idRun_findSomeM? (since := "2025-05-21")]
theorem List.findSomeM?_id {α : Type u_1} {β : Type u_2} (f : α → Id (Option β)) (as : List α) :
findSomeM? f as = findSome? f as
source
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
source
@[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 ⋯

Instances For

source
@[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

Instances For

source
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' }

source
@[simp]
theorem List.forIn'_eq_forIn' {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] :
List.forIn' = forIn'
source
@[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
source
@[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
source
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 }

source
@[simp]
theorem List.forM_eq_forM {m : Type u_1 → Type u_2} {α : Type u_3} [Monad m] :
List.forM = forM
source
@[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
source
@[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
source
instance List.instFunctor :
Functor List
Equations

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