λ演算中的有类型系统的子类型算法

1. 子类型的基本概念
   子类型（subtyping）是类型系统中一种关系，记为 \(S <: T\)，表示类型 \(S\) 是类型 \(T\) 的子类型。其核心含义是：任何属于类型 \(S\) 的值都可以安全地用在需要类型 \(T\) 的上下文中（称为子类型多态）。例如，若“狗”是“动物”的子类型，则所有狗都可以被当作动物处理。

2. 子类型关系的规则
   子类型关系通常通过一组推理规则定义：

   • 自反性：对任意类型 \(T\)，有 \(T <: T\)。
   • 传递性：若 \(S <: U\) 且 \(U <: T\)，则 \(S <: T\)。
   • 函数类型的子类型规则（协变与逆变）：
     若 \(S_1 <: T_1\) 且 \(T_2 <: S_2\)，则 \((T_1 → T_2) <: (S_1 → S_2)\)。
     这里参数类型是逆变的（方向相反），返回类型是协变的（方向相同）。

3. 记录类型的子类型规则
   对于记录类型（如结构体），子类型通过字段扩展或细化定义：

   • 若记录 \(R_1\) 包含 \(R_2\) 的所有字段（且对应字段类型满足子类型关系），则 \(R_1 <: R_2\)。
   • 字段类型的子类型需满足：若 \(S_i <: T_i\)，则 \(\{ l_1: S_1, ..., l_n: S_n \} <: \{ l_1: T_1, ..., l_n: T_n \}\)。

4. 子类型判定的算法化
   子类型算法需递归地比较类型结构：

   • 基础类型：直接比较（如 Int <: Int）。
   • 复合类型（如函数、记录）：递归检查组件类型，并应用协变/逆变规则。
   • 算法需处理递归类型：通过维护“已比较类型对”的集合避免无限递归。

5. 子类型与类型检查的集成
   在类型检查中，子类型通过子sumption规则引入：

\[ \frac{\Gamma \vdash t : S \quad S <: T}{\Gamma \vdash t : T} \]

该规则允许子类型的值自动提升为超类型。算法需在类型推导中动态调用子类型判定。

6. 典型子类型算法示例
   以函数和记录类型为例，算法的伪代码如下：

   Subtype(S, T):
     if S = T: return True
     if S = S1 → S2 and T = T1 → T2:
       return Subtype(T1, S1) and Subtype(S2, T2)  // 注意参数逆变
     if S = { l_i: S_i } and T = { l_j: T_j }:
       检查 T 的每个字段 l_j 在 S 中存在，且 Subtype(S_j, T_j)
     // 处理其他类型（如顶类型 Top、并类型等）
   

7. 挑战与扩展

   • 递归类型需通过记忆化避免循环。
   • 联合类型（union）和交集类型（intersection）需扩展规则。
   • 算法需保证终止性、完备性与一致性。