命令式对象与有界量化的类型系统研究

### 命令式对象与有界量化的类型系统研究 #### 1. 命令式对象的优化历程 在编程中，命令式对象的实现效率一直是关注的重点。最初，在定义类时，我们采用了一种基本的方法。例如，对于具有 `get`、`set` 和 `inc` 方法的计数器对象类： ``` SetCounter = {get:Unit→Nat, set:Nat→Unit, inc:Unit→Unit}; CounterRep = {x: Ref Nat}; setCounterClass = λr:CounterRep. λself: Source SetCounter. {get = λ_:Unit. !(r.x), set = λi:Nat. r.x:=i, inc = λ_:Unit. (!self).set (succ ((!self).get unit))}; ``` 这里使用 `Source SetCounter` 作为 `self` 参数的类型，是为了在定义子类时能更好地处理类型差异。比如，对于带检测功能的计数器对象类： ``` InstrCounter = {get:Unit→Nat, set:Nat→Unit, inc:Unit→Unit, accesses:Unit→Nat}; InstrCounterRep = {x: Ref Nat, a: Ref Nat}; instrCounterClass = λr:InstrCounterRep. λself: Source InstrCounter. let super = setCounterClass r self in {get = super.get, set = λi:Nat. (r.a:=succ(!(r.a)); super.set i), inc = super.inc, accesses = λ_:Unit. !(r.a)}; ``` 然而，这种实现的效率并非最优。因为每个从给定类实例化的对象都关联着相同的方法表，我们应该在类创建时只构建一次方法表，然后在每次创建对象时复用它。于是，我们对 `setCounterClass` 进行了重写： ``` setCounterClass = λself: Source (CounterRep→SetCounter). λr:CounterRep. {get = λ_:Unit. !(r.x), set = λi:Nat. r.x:=i, inc = λ_:Unit. (!self r).set (succ ((!self r).get unit))}; ``` 这个新版本有三个显著变化： - 先接收 `self` 参数，再接收 `r` 参数。 - `self` 的类型从 `SetCounter` 变为 `CounterRep→SetCounter`。 - 类体中所有对 `!self` 的使用都变为 `(!self r)`。 同时，新计数器的实例化函数定义如下： ``` newSetCounter = let m = ref (λr:CounterRep. error as SetCounter) in let m’ = setCounterClass m in (m := m’; λ_:Unit. let r = {x=ref 1} in m’ r); ``` 但这种重排引入了一个问题，当定义 `setCounterClass` 的子类时，会出现参数类型不匹配的错误。为了解决这个问题，我们再次重写 `setCounterClass`，使用有界量化： ``` setCounterClass = λR<:CounterRep. λself: Source(R→SetCounter). λr: R. {get = λ_:Unit. !(r.x), set = λi:Nat. r.x:=i, inc = λ_:Unit. (!self r).set (succ((!self r).get unit))}; ``` 这样，`setCounterClass` 对传入的 `self` 参数要求降低了。在定义子类 `instrCounterClass` 时： ``` instrCounterClass = ```