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.
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
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.
Instances For
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.
Instances For
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.
Instances For
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
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
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
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
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
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
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
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
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
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
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
Instances For
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
Instances For
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
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
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
Equations
- List.instForIn'InferInstanceMembership = { forIn' := fun {β : Type ?u.15} [Monad m] => List.forIn' }
Equations
- List.instFunctor = { map := fun {α β : Type ?u.9} => List.map }