Academic Journal
Elaborating Intersection and Union Types
| العنوان: | Elaborating Intersection and Union Types |
|---|---|
| المؤلفون: | Joshua Dunfield |
| المساهمون: | The Pennsylvania State University CiteSeerX Archives |
| المصدر: | http://web.cs.cmu.edu/%7Ejoshuad/papers/intcomp/Dunfield12_elaboration.pdf. |
| المجموعة: | CiteSeerX |
| مصطلحات موضوعية: | Categories and Subject Descriptors F.3.3 [Mathematical Logic and Formal Languages, Studies of Program Constructs—Type structure Keywords intersection |
| الوصف: | Designing and implementing typed programming languages is hard. Every new type system feature requires extending the metatheory and implementation, which are often complicated and fragile. To ease this process, we would like to provide general mechanisms that subsume many different features. In modern type systems, parametric polymorphism is fundamental, but intersection polymorphism has gained little traction in programming languages. Most practical intersection type systems have supported only refinement intersections, which increase the expressiveness of types (more precise properties can be checked) without altering the expressiveness of terms; refinement intersections can simply be erased during compilation. In contrast, unrestricted intersections increase the expressiveness of terms, and can be used to encode diverse language features, promising an economy of both theory and implementation. We describe a foundation for compiling unrestricted intersection and union types: an elaboration type system that generates ordinary λ-calculus terms. The key feature is a Forsythe-like merge construct. With this construct, not all reductions of the source program preserve types; however, we prove that ordinary call-byvalue evaluation of the elaborated program corresponds to a typepreserving evaluation of the source program. We also describe a prototype implementation and applications of unrestricted intersections and unions: records, operator overloading, and simulating dynamic typing. |
| نوع الوثيقة: | text |
| وصف الملف: | application/pdf |
| اللغة: | English |
| Relation: | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.303.7702; http://web.cs.cmu.edu/%7Ejoshuad/papers/intcomp/Dunfield12_elaboration.pdf |
| الاتاحة: | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.303.7702 http://web.cs.cmu.edu/%7Ejoshuad/papers/intcomp/Dunfield12_elaboration.pdf |
| Rights: | Metadata may be used without restrictions as long as the oai identifier remains attached to it. |
| رقم الانضمام: | edsbas.D1C9D2BB |
| قاعدة البيانات: | BASE |
| الوصف غير متاح. |