其他便利功能

Lean 包含许多便利功能，能够让程序更加简洁。

自动隐式参数

在 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)

这能极大简化地需要很多隐式参数的高级多态定义。

模式匹配定义

用 def 定义函数时，通常会给参数命名，然后立即用模式匹配使用它。 例如，在 length 中，参数 xs 仅在 match 中使用。在这些情况下，match 表达式的 case 可以直接编写，而无需给参数命名。

第一步是将参数类型移到冒号的右侧，因此返回类型是函数类型。例如，length 的类型是 List α → Nat。然后，用模式匹配的每个 case 替换 :=：

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 xs

已命名的参数和模式也可以在同一定义中使用。例如，一个函数接受一个默认值和一个可选值， 当可选值为 none 时返回默认值，可以写成：

def fromOption (default : α) : Option α → α
  | none => default
  | some x => x

此函数在标准库中称为 Option.getD，可以用点表示法调用：

#eval (some "salmonberry").getD ""

"salmonberry"

#eval none.getD ""

""

局部定义

在计算中对中间步骤命名通常很有用。在许多情况下，中间值本身就代表有用的概念， 明确地命名它们可以使程序更易于阅读。在其他情况下，中间值被使用多次。与大多数其他语言一样， 在 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 关键字的列。 例如，let 可以像这样用于 unzip：

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 包含输入的反转版本。

类型推断

在许多情况下，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

14 : Nat

#check (14 : Int)

14 : Int

缺少类型标注可能会产生令人困惑的错误信息。从 unzip 的定义中省略所有类型：

def unzip pairs :=
  match pairs with
  | [] => ([], [])
  | (x, y) :: xys =>
    let unzipped := unzip xys
    (x :: unzipped.fst, y :: unzipped.snd)

会产生有关 match 表达式的信息：

invalid match-expression, pattern contains metavariables
  []

这是因为 match 需要知道正在检查的值的类型，但该类型不可用。 「元变量」是程序中未知的部分，在错误消息中写为 ?m.XYZ， 它们在多态性一节中进行了描述。 在此程序中，参数上的类型标注是必需的。

即使一些非常简单的程序也需要类型标注。例如，恒等函数只返回传递给它的任何参数。 使用参数和类型标注，它看起来像这样：

def id (x : α) : α := x

Lean 能够自行确定返回类型：

def id (x : α) := x

然而，省略参数类型会导致错误：

def id x := x

failed to infer binder type

一般来说，类似于「无法推断」或提及元变量的消息通常表示需要更多类型标注。 特别是在学习 Lean 时，显式提供大多数类型是很有用的。

同时匹配

模式匹配表达式，和模式匹配定义一样，可以一次匹配多个值。 要检查的表达式和它们匹配的模式都用逗号分隔，类似于用于定义的语法。 以下是使用同时匹配的 drop 版本：

def drop (n : Nat) (xs : List α) : List α :=
  match n, xs with
  | Nat.zero, ys => ys
  | _, [] => []
  | Nat.succ n , y :: ys => drop n ys

自然数模式

在数据类型与模式一节中，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)。

在使用这个语法时，+的第二个参数应始终是一个字面量 Nat。 尽管加法是可交换的，但是在模式中交换参数可能会产生以下错误：

def halve : Nat → Nat
  | 0 => 0
  | 1 => 0
  | 2 + n => halve n + 1

invalid patterns, `n` is an explicit pattern variable, but it only occurs in positions that are inaccessible to pattern matching
  .(Nat.add 2 n)

此限制使 Lean 能够将模式中所有 + 号的用法转换为底层 Nat.succ 的用法， 从而在幕后使语言更简单。

匿名函数

Lean 中的函数不必在顶层定义。作为表达式，函数使用 fun 语法定义。 函数表达式以关键字 fun 开头，后跟一个或多个参数，这些参数使用 => 与返回表达式分隔。 例如，可以编写一个将数字加 1 的函数：

#check fun x => x + 1

fun x => x + 1 : Nat → Nat

类型标注的写法与 def 相同，使用括号和冒号：

#check fun (x : Int) => x + 1

fun x => x + 1 : Int → Int

同样，隐式参数可以用大括号编写：

#check fun {α : Type} (x : α) => x

fun {α} x => x : {α : Type} → α → α

这种匿名函数表达式风格通常称为 λ-表达式（Lambda Expression） ， 因为编程语言在数学描述中使用的典型符号，将 Lean 中使用关键字 fun 的地方换成了希腊字母 λ（Lambda）。即使 Lean 允许使用 λ 代替 fun， 但最常见的仍然是写作 fun。

匿名函数还支持 def 中使用的多模式风格。例如，可以编写一个返回自然数的前驱（如果存在）的函数：

#check fun
  | 0 => none
  | n + 1 => some n

fun x =>
  match x with
  | 0 => none
  | Nat.succ n => some n : Nat → Option Nat

注意，Lean 函数的描述本身有一个命名参数和一个 match 表达式。 Lean 的许多便捷语法缩写都会在幕后扩展为更简单的语法，但有时会泄漏抽象，暴露出具体细节。

使用 def 定义带有参数的函数可以重写为函数表达式。例如，一个将其参数翻倍的函数可以写成以下形式：

def double : Nat → Nat := fun
  | 0 => 0
  | k + 1 => double k + 2

当匿名函数非常简单时，例如 fun x => x + 1， 创建函数的语法会相当冗长。在此例中，有六个非空白字符用于引入函数， 其函数体仅包含三个非空白字符。对于这些简单的情况，Lean 提供了一个简写。 在括号包围的表达式中，间点号 · 可以表示一个参数，括号内的表达式为函数体， 因此该函数也可以写成 (· + 1)。

间点号总是将 最靠近 的一对括号创建为函数。 例如，(· + 5, 3) 是返回一对数字的函数， 而 ((· + 5), 3) 是一个函数和一个数字的偶对。 如果使用多个点，则它们按从左到右的顺序成为参数：

(· , ·) 1 2
===>
(1, ·) 2
===>
(1, 2)

匿名函数的应用方式与 def 或 let 定义的函数完全相同。 命令 #eval (fun x => x + x) 5 的结果是：

10

而 #eval (· * 2) 5 的结果是：

10

命名空间

Lean 中的每个名称都出现在一个 命名空间（Namespace） 中，它是一个名称的集合。 名称使用 . 放在命名空间中，因此 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

8

除了直接在命名空间中定义名称外，还可以使用 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

NewNamespace.triple (x : Nat) : Nat

#check NewNamespace.quadruple

NewNamespace.quadruple (x : Nat) : Nat

命名空间可以 打开 ，这允许在不显式指定的情况下使用其中的名称。 在表达式之前编写 open MyNamespace in 会使 MyNamespace 中的内容在表达式中可用。例如，timesTwelve 在打开 NewNamespace 后同时使用了 quadruple 和 triple：

def timesTwelve (x : Nat) :=
  open NewNamespace in
  quadruple (triple x)

命名空间也可以在命令之前打开。这能让命令中的所有部分引用命名空间的内容， 而不仅仅是一个表达式。为此，请在命令之前写上 open ... in。

open NewNamespace in
#check quadruple

NewNamespace.quadruple (x : Nat) : Nat

函数签名会显示名称的完整命名空间，还可以为文件其余部分的所有后续命令打开命名空间。 为此，只需从 open 的顶级用法中省略 in。

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
  | _ => none

另一种编写此函数体的方法是将 if 与 let 联用：

def Inline.string? (inline : Inline) : Option String :=
  if let Inline.string s := inline then
    some s
  else none

这与模式匹配 let 的语法非常相似，不同之处在于它可以与和类型一起使用， 因为在 else 的情况中提供了备选项。在某些情况下，使用 if let 代替 match 可以让代码更易读。

带位置的结构体参数

结构体一节中介绍了构造结构体的两种方法：

1. 构造子可以直接调用，如 Point.mk 1 2.
2. 可以使用大括号记法，如 { x := 1, y := 2 }.

在某些情况下，按位置传递参数要比按名称传递参数更方便，因为无需直接命名构造子。 例如，定义各种相似的结构体类型有助于保持领域概念的隔离， 但阅读代码的自然方式可能是将它们都视为本质上是一个元组。 在这种情况下，参数可以用尖括号 ⟨ 和 ⟩ 括起来，如 Point 可以写成 ⟨1, 2⟩。 注意！即使它们看起来像小于号 < 和大于号 >，这些括号也不同。 它们可以分别使用 \< 和 \> 来输入。

与命名构造子参数的大括号记法一样，此位置语法只能在 Lean 可以根据类型标注或程序中的其他类型信息，来确定结构体类型的语境中使用。 例如，#eval ⟨1, 2⟩ 会产生以下错误：

invalid constructor ⟨...⟩, expected type must be an inductive type 
  ?m.34991

错误中出现元变量是因为没有可用的类型信息。添加标注，例如 #eval (⟨1, 2⟩ : Point)，可以解决此问题：

{ x := 1.000000, y := 2.000000 }

字符串插值

在 Lean 中，在字符串前加上 s! 会触发 插值（Interpolation） ， 其中字符串中大括号内的表达式会被其值替换。这类似于 Python 中的 f 字符串和 C# 中以 $ 为前缀的字符串。例如，

#eval s!"three fives is {NewNamespace.triple 5}"

会产生输出

"three fives is 15"

并非所有的表达式都可以插值到字符串中。例如，尝试插值一个函数会产生错误。

#check s!"three fives is {NewNamespace.triple}"

会产生输出

failed to synthesize instance
  ToString (Nat → Nat)

这是因为没有将函数转换为字符串的标准方法。Lean 编译器维护了一个表， 描述如何将各种类型的值转换为字符串，而消息 failed to synthesize instance 意味着 Lean 编译器未在此表中找到给定类型的条目。 这使用了与结构体一节中描述的 deriving Repr 语法相同的语言特性。