类型方案

形式陈述 ​

类型方案是表达参数多态理路参数多态Parametric polymorphism程序对类型参数统一工作而不依赖其具体表示的多态。的一种方式。先固定通常的 Hindley–Milner 情形，所有量化变量的种类都是值类型 Type，方案形如

的多态类型，其中 $\tau$ 是单态类型，使用方案时，先把量化变量换成新鲜的单态类型变量，再由该次使用把它们约束为具体单态类型。按类型变量的绑定与自由出现理路变量绑定Variable binding · Binding occurrence把变量的使用出现关联到作用域内声明，并区分自由出现、绑定出现与遮蔽。区分，方案的自由类型变量为 $\mathrm{FTV}(\sigma )=\mathrm{FTV}(\tau )\setminus \{{\alpha }_1,\dots ,{\alpha }_n\}$。在 Hindley–Milner 的类型判断理路类型判断Typing judgment由类型规则推导的上下文判断，记录项在给定变量假设下具有的静态类型。中，类型环境理路环境Environment · Lexical environment · Evaluation environment在某个程序位置把标识符解析为值、存储位置或类型信息的有限映射。把变量映射到类型方案；读取变量时实例化量化变量，let 绑定时则相对于环境泛化

未被量化的类型变量仍受当前上下文约束，不能任意实例化。

带种类与约束的行方案 ​

记录行系统可在这个外层量化结构上加入种类和约束。这里另取两种种类：Type 表示单态值类型，Row 表示有限、标签不重复的字段行，允许一个尚未确定的行变量作尾部。记录构造 $\mathrm{Rec}(\rho )$ 把 Row 变成 Type。相应方案写为

其中 $Q$ 是有限个行约束，例如 $\ell \notin \rho$ 表示字段标签 $\ell$ 不在该行中。一次实例化对所有量化变量作避免捕获的同时替换，并保持种类：Type 变量换成新鲜值类型变量，Row 变量换成新鲜行变量；同一个绑定变量的所有出现共享同一个新变量。替换同样作用于 $Q$，其得到的 lacks 义务随实例保留。后续求解必须保持种类且满足这些义务；不能把行变量当作普通值类型变量，也不能在实例化时丢掉条件。

例如

允许实例 $r=\{\mathrm{age}:\mathrm{Int}\}$，却拒绝 $r=\{\mathrm{name}:\mathrm{Bool}\}$，因为后者违反实例化后的 lacks 条件。这正是行多态理路行多态Row polymorphism · Row types以开放行变量保留记录的未知字段，并用标签无序相等和lacks约束维持唯一标签。中保留未知字段的方案形式。

对这份扩展，自由变量还要计入 $Q$，即从 $\mathrm{FV}(Q)\cup \mathrm{FV}(\tau )$ 中删去量化变量，并分别记录其种类。泛化须遵守该行系统的约束生成与求解规则，不能只泛化类型表达式而遗失其约束。只有所有绑定变量都是 Type 且 $Q$ 为空时，才退回前面的普通 HM 方案和实例化规则。