7.4. API Reference

In addition to the general functions described here, there are some functions that are conventionally defined as part of the API of in the namespace of each collection type:

mapM maps a monadic function.
forM maps a monadic function, throwing away the result.
filterM filters using a monadic predicate, returning the values that satisfy it.

Monadic Collection Operations

Array.filterM can be used to write a filter that depends on a side effect.

def values := #[1, 2, 3, 5, 8]
def main : IO Unit := do
  let filtered ← values.filterM fun v => do
    repeat
      IO.println s!"Keep {v}? [y/n]"
      let answer := (← (← IO.getStdin).getLine).trim
      if answer == "y" then return true
      if answer == "n" then return false
    return false
  IO.println "These values were kept:"
  for v in filtered do
    IO.println s!" * {v}"

              stdinynoopsyny

              stdoutKeep 1? [y/n]Keep 2? [y/n]Keep 3? [y/n]Keep 3? [y/n]Keep 5? [y/n]Keep 8? [y/n]These values were kept: * 1 * 3 * 8

7.4.1. Discarding Results

The discard function is especially useful when using an action that returns a value only for its side effects.

def

Functor.discard.{u, v} {f : Type u → Type v}
    {α : Type u} [Functor f] (x : f α) : f PUnit

7.4.2. Control Flow

def

guard.{v} {f : Type → Type v} [Alternative f]
    (p : Prop) [Decidable p] : f Unit

If the proposition p is true, does nothing, else fails (using failure).

def

optional.{u, v} {f : Type u → Type v}
    [Alternative f] {α : Type u} (x : f α)
    : f (Option α)

Returns some x if f succeeds with value x, else returns none.

7.4.3. Lifting Boolean Operations

def

andM.{u, v} {m : Type u → Type v} {β : Type u}
    [Monad m] [ToBool β] (x y : m β) : m β

def

orM.{u, v} {m : Type u → Type v} {β : Type u}
    [Monad m] [ToBool β] (x y : m β) : m β

def

notM.{v} {m : Type → Type v} [Applicative m]
    (x : m Bool) : m Bool

7.4.4. Kleisli Composition

Kleisli composition is the composition of monadic functions, analogous to Function.comp for ordinary functions.

def

Bind.kleisliRight.{u, u_1, u_2} {α : Type u}
    {m : Type u_1 → Type u_2} {β γ : Type u_1}
    [Bind m] (f₁ : α → m β) (f₂ : β → m γ)
    (a : α) : m γ

Left-to-right composition of Kleisli arrows.

def

Bind.kleisliLeft.{u, u_1, u_2} {α : Type u}
    {m : Type u_1 → Type u_2} {β γ : Type u_1}
    [Bind m] (f₂ : β → m γ) (f₁ : α → m β)
    (a : α) : m γ

Right-to-left composition of Kleisli arrows.

7.4.5. Re-Ordered Operations

Sometimes, it can be convenient to partially apply a function to its second argument. These functions reverse the order of arguments, making it this easier.

def

Functor.mapRev.{u, v} {f : Type u → Type v}
    [Functor f] {α β : Type u}
    : f α → (α → β) → f β

def

Bind.bindLeft.{u, u_1} {α : Type u}
    {m : Type u → Type u_1} {β : Type u}
    [Bind m] (f : α → m β) (ma : m α) : m β

Same as Bind.bind but with arguments swapped.