幽灵类型和子类型
摘要：使用文献中提到的幽灵类型技术，我们研究了一种使用参数化多态、类型约束和多态类型的一致性建模子类型层次结构的技术。 Hindley-Milner类型系统（如在标准ML中找到的）可以用于强制子类型关系，至少对于一阶值而言。我们证明了这种技术可以用来编码任何有限的子类型层次结构（包括来自多接口继承的层次结构）。我们正式证明了幽灵类型技术适用于捕捉一阶子类型，通过展示从具备有界多态性的简单演算到体现SML类型系统的演算的类型保持的翻译。
作者：Matthew Fluet, Riccardo Pucella
论文ID：cs/0403034
分类：Programming Languages
分类简称：cs.PL
提交时间：2007-05-23