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.
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}"
stdinynoopsynystdoutKeep 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
The discard function is especially useful when using an action that returns a value only for its side effects.
Functor.discard.{u, v} {f : Type u → Type v}
{α : Type u} [Functor f] (x : f α) : f PUnitDiscards 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.
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).
optional.{u, v} {f : Type u → Type v}
[Alternative f] {α : Type u} (x : f α) :
f (Option α)
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.
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.
notM.{v} {m : Type → Type v} [Applicative m]
(x : m Bool) : m BoolRuns a monadic action and returns the negation of its result.
Kleisli composition is the composition of monadic functions, analogous to Function.comp for ordinary functions.
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.
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.
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.
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.