5.6. 完整定义🔗

既然所有相关语言特性都已经介绍完毕，本节将说明 Lean 标准库中 Functor、Applicative 和 Monad 实际出现时的完整、真实定义。为便于理解，这里不省略任何细节。

5.6.1. 函子🔗

Functor 类的完整定义使用了宇宙多态性和默认方法实现：

class Functor (f : Type u → Type v) : Type (max (u+1) v) where
  map : {α β : Type u} → (α → β) → f α → f β
  mapConst : {α β : Type u} → α → f β → f α :=
    Function.comp map (Function.const _)

在这个定义中，Function.comp 是函数复合，通常用 ∘ 运算符书写。 Function.const 是常量函数，它是一个二元函数，会忽略其第二个参数。只将此函数应用于一个参数，会产生一个总是返回同一值的函数；当 API 要求一个函数而程序并不需要针对不同参数计算不同结果时，这很有用。 Function.const 的一个简单版本可以写成如下形式：

def simpleConst (x : α) (_ : β) : α := x

将它以一个参数作为传给 List.map 的函数参数来使用，可以展示它的效用：

["same", "same", "same"]#eval [1, 2, 3].map (simpleConst "same")

["same", "same", "same"]

实际函数具有如下签名：

Function.const.{u, v} {α : Sort u} (β : Sort v) (a : α) : β → α

这里，类型实参 β 是一个显式实参，因此 mapConst 的默认定义提供了一个 _ 实参，指示 Lean 寻找一个唯一的类型传递给 Function.const，使程序能够通过类型检查。 Function.comp map (Function.const _) 等价于 fun (x : α) (y : f β) => map (fun _ => x) y。

Functor 类型类居于一个宇宙中，该宇宙是 u+1 与 v 中较大的那个。这里，u 是作为参数传给 f 时所接受的宇宙层级，而 v 是 f 返回的宇宙。要理解为什么实现 Functor 类型类的结构必须位于一个大于 u 的宇宙中，可以从该类的一个简化定义开始：

class Functor (f : Type u → Type v) : Type (max (u+1) v) where
  map : {α β : Type u} → (α → β) → f α → f β

这个类型类的结构类型等价于以下归纳类型：

inductive Functor (f : Type u → Type v) : Type (max (u+1) v) where
  | mk : ({α β : Type u} → (α → β) → f α → f β) → Functor f

作为参数传递给 mk 的 map 方法的实现包含一个函数，该函数以 Type u 中的两个类型作为参数。这意味着该函数本身的类型位于 Type (u+1) 中，因此 Functor 也必须处于至少为 u+1 的层级。类似地，该函数的其他参数具有通过应用 f 构造出的类型，因此它也必须具有至少为 v 的层级。本节中的所有类型类都具有这一性质。

5.6.2. 应用函子🔗

Applicative 类型类实际上由若干更小的类构成，每个类都包含一部分相关方法。首先是 Pure 和 Seq，它们分别包含 pure 和 seq：

class Pure (f : Type u → Type v) : Type (max (u+1) v) where
  pure {α : Type u} : α → f α

class Seq (f : Type u → Type v) : Type (max (u+1) v) where
  seq : {α β : Type u} → f (α → β) → (Unit → f α) → f β

除此之外，Applicative 还依赖于 SeqRight 以及一个类似的 SeqLeft 类：

class SeqRight (f : Type u → Type v) : Type (max (u+1) v) where
  seqRight : {α β : Type u} → f α → (Unit → f β) → f β

class SeqLeft (f : Type u → Type v) : Type (max (u+1) v) where
  seqLeft : {α β : Type u} → f α → (Unit → f β) → f α

seqRight 函数是在关于 alternatives 与 validation 的小节中引入的，从效应的角度最容易理解。 E1 *> E2 会脱糖为 SeqRight.seqRight E1 (fun () => E2)，可理解为先执行 E1，然后执行 E2，最终只得到 E2 的结果。来自 E1 的效应可能导致 E2 不运行，或者运行多次。事实上，如果 f 有一个 Monad 实例，那么 E1 *> E2 等价于 do let _ ← E1; E2，但 seqRight 可以用于像 Validate 这样不是单子的类型。

它的近亲 seqLeft 非常相似，只是返回最左侧表达式的值。 E1 <* E2 会被脱糖为 SeqLeft.seqLeft E1 (fun () => E2)。 SeqLeft.seqLeft 的类型为 f α → (Unit → f β) → f α，除了它返回 f α 这一点之外，该类型与 seqRight 的类型相同。 E1 <* E2 可以理解为一个程序：它先执行 E1，然后执行 E2，并返回 E1 的原始结果。如果 f 有一个 Monad 实例，那么 E1 <* E2 等价于 do let x ← E1; _ ← E2; pure x。一般而言，seqLeft 可用于在验证或类似解析器的工作流中为某个值指定额外条件，而不改变该值本身。

Applicative 的定义扩展了所有这些类，并且还扩展了 Functor：

class Applicative (f : Type u → Type v)
    extends Functor f, Pure f, Seq f, SeqLeft f, SeqRight f where
  map      := fun x y => Seq.seq (pure x) fun _ => y
  seqLeft  := fun a b => Seq.seq (Functor.map (Function.const _) a) b
  seqRight := fun a b => Seq.seq (Functor.map (Function.const _ id) a) b

完整定义 Applicative 只需要为 pure 和 seq 给出定义。这是因为来自 Functor、SeqLeft 和 SeqRight 的所有方法都有默认定义。 Functor 的 mapConst 方法有其自身基于 Functor.map 的默认实现。只有在新函数与默认实现行为等价但效率更高时，才应覆盖这些默认实现。这些默认实现应被看作正确性的规范，同时也是自动生成的代码。

seqLeft 的默认实现非常紧凑。将其中一些名称替换为相应的语法糖或定义，可以从另一角度理解它，因此：

Seq.seq (Functor.map (Function.const _) a) b

变为

fun a b => Seq.seq ((fun x _ => x) <$> a) b

应当如何理解 (fun x _ => x) <$> a？这里，a 的类型是 f α，而 f 是一个函子。如果 f 是 List，那么 (fun x _ => x) <$> [1, 2, 3] 求值为 [fun _ => 1, fun _ => 2, fun _ => 3。如果 f 是 Option，那么 (fun x _ => x) <$> some "hello" 求值为 some (fun _ => "hello")。在每种情形中，函子中的值都被替换为返回原值并忽略其参数的函数。当与 seq 结合时，此函数会丢弃来自 seq 的第二个参数的值。

seqRight 的默认实现非常相似，只是 Function.const 有一个额外的参数 id。可以用类似的方式理解这个定义：先引入一些标准的语法糖，然后将某些名称替换为它们的定义：

                fun a b => Seq.seq (Functor.map (Function.const _ id) a) bfun a b => Seq.seq ((fun _ => id) <$> a) bfun a b => Seq.seq ((fun _ => fun x => x) <$> a) bfun a b => Seq.seq ((fun _ x => x) <$> a) b

应当如何理解 (fun _ x => x) <$> a？例子再次很有帮助。 fun _ x => x) <$> [1, 2, 3] 等价于 [fun x => x, fun x => x, fun x => x]，而 (fun _ x => x) <$> some "hello" 等价于 some (fun x => x)。换言之，(fun _ x => x) <$> a 保留了 a 的整体形状，但每个值都被替换为恒等函数。从效果的角度看，a 的副作用会发生，但当它与 seq 一起使用时，其值会被丢弃。

5.6.3. 单子🔗

正如 Applicative 的组成操作被拆分到各自的类型类中一样，Bind 也有自己的类：

class Bind (m : Type u → Type v) where
  bind : {α β : Type u} → m α → (α → m β) → m β

Monad 用 Bind 扩展了 Applicative：

class Monad (m : Type u → Type v) : Type (max (u+1) v)
    extends Applicative m, Bind m where
  map      f x := bind x (Function.comp pure f)
  seq      f x := bind f fun y => Functor.map y (x ())
  seqLeft  x y := bind x fun a => bind (y ()) (fun _ => pure a)
  seqRight x y := bind x fun _ => y ()

追踪整个层级结构中继承方法与默认方法的集合可知，一个 Monad 实例只需要实现 bind 和 pure。换言之，Monad 实例会自动产生 seq、seqLeft、seqRight、map 和 mapConst 的实现。从 API 边界的角度看，任何具有 Monad 实例的类型都会获得 Bind、Pure、Seq、Functor、SeqLeft 和 SeqRight 的实例。

5.6.4. 练习🔗

通过推演诸如 Option 和 Except 这样的例子，理解 Monad 中 map、seq、seqLeft 和 seqRight 的默认实现。换言之，将 bind 和 pure 的定义代入这些默认定义，并将其化简，以恢复出手写时会写出的版本 map、seq、seqLeft 和 seqRight。
在纸上或文本文件中向自己证明，map 和 seq 的默认实现满足 Functor 和 Applicative 的约定。在这个论证中，你可以使用 Monad 约定中的规则以及通常的表达式求值。

5.6.1.	函子
5.6.2.	应用函子
5.6.3.	单子
5.6.4.	练习