普遍量词的扩展
摘要：扩展是对类型（即类型环境和结果类型的对）的操作，最初在带有交集类型的lambda演算的类型系统中定义，以获取主要的（即最具信息性和最强大的）类型。在类型推断场景中，扩展允许推迟选择是否以及如何使用非语法驱动的类型规则（例如交集引入），直到收集足够的信息以做出正确的决策。此外，这些选择可以等效于在类型推导中深嵌套位置插入使用此类类型规则，而无需实际检查、修改（甚至具有）类型推导。由于使用了扩展变量（例如在System E中），近年来扩展变得更加简单。本文将扩展和扩展变量扩展到具有forall量化器的系统。我们提出System Fs，这是System F的扩展，证明了其主要性质。该系统将类型推断转化为约束求解问题；这对于未来设计模块化类型推断算法可能会有所帮助。
作者：Sergue"i Lenglet and J. B. Wells
论文ID：1201.1101
分类：Programming Languages
分类简称：cs.PL
提交时间：2012-01-06