完整定义

现在所有相关的语言特性都已介绍完毕，本节将讲述 Lean 的标准库中 Functor、Applicative 和 Monad 的完整、准确的定义。为了便于理解，没有任何细节会被省略。

函子

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 的函数参数可以演示它的实用性：

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

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

实际的函数具有以下签名：

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

这里，类型参数 β 是一个显式参数，因此 Functor.mapConst 的默认定义提供了一个 _ 参数，这个参数指示着 Lean 去找到一个唯一的类型来传递给 Function.const，以使程序通过类型检查。 (Function.comp map (Function.const _) : α → f β → f α) 等价于 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

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

应用类型类

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 函数在关于选择子和验证的小节中介绍过，从作用的角度来看，它是最容易理解的。 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 α，与 seqRight 的类型相同，只是它返回 f α。 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 的默认实现非常简洁。将其中一些名称替换为它们的语法糖或它们的定义可以提供另一种视角，因此：

fun a b => 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 的默认实现非常相似，只不过 const 有一个额外的参数 id。这个定义可以类似地理解，首先引入一些标准的语法糖，然后用它们的定义替换一些名称：

fun a b => Seq.seq (Functor.map (Function.const _ id) a) b
===>
fun a b => Seq.seq ((fun _ => id) <$> a) b
===>
fun a b => Seq.seq ((fun _ => fun x => x) <$> a) b
===>
fun 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 一起使用时，其值会被丢弃。

单子

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

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

Monad 扩展自 Applicative，以及 Bind：

class Monad (m : Type u → Type v) extends Applicative m, Bind m : Type (max (u+1) v) 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 的实例。

练习

通过研究诸如 Option 和 Except 等例子来理解 Monad 中 map、seq、seqLeft 和 seqRight 的默认实现。换句话说，将它们对 bind 和 pure 的定义去替换默认定义，并简化它们以恢复手写版本的 map、seq、seqLeft 和 seqRight。
在纸上或文本文件中，向自己证明 map 和 seq 的默认实现满足 Functor 和 Applicative 的契约。在这个论证中，你允许使用 Monad 契约中的规则以及普通的表达式求值。

Lean 函数式编程

完整定义

函子

应用类型类

单子

练习