函数与定义

在 Lean 中，需使用 def 关键字引入定义。例如，若要定义名称 hello 来引用字符串 "Hello"，请编写：

def hello := "Hello"

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

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

def lean : String := "Lean"

定义了名称后，就可以使用它们了，因此

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

会输出

"Hello Lean"

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

在很多语言中，函数定义的语法与其他值的不同。例如，Python 函数定义以 def 关键字开头，而其他定义则以等号定义。在 Lean 中，函数使用与其他值相同的 def 关键字定义。尽管如此，像 hello 这类的定义引入的名字会直接引用其值，而非每次调用一个零参函数返回等价的值。

定义函数

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

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

测试此函数时，#eval 给出了 8，符合预期：

#eval add1 7

就像将函数应用于多个参数会用空格分隔一样，接受多个参数的函数定义也是在参数名与类型之间加上空格。函数 maximum 的结果等于其两个参数中最大的一个，它接受两个 Nat 参数 n 和 k，并返回一个 Nat。

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

当向 maximum 这样的已定义函数提供参数时，其结果会首先用提供的值替换函数体中对应的参数名称，然后对产生的函数体求值。例如：

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

求值结果为自然数、整数和字符串的表达式具有表示它们的类型（分别为 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 的箭头 ->，因此前面的函数类型可以分别写作 Nat -> Nat 和 Nat -> Nat -> Nat。

在幕后，所有函数实际上都刚好接受一个参数。像 maximum 这样的函数看起来需要多个参数，但实际上它们会接受一个参数并返回一个新的函数，新函数接受下一个参数，直到不再需要更多参数为止。可以通过向一个多参数函数提供一个参数来看到这一点： #check maximum 3 会产生 maximum 3 : Nat → Nat，而 #check String.append "Hello " 会产生 String.append "Hello " : String → String。使用返回函数的函数来实现多参数函数被称为" 柯里化（Currying） ，以数学家哈斯克尔·柯里（Haskell Curry）命名。函数箭头是右结合的，这意味着 Nat → Nat → Nat 等价于 Nat → (Nat → Nat)。

练习

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

定义类型

大多数类型化编程语言都有一些方法来定义类型的别名，例如 C 语言的 typedef。然而，在 Lean 中，类型是语言的一等部分——它们与其他表达式一样都是表达式，这意味着定义可以引用类型，就像它们可以引用其他值一样。

例如，如果 String 输入起来太长，可以定义一个简写 Str：

def Str : Type := String

然后就可以使用 Str 而非 String 作为定义的类型：

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

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

你可能会遇到的信息

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

def NaturalNumber : Type := Nat

然而，使用 NaturalNumber 作为定义的类型而非 Nat 并没有达到预期的效果。特别是，定义：

def thirtyEight : NaturalNumber := 38

会导致以下错误：

failed to synthesize instance
  OfNat NaturalNumber 38

产生该错误的原因是 Lean 允许数字字面量被 重载（Overload） 。当有意义时，自然数字面量可用作新类型，就像这些类型内置在系统中一样。这能让 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

都会被接受而不会出现问题。

在幕后，一些定义会在重载解析期间被内部标记为可展开的，而另一些则不会标记。可展开的定义称为 可约的（Reducible） 。控制可约性对 Lean 的灵活性而言至关重要：完全展开所有的定义可能会产生非常大的类型，这对于机器处理和用户理解来说都很困难。使用 abbrev 生成的定义会被标记为可约定义。

Lean 函数式编程

函数与定义

定义函数

练习

定义类型

你可能会遇到的信息