18. 函子、单子与 `do` 记法🔗

类型类 Functor、Applicative 和 Monad 为函数式编程提供了基本工具。关于如何使用这些抽象进行编程的介绍，参见 Lean 函数式编程。它们的灵感来自范畴论中的函子和单子概念，但编程中使用的版本限制更多。 Lean 标准库中的类型类所表示的是用于编程的概念，而非一般的数学定义。

Functor 函子的实例允许在某种多态上下文中一致地应用操作。例如，可以通过应用函数来变换列表中的每个元素，也可以安排将纯函数应用于现有 IO 动作的结果，从而创建新的 IO 动作。 Monad 单子的实例允许编码带有数据依赖的副作用；例如，用元组模拟可变状态、用和类型模拟异常，以及用 IO 表示真实的副作用。 Applicative 应用函子介于二者之间：它们与单子一样，允许把通过效应计算出的函数应用于同样通过效应计算出的实参；但不允许顺序数据依赖，即一个效应的输出成为另一个效应操作的输入。

另外几个类型类 Pure、Bind、SeqLeft、SeqRight 和 Seq 分别抽取了 Applicative 与 Monad 中的单项操作，使这些操作可以重载，并用于不一定是 Applicative 应用函子或 Monad 单子的类型。类型类 Alternative 描述还具有某种失败与恢复概念的应用函子。

类型类

Functor.{u, v} (f : Type u → Type v) : Type (max (u + 1) v)
Functor.{u, v} (f : Type u → Type v) :
  Type (max (u + 1) v)

函数式编程意义下的函子：函数 f : Type u → Type v 能将一个函数映射到其内容之上。这个 map 运算符写作 <$>，并通过 Functor 实例重载。

此 map 函数应当保持恒等函数和函数复合。换言之，对于所有项 v : f α，应有：

id <$> v = v
对所有函数 h : β → γ 和 g : α → β，(h ∘ g) <$> v = h <$> g <$> v

所有 Functor 实例都应满足这些要求，但不要求它们_证明_这一点。可以通过 LawfulFunctor 类型类要求或提供这些证明。

假定实例合法，这一定义对应于范畴论中的函子概念，其中所考虑的特殊范畴以类型为对象、以类型间的函数为态射。

实例构造子

Functor.mk.{u, v}

方法

map : {α β : Type u} → (α → β) → f α → f β

在函子内部应用函数。此方法用于重载 <$> 运算符。

映射常值函数时，应改用 Functor.mapConst，因为它可能效率更高。

标识符中记法的约定：

<$> 在标识符中的推荐拼写是 map。

mapConst : {α β : Type u} → α → f β → f α

映射常值函数。

给定 a : α 和 v : f β，mapConst a v 等价于 (fun _ => a) <$> v。对某些函子，可以更高效地实现它；其他所有函子都可使用默认实现。

类型类

Pure.{u, v} (f : Type u → Type v) : Type (max (u + 1) v)
Pure.{u, v} (f : Type u → Type v) :
  Type (max (u + 1) v)

pure 函数通过 Pure 实例重载。

Pure 通常经由 Monad 或 Applicative 实例使用。

实例构造子

Pure.mk.{u, v}

方法

pure : {α : Type u} → α → f α

给定 a : α，pure a : f α 表示一个什么也不做并返回 a 的动作。

示例：

(pure "hello" : Option String) = some "hello"
(pure "hello" : Except (Array String) String) = Except.ok "hello"
(pure "hello" : StateM Nat String).run 105 = ("hello", 105)

类型类

Seq.{u, v} (f : Type u → Type v) : Type (max (u + 1) v)
Seq.{u, v} (f : Type u → Type v) :
  Type (max (u + 1) v)

<*> 运算符使用函数 Seq.seq 重载。

Functor 类型类中的 <$> 可将普通函数映射到函子的内容上，而 <*> 则可应用位于函子 “内部”的函数。将 f 看作可能的副作用时，这会刻画求值顺序：seq 安排产生函数的副作用先于产生实参值的副作用发生。

对大多数应用，应使用 Applicative 或 Monad，而不是直接使用 Seq。

实例构造子

Seq.mk.{u, v}

方法

seq : {α β : Type u} → f (α → β) → (Unit → f α) → f β

<*> 运算符的实现。

在单子中，mf <*> mx 与 do let f ← mf; x ← mx; pure (f x) 相同：它先对函数求值，再对实参求值，最后将前者应用于后者。

为避免令人意外的求值语义，mx 以“惰性”方式取得，即使用 Unit → f α 函数。

标识符中记法的约定：

<*> 在标识符中的推荐拼写是 seq。

类型类

SeqLeft.{u, v} (f : Type u → Type v) : Type (max (u + 1) v)
SeqLeft.{u, v} (f : Type u → Type v) :
  Type (max (u + 1) v)

<* 运算符使用 seqLeft 重载。

将 f 看作潜在副作用时，<* 先对左实参求值，再对右实参求值以执行二者的副作用，丢弃右实参的值并返回左实参的值。

对大多数应用，应使用 Applicative 或 Monad，而不是直接使用 SeqLeft。

实例构造子

SeqLeft.mk.{u, v}

方法

seqLeft : {α β : Type u} → f α → (Unit → f β) → f α

依次执行两个项的副作用，并丢弃第二个项的值。此函数通常通过 <* 运算符调用。

给定 x : f α 和 y : f β，x <* y 先运行 x，再运行 y，最后返回 x 的结果。

第二个实参的求值通过将它包装在函数中而延迟，从而使 f 能实现“短路”行为。

标识符中记法的约定：

<* 在标识符中的推荐拼写是 seqLeft。

类型类

SeqRight.{u, v} (f : Type u → Type v) : Type (max (u + 1) v)
SeqRight.{u, v} (f : Type u → Type v) :
  Type (max (u + 1) v)

*> 运算符使用 seqRight 重载。

将 f 看作潜在副作用时，*> 先对左实参求值，再对右实参求值以执行二者的副作用，丢弃左实参的值并返回右实参的值。

对大多数应用，应使用 Applicative 或 Monad，而不是直接使用 SeqRight。

实例构造子

SeqRight.mk.{u, v}

方法

seqRight : {α β : Type u} → f α → (Unit → f β) → f β

依次执行两个项的副作用，并丢弃第一个项的值。此函数通常通过 *> 运算符调用。

给定 x : f α 和 y : f β，x *> y 先运行 x，再运行 y，最后返回 y 的结果。

第二个实参的求值通过将它包装在函数中而延迟，从而使 f 能实现“短路”行为。

标识符中记法的约定：

*> 在标识符中的推荐拼写是 seqRight。

类型类

Applicative.{u, v} (f : Type u → Type v) : Type (max (u + 1) v)
Applicative.{u, v} (f : Type u → Type v) :
  Type (max (u + 1) v)

应用函子比 Functor 更强大，但不如 Monad 强大。

应用函子使用 <*> 运算符（重载为 seq）刻画副作用的顺序执行，但不能刻画依赖数据的副作用。较早计算的结果不能用于控制较晚的副作用。

应用函子应满足四条定律。Applicative 实例不要求证明这些定律；这些定律是 LawfulApplicative 类型类的一部分。

实例构造子

Applicative.mk.{u, v}

扩展

Functor f
Pure f
Seq f
SeqLeft f
SeqRight f

方法

map : {α β : Type u} → (α → β) → f α → f β

继承自父结构。

mapConst : {α β : Type u} → α → f β → f α

继承自父结构。

pure : {α : Type u} → α → f α

继承自父结构。

seq : {α β : Type u} → f (α → β) → (Unit → f α) → f β

继承自父结构。

seqLeft : {α β : Type u} → f α → (Unit → f β) → f α

继承自父结构。

seqRight : {α β : Type u} → f α → (Unit → f β) → f β

继承自父结构。

以定长列表作为应用函子

结构 LenList 将列表与其长度为所需值的证明配对。因此，它的 zipWith 运算无需为输入长度不同时提供后备方案。

structure LenList (length : Nat) (α : Type u) where
  list : List α
  lengthOk : list.length = length

def LenList.head (xs : LenList (n + 1) α) : α :=
  xs.list.head <| byα:Type uβ:Type un:Natxs:LenList (n + 1) α⊢ xs.list ≠ []
    intro hα:Type uβ:Type un:Natxs:LenList (n + 1) αh:xs.list = []⊢ False
    cases xsmkα:Type uβ:Type un:Natlist✝:List αlengthOk✝:list✝.length = n + 1h:{ list := list✝, lengthOk := lengthOk✝ }.list = []⊢ False
    simp_allmkα:Type uβ:Type un:Natlist✝:List αlengthOk✝:list✝.length = n + 1h:list✝ = []⊢ False
    subst_eqsAll goals completed! 🐙

def LenList.tail (xs : LenList (n + 1) α) : LenList n α :=
  match xs with
  | ⟨_ :: xs', _⟩ => ⟨xs', byα:Type uβ:Type un:Natxs:LenList (n + 1) αhead✝:αxs':List αlengthOk✝:(head✝ :: xs').length = n + 1⊢ xs'.length = n simp_allAll goals completed! 🐙⟩

def LenList.map (f : α → β) (xs : LenList n α) : LenList n β where
  list := xs.list.map f
  lengthOk := byα:Type uβ:Type un:Natf:α → βxs:LenList n α⊢ (List.map f xs.list).length = n
    cases xsmkα:Type uβ:Type un:Natf:α → βlist✝:List αlengthOk✝:list✝.length = n⊢ (List.map f { list := list✝, lengthOk := lengthOk✝ }.list).length = n
    simp [List.length_map, *]All goals completed! 🐙

def LenList.zipWith (f : α → β → γ)
    (xs : LenList n α) (ys : LenList n β) :
    LenList n γ where
  list := xs.list.zipWith f ys.list
  lengthOk := byα:Type uβ:Type uγ:Type ?u.15n:Natf:α → β → γxs:LenList n αys:LenList n β⊢ (List.zipWith f xs.list ys.list).length = n
    cases xsmkα:Type uβ:Type uγ:Type ?u.15n:Natf:α → β → γys:LenList n βlist✝:List αlengthOk✝:list✝.length = n⊢ (List.zipWith f { list := list✝, lengthOk := lengthOk✝ }.list ys.list).length = n; cases ysmk.mkα:Type uβ:Type uγ:Type ?u.15n:Natf:α → β → γlist✝¹:List αlengthOk✝¹:list✝.length = nlist✝:List βlengthOk✝:list✝.length = n⊢ (List.zipWith f { list := list✝¹, lengthOk := lengthOk✝¹ }.list { list := list✝, lengthOk := lengthOk✝ }.list).length =
  n
    simp [List.length_zipWith, *]All goals completed! 🐙

这个行为良好的 Applicative 实例逐元素地将函数应用于实参。由于 Applicative 扩展了 Functor，无需另外定义 Functor 实例；map 可以作为 Applicative 实例的一部分来定义。

instance : Applicative (LenList n) where
  map := LenList.map
  pure x := {
    list := List.replicate n x
    lengthOk := List.length_replicate
  }
  seq {α β} fs xs := fs.zipWith (· ·) (xs ())

这个行为良好的 Monad 实例取函数应用结果的对角线：

@[simp]
theorem LenList.list_length_eq (xs : LenList n α) :
    xs.list.length = n := byα:Type un:Natxs:LenList n α⊢ xs.list.length = n
  cases xsmkα:Type un:Natlist✝:List αlengthOk✝:list✝.length = n⊢ { list := list✝, lengthOk := lengthOk✝ }.list.length = n
  simp [*]All goals completed! 🐙

def LenList.diagonal (square : LenList n (LenList n α)) : LenList n α :=
  match n with
  | 0 => ⟨[], rfl⟩
  | n' + 1 => {
    list :=
      square.head.head :: (square.tail.map (·.tail)).diagonal.list
    lengthOk := byα:Type uβ:Type un:Natn':Natsquare:LenList (n' + 1) (LenList (n' + 1) α)⊢ (square.head.head :: (diagonal (map (fun x => x.tail) square.tail)).list).length = n' + 1 simpAll goals completed! 🐙
  }

在线查看 ↪

类型类

Alternative.{u, v} (f : Type u → Type v) : Type (max (u + 1) v)
Alternative.{u, v} (f : Type u → Type v) :
  Type (max (u + 1) v)

Alternative 函子是一个可以“失败”或“为空”的 Applicative 函子，并带有二元运算 <|>，该运算会“收集值”或寻找“最靠左的成功”。

重要实例包括：

Option，其中 failure := none，而 <|> 返回最靠左的 some。
解析器组合子通常为错误处理和回溯提供 Applicative 实例。

错误恢复与状态可能以微妙方式相互作用。例如，OptionT (StateT σ Id) 的 Alternative 实现在从失败中恢复时保留对状态所作的修改，而 StateT σ (OptionT Id) 则丢弃这些修改。

实例构造子

Alternative.mk.{u, v}

扩展

Applicative f

方法

map : {α β : Type u} → (α → β) → f α → f β

继承自父结构。

mapConst : {α β : Type u} → α → f β → f α

继承自父结构。

pure : {α : Type u} → α → f α

继承自父结构。

seq : {α β : Type u} → f (α → β) → (Unit → f α) → f β

继承自父结构。

seqLeft : {α β : Type u} → f α → (Unit → f β) → f α

继承自父结构。

seqRight : {α β : Type u} → f α → (Unit → f β) → f β

继承自父结构。

failure : {α : Type u} → f α

产生空集合或可恢复的失败。<|> 运算符收集值或从失败中恢复。详见 Alternative。

orElse : {α : Type u} → f α → (Unit → f α) → f α

依照 Alternative 实例，收集值或通过返回最靠左的成功从 failure 中恢复。也可使用 <|> 运算符语法书写。

类型类

Bind.{u, v} (m : Type u → Type v) : Type (max (u + 1) v)
Bind.{u, v} (m : Type u → Type v) :
  Type (max (u + 1) v)

>>= 运算符通过 bind 的实例重载。

Bind 通常经由扩展它的 Monad 使用。

实例构造子

Bind.mk.{u, v}

方法

bind : {α β : Type u} → m α → (α → m β) → m β

依次执行两个计算，并允许第二个计算依赖第一个计算所得的值。

若 x : m α 且 f : α → m β，则 x >>= f : m β 表示执行 x 得到类型为 α 的值，然后将它传给 f 所得的结果。

标识符中记法的约定：

>>= 在标识符中的推荐拼写是 bind。

类型类

Monad.{u, v} (m : Type u → Type v) : Type (max (u + 1) v)
Monad.{u, v} (m : Type u → Type v) :
  Type (max (u + 1) v)

单子是函数式编程中顺序控制流与副作用的一种抽象。单子既允许副作用依次执行，也允许依赖数据的副作用：较早步骤产生的值可以影响较晚步骤执行的副作用。

可以直接使用 Monad 接口。不过，最常见的用法是通过 do 记法访问它。

大多数 Monad 实例会提供 pure 和 bind 的实现，并对从 Applicative 继承的其他方法使用默认实现。单子应满足某些定律，但实例不要求证明这一点。LawfulMonad 实例表示给定单子的运算是合法的。

实例构造子

Monad.mk.{u, v}

扩展

Applicative m
Bind m

方法

map : {α β : Type u} → (α → β) → m α → m β

继承自父结构。

mapConst : {α β : Type u} → α → m β → m α

继承自父结构。

pure : {α : Type u} → α → m α

继承自父结构。

seq : {α β : Type u} → m (α → β) → (Unit → m α) → m β

继承自父结构。

seqLeft : {α β : Type u} → m α → (Unit → m β) → m α

继承自父结构。

seqRight : {α β : Type u} → m α → (Unit → m β) → m β

继承自父结构。

bind : {α β : Type u} → m α → (α → m β) → m β

继承自父结构。

18. 函子、单子与 do 记法🔗

18. 函子、单子与 `do` 记法🔗