18.4. API 参考🔗

除了此处描述的一般函数之外，还有一些函数通常定义为每个集合类型的命名空间中的 API 的一部分：

mapM 映射一元函数。
forM 映射一个单子函数，丢弃结果。
filterM 使用一元谓词进行过滤，返回满足它的值。

Monadic Collection Operations

Array.filterM 可用于编写依赖于副作用的过滤器。

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).trimAscii.copy
      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

18.4.1. 丢弃结果🔗

当使用仅为其副作用返回值的操作时，discard 函数特别有用。

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.

18.4.2. 控制流程🔗

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.

18.4.3. 提升布尔运算🔗

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

18.4.4. 克莱斯利成分🔗

Kleisli Composition是一元函数的组合，类似于普通函数的Function.comp。

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.

18.4.5. 重新排序的操作🔗

有时，将函数部分应用到其第二个参数可能会很方便。这些函数颠倒了参数的顺序，使其变得更容易。

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.

18.1.	法律
18.2.	提升单子
18.3.	句法
18.4.	API 参考
18.5.	单子的种类