doc-next-gen

Mathlib.Control.Combinators

Module docstring

{"# Monad combinators, as in Haskell's Control.Monad. "}

joinM definition
{m : Type u → Type u} [Monad m] {α : Type u} (a : m (m α)) : m α
Full source 
/-- Collapses two layers of monadic structure into one,
passing the effects of the inner monad through the outer. -/
def joinM {m : Type u → Type u} [Monad m] {α : Type u} (a : m (m α)) : m α :=
  bind a id
Monadic join operation
Informal description
Given a monad `m` and a nested monadic value `a : m (m α)`, the function `joinM` flattens the two layers of monadic structure into one, resulting in a value of type `m α`. This is equivalent to applying the monadic bind operation with the identity function.
when definition
{m : Type → Type} [Monad m] (c : Prop) [Decidable c] (t : m Unit) : m Unit
Full source 
/-- Executes `t` conditional on `c` holding true, doing nothing otherwise. -/
@[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 :=
  ite c t (pure ())
Conditional monadic execution
Informal description
Given a monad `m`, a proposition `c` with a decision procedure, and a monadic action `t : m Unit`, the function `when` executes `t` if `c` is true, and does nothing (returns `pure ()`) otherwise.
condM definition
{m : Type → Type} [Monad m] {α : Type} (mbool : m Bool) (tm fm : m α) : m α
Full source 
/-- Executes `tm` or `fm` depending on whether the result of `mbool` is `true` or `false`
respectively. -/
def condM {m : Type → Type} [Monad m] {α : Type} (mbool : m Bool) (tm fm : m α) : m α := do
  let b ← mbool
  cond b tm fm
Monadic conditional execution
Informal description
Given a monad `m`, a monadic boolean value `mbool : m Bool`, and two monadic values `tm : m α` and `fm : m α`, the function `condM` executes `tm` if `mbool` evaluates to `true`, and executes `fm` otherwise. The result is a monadic value of type `m α`.
whenM definition
{m : Type → Type} [Monad m] (c : m Bool) (t : m Unit) : m Unit
Full source 
/-- Executes `t` if `c` results in `true`, doing nothing otherwise. -/
@[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 :=
  condM c t (return ())
Monadic conditional execution of unit action
Informal description
Given a monad `m`, a monadic boolean value `c : m Bool`, and a monadic action `t : m Unit`, the function `whenM` executes `t` if `c` evaluates to `true`, and does nothing (returns `pure ()`) otherwise.
Monad.mapM definition
Full source 
@[deprecated List.mapM (since := "2025-04-07"), inherit_doc List.mapM]
def mapM :=
  @List.mapM
Monadic map over a list
Informal description
The function `Monad.mapM` maps a monadic function over a list, collecting the results in the monad. Given a monad `m`, a function `f : α → m β`, and a list `[a₁, a₂, ..., aₙ]`, it applies `f` to each element of the list and combines the results in sequence, returning a monadic value `m [b₁, b₂, ..., bₙ]` where each `bᵢ` is the result of applying `f` to `aᵢ`.
Monad.mapM' definition
Full source 
@[deprecated List.mapM' (since := "2025-04-07"), inherit_doc List.mapM']
def mapM' :=
  @List.mapM'
Strict monadic map over a list
Informal description
The function `mapM'` applies a monadic function `f : α → m β` to each element of a list `[a₁, a₂, ..., aₙ]` and collects the results in sequence, returning a monadic action `m [b₁, b₂, ..., bₙ]` where each `bᵢ` is the result of applying `f` to `aᵢ`.
Monad.join definition
Full source 
@[deprecated joinM (since := "2025-04-07"), inherit_doc joinM]
def join :=
  @joinM
Monadic join operation
Informal description
The function `Monad.join` flattens a nested monadic value `m (m α)` into a single monadic value `m α` for any monad `m`. This is equivalent to applying the monadic bind operation with the identity function.
Monad.filter definition
Full source 
@[deprecated List.filterM (since := "2025-04-07"), inherit_doc List.filterM]
def filter :=
  @List.filterM
Monadic filter for lists
Informal description
The function `Monad.filter` filters elements of a list based on a monadic predicate, retaining only those elements for which the predicate holds in the monadic context.
Monad.foldl definition
Full source 
@[deprecated List.filterM (since := "2025-04-07"), inherit_doc List.foldlM]
def foldl :=
  @List.filterM
Monadic left fold
Informal description
The function `Monad.foldl` performs a left fold over a list within a monadic context. Given a monad `m`, an initial accumulator value `b`, a function `f : β → α → m β`, and a list `[α]`, it sequentially applies `f` to each element of the list, threading the accumulator through the monadic computations.
Monad.cond definition
Full source 
@[deprecated condM (since := "2025-04-07"), inherit_doc condM]
def cond :=
  @condM
Monadic conditional execution
Informal description
The function `Monad.cond` is a monadic conditional execution operator. Given a monad `m`, a monadic boolean value `mbool : m Bool`, and two monadic values `tm : m α` and `fm : m α`, it executes `tm` if `mbool` evaluates to `true`, and executes `fm` otherwise, returning the result as a monadic value of type `m α`.
Monad.sequence definition
{m : Type u → Type v} [Monad m] {α : Type u} : List (m α) → m (List α)
Full source 
/-- Executes a list of monadic actions in sequence, collecting the results. -/
@[deprecated "Use `_root_.sequence` instead." (since := "2025-04-07")]
def sequence {m : Type u → Type v} [Monad m] {α : Type u} : List (m α) → m (List α)
  | [] => return []
  | h :: t => do
    let h' ← h
    let t' ← sequence t
    return (h' :: t')
Sequential execution of monadic actions
Informal description
Given a monad `m` and a list of monadic actions `List (m α)`, this function executes each action in sequence and collects their results into a monadic action `m (List α)`. Specifically: - For an empty list, it returns the empty list inside the monad. - For a non-empty list `h :: t`, it first executes `h` to get a result `h'`, then recursively processes the tail `t` to get `t'`, and finally returns the concatenation `h' :: t'` inside the monad.
Monad.sequence' definition
{m : Type → Type u} [Monad m] {α : Type} : List (m α) → m Unit
Full source 
/-- Executes a list of monadic actions in sequence, discarding the results. -/
@[deprecated "Use `_root_.sequence` instead." (since := "2025-04-07")]
def sequence' {m : Type → Type u} [Monad m] {α : Type} : List (m α) → m Unit
  | [] => return ()
  | h :: t => h *> sequence' t
Sequence monadic actions discarding results
Informal description
Given a monad `m` and a list of monadic actions `List (m α)`, the function executes these actions in sequence and discards their results, returning the unit value `()` of the monad.
Monad.whenb definition
{m : Type → Type} [Monad m] (b : Bool) (t : m Unit) : m Unit
Full source 
/-- Executes `t` if `b` is `true`, doing nothing otherwise.

See also `when` and `whenM`. -/
@[deprecated "Use `if ... then` without `else` in `do` notation instead." (since := "2025-04-07")]
def whenb {m : Type → Type} [Monad m] (b : Bool) (t : m Unit) : m Unit :=
  _root_.cond b t (return ())
Conditional execution of a monadic action
Informal description
Given a monad `m`, a boolean `b`, and a monadic action `t : m Unit`, the function executes `t` if `b` is `true`, and does nothing (returns the unit action) otherwise.
Monad.unlessb definition
{m : Type → Type} [Monad m] (b : Bool) (t : m Unit) : m Unit
Full source 
/-- Executes `t` if `b` is `false`, doing nothing otherwise. -/
@[deprecated "Use `unless` in `do` notation instead." (since := "2025-04-07")]
def unlessb {m : Type → Type} [Monad m] (b : Bool) (t : m Unit) : m Unit :=
  _root_.cond b (return ()) t
Monadic unless condition
Informal description
Given a monad `m` and a boolean condition `b`, the function executes the monadic action `t` if `b` is `false`, otherwise it does nothing (returns the unit action).