λ演算中的有类型系统的参数多态性

参数多态性（parametric polymorphism）是类型系统中允许函数或数据类型以统一方式处理多种类型的能力。下面我将循序渐进地解释这个概念。

1. 类型系统的基础
   在简单类型λ演算中，每个项都有固定的单一类型（如自然数类型 Nat）。例如，恒等函数 λx:Nat.x 仅适用于 Nat 类型。若需处理其他类型（如布尔值 Bool），必须为每个类型重新定义恒等函数，导致代码冗余。

2. 参数多态性的引入
   参数多态性通过类型变量扩展简单类型系统，允许函数抽象化具体类型。例如，多态恒等函数写作：

   id = ΛA. λx:A. x
   

   这里 ΛA 表示对类型 A 的抽象。应用时需显式指定类型参数：

   id[Nat] 42  →  42
   id[Bool] true  →  true
   

3. 系统F：形式化基础
   参数多态性的经典形式化是系统F（由Girard和Reynolds分别提出）。其核心规则包括：

   • 类型抽象：若项 M 在类型变量 A 的假设下具有类型 τ，则 ΛA.M 具有类型 ∀A.τ。
   • 类型应用：若项 M 具有类型 ∀A.τ，则对具体类型 σ 应用 M[σ] 得到类型 τ[σ/A]（替换 A 为 σ）。

4. 多态性与代码复用
   参数多态性支持通用数据结构的定义。例如，多态列表类型：

   List = ∀A. (Nil: List A, Cons: A → List A → List A)
   

   可统一实现映射函数 map : ∀A.∀B. (A → B) → List A → List B，无需为每种类型重写。

5. 参数性与自由定理
   Reynolds的参数性定理指出，多态函数的行为必须统一适用于所有类型。例如，类型 ∀A. A → A 的唯一可能实现是恒等函数，这一性质可通过数学证明推导，无需测试具体类型。

6. 类型推断的挑战
   系统F的类型推断是不可判定的（与简单类型λ演算相反）。实际语言（如Haskell）采用受限形式（如Hindley-Milner类型系统），通过let多态在可推断性与表达能力间取得平衡。