4.6. 额外便利🔗

4.6.1. 共享的参数类型🔗

在定义一个接受多个相同类型参数的函数时，可以把这些参数都写在同一个冒号之前。例如，

def equal? [BEq α] (x : α) (y : α) : Option α :=
  if x == y then
    some x
  else
    none

可以写作

def equal? [BEq α] (x y : α) : Option α :=
  if x == y then
    some x
  else
    none

当类型签名很大时，这尤其有用。

归纳类型的构造子位于命名空间中。这允许多个相关的归纳类型使用相同的构造子名称，但也可能导致程序变得冗长。在已知所讨论的归纳类型的上下文中，可以通过在构造子名称前加一个点来省略命名空间，Lean 会使用期望类型来解析构造子名称。例如，镜像一棵二叉树的函数可以写作：

def BinTree.mirror : BinTree α → BinTree α
  | BinTree.leaf => BinTree.leaf
  | BinTree.branch l x r => BinTree.branch (mirror r) x (mirror l)

省略命名空间会使它显著缩短，但代价是在不包含 Lean 编译器的上下文（例如代码审查工具）中，程序会更难阅读：

def BinTree.mirror : BinTree α → BinTree α
  | .leaf => .leaf
  | .branch l x r => .branch (mirror r) x (mirror l)

使用表达式的期望类型来消解命名空间歧义，也适用于构造子以外的名称。如果 BinTree.empty 被定义为创建 BinTree 的另一种方式，那么它也可以与点记法一起使用：

def BinTree.empty : BinTree α := .leafBinTree.empty : BinTree Nat#check (.empty : BinTree Nat)

BinTree.empty : BinTree Nat

在允许多个模式的上下文中，例如 match 表达式，多个模式可以共享其结果表达式。表示星期几的数据类型 Weekday：

inductive Weekday where
  | monday
  | tuesday
  | wednesday
  | thursday
  | friday
  | saturday
  | sunday
deriving Repr

可以使用模式匹配来检查某一天是否是周末：

def Weekday.isWeekend (day : Weekday) : Bool :=
  match day with
  | Weekday.saturday => true
  | Weekday.sunday => true
  | _ => false

这已经可以通过使用构造子的点记法来简化：

def Weekday.isWeekend (day : Weekday) : Bool :=
  match day with
  | .saturday => true
  | .sunday => true
  | _ => false

由于两个周末模式具有相同的结果表达式（true），它们可以合并为一个：

def Weekday.isWeekend (day : Weekday) : Bool :=
  match day with
  | .saturday | .sunday => true
  | _ => false

这还可以进一步简化为一个不命名参数的版本：

def Weekday.isWeekend : Weekday → Bool
  | .saturday | .sunday => true
  | _ => false

在幕后，结果表达式只是被复制到每个模式中。这意味着模式可以绑定变量，如下面这个例子所示：它从一个和类型中移除 inl 和 inr 构造子，而这两个构造子都包含同一类型的值：

def condense : α ⊕ α → α
  | .inl x | .inr x => x

由于结果表达式会被复制，由模式绑定的变量不必具有相同的类型。可以使用适用于多种类型的重载函数，来编写一个单一的结果表达式，使其适用于绑定不同类型变量的模式：

def stringy : Nat ⊕ Weekday → String
  | .inl x | .inr x => s!"It is {repr x}"

在实践中，只有所有模式共享的变量才能在结果表达式中被引用，因为结果必须对每个模式都有意义。在 getTheNat 中，只有 n 可以被访问；尝试使用 x 或 y 都会导致错误。

def getTheNat : (Nat × α) ⊕ (Nat × β) → Nat
  | .inl (n, x) | .inr (n, y) => n

试图在类似定义中访问 x 会导致错误，因为第二个模式中没有可用的 x：

def getTheAlpha : (Nat × α) ⊕ (Nat × α) → α
  | .inl (n, x) | .inr (n, y) => Unknown identifier `x`x

Unknown identifier `x`

结果表达式本质上被复制粘贴到模式匹配的每个分支这一事实，可能导致一些令人意外的行为。例如，以下定义是可接受的，因为结果表达式的 inr 版本引用的是 str 的全局定义：

def str := "Some string"

def getTheString : (Nat × String) ⊕ (Nat × β) → String
  | .inl (n, str) | .inr (n, y) => str

在两个构造子上调用此函数会揭示这种令人困惑的行为。在第一种情况下，需要一个类型标注来告诉 Lean β 应当是什么类型：

"twenty"#eval getTheString (.inl (20, "twenty") : (Nat × String) ⊕ (Nat × String))

"twenty"

在第二种情况下，使用全局定义：

"Some string"#eval getTheString (.inr (20, "twenty"))

"Some string"

使用或模式可以极大地简化某些定义并提高其清晰度，如 Weekday.isWeekend 所示。由于存在产生混淆行为的可能性，使用它们时应当谨慎，尤其是在涉及多种类型的变量或互不相交的变量集合时。