1.7. 附加便利功能
Lean 包含若干便利特性，使程序能够更加简洁。
1.7.1. 自动隐式参数
在 Lean 中编写多态函数时，通常不必列出所有隐式参数。
相反，只需提及它们即可。
如果 Lean 能够确定它们的类型，那么它们会被自动插入为隐式参数。
换言之，先前对 length 的定义：
def length {α : Type} (xs : List α) : Nat :=
match xs with
| [] => 0
| y :: ys => Nat.succ (length ys)
可以不使用 {α : Type} 来写成：
def length (xs : List α) : Nat :=
match xs with
| [] => 0
| y :: ys => Nat.succ (length ys)这可以极大地简化带有许多隐式参数的高度多态定义。
1.7.2. 模式匹配定义
在使用 def 定义函数时，经常会先命名一个参数，然后立即对它进行模式匹配。
例如，在 length 中，参数 xs 只在 match 中使用。
在这些情况下，可以直接写出 match 表达式的各个情形，而完全不必命名该参数。
第一步是将参数的类型移到冒号右侧，使返回类型成为一个函数类型。
例如，length 的类型是 List α → Nat。
然后，用模式匹配的每一种情况替换 :=：
def length : List α → Nat
| [] => 0
| y :: ys => Nat.succ (length ys)
这种语法也可以用于定义接受多个参数的函数。
在这种情况下，它们的模式以逗号分隔。
例如，drop 接受一个数 n 和一个列表，并在移除前 n 个条目后返回该列表。
def drop : Nat → List α → List α
| Nat.zero, xs => xs
| _, [] => []
| Nat.succ n, x :: xs => drop n xs1.7.3. 局部定义
为计算中的中间步骤命名通常很有用。 在许多情况下，中间值本身就表示有用的概念，显式地为它们命名可以使程序更易读。 在另一些情况下，中间值会被使用多次。 与大多数其他语言一样，在 Lean 中把同一段代码写两次会导致它被计算两次，而将结果保存在变量中则会使计算结果被保存并复用。
例如，unzip 是一个将由对组成的列表转换为由列表组成的对的函数。
当由对组成的列表为空时，unzip 的结果是一对空列表。
当由对组成的列表的头部有一个对时，该对的两个字段会被加入到对列表其余部分进行 unzip 后的结果中。
unzip 的这个定义正是遵循这一描述：
def unzip : List (α × β) → List α × List β
| [] => ([], [])
| (x, y) :: xys =>
(x :: (unzip xys).fst, y :: (unzip xys).snd)遗憾的是，这里有一个问题：这段代码比必要的要慢。 列表中的每个序对条目都会导致两次递归调用，这使得该函数花费指数时间。 然而，两次递归调用会得到相同的结果，因此没有理由进行两次递归调用。
在 Lean 中，可以使用 let 为递归调用的结果命名，从而将其保存下来。
带有 let 的局部定义类似于带有 def 的顶层定义：它接受一个要在局部定义的名称、需要时给出参数、一个类型签名，然后在 := 之后给出主体。
在局部定义之后，可以使用该局部定义的表达式（称为 let 表达式的主体）必须位于新的一行，并且在文件中从小于或等于 let 关键字所在列的位置开始。
在 unzip 中使用 let 的局部定义如下所示：
def unzip : List (α × β) → List α × List β
| [] => ([], [])
| (x, y) :: xys =>
let unzipped : List α × List β := unzip xys
(x :: unzipped.fst, y :: unzipped.snd)
若要在单行中使用 let，请用分号将局部定义与主体分隔开。
使用 let 的局部定义，在一个模式足以匹配某个数据类型的所有情形时，也可以使用模式匹配。
在 unzip 的情形中，递归调用的结果是一个二元组。
因为二元组只有一个构造子，名称 unzipped 可以替换为一个二元组模式：
def unzip : List (α × β) → List α × List β
| [] => ([], [])
| (x, y) :: xys =>
let (xs, ys) : List α × List β := unzip xys
(x :: xs, y :: ys)
与手工编写访问器调用相比，审慎地将模式与 let 配合使用可以使代码更易读。
let 与 def 之间最大的区别在于，递归的 let 定义必须通过写出 let rec 来显式标明。
例如，反转列表的一种方式涉及一个递归辅助函数，如下面这个定义所示：
def reverse (xs : List α) : List α :=
let rec helper : List α → List α → List α
| [], soFar => soFar
| y :: ys, soFar => helper ys (y :: soFar)
helper xs []
该辅助函数沿着输入列表向下遍历，每次将一个条目移至 soFar。
当它到达输入列表的末尾时，soFar 包含该输入的一个反转版本。
1.7.4. 类型推断
在许多情况下，Lean 可以自动确定表达式的类型。
在这些情况下，顶层定义（使用 def）和局部定义（使用 let）中的显式类型都可以省略。
例如，对 unzip 的递归调用不需要标注：
def unzip : List (α × β) → List α × List β
| [] => ([], [])
| (x, y) :: xys =>
let unzipped := unzip xys
(x :: unzipped.fst, y :: unzipped.snd)
作为经验法则，省略字面值（如字符串和数字）的类型通常可行，尽管 Lean 可能会为数字字面值选择一个比预期类型更具体的类型。
Lean 通常能够确定函数应用的类型，因为它已经知道实参类型和返回类型。
省略函数定义的返回类型通常可行，但函数参数通常需要标注。
不是函数的定义，例如示例中的 unzipped，如果其主体不需要类型标注，则它们也不需要类型标注；而此定义的主体是一个函数应用。
在使用显式的 match 表达式时，可以省略 unzip 的返回类型：
def unzip (pairs : List (α × β)) :=
match pairs with
| [] => ([], [])
| (x, y) :: xys =>
let unzipped := unzip xys
(x :: unzipped.fst, y :: unzipped.snd)
一般而言，类型标注宁可过多，也不要过少，这是一个好主意。
首先，显式类型向读者传达关于代码的假设。
即使 Lean 能自行确定类型，不必反复向 Lean 查询类型信息也仍然可以使代码更易读。
其次，显式类型有助于定位错误。
一个程序对其类型说明得越显式，错误消息就可能越有信息量。
这在 Lean 这样具有非常强表达能力的类型系统的语言中尤其重要。
第三，显式类型使一开始编写程序变得更容易。
类型是一种规范，编译器的反馈可以成为编写满足该规范的程序时的有用工具。
最后，Lean 的类型推断是一种尽力而为的系统。
由于 Lean 的类型系统表达能力如此之强，并不存在对所有表达式都要找到的“最佳”或最一般类型。
这意味着，即使你得到了一个类型，也不能保证它就是给定应用所需的正确类型。
例如，14 可以是一个 Nat 或一个 Int：
#check 14#check (14 : Int)
缺少类型标注可能会产生令人困惑的错误消息。
从 unzip 的定义中省略所有类型：
def unzip pairs :=
match pairs with
| [] => ([], [])
| (x, y) :: xys =>
let unzipped := unzip xys
(x :: unzipped.fst, y :: unzipped.snd)
会产生一条关于 match 表达式的消息：
这是因为 match 需要知道被检查的值的类型，但该类型不可获得。
“元变量”是程序中的未知部分，在错误消息中写作 ?m.XYZ——它们在关于多态的章节中说明。
在此程序中，参数上的类型标注是必需的。
即使某些非常简单的程序也需要类型标注。 例如，恒等函数只是返回传给它的任意实参。 带有参数和类型标注时，它如下所示：
def id (x : α) : α := xLean 能够自行确定返回类型：
def id (x : α) := x然而，省略参数类型会导致错误：
def id x := x一般而言，类似于“failed to infer”的消息，或提到元变量的消息，通常表明需要更多类型标注。 特别是在仍在学习 Lean 时，显式给出大多数类型是有益的。
1.7.5. 同时匹配
模式匹配表达式与模式匹配定义一样，可以一次匹配多个值。
待检查的表达式以及与之匹配的模式都用逗号分隔书写，类似于定义所用的语法。
下面是使用同时匹配的 drop 版本：
def drop (n : Nat) (xs : List α) : List α :=
match n, xs with
| Nat.zero, ys => ys
| _, [] => []
| Nat.succ n , y :: ys => drop n ys
同时匹配类似于对二元组进行匹配，但二者有一个重要区别。
Lean 会跟踪被匹配表达式与模式之间的联系，并且这些信息会用于多种目的，包括检查终止性和传播静态类型信息。
因此，对二元组进行匹配的 sameLength 版本会被终止性检查器拒绝，因为 xs 与 x :: xs' 之间的联系被中间的二元组遮蔽了：
def sameLength (xs : List α) (ys : List β) : Bool :=
match (xs, ys) with
| ([], []) => true
| (x :: xs', y :: ys') => sameLength xs' ys'
| _ => false同时匹配两个列表是被接受的：
def sameLength (xs : List α) (ys : List β) : Bool :=
match xs, ys with
| [], [] => true
| x :: xs', y :: ys' => sameLength xs' ys'
| _, _ => false1.7.6. 自然数模式
在关于 数据类型与模式 的一节中，even 是这样定义的：
def even (n : Nat) : Bool :=
match n with
| Nat.zero => true
| Nat.succ k => not (even k)
正如有特殊语法使列表模式比直接使用 List.cons 和 List.nil 更可读一样，自然数也可以使用数字字面量和 + 来匹配。
例如，even 也可以这样定义：
def even : Nat → Bool
| 0 => true
| n + 1 => not (even n)
在此记法中，+ 模式的各个参数承担不同的角色。
在幕后，左参数（上面的 n）会成为若干个 Nat.succ 模式的参数，而右参数（上面的 1）决定要在该模式外包裹多少个 Nat.succ。
halve 中的显式模式，它将一个 Nat 除以二并舍去余数：
def halve : Nat → Nat
| Nat.zero => 0
| Nat.succ Nat.zero => 0
| Nat.succ (Nat.succ n) => halve n + 1
可以替换为数字字面值和 +：
def halve : Nat → Nat
| 0 => 0
| 1 => 0
| n + 2 => halve n + 1
在幕后，这两个定义完全等价。
请记住：halve n + 1 等价于 (halve n) + 1，而不是 halve (n + 1)。
1.7.7. 匿名函数
Lean 中的函数不必在顶层定义。
作为表达式，函数由 fun 语法产生。
函数表达式以关键字 fun 开始，后跟一个或多个参数，并使用 => 将这些参数与返回表达式分隔开。
例如，将一个数加一的函数可以写作：
#check fun x => x + 1
类型标注的写法与在 def 上相同，使用圆括号和冒号：
#check fun (x : Int) => x + 1类似地，隐式参数可以用花括号书写：
#check fun {α : Type} (x : α) => x
这种匿名函数表达式的风格通常称为 lambda 表达式，因为在编程语言的数学描述中使用的典型记号，会在 Lean 使用关键字 fun 的位置使用希腊字母 λ（lambda）。
尽管 Lean 的确允许使用 λ 来代替 fun，但最常见的写法是 fun。
匿名函数也支持 def 中使用的多模式风格。
例如，一个在自然数的前驱存在时返回其前驱的函数可以写作：
#check fun
| 0 => none
| n + 1 => some n
注意，Lean 自己对该函数的描述包含一个命名参数和一个 match 表达式。
Lean 的许多便利语法缩写都会在幕后展开为更简单的语法，而这种抽象有时会泄漏。
1.7.8. 命名空间
Lean 中的每个名称都位于一个命名空间中，命名空间是一组名称的集合。
名称使用 . 放置在命名空间中，因此 List.map 是 List 命名空间中的名称 map。
不同命名空间中的名称彼此不冲突，即使它们在其他方面完全相同。
这意味着 List.map 和 Array.map 是不同的名称。
命名空间可以嵌套，因此 Project.Frontend.User.loginTime 是嵌套命名空间 Project.Frontend.User 中的名称 loginTime。
名称可以直接在命名空间内定义。
例如，名称 double 可以在 Nat 命名空间中定义：
def Nat.double (x : Nat) : Nat := x + x
由于 Nat 也是一个类型的名称，因此可以使用点记法，在类型为 Nat 的表达式上调用 Nat.double：
#eval (4 : Nat).double
除了直接在命名空间中定义名称之外，还可以使用 namespace 和 end 命令将一系列声明放入一个命名空间中。
例如，下面在命名空间 NewNamespace 中定义了 triple 和 quadruple：
namespace NewNamespace
def triple (x : Nat) : Nat := 3 * x
def quadruple (x : Nat) : Nat := 2 * x + 2 * x
end NewNamespace
要引用它们，请在其名称前加上 NewNamespace.：
#check NewNamespace.triple#check NewNamespace.quadruple
命名空间可以被打开，这使得其中的名称无需显式限定即可使用。
在表达式之前写 open MyNamespace in 会使 MyNamespace 的内容在该表达式中可用。
例如，timesTwelve 在打开 NewNamespace 后同时使用了 quadruple 和 triple：
def timesTwelve (x : Nat) :=
open NewNamespace in
quadruple (triple x)
1.7.9. if let
在消费具有和类型的值时，常常只有一个构造子是关心的对象。 例如，给定如下类型，它表示 Markdown 行内元素的一个子集：
inductive Inline : Type where
| lineBreak
| string : String → Inline
| emph : Inline → Inline
| strong : Inline → Inline一个识别字符串元素并提取其内容的函数可以写作：
def Inline.string? (inline : Inline) : Option String :=
match inline with
| Inline.string s => some s
| _ => none1.7.10. 按位置给出的结构参数
关于结构的一节给出了构造结构的两种方式：
-
可以直接调用该构造子，如
Point.mk 1 2。 -
可以使用花括号记法，如
{ x := 1, y := 2 }中所示。
在某些语境中，按位置而非按名称传递参数会很方便，但又不必直接写出构造子的名称。
例如，定义多种相似的结构类型有助于将领域概念彼此分离，但阅读代码时的自然方式可能会把它们中的每一个实质上都视为一个元组。
在这些语境中，参数可以括在尖括号 ⟨ 和 ⟩ 中。
一个 Point 可以写作 ⟨1, 2⟩。
请注意！
尽管它们看起来像小于号 < 和大于号 >，但这些括号是不同的。
它们可以分别用 \< 和 \> 输入。
1.7.11. 字符串插值
在 Lean 中，在字符串前加上 s! 会触发插值，其中字符串内部花括号中的表达式会被替换为它们的值。
这类似于 Python 中的 f-字符串以及 C# 中带 $ 前缀的字符串。
例如，
#eval s!"three fives is {NewNamespace.triple 5}"产生输出