类型

类型根据程序可以计算的值对程序进行分类。类型在程序中扮演着多种角色：

让编译器对值在内存中的表示做出决策。
帮助程序员向他人传达他们的意图，作为函数输入和输出的轻量级规范，编译器可以确保程序遵守该规范。
防止各种潜在错误，例如将数字加到字符串上，从而减少程序所需的测试数量。
帮助 Lean 编译器自动生成辅助代码，可以节省样板代码。

Lean 的类型系统具有非同寻常的表现力。类型可以编码强规范，如「此排序函数返回其输入的顺序排列」，以及灵活的规范，如「此函数具有不同的返回类型，具体取决于其参数的值」。类型系统甚至可以用作证明数学定理的完整逻辑系统。然而，这种顶尖的表现力并不能消除对更简单类型的需求，理解这些更简单的类型是使用更高级的功能的先决条件。

Lean 中的每个程序都必须有一个类型。特别是，每个表达式在求值之前都必须具有类型。在迄今为止的示例中，Lean 已经能够自行推导出类型，但有时也需要提供一个类型。这是使用冒号运算符完成的：

#eval (1 + 2 : Nat)

在这里，Nat 是 自然数 的类型，它们是任意精度的无符号整数。在 Lean 中，Nat 是非负整数字面量的默认类型。此默认类型并不总是最佳选择。在 C 中，当减法运算结果小于零时，无符号整数会下溢到最大的可表示数字。然而，Nat 可以表示任意大的无符号数字，因此没有最大的数字可以下溢。因此，当答案原本为负数时，Nat 上的减法运算会返回 0。例如，

#eval 1 - 2

会求值为 0 而非 -1。若要使用可以表示负整数的类型，请直接提供它：

#eval (1 - 2 : Int)

使用此类型后，结果为 -1，符合预期。

若要检查表达式的类型而不求值，请使用 #check 而非 #eval。例如：

#check (1 - 2 : Int)

会报告 1 - 2 : Int 而不会实际执行减法运算。

当无法为程序指定类型时，#check 和 #eval 都会返回错误。例如：

#check String.append "hello" [" ", "world"]

会输出

application type mismatch
  String.append "hello" [" ", "world"]
argument
  [" ", "world"]
has type
  List String : Type
but is expected to have type
  String : Type

应用程序类型不匹配"
  String.append "hello" [" ", "world"]
参数
  [" ", "world"]
类型为
  List String : Type
但预期类型为
  String : Type

因为 String.append 的第二个参数需要是字符串，但提供的是字符串列表。

Lean 函数式编程

类型