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} [inst : Monad m] {α : Type w} {β : Type u} (f : α → m β) (as : List α) : m (List β)

Equations

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

@[specialize #[]]

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

Equations

• List.mapM.loop f [] x = pure (List.reverse x)
• 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} [inst : Applicative m] {α : Type w} {β : Type u} (f : α → m β) : List α → m (List β)

Equations

• List.mapA f [] = pure []
• List.mapA f (a :: as) = Seq.seq (List.cons <$> f a) fun x => List.mapA f as

@[specialize #[]]

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

Equations

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

@[specialize #[]]

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

Equations

• List.forA [] f = pure PUnit.unit
• List.forA (a :: as_1) f = SeqRight.seqRight (f a) fun x => List.forA as_1 f

@[specialize #[]]

def List.filterAuxM {m : Type → Type v} [inst : 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} [inst : Monad m] {α : Type} (f : α → m Bool) (as : List α) : m (List α)

Equations

• List.filterM f as = do let as ← List.filterAuxM f as [] pure (List.reverse as)

@[inline]

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

Equations

• List.filterRevM f as = List.filterAuxM f (List.reverse as) []

@[inline]

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

Equations

• List.filterMapM f as = List.filterMapM.loop f (List.reverse as) []

@[specialize #[]]

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

Equations

• List.filterMapM.loop f [] x = pure x
• 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} [inst : Monad m] {s : Type u} {α : Type w} (f : s → α → m s) (init : s) : List α → m s

Equations

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

@[inline]

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

Equations

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

@[specialize #[]]

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

Equations

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

@[specialize #[]]

def List.anyM {m : Type → Type u} [inst : 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} [inst : 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} [inst : 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} [inst : 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} [inst : Monad m] (as : List α) (init : β) (f : α → β → m (ForInStep β)) : m β

Equations

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

@[specialize #[]]

def List.forIn.loop {α : Type u} {β : Type v} {m : Type v → Type w} [inst : 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.instForInList {m : Type u_1 → Type u_2} {α : Type u_3} : ForIn m (List α) α

Equations

• List.instForInList = { forIn := fun {β} [Monad m] => List.forIn }

@[simp]

theorem List.forIn_nil {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : 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} [inst : 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} [inst : Monad m] (as : List α) (init : β) (f : (a : α) → a ∈ as → β → m (ForInStep β)) : m β

Equations

• List.forIn' as init f = List.forIn'.loop as f as init (_ : ∃ bs, bs ++ as = as)

@[specialize #[]]

def List.forIn'.loop {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (as : List α) (f : (a : α) → a ∈ as → β → m (ForInStep β)) (as' : List α) (b : β) : (∃ bs, 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'ListInferInstanceMembershipInstMembershipList {m : Type u_1 → Type u_2} {α : Type u_3} : ForIn' m (List α) α inferInstance

Equations

• List.instForIn'ListInferInstanceMembershipInstMembershipList = { forIn' := fun {β} [Monad m] => List.forIn' }

@[simp]

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

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

Equations

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

@[simp]

theorem List.forM_nil {m : Type u_1 → Type u_2} {α : Type u_3} [inst : 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} [inst : Monad m] (f : α → m PUnit) (a : α) (as : List α) : forM (a :: as) f = do f a forM as f

instance List.instFunctorList : Functor List

Equations

• List.instFunctorList = { map := fun {α β} => List.map, mapConst := fun {α β} => List.map ∘ Function.const β }