14.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

14.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
Functor.discard.{u, v}
  {f : Type u → Type v} {α : Type u}
  [Functor f] (x : f α) : f PUnit

Discards the value in a functor, retaining the functor's structure.

Discarding values is especially useful when using Applicative functors or Monads to implement effects, and some operation should be carried out only for its effects. In do-notation, statements whose values are discarded must return Unit, and discard can be used to explicitly discard their values.

14.4.2. Control Flow

def

guard.{v} {f : Type → Type v} [Alternative f] (p : Prop) [Decidable p] :
  f Unit
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 α)
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.

14.4.3. Lifting Boolean Operations

def

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

Converts the result of the monadic action x to a Bool. If it is true, returns y; otherwise, returns the original result of x.

This a monadic counterpart to the short-circuiting && operator, usually accessed via the <&&> operator.

Conventions for notations in identifiers:

The recommended spelling of <&&> in identifiers is andM.

def

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

Converts the result of the monadic action x to a Bool. If it is true, returns it and ignores y; otherwise, runs y and returns its result.

This a monadic counterpart to the short-circuiting || operator, usually accessed via the <||> operator.

Conventions for notations in identifiers:

The recommended spelling of <||> in identifiers is orM.

def

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

Runs a monadic action and returns the negation of its result.

14.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 γ
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.

Conventions for notations in identifiers:

The recommended spelling of >=> in identifiers is kleisliRight.

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 γ
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.

Conventions for notations in identifiers:

The recommended spelling of <=< in identifiers is kleisliLeft.

14.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 β
Functor.mapRev.{u, v}
  {f : Type u → Type v} [Functor f]
  {α β : Type u} : f α → (α → β) → f β

Maps a function over a functor, with parameters swapped so that the function comes last.

This function is Functor.map with the parameters reversed, typically used via the <&> operator.

Conventions for notations in identifiers:

The recommended spelling of <&> in identifiers is mapRev.

def

Bind.bindLeft.{u, u_1} {α : Type u} {m : Type u → Type u_1} {β : Type u}
  [Bind m] (f : α → m β) (ma : m α) : m β
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.

Conventions for notations in identifiers:

The recommended spelling of =<< in identifiers is bindLeft.