1.3. 函数与定义🔗

在 Lean 中，定义使用 def 关键字引入。例如，若要定义名称 hello 以指代字符串 "Hello"，可写作：

def hello := "Hello"

在 Lean 中，新名称使用冒号等号运算符 := 来定义，而不是使用 =。这是因为 = 用于描述已有表达式之间的等式，而使用两个不同的运算符有助于避免混淆。

在 hello 的定义中，表达式 "Hello" 足够简单，因此 Lean 能够自动确定该定义的类型。然而，大多数定义并不如此简单，所以通常需要添加类型。这是通过在被定义的名称后使用冒号来完成的：

def lean : String := "Lean"

既然这些名称已经定义，就可以使用它们，因此

"Hello Lean"#eval String.append hello (String.append " " lean)

输出

"Hello Lean"

在 Lean 中，已定义的名称只能在其定义之后使用。

在许多语言中，函数的定义与其他值的定义使用不同的语法。例如，Python 的函数定义以 def 关键字开头，而其他定义则用等号来定义。在 Lean 中，函数与其他值一样，使用相同的 def 关键字来定义。不过，诸如 hello 这样的定义所引入的名称是直接指向其值，而不是指向每次被调用时都返回等价结果的零参数函数。

1.3.1. 定义函数🔗

在 Lean 中定义函数有多种方式。最简单的方式是将函数的参数放在定义的类型之前，并用空格分隔。例如，一个给其参数加一的函数可以写作：

def add1 (n : Nat) : Nat := n + 1

用 #eval 测试此函数会得到预期的 8：

8#eval add1 7

正如通过在各个实参之间写空格来将函数应用于多个实参一样，接受多个实参的函数也是通过在各参数的名称与类型之间写空格来定义的。函数 maximum 的结果等于其两个实参中的较大者；它接受两个 Nat 实参 n 和 k，并返回一个 Nat。

def maximum (n : Nat) (k : Nat) : Nat :=
  if n < k then
    k
  else n

类似地，函数 spaceBetween 将两个字符串用一个空格连接起来。

def spaceBetween (before : String) (after : String) : String :=
  String.append before (String.append " " after)

当像 maximum 这样已定义的函数获得其参数后，其结果通过如下方式确定：首先在函数体中用所提供的值替换参数名，然后对所得函数体求值。例如：

                  maximum (5 + 8) (2 * 7)maximum 13 14if 13 < 14 then 14 else 1314

求值结果为自然数、整数和字符串的表达式具有说明这一点的类型（分别为 Nat、Int 和 String）。函数也是如此。一个接受 Nat 并返回 Bool 的函数具有类型 Nat → Bool，而一个接受两个 Nat 并返回 Nat 的函数具有类型 Nat → Nat → Nat。

作为一种特殊情形，当函数名直接与 #check 一起使用时，Lean 会返回该函数的签名。输入 #check add1 会得到 add1 (n : Nat) : Nat。然而，可以通过将函数名写在括号中来“诱使” Lean 显示该函数的类型；这会使该函数被当作普通表达式处理，因此 #check (add1) 会得到 add1 : Nat → Nat，而 #check (maximum) 会得到 maximum : Nat → Nat → Nat。这个箭头也可以用 ASCII 替代箭头 -> 来书写，因此前述函数类型可分别写作 example : Nat -> Nat := add1 和 example : Nat -> Nat -> Nat := maximum。

在幕后，所有函数实际上都精确地期望一个参数。像 maximum 这样看起来接受多个参数的函数，事实上是接受一个参数然后返回一个新函数的函数。这个新函数接受下一个参数，如此过程持续下去，直到不再期望更多参数。向一个多参数函数提供一个参数即可看出这一点：#check maximum 3 得到 maximum 3 : Nat → Nat，而 #check spaceBetween "Hello " 得到 spaceBetween "Hello " : String → String。用返回函数的函数来实现多参数函数，称为柯里化，这一名称来自数学家 Haskell Curry。函数箭头向右结合，这意味着 Nat → Nat → Nat 应当加括号为 Nat → (Nat → Nat)。

1.3.1.1. 练习🔗

定义类型为 String → String → String → String 的函数 joinStringsWith，它通过把第一个参数放在第二个参数和第三个参数之间来创建一个新字符串。joinStringsWith ", " "one" "and another" 应求值为 "one, and another"。
joinStringsWith ": " 的类型是什么？请用 Lean 检查你的答案。
定义一个类型为 Nat → Nat → Nat → Nat 的函数 volume，用于计算具有给定高度、宽度和深度的长方体的体积。

1.3.2. 定义类型🔗

大多数带类型的编程语言都有某种为类型定义别名的手段，例如 C 的 typedef。然而，在 Lean 中，类型是语言的一等组成部分——它们像其他任何事物一样是表达式。这意味着定义既可以引用类型，也可以引用其他值。

例如，如果 String 输入起来过于繁琐，可以定义一个较短的缩写 Str：

def Str : Type := String

于是可以使用 Str 作为定义的类型，而不是使用 String：

def aStr : Str := "This is a string."

这一点之所以成立，是因为类型遵循与 Lean 其余部分相同的规则。类型是表达式，而在表达式中，已定义的名称可以用其定义替换。由于 Str 已被定义为表示 String，因此 aStr 的定义是有意义的。

1.3.2.1. 你可能遇到的消息🔗

由于 Lean 支持重载的整数字面量，用定义来表示类型的实验会因此变得更复杂。如果 Nat 太短，可以定义一个更长的名称 NaturalNumber：

def NaturalNumber : Type := Nat

然而，使用 NaturalNumber 作为定义的类型而不是 Nat，并不会产生预期的效果。特别地，以下定义：

def thirtyEight : NaturalNumber := failed to synthesize
  OfNat NaturalNumber 38
numerals are polymorphic in Lean, but the numeral `38` cannot be used in a context where the expected type is
  NaturalNumber
due to the absence of the instance above

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.38

导致以下错误：

failed to synthesize
  OfNat NaturalNumber 38
numerals are polymorphic in Lean, but the numeral `38` cannot be used in a context where the expected type is
  NaturalNumber
due to the absence of the instance above

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.

这个错误发生是因为 Lean 允许数值字面量被重载。在有意义时，自然数字面量可以用于新类型，就好像这些类型是系统内建的一样。这是 Lean 使命的一部分，即让表示数学变得方便；而数学的不同分支会出于非常不同的目的使用数字记号。允许这种重载的具体功能在查找重载之前，并不会把所有已定义名称替换为它们的定义，这正是导致上述错误消息的原因。

绕过这一限制的一种方法是在定义右侧给出类型 Nat，从而使 Nat 的重载规则被用于 38：

def thirtyEight : NaturalNumber := (38 : Nat)

该定义仍然是类型正确的，因为 NaturalNumber 与 Nat 是同一个类型——根据定义即如此！

另一种解决方案是为 NaturalNumber 定义一个重载，使其工作方式等同于 Nat 的重载。不过，这需要 Lean 的更高级特性。

最后，使用 abbrev 而不是 def 为 Nat 定义新名称，使得重载解析能够用该名称的定义替换被定义的名称。使用 abbrev 写出的定义总是会被展开。例如，

abbrev N : Type := Nat

以及

def thirtyNine : N := 39

会被顺利接受。

在幕后，有些定义在内部被标记为可在重载解析期间展开，而另一些则不是。将要被展开的定义称为可约的。对可约性的控制对于使 Lean 能够扩展至关重要：完全展开所有定义可能产生非常大的类型，机器处理起来很慢，用户也难以理解。用 abbrev 产生的定义会被标记为可约。