应用函子

应用函子 (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 y
===>
Pair.mk x (id y)
===>
Pair.mk x y

第二个属性可以通过逐步检查两侧来验证，并注意它们产生了相同的结果：

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

(f ∘ g) <$> Pair.mk x y
===>
Pair.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:
β α : Type
x : β
⊢ Pair α β

在当前作用域内有一个类型为 β 的值（即 x），下划线处的错误信息表明了下一步是使用构造子 Pair.mk：

def Pair.pure (x : β) : Pair α β := Pair.mk _ x

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

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

一个非单子的应用函子

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

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

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

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

用户输入

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

structure RawInput where
  name : String
  birthYear : String

要实现的业务逻辑如下：

1. 姓名不能为空
2. 出生年份必须是数字且非负
3. The birth year must be greater than 1900, and less than or equal to the year in which the form is validated 出生年份必须大于1900，并且小于或等于表单被验证的年份

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

子类型

表示这些条件最简单的方法就是使用 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}

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

def one : FastPos := ⟨1, by simp⟩

OfNat 实例十分类似于 Pos 实例，只不过它使用了一个简短的策略证明来提供 n + 1 > 0 的证据：

instance : OfNat FastPos (n + 1) where
  ofNat := ⟨n + 1, by simp_arith⟩

simp_arith 策略是 simp 的一个版本，它考虑了额外的算术恒等式。

子类型是一把双刃剑。 它们允许高效地表示验证规则，但它们将维护这些规则的负担转移到了库的使用者身上，使用者必须 证明 他们没有违反重要的不变量。 通常，最好在库的内部使用子类型，这为使用者提供了一个自动确保满足所有不变量的API，并且将任何必要的证明放在库的内部去进行处理。

检查类型为 α 的值是否属于子类型 {x : α // p x}，通常需要命题 p x 是 可判定的 (Decidable)。 关于相等性和排序类的小节 描述了如何将可判定命题与 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 构造子的第二个参数。

经验证输入

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

• 结构类型本身编码了被检验了有效性的年份，因此 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。 唯一的区别是 error 构造子可能包含多个失败。

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, by simp [*]⟩
    else reportError "birth year" s!"Must be no later than {thisYear}"
  else reportError "birth year" "Must be after 1900"

最后，这三个组件可以使用 seq 进行组合：

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 体现了它确实可以返回多条反馈信息：

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

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

#eval checkInput 2023 {name := "", birthYear := "2045"}

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

#eval checkInput 2023 {name := "David", birthYear := "syzygy"}

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

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