5.2. 应用函子🔗

应用函子是具有两个额外可用操作的函子：pure 和 seq。 pure 与 Monad 中使用的是同一个运算符，因为 Monad 实际上继承自 Applicative。 seq 很像 map：它允许使用一个函数来变换某个数据类型中的内容。然而，对于 seq，函数本身也包含在该数据类型中：f (α → β) → (Unit → f α) → f β。将函数置于类型 f 之下，使得 Applicative 实例能够控制该函数如何被应用，而 Functor.map 则无条件地应用一个函数。第二个参数的类型以 Unit → 开头，以便在函数永远不会被应用的情况下，允许 seq 的定义短路。

这种短路行为的价值可以在 Applicative Option 的实例中看到：

instance : Applicative Option where
  pure x := .some x
  seq f x :=
    match f with
    | none => none
    | some g => g <$> x ()

在这种情况下，如果没有可供 seq 应用的函数，那么就无需计算其参数，因此 x 永远不会被调用。同样的考虑也影响了 Except 的 Applicative 实例：

instance : Applicative (Except ε) where
  pure x := .ok x
  seq f x :=
    match f with
    | .error e => .error e
    | .ok g => g <$> x ()

这种短路行为仅依赖于包围该函数的 Option 或 Except 结构，而不依赖于函数本身。

单子可以看作是在纯函数式语言中捕获顺序执行语句这一概念的一种方式。一个语句的结果可以影响接下来运行哪些语句。这可以从 bind 的类型中看出：m α → (α → m β) → m β。第一个语句产生的值会作为输入传给一个函数，该函数计算下一个要执行的语句。连续使用 bind 就像命令式编程语言中的语句序列，而 bind 足够强大，可以实现条件和循环等控制结构。

按照这个类比，Applicative 捕获的是带有副作用的语言中的函数应用。在 Kotlin 或 C# 这样的语言中，函数的参数从左到右求值。较早参数执行的副作用发生在较晚参数执行的副作用之前。然而，函数本身并不足以实现依赖于某个参数具体值的自定义短路运算符。

通常不会直接调用 seq。相反，会使用运算符 <*>。该运算符把它的第二个参数包装在 fun () => ... 中，从而简化调用位置。换言之，E1 <*> E2 是 Seq.seq E1 (fun () => E2) 的语法糖。

使 seq 能够与多个参数一起使用的关键特性在于，Lean 中的多参数函数实际上是一个单参数函数，它返回另一个正在等待其余参数的函数。换言之，如果 seq 的第一个参数正在等待多个参数，那么 seq 的结果将会等待其余参数。例如，some Plus.plus 可以具有类型 Option (Nat → Nat → Nat)。提供一个参数 some Plus.plus <*> some 4 后，得到类型 Option (Nat → Nat)。这本身又可以与 seq 一起使用，因此 some Plus.plus <*> some 4 <*> some 7 具有类型 Option Nat。

并非每个函子都是应用函子。 Pair 类似于内建的积类型 Prod：

structure Pair (α β : Type) : Type where
  first : α
  second : β

与 Except 一样，Pair 的类型是 Type → Type → Type。这意味着 Pair α 的类型是 Type → Type，并且可以给出一个 Functor 实例：

instance : Functor (Pair α) where
  map f x := ⟨x.first, f x.second⟩

此实例遵守 Functor 契约。

需要检查的两个性质是 id <$> Pair.mk x y = Pair.mk x y 以及 f <$> g <$> Pair.mk x y = (f ∘ g) <$> Pair.mk x y。第一个性质可以只通过逐步求值左侧来检查，并注意到它求值为右侧：

              id <$> Pair.mk x yPair.mk x (id y)Pair.mk x y

第二个可以通过逐步执行两边并注意到它们产生相同结果来检查：

              f <$> g <$> Pair.mk x yf <$> Pair.mk x (g y)Pair.mk x (f (g y))

              (f ∘ g) <$> Pair.mk x yPair.mk x ((f ∘ g) y)Pair.mk x (f (g y))

然而，尝试定义一个 Applicative 实例并不顺利。它将需要一个 pure 的定义：

def Pair.pure (x : β) : Pair α β := don't know how to synthesize placeholder
context:
β α:Typex:β⊢ Pair α β_

don't know how to synthesize placeholder
context:
β α:Typex:β⊢ Pair α β

作用域中有一个类型为 β 的值（即 x），而下划线给出的错误消息提示下一步是使用构造子 Pair.mk：

def Pair.pure (x : β) : Pair α β := Pair.mk don't know how to synthesize placeholder for argument `first`
context:
β α:Typex:β⊢ α_ x

don't know how to synthesize placeholder for argument `first`
context:
β α:Typex:β⊢ α

遗憾的是，并不存在可用的 α。因为为了定义 Applicative (Pair α) 的实例，pure 必须对所有可能的类型 α 都起作用，所以这是不可能的。毕竟，调用者可以选择令 α 为 Empty，而它根本没有任何值。

5.2.1. 一个非单子的应用函子🔗

在验证表单中的用户输入时，通常认为最好一次性提供多个错误，而不是一次只提供一个错误。这使用户能够总体了解需要做什么才能让计算机满意，而不是在逐个字段纠正错误时感到不断被催促。

理想情况下，验证用户输入这一事实应当在执行验证的函数类型中可见。它应当返回一个具体的数据类型——例如，检查一个文本框是否包含数字时，应当返回真正的数值类型。验证例程可以在输入未通过验证时抛出异常。然而，异常有一个主要缺点：它们会在第一个错误处终止程序，从而使得累积错误列表成为不可能。

另一方面，累积错误列表并在其非空时失败这一常见设计模式也有问题。一长串嵌套的 if 语句若逐一验证输入数据的各个小节，会很难维护，并且很容易漏掉一两条错误消息。理想情况下，验证应当能够通过一个 API 执行；该 API 既允许返回一个新值，又能自动跟踪并累积错误消息。

一个名为 Validate 的应用函子提供了一种实现这种 API 风格的方法。类似于 Except 单子，Validate 允许构造一个新值，以准确刻画经过验证的数据。不同于 Except，它允许累积多个错误，而没有忘记检查列表是否为空的风险。

5.2.1.1. 用户输入🔗

作为用户输入的一个例子，考虑如下结构：

structure RawInput where
  name : String
  birthYear : String

要实现的业务逻辑如下：

名称不得为空
出生年份必须是数字且非负
出生年份必须大于 1900，并且小于或等于该表单被验证时所在的年份

将这些表示为一个数据类型将需要一种称为子类型的新特性。有了这个工具，就可以编写一个使用应用函子来跟踪错误的验证框架，并在该框架中实现这些规则。

5.2.1.2. 子类型🔗

表示这些条件最容易的方式是使用一个额外的 Lean 类型，称为 Subtype：

structure Subtype {α : Type} (p : α → Prop) where
  val : α
  property : p val

这个结构有两个类型参数：一个隐式参数，即数据 α 的类型；以及一个显式参数 p，它是关于 α 的谓词。谓词是一个含有变量的逻辑陈述；用一个值替换该变量即可得到实际陈述，例如GetElem 的参数，它描述索引对于一次查找而言处于界内意味着什么。在 Subtype 的情形中，该谓词从 α 的值中切分出使谓词成立的某个子集。该结构的两个字段分别是来自 α 的一个值，以及该值满足谓词 p 的证据。 Lean 对 Subtype 有特殊语法。如果 p 的类型是 α → Prop，那么类型 Subtype p 也可以写作 {x : α // p x}，甚至在类型 α 能被自动推断时写作 {x // p x}。

将正数表示为归纳类型清晰明了，并且易于编程使用。然而，它有一个关键缺点。虽然从 Lean 程序的角度看，Nat 和 Int 具有普通归纳类型的结构，但编译器会对它们作特殊处理，并使用快速的任意精度数值库来实现它们。对于额外的用户定义类型，情况并非如此。不过，Nat 的一个将其限制为非零数的子类型，使得新类型既能使用高效表示，又仍能在编译时排除零：

def FastPos : Type := {x : Nat // x > 0}

最小的快速正数仍然是一。现在，它不再是归纳类型的构造子，而是一个用尖括号构造的结构实例。第一个参数是底层的 Nat，第二个参数是说明该 Nat 大于零的证据：

def one : FastPos := ⟨1, by⊢ 1 > 0 decideAll goals completed! 🐙⟩

命题 1 > 0 是可判定的，因此 decide 策略会产生必要的证据。 OfNat 实例非常类似于 Pos 的实例，只是它使用一个简短的策略证明来提供 n + 1 > 0 的证据：

instance : OfNat FastPos (n + 1) where
  ofNat := ⟨n + 1, byn:Nat⊢ n + 1 > 0 simpAll goals completed! 🐙⟩

这里需要 simp，因为 decide 需要具体的值，但所讨论的命题是 n + 1 > 0。

子类型是一把双刃剑。它们允许高效地表示验证规则，但也把维护这些规则的负担转移给库的用户，用户必须证明自己没有违反重要的不变量。一般而言，将它们用于库的内部是个好主意，同时向用户提供一个能自动确保所有不变量都得到满足的 API，并将任何必要证明都保留在库的内部。

检查类型为 α 的值是否属于子类型 {x : α // p x}，通常要求命题 p x 是可判定的。关于相等性和序关系类的一节描述了可判定命题如何与 if 一起使用。当 if 与一个可判定命题一起使用时，可以提供一个名称。在 then 分支中，该名称绑定到该命题为真的证据；在 else 分支中，它绑定到该命题为假的证据。这在检查给定的 Nat 是否为正时很有用：

def Nat.asFastPos? (n : Nat) : Option FastPos :=
  if h : n > 0 then
    some ⟨n, h⟩
  else none

在 then 分支中，h 被绑定为表明 n > 0 的证据，而此证据可用作 Subtype 的构造子的第二个实参。

5.2.1.3. 已验证的输入🔗

经过验证的用户输入是一个结构，它使用多种技术表达业务逻辑：

该结构类型本身编码了它被检查为有效时的年份，因此 CheckedInput 2019 与 CheckedInput 2020 不是同一个类型
出生年份表示为 Nat，而不是 String
子类型用于约束名称字段和诞生年份字段中的允许值

structure CheckedInput (thisYear : Nat) : Type where
  name : {n : String // n ≠ ""}
  birthYear : {y : Nat // y > 1900 ∧ y ≤ thisYear}

输入验证器应当以当前年份和一个 RawInput 作为实参，并返回一个已检查的输入，或者至少一个验证失败。这由 Validate 类型表示：

inductive Validate (ε α : Type) : Type where
  | ok : α → Validate ε α
  | errors : NonEmptyList ε → Validate ε α

它看起来非常像 Except。唯一的区别是，errors 构造子可以包含不止一个失败。

Validate 是一个函子。在其上映射一个函数，会变换其中可能存在的任何成功值，就如同 Except 的 Functor 实例中那样：

instance : Functor (Validate ε) where
  map f
   | .ok x => .ok (f x)
   | .errors errs => .errors errs

Validate 的 Applicative 实例与 Except 的实例有一个重要区别：Except 的实例会在遇到第一个错误时终止，而 Validate 的实例会谨慎地累积来自函数分支和参数分支两者的所有错误：

instance : Applicative (Validate ε) where
  pure := .ok
  seq f x :=
    match f with
    | .ok g => g <$> (x ())
    | .errors errs =>
      match x () with
      | .ok _ => .errors errs
      | .errors errs' => .errors (errs ++ errs')

将 .errors 与 NonEmptyList 的构造子一起使用有些冗长。像 reportError 这样的辅助函数能使代码更可读。在此应用中，错误报告将由字段名与消息配对组成：

def Field := String

def reportError (f : Field) (msg : String) : Validate (Field × String) α :=
  .errors { head := (f, msg), tail := [] }

Validate 的 Applicative 实例允许分别编写每个字段的检查过程，然后将它们组合起来。检查名称包括确保字符串非空，然后以 Subtype 的形式返回这一事实的证据。这使用了 if 的证据绑定版本：

def checkName (name : String) :
    Validate (Field × String) {n : String // n ≠ ""} :=
  if h : name = "" then
    reportError "name" "Required"
  else pure ⟨name, h⟩

在 then 分支中，h 被绑定为表明 name = "" 的证据；而在 else 分支中，它被绑定为表明 ¬name = "" 的证据。

确实有些验证错误会使其他检查无法进行。例如，如果一个困惑的用户写下单词 "syzygy" 而不是一个数字，那么检查出生年份字段是否大于 1900 就毫无意义。只有在确保该字段事实上包含一个数字之后，检查该数字的允许范围才有意义。这可以用函数 andThen 表达：

def Validate.andThen (val : Validate ε α)
    (next : α → Validate ε β) : Validate ε β :=
  match val with
  | .errors errs => .errors errs
  | .ok x => next x

虽然此函数的类型签名使其适合在 Monad 实例中用作 bind，但有充分理由不这样做。这些理由在描述 Applicative 约定的那一节中说明。

为了检查出生年份是否为数字，一个名为 String.toNat? : String → Option Nat 的内置函数很有用。最为用户友好的做法是先使用 String.trim 去除首尾空白：

def checkYearIsNat (year : String) : Validate (Field × String) Nat :=
  match year.trim.toNat? with
  | none => reportError "birth year" "Must be digits"
  | some n => pure n

为了检查所提供的年份是否处于预期范围内，应当嵌套使用 if 的提供证据形式：

def checkBirthYear (thisYear year : Nat) :
    Validate (Field × String) {y : Nat // y > 1900 ∧ y ≤ thisYear} :=
  if h : year > 1900 then
    if h' : year ≤ thisYear then
      pure ⟨year, bythisYear:Natyear:Nath:year > 1900h':year ≤ thisYear⊢ year > 1900 ∧ year ≤ thisYear simp [*]All goals completed! 🐙⟩
    else reportError "birth year" s!"Must be no later than {thisYear}"
  else reportError "birth year" "Must be after 1900"

最后，可以使用 <*> 将这三个组成部分组合起来：

def checkInput (year : Nat) (input : RawInput) :
    Validate (Field × String) (CheckedInput year) :=
  pure CheckedInput.mk <*>
    checkName input.name <*>
    (checkYearIsNat input.birthYear).andThen fun birthYearAsNat =>
      checkBirthYear year birthYearAsNat

测试 checkInput 表明，它确实可以返回多条反馈：

Validate.ok { name := "David", birthYear := 1984 }#eval checkInput 2023 {name := "David", birthYear := "1984"}

Validate.ok { name := "David", birthYear := 1984 }

Validate.errors { head := ("name", "Required"), tail := [("birth year", "Must be no later than 2023")] }#eval checkInput 2023 {name := "", birthYear := "2045"}

Validate.errors { head := ("name", "Required"), tail := [("birth year", "Must be no later than 2023")] }

Validate.errors { head := ("birth year", "Must be digits"), tail := [] }#eval checkInput 2023 {name := "David", birthYear := "syzygy"}

Validate.errors { head := ("birth year", "Must be digits"), tail := [] }

使用 checkInput 进行表单验证，展示了 Applicative 相对于 Monad 的一个关键优势。由于 >>= 提供了足够的能力，可以根据第一步得到的值来修改程序其余部分的执行，它就必须从第一步接收一个值以便继续传递。如果没有接收到值（例如因为发生了错误），那么 >>= 就无法执行程序的其余部分。 Validate 展示了为什么无论如何运行程序的其余部分可能是有用的：在不需要先前数据的情况下，运行程序的其余部分可以产生有用信息（在此情形中，是更多验证错误）。 Applicative 的 <*> 可以在重新组合结果之前运行其两个参数。类似地，>>= 强制顺序执行。每一步都必须完成后，下一步才可以运行。这通常是有用的，但它使得不同线程无法并行执行，而这种并行本可从程序的实际数据依赖关系中自然产生。像 Monad 这样更强大的抽象增加了 API 使用者可获得的灵活性，但降低了 API 实现者可获得的灵活性。