跳到主要内容

Lean 高阶函数

高阶函数是函数式编程中的一个核心概念。它指的是可以接受函数作为参数，或者返回一个函数作为结果的函数。在 Lean 中，高阶函数的使用非常普遍，它们使得代码更加简洁、灵活和可重用。

什么是高阶函数？​

在 Lean 中，函数是一等公民，这意味着函数可以像其他值一样被传递和操作。高阶函数就是利用这一特性，将函数作为参数或返回值来使用。通过高阶函数，我们可以编写更加通用的代码，减少重复逻辑。

高阶函数的定义​

高阶函数可以分为两类：

  1. 接受函数作为参数的函数：这类函数可以接受一个或多个函数作为输入，并在其内部调用这些函数。
  2. 返回函数作为结果的函数：这类函数会生成并返回一个新的函数。

让我们通过一些简单的例子来理解这两种情况。

接受函数作为参数的函数​

假设我们有一个函数 applyTwice，它接受一个函数 f 和一个值 x，并将 f 应用两次到 x 上。

lean
def applyTwice (f : Nat → Nat) (x : Nat) : Nat :=
  f (f x)

在这个例子中，applyTwice 是一个高阶函数，因为它接受一个函数 f 作为参数。我们可以这样使用它：

lean
def double (x : Nat) : Nat :=
  x * 2

#eval applyTwice double 3  -- 输出: 12

这里，applyTwice 将 double 函数应用了两次，最终结果是 12。

返回函数作为结果的函数​

接下来，我们来看一个返回函数的例子。假设我们有一个函数 createMultiplier，它接受一个整数 n，并返回一个将输入值乘以 n 的函数。

lean
def createMultiplier (n : Nat) : Nat → Nat :=
  fun x => x * n

我们可以这样使用它：

lean
def triple := createMultiplier 3

#eval triple 5  -- 输出: 15

这里，createMultiplier 返回了一个新的函数 triple，它将输入值乘以 3。

高阶函数的实际应用​

高阶函数在实际编程中有很多应用场景。以下是一些常见的例子：

1. 列表操作​

在 Lean 中，列表操作经常使用高阶函数。例如，List.map 函数接受一个函数和一个列表，并将该函数应用到列表的每个元素上。

lean
def numbers := [1, 2, 3, 4, 5]

def doubledNumbers := List.map double numbers

#eval doubledNumbers  -- 输出: [2, 4, 6, 8, 10]

2. 函数组合​

高阶函数还可以用于函数组合。例如，我们可以定义一个函数 compose，它接受两个函数 f 和 g，并返回一个新的函数，该函数先应用 g，再应用 f。

lean
def compose (f : Nat → Nat) (g : Nat → Nat) : Nat → Nat :=
  fun x => f (g x)

def addOne (x : Nat) : Nat :=
  x + 1

def square (x : Nat) : Nat :=
  x * x

def addOneThenSquare := compose square addOne

#eval addOneThenSquare 3  -- 输出: 16

在这个例子中，addOneThenSquare 函数先将输入值加 1，然后再平方。

总结​

高阶函数是 Lean 中非常强大的工具，它们使得代码更加模块化和可重用。通过将函数作为参数传递或返回，我们可以编写更加通用和灵活的代码。

提示

提示：尝试自己编写一些高阶函数，例如 filter 或 reduce，来进一步理解它们的用法。

附加资源​

练习​

  1. 编写一个高阶函数 applyNTimes，它接受一个函数 f、一个整数 n 和一个值 x，并将 f 应用 n 次到 x 上。
  2. 使用 List.map 和 List.filter 高阶函数，对一个整数列表进行平方并过滤出偶数。

通过完成这些练习，你将更好地掌握高阶函数的概念和应用。