18.4. 接口参考🔗

除了这里介绍的通用函数之外，按照惯例，每种集合类型的命名空间中还会定义一些函数，作为其接口的一部分：

mapM 映射一个单子函数。
forM 映射一个单子函数并丢弃结果。
filterM 使用单子谓词进行筛选，返回满足该谓词的值。

单子式集合操作

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 尤其有用。

定义

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

丢弃函子中的值，同时保留函子的结构。

当使用 Applicative 函子或 Monad 实现副作用，而某个操作只应为其副作用而执行时，丢弃值尤其有用。在 do 记法中，值被丢弃的语句必须返回 Unit；可以使用 discard 显式丢弃这些语句的值。

18.4.2. 控制流🔗

定义

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

若命题 p 为真，则什么也不做；否则（使用 failure）失败。

定义

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 α)

若 f 成功并得到值 x，则返回 some x；否则返回 none。

18.4.3. 提升布尔操作🔗

定义

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 β

将单子动作 x 的结果转换为 Bool。若结果为 true，则返回 y；否则返回 x 的原始结果。

这是短路运算符 && 的单子对应物，通常通过 <&&> 运算符使用。

标识符中记法的约定：

<&&> 在标识符中的推荐拼写是 andM。

定义

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 β

将单子动作 x 的结果转换为 Bool。若结果为 true，则返回该结果并忽略 y；否则运行 y 并返回其结果。

这是短路运算符 || 的单子对应物，通常通过 <||> 运算符使用。

标识符中记法的约定：

<||> 在标识符中的推荐拼写是 orM。

定义

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

运行单子动作并返回其结果的否定。

18.4.4. 克莱斯利复合🔗

克莱斯利复合是单子函数的复合，类似于普通函数所用的 Function.comp。

定义

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 γ

Kleisli 箭头的从左到右复合。

标识符中记法的约定：

>=> 在标识符中的推荐拼写是 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 γ
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 γ

Kleisli 箭头的从右到左复合。

标识符中记法的约定：

<=< 在标识符中的推荐拼写是 kleisliLeft。

18.4.5. 重排实参的操作🔗

有时，对函数的第二个实参进行部分应用会更方便。以下函数反转实参顺序，使这一做法更容易。

定义

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 β

将函数映射到函子上，但交换参数顺序，使函数位于最后。

此函数是参数顺序反转的 Functor.map，通常通过 <&> 运算符使用。

标识符中记法的约定：

<&> 在标识符中的推荐拼写是 mapRev。

定义

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 β

与 Bind.bind 相同，但实参顺序相反。

标识符中记法的约定：

=<< 在标识符中的推荐拼写是 bindLeft。

18.1.	定律
18.2.	提升单子
18.3.	语法
18.4.	接口参考
18.5.	单子的种类