کد مقاله کد نشریه سال انتشار مقاله انگلیسی نسخه تمام متن
422055 685008 2008 24 صفحه PDF دانلود رایگان
عنوان انگلیسی مقاله ISI
Dynamic Translucency with Abstraction Kinds and Higher-Order Coercions
موضوعات مرتبط
مهندسی و علوم پایه مهندسی کامپیوتر نظریه محاسباتی و ریاضیات
پیش نمایش صفحه اول مقاله
Dynamic Translucency with Abstraction Kinds and Higher-Order Coercions
چکیده انگلیسی

When a module language is combined with forms of non-parametric type analysis, abstract types require an opaque dynamic representation in order to maintain abstraction safety. As an idealisation of such a module language, we present a foundational calculus that combines higher-order type generation, modelling type abstraction, with singleton kinds, modelling translucency. In this calculus, type analysis can dynamically exploit translucency, without breaking abstraction. Abstract types are classified by a novel notion of abstraction kinds. These are analogous to singletons, but instead of inducing equivalence they induce an isomorphism that is witnessed by explicit type coercions on the term level. To encompass higher-order forms of translucent abstraction, we give an account for higher-order coercions in a rich type system with higher-order polymorphism and dependent kinds. The latter necessitate the introduction of an analogous notion of kind coercions on the type level. Finally, we give an abstraction-safe encoding of ML-style module sealing in terms of higher-kinded type generation and higher-order coercion.

ناشر
Database: Elsevier - ScienceDirect (ساینس دایرکت)
Journal: Electronic Notes in Theoretical Computer Science - Volume 218, 22 October 2008, Pages 313-336