5.4. 选择子🔗

5.4.1. 从失败中恢复🔗

Validate 还可以用于当输入有多种可接受方式的情况。对于输入表单 RawInput，实现来自遗留系统的约定的替代业务规则集合可能如下：

所有人类用户必须提供四位数的出生年份。
由于旧记录不完整，1970年以前出生的用户不需要提供姓名。
1970年以后出生的用户必须提供姓名。
公司应输入 "FIRM" 作为其出生年份并提供公司名称。

对于出生于1970年的用户，没有做出特别的规定。预计他们要么放弃，要么谎报出生年份，要么打电话咨询。公司认为这是可以接受的经营成本。

以下归纳类型捕获了可以从这些既定规则中生成的值：

abbrev NonEmptyString := {s : String // s ≠ ""}

inductive LegacyCheckedInput where
  | humanBefore1970 :
    (birthYear : {y : Nat // y > 999 ∧ y < 1970}) →
    String →
    LegacyCheckedInput
  | humanAfter1970 :
    (birthYear : {y : Nat // y > 1970}) →
    NonEmptyString →
    LegacyCheckedInput
  | company :
    NonEmptyString →
    LegacyCheckedInput
deriving Repr

然而，一个针对这些规则的验证器会更复杂，因为它必须处理所有三种情况。虽然可以将其写成一系列嵌套的 if 表达式，但更容易的方式是独立设计这三种情况，然后再将它们组合起来。这需要一种在保留错误信息的同时从失败中恢复的方法：

def Validate.orElse
    (a : Validate ε α)
    (b : Unit → Validate ε α) :
    Validate ε α :=
  match a with
  | .ok x => .ok x
  | .errors errs1 =>
    match b () with
    | .ok x => .ok x
    | .errors errs2 => .errors (errs1 ++ errs2)

这种从失败中恢复的模式非常常见，以至于 Lean 为此内置了一种语法，并将其附加到了一个名为 OrElse 的类型类上：

class OrElse (α : Type) where
  orElse : α → (Unit → α) → α

表达式 E1 <|> E2 是 OrElse.orElse E1 (fun () => E2) 的简写形式。 Validate 的 OrElse 实例允许使用这种语法去进行错误恢复：

instance : OrElse (Validate ε α) where
  orElse := Validate.orElse

LegacyCheckedInput 的验证器可以由每个构造子的验证器构建而成。对于公司的规则，规定了其出生年份应为字符串 "FIRM"，且名称应为非空。然而，构造子 LegacyCheckedInput.company 根本没有出生年份的表示，因此无法通过 <*> 去轻松执行此操作。关键是使用一个带有 <*> 的函数，该函数忽略其参数。

检查布尔条件成立而不将此事实的任何证据记录在类型中，可以通过 checkThat 来完成：

def checkThat (condition : Bool)
    (field : Field) (msg : String) :
    Validate (Field × String) Unit :=
  if condition then pure () else reportError field msg

checkCompany 的这个定义使用了 checkThat，然后丢弃了结果中的 Unit 值：

def checkCompany (input : RawInput) :
    Validate (Field × String) LegacyCheckedInput :=
  pure (fun () name => .company name) <*>
    checkThat (input.birthYear == "FIRM")
      "birth year" "FIRM if a company" <*>
    checkName input.name

然而，这个定义相当嘈杂。它可以通过两种方式简化。第一种是将第一次使用的 <*> 替换为一个专门的版本，该版本会自动忽略第一个参数返回的值，称为 *>。这个运算符也由一个名为 SeqRight 的类型类控制，E1 *> E2 是 SeqRight.seqRight E1 (fun () => E2) 的语法糖：

class SeqRight (f : Type → Type) where
  seqRight : f α → (Unit → f β) → f β

seqRight 有一个基于 seq 的默认实现：seqRight (a : f α) (b : Unit → f β) : f β := pure (fun _ x => x) <*> a <*> b ()。

使用 seqRight，checkCompany 变得更简单：

def checkCompany (input : RawInput) :
    Validate (Field × String) LegacyCheckedInput :=
  checkThat (input.birthYear == "FIRM")
    "birth year" "FIRM if a company" *>
  pure .company <*> checkName input.name

还有一种简化是可能的。对于每个 Applicative，pure f <*> E 等价于 f <$> E。换句话说，使用 seq 来应用一个通过 pure 放入 Applicative 类型的函数是大材小用，该函数本可以直接使用 Functor.map 来应用。这种简化产生：

def checkCompany (input : RawInput) :
    Validate (Field × String) LegacyCheckedInput :=
  checkThat (input.birthYear == "FIRM")
    "birth year" "FIRM if a company" *>
  .company <$> checkName input.name

LegacyCheckedInput 的其余两个构造子对其字段使用子类型。一个用于检查子类型的通用工具将使这些更容易阅读：

def checkSubtype {α : Type} (v : α) (p : α → Prop) [Decidable (p v)]
    (err : ε) : Validate ε {x : α // p x} :=
  if h : p v then
    pure ⟨v, h⟩
  else
    .errors { head := err, tail := [] }

在函数的参数列表中，类型类 [Decidable (p v)] 出现在参数 v 和 p 的规范之后是很重要的。否则，它将引用一组额外的自动隐式参数，而不是手动提供的值。 Decidable 实例允许使用 if 检查命题 p v。

两种人类情况不需要任何额外的工具：

def checkHumanBefore1970 (input : RawInput) :
    Validate (Field × String) LegacyCheckedInput :=
  (checkYearIsNat input.birthYear).andThen fun y =>
    .humanBefore1970 <$>
      checkSubtype y (fun x => x > 999 ∧ x < 1970)
        ("birth year", "less than 1970") <*>
      pure input.name

def checkHumanAfter1970 (input : RawInput) :
    Validate (Field × String) LegacyCheckedInput :=
  (checkYearIsNat input.birthYear).andThen fun y =>
    .humanAfter1970 <$>
      checkSubtype y (· > 1970)
        ("birth year", "greater than 1970") <*>
      checkName input.name

三种情况的验证器可以使用 <|> 组合：

def checkLegacyInput (input : RawInput) :
    Validate (Field × String) LegacyCheckedInput :=
  checkCompany input <|>
  checkHumanBefore1970 input <|>
  checkHumanAfter1970 input

成功的情况返回 LegacyCheckedInput 的构造子，正如预期的那样：

Validate.ok (LegacyCheckedInput.company "Johnny's Troll Groomers")#eval checkLegacyInput ⟨"Johnny's Troll Groomers", "FIRM"⟩

Validate.ok (LegacyCheckedInput.company "Johnny's Troll Groomers")

Validate.ok (LegacyCheckedInput.humanBefore1970 1963 "Johnny")#eval checkLegacyInput ⟨"Johnny", "1963"⟩

Validate.ok (LegacyCheckedInput.humanBefore1970 1963 "Johnny")

Validate.ok (LegacyCheckedInput.humanBefore1970 1963 "")#eval checkLegacyInput ⟨"", "1963"⟩

Validate.ok (LegacyCheckedInput.humanBefore1970 1963 "")

最糟糕的输入返回所有可能的失败：

Validate.errors
  { head := ("birth year", "FIRM if a company"),
    tail := [("name", "Required"),
             ("birth year", "less than 1970"),
             ("birth year", "greater than 1970"),
             ("name", "Required")] }#eval checkLegacyInput ⟨"", "1970"⟩

Validate.errors
  { head := ("birth year", "FIRM if a company"),
    tail := [("name", "Required"),
             ("birth year", "less than 1970"),
             ("birth year", "greater than 1970"),
             ("name", "Required")] }

5.4.2. Alternative 类🔗

许多类型支持失败和恢复的概念。来自在各种单子中求值算术表达式一节中的 Many 单子就是这样一种类型，Option 也是。两者都支持失败而不提供原因（不像 Except 和 Validate，它们需要一些关于出了什么问题的指示）。

Alternative 类描述了具有用于失败和恢复的额外运算符的应用函子：

class Alternative (f : Type → Type) extends Applicative f where
  failure : f α
  orElse : f α → (Unit → f α) → f α

就像 Add α 的实现者免费获得 HAdd α α α 实例一样，Alternative 的实现者免费获得 OrElse 实例：

instance [Alternative f] : OrElse (f α) where
  orElse := Alternative.orElse

Option 的 Alternative 实现保留第一个非 none 参数：

instance : Alternative Option where
  failure := none
  orElse
    | some x, _ => some x
    | none, y => y ()

同样，Many 的实现遵循 Many.union 的一般结构，由于导致惰性的 Unit 参数放置位置不同而略有差异：

def Many.orElse : Many α → (Unit → Many α) → Many α
  | .none, ys => ys ()
  | .more x xs, ys => .more x (fun () => orElse (xs ()) ys)

instance : Alternative Many where
  failure := .none
  orElse := Many.orElse

像其他类型类一样，Alternative 能够定义适用于实现 Alternative 的任何应用函子的各种操作。其中最重要的是 guard，当可判定命题为假时，它会导致 failure：

def guard [Alternative f] (p : Prop) [Decidable p] : f Unit :=
  if p then
    pure ()
  else failure

在单子程序中提前终止执行非常有用。在 Many 中，它可以用来过滤掉搜索的整个分支，如下面的程序计算自然数的所有偶数除数：

def Many.countdown : Nat → Many Nat
  | 0 => .none
  | n + 1 => .more n (fun () => countdown n)

def evenDivisors (n : Nat) : Many Nat := do
  let k ← Many.countdown (n + 1)
  guard (k % 2 = 0)
  guard (n % k = 0)
  pure k

在 20 上运行它会产生预期的结果：

[20, 10, 4, 2]#eval (evenDivisors 20).takeAll

[20, 10, 4, 2]

5.4.3. 练习🔗

5.4.3.1. 提高验证友好性🔗

使用 <|> 的 Validate 程序返回的错误可能难以阅读，因为包含在错误列表中仅仅意味着可以通过某些代码路径到达该错误。可以使用更结构化的错误报告来更准确地指导用户完成该过程：

将 Validate.errors 中的 NonEmptyList 替换为裸类型变量，然后更新 Applicative (Validate ε) 和 OrElse (Validate ε α) 实例的定义，仅要求有一个可用的 Append ε 实例。
定义一个函数 Validate.mapErrors : Validate ε α → (ε → ε') → Validate ε' α，它转换验证运行中的所有错误。
使用数据类型 TreeError 来表示错误，重写遗留验证系统以跟踪其通过三个备选方案的路径。
编写一个函数 report : TreeError → String，输出 TreeError 累积的警告和错误的对用户友好的视图。

inductive TreeError where
  | field : Field → String → TreeError
  | path : String → TreeError → TreeError
  | both : TreeError → TreeError → TreeError

instance : Append TreeError where
  append := .both