值限制与安全泛化

一个多态恒等函数的不同使用可以选择不同类型，因为函数不保存一份会被后来的使用改写的“当前实参”。一个引用则是真实共享的存储单元：第一次把整数写进去，第二次仍读同一块内容。若两次使用可以各自任意选择该单元的元素类型，就会给一块内存同时签发互相冲突的读写许可。

关键不是“值里绝对不能含引用”。函数值可以捕获引用，但捕获环境中已有的类型变量不会被泛化；函数体内部也可以分配引用，只要每次调用的分配与类型实例相匹配。值限制与“只量化环境外的变量”要一起使用。

一次不安全泛化怎样真的卡住 ​

暂时错误地允许

let r = ref [] in
r := [8];
if head(!r) then 0 else 1

在分配处把r泛化成 $\mathrm{\forall }a.\mathrm{Ref}(\mathrm{List}(a))$。写入时选择 $a=\mathrm{Int}$，读取时另选 $a=\mathrm{Bool}$，坏规则便会让整个程序看起来类型正确。

但运行只有一个地址ℓ：

此例没有空列表head错误，因为真正读出的列表非空。失败恰在整数被冒充布尔值，破坏进展与保持公理库进展与保持定理Progress and preservation · Type safety对按值调用的简单类型 lambda 演算逐层解释规范形、替换、进展与保持，以及类型安全的准确结论。希望保证的运行时安全。

正确规则在 ref [] 处保留一个共享α，令 $r:\mathrm{Ref}(\mathrm{List}(\alpha ))$。写入[8]把α确定为Int；随后if要求同一个α为Bool，检查器报告Int与Bool冲突，程序在执行前被拒绝。

把共享单元改成工厂 ​

下面的接口安全：

let fresh = fun () -> ref [] in
let ri = fresh() in
let rb = fresh() in
ri := [8];
rb := [true]

fresh的右侧是λ值，可取得类型方案公理库类型方案Type scheme · Polytype通过显式量化类型变量表示一族单态类型的多态对象。

两次调用各自产生新地址 ${\ell }_i\ne {\ell }_b$。ri和rb仍分别是单态引用，但它们不共享同一个类型变量，因此可以一处存整数、一处存布尔。改变接口的代价也要看清：原来请求“一份共享缓存”，现在提供“每次新建一个缓存”，两种程序的状态共享语义不同。

反过来，若外层已有 $r:\mathrm{Ref}(\mathrm{List}(\alpha ))$，再写 let read = fun () -> !r，α仍自由出现在Γ中。即使右侧是λ，read也不能取得 $\mathrm{\forall }a.\mathrm{Unit}\to \mathrm{List}(a)$；它只能读r固定的元素类型。

安全程序也可能被保守限制 ​

let id2 = (fun f -> f) (fun x -> x)没有副作用，结果确实是恒等函数。基础值限制仍把右侧看作应用，不泛化其 $\alpha \to \alpha$。编译器不必为了每个let先证明任意函数调用都无状态；句法规则以少量误拒换取简单、局部的检查。

可以把它改成 fun x -> ((fun f -> f) (fun y -> y)) x，使外层成为λ值。不过一般程序的η展开可能把副作用从定义时移到调用时，甚至改变执行次数；不能把它当作无条件保持语义的修复按钮。

放宽的值限制允许对扩张表达式结果类型中只出现在协变位置的候选变量泛化。直观上，不可变List只把元素交给使用者，不允许使用者写入一个不同类型的元素，所以 (fun () -> [])()的结果可获得 $\mathrm{\forall }a.\mathrm{List}(a)$。

协变性与子类型公理库子类型Subtyping允许某类型值在期望其上界类型的位置使用的可替代关系。中的方向相同：若A可替代B，List A可替代List B。函数域反向、函数余域同向，因此 $a\to a$ 中a同时出现在两种方向，不能靠这个放宽规则泛化。可读可写Ref必须不变，否则扩大可写类型后会把不允许的值写回窄类型视图；Ref(List a)中的a也不能据此放宽。

对抽象类型构造器，客户端还须知道接口声明的variance。实现私下使用不可变列表，而接口没有暴露协变性，并不让客户端自动获得这个证明。

值限制解决的是“何时安全地产生类型方案”。它不处理多态函数参数的量词位置，也不允许递归体自动在不同类型上调用自己；这些分别进入高秩多态公理库高秩多态与局部检查Higher-rank polymorphism · Rank-n polymorphism把全称量词放进函数参数类型，并用实例化、刚性变量与逃逸检查验证多态承诺。与多态递归公理库多态递归Polymorphic recursion · Milner–Mycroft recursion让递归定义内部的每次自调用重新实例化显式全称签名，以处理参数类型随结构层次变化的数据。。