5.2. 应用函子🔗

应用函子 (Applicative Functor) 是一种具有两个附加操作的函子：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 结构，而不是函数本身。

单子 (Monad) 可以被看作是一种将按顺序执行语句的概念引入纯函数式语言的方法。一个语句的结果会影响接下来要执行的语句。这可以从 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:β⊢ α

不幸的是，没有可用的 α。因为 pure 需要适用于 所有可能的类型 α ，才能定义 Applicative (Pair α) 的实例，所以这是不可能的。毕竟，调用者可以选择 α 为 Empty，而 Empty 根本没有任何值。

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

在验证表单中的用户输入时，通常认为最好一次性提供多个错误，而不是一次提供一个错误。这样，用户可以大致了解需要做什么才可以满足计算机的要求，而不是逐个对属性地纠正错误时感到烦恼。

理想情况下，验证用户输入将在执行验证的函数类型中可见。它应该返回一个特定的数据类型——例如，检验包含数字的文本框是否返回一个实际的数字类型。验证例程可能会在输入未通过验证时抛出 异常 (Exception)。然而，异常有一个主要缺点：它们在第一个错误出现时终止程序，从而无法累积错误列表。

另一方面，累积错误列表并在列表非空时失效的常见设计模式也是有问题的。一个用于验证输入数据的每个子部分的长嵌套 if 语句序列难以维护，而且很容易遗漏一两条错误信息。理想情况下，可以使用一个 API 来执行验证，该 API 不仅可以返回一个新的值，还能自动跟踪和累积错误信息。

一个名为 Validate 的应用函子提供了一种实现这种风格的 API 的方法。像 Except 单子一样，Validate 允许构造一个准确描述验证数据的新的值与 Except 不同，它允许累积多个错误，而不必担心忘记检查列表是否为空。

5.2.1.1. 用户输入🔗

作为用户输入的示例，请考虑以下结构体：

structure RawInput where
  name : String
  birthYear : String

要实现的业务逻辑如下：

姓名不能为空
出生年份必须是数字且非负
出生年份必须大于1900，并且小于或等于表单被验证的年份

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

5.2.1.2. 子类型🔗

表示这些条件最简单的方法就是使用 Lean 内一种额外的类型，称为 Subtype：

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

这个结构体有两个类型参数：一个是隐式参数，即数据类型 α，另一个是显式参数 p，它是关于 α 的谓词。 谓词 (Predicate) 是一个包含变量的逻辑语句，可以用值替换该变量以产生实际的语句，就像 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 实现者可用的灵活性。