Monad combinators, as in Haskell's Control.Monad. #
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
Instances For
Applies the monadic action f on every element in the list, left-to-right, and returns the list of
results.
This is a non-tail-recursive variant of List.mapM that's easier to reason about. It cannot be used
as the main definition and replaced by the tail-recursive version because they can only be proved
equal when m is a LawfulMonad.
Equations
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
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