Generativity and dynamic opacity for abstract types
Generativity and dynamic opacity for abstract types
复制标题
抽象类型的生成性和动态不透明度
DOI：
--
复制
发表时间：
2003
期刊：
影响因子：
--
通讯作者：
Andreas Rossberg
中科院分区：
文献类型：
--
作者：
Andreas Rossberg
解释抽象类型的标准形式是存在量化。虽然它为完全静态类型语言中的类型抽象提供了足够的模型，但事实证明，对于富含动态类型形式的语言来说，它太弱了，因为动态类型形式违反了参数性。作为解决此缺点的类型抽象的替代方法，我们提出了动态类型生成的演算。它具有用于生成新类型名称的显式构造，并依赖强制来管理生成的类型及其指定表示之间的抽象边界。密封被表示为这些强制的一般形式。微积分动态地维护抽象而不限制类型分析。
The standard formalism for explaining abstract types is existential quantification. While it provides a sufficient model for type abstraction in entirely statically typed languages, it proves to be too weak for languages enriched with forms of dynamic typing, where parametricity is violated. As an alternative approach to type abstraction that addresses this shortcoming we present a calculus for dynamic type generation. It features an explicit construct for generating new type names and relies on coercions for managing abstraction boundaries between generated types and their designated representation. Sealing is represented as a generalized form of these coercions. The calculus maintains abstractions dynamically without restricting type analysis.