18.3. 语法🔗

Lean 通过特殊语法支持使用函子、应用函子和单子进行编程：

为最常用的操作提供了中缀运算符。
一种称为 Lean.Parser.Term.do : termdo 记法的嵌入式语言，允许在单子中编写程序时使用命令式语法。

18.3.1. 中缀运算符🔗

中缀运算符主要适用于较小的表达式，或不存在 Monad 实例的情况。

18.3.1.1. 函子🔗

Functor.map 有两个中缀运算符。

语法函子运算符

g <$> x 是 Functor.map g x 的简写。

term ::= ...
    | term <$> term

x <&> g 是 Functor.map g x 的简写。

term ::= ...
    | term <&> term

18.3.1.2. 应用函子🔗

语法应用函子运算符

g <*> x 是 Seq.seq g (fun () => x) 的简写。插入该函数是为了延迟求值，因为控制流可能不会到达此参数。

term ::= ...
    | term <*> term

e1 *> e2 是 SeqRight.seqRight e1 (fun () => e2) 的简写。

term ::= ...
    | term *> term

e1 <* e2 是 SeqLeft.seqLeft e1 (fun () => e2) 的简写。

term ::= ...
    | term <* term

许多应用函子还通过 Alternative 类型类支持失败与恢复。这个类也有一个中缀运算符。

语法备选运算符

e <|> e' 是 OrElse.orElse e (fun () => e') 的简写。插入该函数是为了延迟求值，因为控制流可能不会到达此参数。

term ::= ...
    | term <|> term

structure User where
  name : String
  favoriteNat : Nat
def main : IO Unit := pure ()

Functor 与 Applicative 的中缀运算符

函数式编程中一种常见的惯用法，是通过 Functor.map 和 Seq.seq 将纯函数应用于某个带效果的语境中。函数通过 <$> 应用于一系列实参，各实参之间用 <*> 分隔。

在此示例中，main 的函数体使用这一惯用法来应用构造函数 User.mk。

def getName : IO String := do
  IO.println "What is your name?"
  return (← (← IO.getStdin).getLine).trimAsciiEnd.copy

partial def getFavoriteNat : IO Nat := do
  IO.println "What is your favorite natural number?"
  let line ← (← IO.getStdin).getLine
  if let some n := line.trimAscii.copy.toNat? then
    return n
  else
    IO.println "Let's try again."
    getFavoriteNat

structure User where
  name : String
  favoriteNat : Nat
deriving Repr

def main : IO Unit := do
  let user ← User.mk <$> getName <*> getFavoriteNat
  IO.println (repr user)

使用以下输入运行时：

stdinA. Lean UserNone42

会产生以下输出：

                      stdoutWhat is your name?What is your favorite natural number?Let's try again.What is your favorite natural number?{ name := "A. Lean User", favoriteNat := 42 }

18.3.1.3. 单子🔗

单子主要通过 Lean.Parser.Term.do : termdo 记法使用。不过，有时用运算符描述单子计算会更方便。

语法单子运算符

act >>= f 是 Bind.bind act f 的语法。

term ::= ...
    | term >>= term

类似地，反向运算符 f =<< act 也是 Bind.bind act f 的语法。

term ::= ...
    | term =<< term

Kleisli 复合运算符 Bind.kleisliRight 和 Bind.kleisliLeft 也有中缀形式。

term ::= ...
    | term >=> term

term ::= ...
    | term <=< term

18.3.2. `do` 记法🔗

单子主要通过 Lean.Parser.Term.do : termdo 记法使用；这是一种以命令式风格编程的嵌入式语言。它为依次执行带效果的操作、提前返回、局部可变变量、循环和异常处理提供了熟悉的语法。所有这些功能都会翻译为 Monad 类型类的操作，其中少数功能还需要 ForIn 等类型类的额外实例，以规定如何遍历容器。有关 Lean.Parser.Term.do : termdo 记法设计的更多细节，请参阅 Ullrich and de Moura (2022)Sebastian Ullrich and Leonardo de Moura, 2022. “do Unchained: Embracing Local Imperativity in a Purely Functional Language”. In Proceedings of the ACM on Programming Languages: ICFP 2022.。

Lean.Parser.Term.do : termdo 项由关键字 Lean.Parser.Term.do : termdo 后接一系列 Lean.Parser.Term.do : termdo 元素组成。

语法do 记法

term ::= ...
    | do doSeqItem*

Lean.Parser.Term.do : termdo 中的元素可以用分号分隔；否则，每个元素应各占一行，并且缩进量相同。

18.3.2.1. 顺序计算🔗

Lean.Parser.Term.do : termdo 元素的一种形式是项。

语法do 记法中的项

doSeqItem ::= ...
    | term

一个项后接一系列元素时，会被翻译为对 bind 的使用；具体而言，do e1; es 会被翻译为 e1 >>= fun () => do es。

`Lean.Parser.Term.do : termdo` 元素	去糖
`do e1 es`	`e1 >>= fun () => do es`

也可以为该项的计算结果命名，以便在后续步骤中使用。这通过 Lean.Parser.Term.doLet : doElemlet 完成。

语法do 记法中的数据依赖

Lean.Parser.Term.do : termdo 块中的单子 Lean.Parser.Term.doLet : doElemlet 绑定有两种形式。第一种将一个标识符绑定到结果，并可附带类型标注：

doSeqItem ::= ...
    | let ident(:term)? ← term

第二种将一个模式绑定到结果。以 | 开头的后备子句规定了模式与结果不匹配时的行为。

doSeqItem ::= ...
    | let term ← term
        (| doSeqIndent)?

这种语法也会被翻译为对 bind 的使用。 do let x ← e1; es 会被翻译为 e1 >>= fun x => do es，而后备子句会被翻译为默认模式匹配。 Lean.Parser.Term.doLet : doElemlet 也可以使用标准定义语法 :=，而非 ←。这表示纯定义，而非单子定义：

语法do 记法中的局部定义

doSeqItem ::= ...
    | let (ident | hole) := term

do let x := e; es 会被翻译为 let x := e; do es。

`Lean.Parser.Term.do : termdo` 元素	去糖
`do let x ← e1 es`	`e1 >>= fun x => do es`
`do let some x ← e1? \| fallback es`	`e1? >>= fun \| some x => do es \| _ => fallback`
`do let x := e es`	`let x := e do es`

在 Lean.Parser.Term.do : termdo 块中，← 可以用作前缀运算符。它所作用的表达式会被一个新变量替换，并在当前步骤之前用 bind 绑定该变量。这样就能在原本可能需要纯值的位置使用单子效果，同时仍然区分对带效果计算的描述与对其效果的实际执行。多个 ← 按从左到右、从内到外的顺序处理。

`Lean.Parser.Term.do : termdo` 元素示例	去糖
`do f (← e1) (← e2) es`	`do let x ← e1 let y ← e2 f x y es`
`do let x := g (← h (← e1)) es`	`do let y ← e1 let z ← h y let x := g z es`

嵌套动作去糖示例

除了便利地支持具有数据依赖的顺序计算外，Lean.Parser.Term.do : termdo 记法还支持在局部加入多种效果，包括提前返回、局部可变状态以及可提前终止的循环。这些效果通过变换整个 Lean.Parser.Term.do : termdo 块来实现，其方式类似于单子变换器，而不是通过局部去糖实现。

18.3.2.2. 提前返回🔗

提前返回会立即以给定值终止计算。该值从包含它的最近 Lean.Parser.Term.do : termdo 块返回；但这个块未必由最近的 do 关键字引入。确定 Lean.Parser.Term.do : termdo 块范围的规则在专门的一节中介绍。

语法提前返回

doSeqItem ::= ...
    | return term

doSeqItem ::= ...
    | return

并非所有单子都包含提前返回。因此，当 Lean.Parser.Term.do : termdo 块包含 Lean.Parser.Term.doReturn : doElemreturn 时，需要改写代码来模拟这一效果。在单子 m 中使用提前返回来计算 α 类型值的程序，可以视为单子 ExceptT α m α 中的程序：提前返回的值走异常路径，普通返回则不走。随后，外层处理器可以返回任一路径产生的值。在内部，Lean.Parser.Term.do : termdo 精译器执行的翻译与此非常相似。

单独使用时，Lean.Parser.Term.doReturn : doElemreturn 是 Lean.Parser.Term.doReturn : doElemreturn () 的简写。

18.3.2.3. 局部可变状态🔗

局部可变状态是无法逸出其定义所在 Lean.Parser.Term.do : termdo 块的可变状态。 Lean.Parser.Term.doLet : doElemlet mut 绑定器引入局部可变绑定。

语法局部可变性

可变绑定既可以用纯计算初始化，也可以用单子计算初始化：

doSeqItem ::= ...
    | let mut (ident | hole) := term

doSeqItem ::= ...
    | let mut ident ← doElem

类似地，它们既可以用纯值更新，也可以用单子计算的结果更新：

doElem ::= ...
    | ident(: term)?  := term

doElem ::= ...
    | term(: term)? := term

doElem ::= ...
    | ident(: term)? ← term

doElem ::= ...
    | term ← term
        (| doSeqIndent)?

这些局部可变绑定不如状态单子强大，因为它们在词法作用域之外不可变；这也使其更易于推理。当 Lean.Parser.Term.do : termdo 块包含可变绑定时，Lean.Parser.Term.do : termdo 精译器会以类似 StateT 的方式变换表达式：构造一个新单子，并用正确的值将其初始化。

18.3.2.4. 控制结构🔗

有一些 Lean.Parser.Term.do : termdo 元素对应于 Lean 的大多数项级控制结构。当它们作为 Lean.Parser.Term.do : termdo 块中的一个步骤出现时，会被解释为 Lean.Parser.Term.do : termdo 元素而不是项。控制结构的每个分支都是一系列 Lean.Parser.Term.do : termdo 元素，而不是一个项；其中一些在语法上比对应的项更灵活。

语法条件语句

在 Lean.Parser.Term.do : termdo 块中，Lean.Parser.Term.doIf : doElemif 语句可以省略 Lean.Parser.Term.doIf : doElemelse 分支。省略 Lean.Parser.Term.doIf : doElemelse 分支等价于以 pure() 作为该分支的内容。

doSeqItem ::= ...
    | if ((ident | hole) :)? term then
        doSeqItem*
      (else
        doSeqItem*)?

从语法上说，Lean.Parser.Term.doIf : doElemthen 分支不能省略。对于这类情况，Lean.Parser.Term.doUnless : doElemunless 仅在条件为假时执行其主体。 Lean.Parser.Term.doUnless : doElemunless 中的 Lean.Parser.Term.do : termdo 是其语法的一部分，不会引入嵌套的 Lean.Parser.Term.do : termdo 块。

语法反向条件语句

doSeqItem ::= ...
    | unless term do
        doSeqItem*

在 Lean.Parser.Term.do : termdo 块中使用 Lean.Parser.Term.doMatch : doElemmatch 时，每个分支都被视为同一块的一部分。除此之外，它等价于 Lean.Parser.Term.match : termmatch 项。

语法模式匹配

doSeqItem ::= ...
    | match (((ident | hole) :)? term),* with
        (| term,* => doSeqItem*)*

18.3.2.5. 迭代🔗

在 Lean.Parser.Term.do : termdo 块中，Lean.Parser.Term.doFor : doElemfor…Lean.Parser.Term.doFor : doElemin 循环可用于遍历数据结构。循环体是包含它的 Lean.Parser.Term.do : termdo 块的一部分，因此可以使用提前返回和可变变量等局部效果。

语法遍历集合

doSeqItem ::= ...
    | for ((ident :)? term in term),* do
        doSeqItem*

Lean.Parser.Term.doFor : doElemfor…Lean.Parser.Term.doFor : doElemin 循环至少需要一个规定如何迭代的子句；该子句由可选的成员关系证明名称及其后的冒号（:）、要绑定的模式、关键字 Lean.Parser.Term.doFor : doElemin 和一个集合项组成。该模式可以只是一个标识符，但必须能匹配集合中的任意元素；此处的模式不能用作隐式过滤器。还可以用逗号分隔并提供更多子句。各集合会同时迭代；任一集合耗尽元素时，迭代即停止。

同时遍历多个集合

同时遍历多个集合时，任一集合耗尽元素，迭代即停止。

#[(0, 'a'), (1, 'b')]#eval Id.run do
  let mut v := #[]
  for x in [0:43], y in ['a', 'b'] do
    v := v.push (x, y)
  return v

#[(0, 'a'), (1, 'b')]

在线查看 ↪

使用 Lean.Parser.Term.doFor : doElemfor 遍历数组索引

使用 Lean.Parser.Term.doFor : doElemfor 遍历数组的有效索引时，为成员关系证明命名，可以使搜索数组索引未越界证明的策略成功。

def satisfyingIndices
    (p : α → Prop) [DecidablePred p]
    (xs : Array α) : Array Nat := Id.run do
  let mut out := #[]
  for h : i in [0:xs.size] do
    if p xs[i] then out := out.push i
  return out

省略假设名称会导致数组查找失败，因为上下文中没有证明迭代变量处于指定范围内的证据。

使用 for 循环的迭代会被翻译为对 ForIn.forIn 的使用；它类似于 ForM.forM，但增加了对局部修改和提前终止的支持。 ForIn.forIn 接收局部可变状态的初始值、一个单子动作以及要遍历的集合作为参数。传给 ForIn.forIn 的单子动作以当前状态为参数，并在单子 m 中执行动作后返回 ForInStep.yield 或 ForInStep.done：前者表示应使用更新后的一组局部可变值继续迭代，后者表示执行了 Lean.Parser.Term.doBreak : doElembreak 或 Lean.Parser.Term.doReturn : doElemreturn。迭代完成时，ForIn.forIn 返回各局部可变值的最终值。

循环的具体去糖方式取决于其主体如何使用状态和提前终止。下面是一些示例：

`Lean.Parser.Term.do : termdo` 元素	去糖
`do let mut b := … for x in xs do b ← f x b es`	`do let b := … let b ← ForIn.forIn xs b fun x b => do let b ← f x b return ForInStep.yield b es`
`do let mut b := … for x in xs do b ← f x b break es`	`do let b := … let b ← ForIn.forIn xs b fun x b => do let b ← f x b return ForInStep.done b es`
`do let mut b := … for h : x in xs do b ← f' x h b es`	`do let b := … let b ← ForIn'.forIn' xs b fun x h b => do let b ← f' x h b return ForInStep.yield b es`
`do let mut b := … for h : x in xs do b ← f' x h b break es`	`do let b := … let b ← ForIn'.forIn' xs b fun x h b => do let b ← f' x h b return ForInStep.done b es`

只要条件保持为真，Lean.doElemWhile_Do_while 循环的主体就会重复执行。可以在未标记为 Lean.Parser.Command.declaration : commandpartial 的函数中使用它们编写无限循环。这是因为 Lean.Parser.Command.declaration : commandpartial 修饰符只适用于被定义函数自身导致的不终止或无限递归，而不适用于它所调用的函数所导致的情况。 Lean.doElemWhile_Do_while 循环的翻译依赖一个单独的辅助函数。

语法条件循环

doSeqItem ::= ...
    | while term do
        doSeqItem*

doSeqItem ::= ...
    | while (ident | hole) : term do
        doSeqItem*

Lean.doElemRepeat__Until_repeat-Lean.doElemRepeat__Until_until 循环的主体总会至少执行一次。每次迭代后都会检查条件；条件为假时继续循环。条件变为真时，迭代停止。

语法后测试循环

doSeqItem ::= ...
    | repeat
        doSeqItem*
      until term

Lean.doElemRepeat_repeat 循环的主体会重复执行，直至执行 Lean.Parser.Term.doBreak : doElembreak 语句。与 Lean.doElemWhile_Do_while 循环一样，这些循环也可用于未标记为 Lean.Parser.Command.declaration : commandpartial 的函数。

语法无条件循环

doSeqItem ::= ...
    | repeat
        doSeqItem*

Lean.Parser.Term.doContinue : doElemcontinue 语句会跳过最近外层 Lean.doElemRepeat_repeat、Lean.doElemWhile_Do_while 或 Lean.Parser.Term.doFor : doElemfor 循环主体的剩余部分，进入下一次迭代。 Lean.Parser.Term.doBreak : doElembreak 语句会终止最近外层的 Lean.doElemRepeat_repeat、Lean.doElemWhile_Do_while 或 Lean.Parser.Term.doFor : doElemfor 循环，使迭代停止。

语法循环控制语句

doSeqItem ::= ...
    | continue

doSeqItem ::= ...
    | break

除了 Lean.Parser.Term.doBreak : doElembreak，循环始终可以由当前单子中的效果终止。从循环中抛出异常会终止循环。

在 Option 单子中终止循环

Alternative 类的 failure 方法可用于终止 Option 单子中原本会无限运行的循环。

none#eval show Option Nat from do
  let mut i := 0
  repeat
    if i > 1000 then failure
    else i := 2 * (i + 1)
  return i

none

在线查看 ↪

18.3.2.6. 识别 `do` 块🔗

Lean.Parser.Term.do : termdo 记法的许多功能都会影响当前 Lean.Parser.Term.do : termdo 块。具体而言，提前返回会中止当前块，使其求值为返回值；而可变绑定只能在其定义所在的块中修改。要理解这些功能，需要精确定义何谓处于“同一”块中。

在实际操作中，可以使用 Lean 语言服务器检查这一点。当光标位于 Lean.Parser.Term.doReturn : doElemreturn 语句上时，对应的 Lean.Parser.Term.do : termdo 关键字会高亮显示。尝试在同一 Lean.Parser.Term.do : termdo 块之外修改可变绑定会产生错误消息。

从 return 高亮显示 do — 高亮显示 `Lean.Parser.Term.do : termdo`

出现错误时从 return 高亮显示 do — 高亮显示 `Lean.Parser.Term.do : termdo`

规则如下：

直接嵌套在开启某个块的 Lean.Parser.Term.do : termdo 关键字下的每个元素都属于该块。
如果一个 Lean.Parser.Term.do : termdo 关键字本身是外层 Lean.Parser.Term.do : termdo 块中的元素，那么直接嵌套在该关键字下的每个元素都属于外层块。
Lean.Parser.Term.doIf : doElemif、Lean.Parser.Term.doMatch : doElemmatch 或 Lean.Parser.Term.doUnless : doElemunless 元素各分支中的元素，与包含它们的控制结构属于同一 Lean.Parser.Term.do : termdo 块。作为 Lean.Parser.Term.doUnless : doElemunless 语法一部分的 Lean.Parser.Term.doUnless : doElemdo 关键字不会引入新的 Lean.Parser.Term.do : termdo 块。
Lean.doElemRepeat_repeat、Lean.doElemWhile_Do_while 和 Lean.Parser.Term.doFor : doElemfor 主体中的元素，与包含它们的循环属于同一 Lean.Parser.Term.do : termdo 块。作为 Lean.doElemWhile_Do_while 和 Lean.Parser.Term.doFor : doElemfor 语法一部分的 Lean.Parser.Term.doFor : doElemdo 关键字不会引入新的 Lean.Parser.Term.do : termdo 块。

嵌套的 do 与分支

以下示例输出 6 而不是 7：

def test : StateM Nat Unit := do
  set 5
  if true then
    set 6
    do return
  set 7
  return

((), 6)#eval test.run 0

((), 6)

这是因为 Lean.Parser.Term.doIf : doElemif 下的 Lean.Parser.Term.doReturn : doElemreturn 语句与其直接父级属于同一 Lean.Parser.Term.do : termdo，而该父级本身又与 Lean.Parser.Term.doIf : doElemif 属于同一 Lean.Parser.Term.do : termdo。如果作为其他 Lean.Parser.Term.do : termdo 块中元素出现的 Lean.Parser.Term.do : termdo 块会创建新块，那么该示例将输出 7。

在线查看 ↪

18.3.2.7. 用于迭代的类型类🔗

若要在没有成员关系证明的 Lean.Parser.Term.doFor : doElemfor 循环中使用，集合必须实现 ForIn 类型类。额外实现 ForIn' 后，还可以使用带成员关系证明的 Lean.Parser.Term.doFor : doElemfor 循环。

类型类

ForIn.{u, v, u₁, u₂} (m : Type u₁ → Type u₂) (ρ : Type u)
  (α : outParam (Type v)) : Type (max (max (max u (u₁ + 1)) u₂) v)
ForIn.{u, v, u₁, u₂}
  (m : Type u₁ → Type u₂) (ρ : Type u)
  (α : outParam (Type v)) :
  Type (max (max (max u (u₁ + 1)) u₂) v)

do 块中的单子迭代，使用 for x in xs 记法。

参数 m 是执行迭代所在 do 块的单子，ρ 是被迭代集合的类型，α 是元素类型。

实例构造子

ForIn.mk.{u, v, u₁, u₂}

方法

forIn : {β : Type u₁} → ρ → β → (α → β → m (ForInStep β)) → m β

以单子方式迭代集合 xs 的内容，带有局部状态 b，并允许提前终止。

由于 do 块支持局部可变绑定以及 return 和 break，传给 ForIn.forIn 的单子动作除了集合的当前元素之外还接收一个初始状态，并返回更新后的状态以及迭代应继续还是终止的指示。若该动作返回 ForInStep.done，则 ForIn.forIn 应停止迭代并返回更新后的状态。若该动作返回 ForInStep.yield，则当还有后续元素时，ForIn.forIn 应继续迭代，并把更新后的状态传给该动作。

关于如何将 for 循环翻译为 ForIn.forIn 的更多信息，见 Lean 参考手册。

类型类

ForIn'.{u, v, u₁, u₂} (m : Type u₁ → Type u₂) (ρ : Type u)
  (α : outParam (Type v)) (d : outParam (Membership α ρ)) :
  Type (max (max (max u (u₁ + 1)) u₂) v)
ForIn'.{u, v, u₁, u₂}
  (m : Type u₁ → Type u₂) (ρ : Type u)
  (α : outParam (Type v))
  (d : outParam (Membership α ρ)) :
  Type (max (max (max u (u₁ + 1)) u₂) v)

do 块中带成员关系证明的单子迭代，使用 for h : x in xs 记法。

参数 m 是执行迭代所在 do 块的单子，ρ 是被迭代集合的类型，α 是元素类型，d 是要提供的特定成员关系谓词。

实例构造子

ForIn'.mk.{u, v, u₁, u₂}

方法

forIn' : {β : Type u₁} → (x : ρ) → β → ((a : α) → a ∈ x → β → m (ForInStep β)) → m β

以单子方式迭代集合 xs 的内容，带有局部状态 b，并允许提前终止。每次迭代时，循环体都会获得当前元素属于该集合的证明。

由于 do 块支持局部可变绑定以及 return 和 break，传给 ForIn'.forIn' 的单子动作除了集合的当前元素及其成员关系证明之外还接收一个初始状态。该动作返回更新后的状态以及迭代应继续还是终止的指示。若动作返回 ForInStep.done，则 ForIn'.forIn' 应停止迭代并返回更新后的状态。若动作返回 ForInStep.yield，则当还有后续元素时，ForIn'.forIn' 应继续迭代，并把更新后的状态传给该动作。

关于如何将 for 循环翻译为 ForIn'.forIn' 的更多信息，见 Lean 参考手册。

归纳类型

ForInStep.{u} (α : Type u) : Type u
ForInStep.{u} (α : Type u) : Type u

用于编译 for x in xs 记法的指示，表明循环体是否提前终止。

集合的 ForIn 或 ForIn' 实例描述如何迭代其元素。表示循环体的单子动作返回 ForInStep α，其中 α 是用于实现 let mut 等功能的局部状态。

构造子

ForInStep.done.{u} {α : Type u} : α → ForInStep α

循环应提前终止。

循环体中使用 break 或 return 会产生 ForInStep.done。

ForInStep.yield.{u} {α : Type u} : α → ForInStep α

循环应带着下一次迭代继续，并使用所返回的状态。

continue 以及到达循环体末尾会产生 ForInStep.yield。

定义

ForInStep.value.{u_1} {α : Type u_1} (x : ForInStep α) : α
ForInStep.value.{u_1} {α : Type u_1}
  (x : ForInStep α) : α

从 ForInStep 中提取值，忽略它是 ForInStep.done 还是 ForInStep.yield。

类型类

ForM.{u, v, w₁, w₂} (m : Type u → Type v) (γ : Type w₁)
  (α : outParam (Type w₂)) : Type (max (max v w₁) w₂)
ForM.{u, v, w₁, w₂} (m : Type u → Type v)
  (γ : Type w₁) (α : outParam (Type w₂)) :
  Type (max (max v w₁) w₂)

在某种容器类型上进行重载的单子迭代。

ForM m γ α 实例描述如何在单子 m 中，把单子运算迭代应用于类型为 γ、元素类型为 α 的容器。元素类型应由单子和容器唯一确定。

使用 ForM.forIn 可从 ForM 实例构造 ForIn 实例，从而能在 do 记法中使用 for 运算符。

实例构造子

ForM.mk.{u, v, w₁, w₂}

方法

forM : γ → (α → m PUnit) → m PUnit

在集合 coll 的每个元素上运行单子动作 f。

定义

ForM.forIn.{u_1, u_2, u_3, u_4} {m : Type u_1 → Type u_2} {β : Type u_1}
  {ρ : Type u_3} {α : Type u_4} [Monad m]
  [ForM (StateT β (ExceptT β m)) ρ α] (x : ρ) (b : β)
  (f : α → β → m (ForInStep β)) : m β
ForM.forIn.{u_1, u_2, u_3, u_4}
  {m : Type u_1 → Type u_2} {β : Type u_1}
  {ρ : Type u_3} {α : Type u_4} [Monad m]
  [ForM (StateT β (ExceptT β m)) ρ α]
  (x : ρ) (b : β)
  (f : α → β → m (ForInStep β)) : m β

从 ForM 实例创建 ForIn.forIn 的适当实现。

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

18.3. 语法🔗

18.3.1. 中缀运算符🔗

18.3.1.1. 函子🔗

18.3.1.2. 应用函子🔗

18.3.1.3. 单子🔗

18.3.2. do 记法🔗

18.3.2.1. 顺序计算🔗

18.3.2.2. 提前返回🔗

18.3.2.3. 局部可变状态🔗

18.3.2.4. 控制结构🔗

18.3.2.5. 迭代🔗

18.3.2.6. 识别 do 块🔗

18.3.2.7. 用于迭代的类型类🔗

18.3.2. `do` 记法🔗

18.3.2.6. 识别 `do` 块🔗