选择子

从失败中恢复

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 β

基于 seq，seqRight 有一个默认实现：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 的构造子，正如预期的那样：

#eval checkLegacyInput ⟨"Johnny's Troll Groomers", "FIRM"⟩

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

#eval checkLegacyInput ⟨"Johnny", "1963"⟩

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

#eval checkLegacyInput ⟨"", "1963"⟩

Validate.ok (LegacyCheckedInput.humanBefore1970 1963 "")

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

#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")] }

`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 上运行它会产生预期的结果：

#eval (evenDivisors 20).takeAll

[20, 10, 4, 2]

练习题

提高验证的友好性

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

将 Validate.error 中的 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

Lean 函数式编程

选择子

从失败中恢复

Alternative 类

练习题

提高验证的友好性

`Alternative` 类