摘要
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 runtime 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 (a1); DEREK DREYER (a1);ANDREAS ROSSBERG (a1). Non-parametric parametricity[J]. Journal of Functional Programming, 2011,21(4-5): 497-562