Gradual typing for first-class classes
Gradual typing for first-class classes
复制标题
一流课程的逐步打字
DOI：
10.1145/2384616.2384674
复制
发表时间：
2012
影响因子：
--
通讯作者：
Matthias Felleisen
中科院分区：
文献类型：
--
作者：
Asumu Takikawa;T. Strickland;Christos Dimoulas;Sam Tobin;Matthias Felleisen
动态类型检查和面向对象编程常常紧密相关；诸如Python、Ruby和JavaScript等脚本语言都采用面向对象（OO）编程。当用这些语言编写的脚本成长并演变成大型程序时，缺乏静态类型规则会降低可维护性。因此，程序员可能希望将此类脚本的部分迁移到具有静态类型系统的同类语言中。不幸的是，现有的类型系统既不支持脚本语言中灵活的面向对象组合机制，也不适应与无类型代码的合理互操作。在本文中，我们提出了一种渐进式类型系统的设计，该系统支持基于类的代码的静态类型单元和动态类型单元之间的合理交互。该类型系统对类使用行多态性，因此支持基于混入（mixin）的面向对象组合。为了保护混入从有类型组件迁移到无类型组件，该系统采用了一种新的契约形式，对类进行部分密封。该设计附带一个定理，即使存在无类型组件，也能保证类型系统的合理性。
Dynamic type-checking and object-oriented programming often go hand-in-hand; scripting languages such as Python, Ruby, and JavaScript all embrace object-oriented (OO) programming. When scripts written in such languages grow and evolve into large programs, the lack of a static type discipline reduces maintainability. A programmer may thus wish to migrate parts of such scripts to a sister language with a static type system. Unfortunately, existing type systems neither support the flexible OO composition mechanisms found in scripting languages nor accommodate sound interoperation with untyped code. In this paper, we present the design of a gradual typing system that supports sound interaction between statically- and dynamically-typed units of class-based code. The type system uses row polymorphism for classes and thus supports mixin-based OO composition. To protect migration of mixins from typed to untyped components, the system employs a novel form of contracts that partially seal classes. The design comes with a theorem that guarantees the soundness of the type system even in the presence of untyped components.