幻影类型与子类型

我们研究了文献中的一种技术，称为幻影类型技术，该技术使用参数化多态、类型约束和多态类型的合一来对子类型层次结构进行建模。Hindley-Milner 类型系统（例如 Standard ML 中的类型系统）可用于强制执行子类型关系，至少对于一阶值是如此。我们表明该技术可用于编码任何有限的子类型层次结构（包括由多重接口继承产生的层次结构）。我们通过展示从具有受限多态的简单演算到体现 SML 类型系统的演算的类型保持翻译，正式论证了幻影类型技术适用于捕获一阶子类型的适用性。