轻量级Java：名义类型系统与结构类型系统解析

### 轻量级Java：名义类型系统与结构类型系统解析 #### 1. 轻量级Java中的计算规则与类型转换 在轻量级Java（FJ）里，方法调用时会把特殊变量`this`替换为接收对象，这和lambda演算的beta - 归约规则（E - AppAbs）类似。不过，关键区别在于接收对象的类决定了方法体的查找位置，支持方法重写，并且用接收对象替换`this`，支持“通过自身的开放递归”。 类型转换规则（E - CastNew）的示例如下： ```plaintext (Pair)new Pair(new A(), new B()) -→ new Pair(new A(), new B()) ``` 当类型转换的主体被归约为对象后，很容易检查构造函数的类是否为转换目标的子类。如果是，就移除类型转换；若不是，如`(A)new B()`，则没有适用规则，计算会卡住，这表示运行时错误。 计算可能卡住的情况有三种： - 尝试访问类未声明的字段。 - 尝试调用类未声明的方法（“消息未理解”）。 - 尝试将对象转换为其运行时类的非超类类型。 在类型良好的程序中，前两种情况不会发生；在不包含向下转换和“愚蠢转换”的类型良好的程序中，第三种情况也不会发生。 采用标准的值调用求值策略，以下是示例项的求值步骤： ```plaintext ((Pair) (new Pair(new Pair(new A(),new B()), new A()) .fst).snd -→ ((Pair)new Pair(new A(),new B())).snd -→ new Pair(new A(), new B()).snd -→ new B() ``` #### 2. 名义类型系统与结构类型系统的差异 在之前的示例中，我们常为长或复杂的复合类型定义短名称，如： ```plaintext NatPair = {fst:Nat, snd:Nat}; ``` 这种定义只是为了美观，`NatPair`只是`{fst:Nat,snd:Nat}`的简单缩写，二者在任何上下文中都可互换。 而在Java等广泛使用的编程语言中，类型定义的作用更重要。Java程序中使用的每个复合类型都有名称，声明局部变量、字段或方法参数的类型时，总是通过名称来进行，像`{fst:Nat,snd:Nat}`这样的“裸”类型不能出现在这些位置。 类型名称在Java的子类型关系中起着关键作用。每次引入新名称（在类或接口定义中）时，程序员要明确声明新类型扩展的类和接口（对于新类和现有接口，是“实现”）。编译器会检查这些声明，确保新类或接口提供的功能确实扩展了每个超类或超接口的功能，这对应于类型化lambda演算中的记录子类型。子类型关系现在定义为类型名称之间的自反和传递闭包。 类型系统可分为名义类型系统和结构类型系统： - **名义类型系统**：名称有重要意义，子类型关系需显式声明，如Java。 - **结构类型系统**：名称不重要，子类型关系直接基于类型结构定义。 #### 3. 名义类型系统的优缺点 ##### 优点 - **运行时类型标签**：名义系统中的类型名称不仅在类型检查时有用，在运行时也有用。大多数名义语言会为每个运行时对象标记包含其类型名称的头字，这对运行时类型测试、打印、数据结构的二进制存储和传输以及反射功能都很方便。在结构系统中也可支持运行时类型标签，但这是额外的机制，而在名义系统中，运行时标签与编译时类型相同。 - **递归类型处理**：名义系统能自然直观地处理递归类型，递归类型在编程中很常见，用于描述列表和树等结构。在名义系统中，在类型声明中引用自身和引用其他类型一样容易，甚至相互递归类型也很直接。虽然结构类型系统也能处理递归类型，但在一些基础演算中，处理递归类型的机制可能很复杂。 - **子类型检查**：检查一个类型是否为另一个类型的子类型几乎很简单。编译器只需在类型定义时验证声明的子类型关系是否安全，而不是在每次子类型检查时都进行验证，这使名义类型系统的类型检查器更容易实现良好性能。 - **防止虚假包含**：显式的子类型声明可防止“虚假包含”，即类型检查器未能拒绝在期望完全不同但结构兼容的类型处使用某个类型值的程序。不过，也有其他更好的方法来防止这种情况。 ##### 缺点 - **定义和证明更冗长**：在结构设置中，类型表达式是封闭实体，携带理解其含义所需的所有信息；而在名义系统中，总是要处理全局的类型名称和相关定义集合，这使定义和证明更冗长。 - **高级特性支持不佳**：研究文献关注的高级类型抽象特性（如参数多态、抽象数据类型等）在名义系统中不太适用。像`List(T)`这样的类型似乎不可约地复合，不能将其视为原子名称。一些名义语言扩展了这些“泛型”特性，但结果不再是纯粹的名义系统，而是两种方法的复杂混合。 #### 4. 轻量级Java的形式定义 ##### 语法 | 语法元素 | 定义 | | ---- | ---- | | 类声明（CL） | `class C extends C {C f; K M}` | | 构造函数声明（K） | `C(C f) {super(f); this.f=f;}` | | 方法声明（M） | `C m(C x) {return t;}` | | 项（t） | `x`（变量）、`t.f`（字段访问）、`t.m(t)`（方法调用）、`new C(t)`（对象创建）、`(C) t`（类型转换） | | 值（v） | `new C(v)`（对象创建） | 子类型关系定义如下： ```plaintext C<:D C <: C C <: D D <: E C <: E CT(C) = class C extends D {...} C <: D ``` 假设变量集包含特殊变量`this`，但`this`不能用作方法参数的名称，它在每个方法声明中被隐式绑定。 用`f`表示`f1,