编辑“︁Lean匿名函数”︁

{{DISPLAYTITLE:Lean匿名函数}}

'''Lean匿名函数'''是[[Lean定理证明器|Lean]]函数式编程中的核心概念之一，允许开发者在不显式命名的情况下定义函数。这种特性在函数式编程中极为常见，特别适用于需要临时函数的场景。

== 简介 ==
匿名函数（又称lambda表达式）是没有绑定标识符的函数定义。在Lean中，匿名函数使用<code>fun</code>关键字定义，语法为：
<syntaxhighlight lang="lean">
fun 参数 => 表达式
</syntaxhighlight>

匿名函数的主要用途包括：
* 作为高阶函数的参数（如<code>List.map</code>）
* 简化局部函数定义
* 实现闭包功能

== 基本语法 ==
最简单的匿名函数是一个单参数函数：

<syntaxhighlight lang="lean">
-- 定义并立即调用一个匿名函数
(fun x => x + 1) 5  -- 结果为6
</syntaxhighlight>

多参数匿名函数可以通过嵌套或元组参数实现：

<syntaxhighlight lang="lean">
-- 嵌套方式
(fun x => fun y => x + y) 3 4  -- 结果为7

-- 元组参数方式
(fun (x, y) => x + y) (3, 4)  -- 结果为7
</syntaxhighlight>

== 类型标注 ==
Lean支持为匿名函数参数添加类型标注：

<syntaxhighlight lang="lean">
(fun (x : Nat) => x + 1)  -- Nat → Nat类型的函数
</syntaxhighlight>

== 实际应用示例 ==
=== 列表操作 ===
匿名函数常用于高阶列表操作：

<syntaxhighlight lang="lean">
def numbers := [1, 2, 3, 4]

-- 使用匿名函数映射列表
#eval List.map (fun x => x * 2) numbers  -- 输出[2, 4, 6, 8]

-- 使用匿名函数过滤列表
#eval List.filter (fun x => x % 2 == 0) numbers  -- 输出[2, 4]
</syntaxhighlight>

=== 函数组合 ===
匿名函数可以与其他函数组合使用：

<syntaxhighlight lang="lean">
def double := fun x => x * 2
def square := fun x => x * x

-- 组合函数
#eval (fun x => square (double x)) 3  -- (3*2)^2 = 36
</syntaxhighlight>

== 闭包特性 ==
匿名函数可以捕获外部作用域的变量，形成闭包：

<syntaxhighlight lang="lean">
def makeAdder (n : Nat) : Nat → Nat :=
  fun x => x + n

def add5 := makeAdder 5
#eval add5 3  -- 输出8
</syntaxhighlight>

== 与命名函数的比较 ==
下表对比了匿名函数与命名函数的区别：

<mermaid>
erDiagram
    FUNCTIONS {
        string 类型
        string 定义方式
        string 作用域
        string 典型用途
    }
    FUNCTIONS ||--|{ NAMED_FUNCTIONS : "命名函数"
    FUNCTIONS ||--|{ ANONYMOUS_FUNCTIONS : "匿名函数"
    NAMED_FUNCTIONS {
        string 类型 = "有名称"
        string 定义方式 = "def关键字"
        string 作用域 = "全局/局部"
        string 典型用途 = "复用逻辑"
    }
    ANONYMOUS_FUNCTIONS {
        string 类型 = "无名称"
        string 定义方式 = "fun关键字"
        string 作用域 = "定义处"
        string 典型用途 = "临时/高阶函数参数"
    }
</mermaid>

== 数学表示 ==
在数学上，匿名函数对应λ演算中的lambda抽象：

<math>
\lambda x. E
</math>

其中<math>x</math>是参数，<math>E</math>是表达式。

== 性能考虑 ==
Lean编译器会对匿名函数进行优化：
* 简单匿名函数通常会被内联
* 复杂匿名函数可能生成闭包对象
* 在热代码路径中，应考虑匿名函数的使用频率

== 高级用法 ==
=== 依赖类型匿名函数 ===
Lean支持依赖类型的匿名函数：

<syntaxhighlight lang="lean">
(fun (n : Nat) (h : n > 0) => n)  -- 类型为Π (n : Nat), n > 0 → Nat
</syntaxhighlight>

=== 模式匹配匿名函数 ===
匿名函数支持模式匹配：

<syntaxhighlight lang="lean">
fun | 0 => 1 | n+1 => n  -- 匹配0和n+1模式
</syntaxhighlight>

== 常见错误 ==
初学者在使用匿名函数时容易犯以下错误：
1. 忘记必要的括号：
<syntaxhighlight lang="lean">
-- 错误示例
fun x => x + 1 5  -- 解析为fun x => (x + 1 5)

-- 正确写法
(fun x => x + 1) 5
</syntaxhighlight>

2. 类型推断失败时未添加类型标注
3. 在递归场景错误使用匿名函数（匿名函数无法直接递归）

== 最佳实践 ==
1. 保持匿名函数简短（通常不超过3行）
2. 复杂的逻辑应提取为命名函数
3. 当需要多次复用时考虑命名函数
4. 在高阶函数中使用匿名函数提高可读性

== 练习 ==
尝试解决以下问题来巩固理解：
1. 编写一个匿名函数，计算两个数的平方和
2. 使用<code>List.map</code>和匿名函数将字符串列表转换为长度列表
3. 创建一个返回匿名函数的高阶函数

== 总结 ==
Lean匿名函数是函数式编程的强大工具，提供了简洁的语法来表达临时函数逻辑。通过合理使用匿名函数，可以使代码更加简洁、表达力更强，特别适合在高阶函数和闭包场景中使用。

[[Category:计算机科学]]
[[Category:Lean]]
[[Category:Lean函数式编程]]