子类型化元理论：算法子类型与算法类型检查

### 子类型化元理论：算法子类型与算法类型检查 #### 1. 问题提出 在带有子类型的简单类型 lambda 演算中，原有的子类型和类型检查规则并不适合直接实现。主要问题在于规则并非语法导向的，尤其是类型关系中的包含规则（T - Sub）和子类型关系中的传递规则（S - Trans）。 - **T - Sub 规则问题**：其结论中的项被指定为一个简单的元变量 t，可应用于任何类型的项，这使得在计算项的类型时，难以确定是应用 T - Sub 规则还是其他匹配项形状的规则。 ```plaintext Γ ⊢ t : S S <: T Γ ⊢ t : T (T - Sub) ``` - **S - Trans 规则问题**： - 其结论与其他规则的结论重叠，在推导子类型陈述时，难以决定是否使用该规则。 ```plaintext S <: U U <: T S <: T (S - Trans) ``` - 规则的两个前提都提到了元变量 U，但结论中却未出现。从下往上读规则时，需要猜测一个类型 U，而可能的 U 有无限多个，这种策略很难成功。 - **S - Refl 规则问题**：该规则也与其他子类型规则的结论重叠，尽管它没有前提，若匹配到要证明的子类型陈述可立即成功，但这也是规则非语法导向的一个原因。 #### 2. 解决方案概述 为解决上述问题，引入了算法子类型关系和算法类型检查关系，其推理规则集是语法导向的。并且证明了原有的子类型和类型检查关系与算法表示实际上是一致的。 #### 3. 算法子类型关系 ##### 3.1 规则重组 在定义算法子类型关系之前，需要对原有的声明系统进行一些重组。 - 增加规则 S - Rcd，将深度、宽度和排列子类型化合并为一个规则，替代 S - RcdDepth、S - Rcd - Width 和 S - Rcd - Perm 规则。 ```plaintext {li i∈1..n} ⊆ {kj j∈1..m} kj = li implies Sj <: Ti {kj:Sj j∈1..m} <: {li:Ti i∈1..n} (S - Rcd) ``` - 证明了在包含 S - Rcd 的系统中，自反性和传递性规则是不必要的。 - 引理 1：对于每个类型 S，无需使用 S - Refl 即可推导出 S <: S。 - 引理 2：如果 S <: T 可推导，则无需使用 S - Trans 也可推导。 ##### 3.2 算法子类型关系定义 算法子类型关系是满足图 16 - 2 中规则的最小类型关系。 ```plaintext Algorithmic subtyping ⊢▶ S <: T ⊢▶ S <: Top (SA - Top) {li i∈1..n} ⊆ {kj j∈1..m} if kj = li, then ⊢▶ Sj <: Ti ⊢▶ {kj:Sj j∈1..m} <: {li:Ti i∈1..n} (SA - Rcd) ⊢▶ T1 <: S1 ⊢▶ S2 <: T2 ⊢▶ S1→S2 <: T1→T2 (SA - Arrow) ``` 该算法子类型关系具有以下性质： - **正确性和完备性**：S <: T 当且仅当 ⊢▶ S <: T。 - **终止性**：如果 ⊢▶ S <: T 可推导，则 subtype(S, T) 将返回 true；否则返回 false。 ##### 3.3 算法实现 算法子类型关系的规则可以直接作为检查算法子类型关系（进而也是声明子类型关系）的算法，用更传统的伪代码表示如下： ```plaintext subtype(S, T) = if T = Top, then true else if S = S1→S2 and T = T1→T2 then subtype(T1, S1) ∧ subtype(S2, T2) else if S = {kj:Sj j∈1..m} and T = {li:Ti i ```