Monad combinators, as in Haskell's Control.Monad. #

source

def joinM {m : Type u → Type u} [Monad m] {α : Type u} (a : m (m α)) :

m α

Collapses two layers of monadic structure into one, passing the effects of the inner monad through the outer.

Equations

joinM a = a >>= id

source

@[deprecated "Use `if c then t` without `else` in `do` notation instead." (since := "2025-04-07")]

def when {m : Type → Type} [Monad m] (c : Prop) [Decidable c] (t : m Unit) :

m Unit

Executes t conditional on c holding true, doing nothing otherwise.

Equations

when c t = if c then t else pure ()

source

def condM {m : Type → Type} [Monad m] {α : Type} (mbool : m Bool) (tm fm : m α) :

m α

Executes tm or fm depending on whether the result of mbool is true or false respectively.

Equations

condM mbool tm fm = do let b ← mbool bif b then tm else fm

source

@[deprecated "Use `if ← c then t` without `else` in `do` notation instead." (since := "2025-04-07")]

def whenM {m : Type → Type} [Monad m] (c : m Bool) (t : m Unit) :

m Unit

Executes t if c results in true, doing nothing otherwise.

Equations

whenM c t = condM c t (pure ())

source

@[deprecated List.mapM (since := "2025-04-07")]

def Monad.mapM {m : Type u_1 → Type u_2} [Monad m] {α : Type u_3} {β : Type u_1} (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

@Monad.mapM = @List.mapM

source

@[deprecated List.mapM' (since := "2025-04-07")]

def Monad.mapM' {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [Monad m] (f : α → m β) :

List α → m (List β)

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

@Monad.mapM' = @List.mapM'

source

@[deprecated joinM (since := "2025-04-07")]

def Monad.join {m : Type u_1 → Type u_1} [Monad m] {α : Type u_1} (a : m (m α)) :

m α

Collapses two layers of monadic structure into one, passing the effects of the inner monad through the outer.

Equations

@Monad.join = @joinM

source

@[deprecated List.filterM (since := "2025-04-07")]

def Monad.filter {m : Type → Type u_1} [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

@Monad.filter = @List.filterM

source

@[deprecated List.filterM (since := "2025-04-07")]

def Monad.foldl {m : Type → Type u_1} [Monad m] {α : Type} (p : α → m Bool) (as : List α) :

m (List α)

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