编辑“︁Lean类型推断”︁

= Lean类型推断 =

'''Lean类型推断'''是Lean定理证明器/编程语言中自动推导表达式类型的过程，它允许开发者省略显式类型标注，使代码更简洁而不失严谨性。本章将系统介绍其工作原理、应用场景及与显式标注的对比。

== 核心概念 ==

类型推断指编译器/解释器通过分析代码结构、变量使用上下文等，自动确定未标注表达式的类型。在Lean中，这一过程基于：

* '''局部上下文分析'''：根据变量定义位置附近的类型信息推导
* '''全局约束求解'''：通过统一类型约束方程组求解最终类型
* '''双向类型检查'''：结合"自上而下"（预期类型）和"自下而上"（表达式结构）的推理

=== 基础示例 ===
<syntaxhighlight lang="lean">
-- 显式标注
def square (x : Nat) : Nat := x * x

-- 类型推断版本
def square_inferred x := x * x  -- Lean自动推断x和返回值为Nat
</syntaxhighlight>

== 工作原理 ==

=== 约束生成与求解 ===
类型推断分为三个阶段：
1. 为每个子表达式生成类型变量（如<math>\alpha_1, \alpha_2</math>）
2. 根据语言规则生成约束（如<math>\alpha_1 \times \alpha_1 \rightarrow \alpha_2</math>）
3. 通过'''合一算法'''求解约束系统

<mermaid>
graph TD
    A[表达式解析] --> B[生成类型变量]
    B --> C[收集约束条件]
    C --> D[约束求解]
    D --> E[具体类型赋值]
</mermaid>

=== 多态性处理 ===
Lean支持参数多态，类型推断会生成最通用的类型：
<syntaxhighlight lang="lean">
def identity x := x  -- 推断为∀ (α : Type), α → α
#check identity      -- 输出：identity : ∀ {α : Type u_1}, α → α
</syntaxhighlight>

== 实际应用 ==

=== 案例1：数学证明简化 ===
在证明中自动推断命题类型：
<syntaxhighlight lang="lean">
example (n : Nat) : n + 0 = n := by
  induction n with
  | zero => simp          -- 自动推断目标类型为0 + 0 = 0
  | succ n ih => simp [ih] -- 推断ih : n + 0 = n
</syntaxhighlight>

=== 案例2：依赖类型编程 ===
处理依赖类型时的推断能力：
<syntaxhighlight lang="lean">
def Vector (α : Type) : Nat → Type
  | 0 => Unit
  | n+1 => α × Vector α n

def head (v : Vector α (n+1)) := v.1  -- 自动推断n必须为Nat
</syntaxhighlight>

== 高级主题 ==

=== 类型注解与推断的交互 ===
部分显式标注可指导推断过程：
<syntaxhighlight lang="lean">
def add {α} [Add α] (x y : α) := x + y  -- 需要类型类约束
#check add (1 : Int) 2  -- 推断第二个参数为Int
</syntaxhighlight>

=== 推断局限性 ===
当出现以下情况时需要显式标注：
1. 重载解析歧义
2. 存在多个可能类型实例时
3. 递归定义中的初始类型提示

== 最佳实践 ==
* 在公开API中推荐混合使用显式类型与推断
* 复杂递归函数建议提供返回类型标注
* 使用<code>#check</code>命令验证推断结果

== 参见 ==
* [[类型系统]]（基础理论）
* [[统一算法]]（实现细节）
* [[依赖类型]]（高级应用）

[[Category:Lean类型系统]]
[[Category:编程语言特性]]

[[Category:计算机科学]]
[[Category:Lean]]