文章基本信息

标题：Row and Bounded Polymorphism via Disjoint Polymorphism
本地全文：下载
作者：Ningning Xie ; Bruno C. d. S. Oliveira ; Xuan Bi 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2020
卷号：166
页码：1-30
DOI：10.4230/LIPIcs.ECOOP.2020.27
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：Polymorphism and subtyping are important features in mainstream OO languages. The most common way to integrate the two is via ð-¥_{< :} style bounded quantification. A closely related mechanism is row polymorphism, which provides an alternative to subtyping, while still enabling many of the same applications. Yet another approach is to have type systems with intersection types and polymorphism. A recent addition to this design space are calculi with disjoint intersection types and disjoint polymorphism. With all these alternatives it is natural to wonder how they are related. This paper provides an answer to this question. We show that disjoint polymorphism can recover forms of both row polymorphism and bounded polymorphism, while retaining key desirable properties, such as type-safety and decidability. Furthermore, we identify the extra power of disjoint polymorphism which enables additional features that cannot be easily encoded in calculi with row polymorphism or bounded quantification alone. Ultimately we expect that our work is useful to inform language designers about the expressive power of those common features, and to simplify implementations and metatheory of feature-rich languages with polymorphism and subtyping.
关键词：Intersection types; bounded polymorphism; row polymorphism