Intensional polymorphism in type-erasure semantics
Intensional polymorphism in type-erasure semantics
复制标题
类型擦除语义中的内涵多态性
DOI：
--
复制
发表时间：
1998
期刊：
影响因子：
--
通讯作者：
G. Morrisett
中科院分区：
文献类型：
--
作者：
Karl Crary;Stephanie Weirich;G. Morrisett
内涵多态性，即在运行时根据类型分派到不同例程的能力，支持多态语言的各种高级实现技术，包括无标记垃圾收集、拆箱函数参数、多态编组和扁平化数据结构。迄今为止，支持内涵多态性的语言需要类型传递（而不是类型擦除）解释，其中类型在运行时构造并传递给多态函数。不幸的是，类型传递有许多缺点：它需要在术语和类型级别上重复构造，它阻止了抽象，并且使多态闭包转换严重复杂化。我们提出了一个支持内涵多态性的类型理论框架，但避免了类型传递的许多缺点。在我们的方法中，运行时类型信息由普通术语表示。这避免了重复问题，使我们能够恢复抽象，并避免闭包转换的复杂性。此外，我们的类型系统在表现力方面提供了另一项改进；它允许就地改进未知类型，从而避免其他框架所需的某些 beta 扩展。
Intensional polymorphism, the ability to dispatch to different routines based on types at run time, enables a variety of advanced implementation techniques for polymorphic languages, including tag-free garbage collection, unboxed function arguments, polymorphic marshalling, and flattened data structures. To date, languages that support intensional polymorphism have required a type-passing (as opposed to type-erasure) interpretation where types are constructed and passed to polymorphic functions at run time. Unfortunately, type-passing suffers from a number of drawbacks: it requires duplication of constructs at the term and type levels, it prevents abstraction, and it severely complicates polymorphic closure conversion.We present a type-theoretic framework that supports intensional polymorphism, but avoids many of the disadvantages of type passing. In our approach, run-time type information is represented by ordinary terms. This avoids the duplication problem, allows us to recover abstraction, and avoids complications with closure conversion. In addition, our type system provides another improvement in expressiveness; it allows unknown types to be refined in place thereby avoiding certain beta-expansions required by other frameworks.