编辑“︁Lean函数类型”︁

{{DISPLAYTITLE:Lean函数类型}}  
'''Lean函数类型'''是[[Lean定理证明器]]类型系统的核心组成部分，它表示输入类型到输出类型的映射关系。函数类型在Lean中不仅是编程的基础构造，也是数学命题和证明的载体。本文将详细解释其语法、行为及实际应用。

== 基本概念 ==  
在Lean中，函数类型写作 <code>α → β</code>（或 <code>∀ (x : α), β</code>），表示从类型 <code>α</code> 到类型 <code>β</code> 的映射。若 <code>β</code> 依赖输入值 <code>x : α</code>，则使用Π类型（<code>Π (x : α), β x</code>），但在非依赖情况下与箭头类型等价。

=== 语法示例 ===  
<syntaxhighlight lang="lean">  
-- 非依赖函数类型  
def double : Nat → Nat := fun x => x * 2  

-- 依赖函数类型（Π类型）  
def repeat : Π (n : Nat) (s : String), String :=  
  fun n s => String.append s (String.replicate (n - 1) s)  
</syntaxhighlight>  

=== 求值行为 ===  
函数调用通过传递参数实现：  
<syntaxhighlight lang="lean">  
#eval double 3  -- 输出: 6  
#eval repeat 2 "hi"  -- 输出: "hihi"  
</syntaxhighlight>  

== 高阶函数 ==  
Lean支持将函数作为参数或返回值。例如：  
<syntaxhighlight lang="lean">  
def applyTwice : (Nat → Nat) → Nat → Nat :=  
  fun f x => f (f x)  

#eval applyTwice double 2  -- 输出: 8（2 → 4 → 8）  
</syntaxhighlight>  

== 柯里化与部分应用 ==  
Lean函数默认柯里化，可部分应用：  
<syntaxhighlight lang="lean">  
def add : Nat → Nat → Nat := fun x y => x + y  
def addFive := add 5  -- 类型: Nat → Nat  

#eval addFive 3  -- 输出: 8  
</syntaxhighlight>  

== 函数与命题 ==  
在命题即类型（Curry-Howard对应）下，函数类型对应逻辑蕴含：  
* <code>α → β</code> 表示“若α成立，则β成立”。  
* 函数实现即为蕴含的证明。  

=== 示例证明 ===  
<syntaxhighlight lang="lean">  
example : ∀ (P Q : Prop), P → (Q → P) :=  
  fun P Q p q => p  -- 构造一个忽略Q的常量函数  
</syntaxhighlight>  

== 实际应用案例 ==  
=== 列表映射 ===  
使用函数类型处理列表：  
<syntaxhighlight lang="lean">  
def mapList : (α → β) → List α → List β  
  | _, [] => []  
  | f, h :: t => f h :: mapList f t  

#eval mapList double [1, 2, 3]  -- 输出: [2, 4, 6]  
</syntaxhighlight>  

=== 依赖函数与定理 ===  
依赖类型允许精确约束：  
<syntaxhighlight lang="lean">  
-- 定义长度索引向量  
inductive Vec (α : Type) : Nat → Type  
  | nil : Vec α 0  
  | cons : α → Vec α n → Vec α (n + 1)  

-- 确保返回向量长度与输入相同  
def mapVec : (α → β) → Vec α n → Vec β n  
  | _, Vec.nil => Vec.nil  
  | f, Vec.cons x xs => Vec.cons (f x) (mapVec f xs)  
</syntaxhighlight>  

== 可视化：函数类型关系 ==  
<mermaid>  
graph LR  
    A[α] -->|输入| B[函数 f : α → β]  
    B -->|输出| C[β]  
</mermaid>  

== 数学表示 ==  
函数类型可形式化为：  
<math>  
f \colon \alpha \to \beta \quad \text{或} \quad \prod_{x : \alpha} \beta(x)  
</math>  

== 总结 ==  
* Lean函数类型是**一等公民**，支持高阶操作。  
* 箭头类型与Π类型统一处理非依赖/依赖场景。  
* 柯里化简化部分应用，便于组合。  
* 在命题证明中，函数对应逻辑蕴含的构造过程。  

通过本文的代码示例和理论解释，读者应能掌握Lean函数类型的核心机制及其在编程与证明中的双重作用。

[[Category:计算机科学]]
[[Category:Lean]]
[[Category:Lean类型系统]]