摘要
Type abstraction and intensional type analysis are features seemingly at odds-type abstraction is intended to guarantee parametricity and representation independence, while type analysis is inherently non-parametric. Recently, however, several researchers have proposed and implemented "dynamic type generation" as a way to reconcile these features. The idea is that, when one defines an abstract type, one should also be able to generate at run time a fresh type name, which may be used as a dynamic representative of the abstract type for purposes of type analysis. The question remains: in a language with non-parametric polymorphism, does dynamic type generation provide us with the same kinds of abstraction guarantees that we get from parametric polymorphism?
摘要译文
类型抽象和内涵类型分析似乎是相矛盾的功能-类型抽象旨在保证参数性和表示独立性,而类型分析本质上是非参数性的。但是,最近,一些研究人员提出并实现了动态类型生成,以协调这些功能。想法是,当定义抽象类型时,还应该能够在运行时生成一个新的类型名称,该名称可以用作类型分析目的抽象类型的动态表示。问题仍然存在:在具有非参数多态性的语言中,动态类型生成是否为我们提供了与我们从参数多态性中获得的相同的抽象保证?
Georg Neis[1];Derek Dreyer[1];Andreas Rossberg[1]. Non-parametric parametricity[C]//ICFP '09:Proceedings of the 14th ACM SIGPLAN international conference on Functional programming, Edinburgh ,Scotland, August, 2009, UK: ACM, 2009: 135–148