Gradual Typing for Objects
Gradual Typing for Objects
复制标题
DOI：
10.1007/978-3-540-73589-2_2
复制
发表时间：
2007-07
期刊：
影响因子：
--
通讯作者：
Jeremy G. Siek;Walid Taha
中科院分区：
文献类型：
--
作者：
Jeremy G. Siek;Walid Taha
静态和动态类型系统有众所周知的优点和缺点。在以前的工作中，我们为一个名为的函数演算开发了一个模型式系统。渐进式类型通过允许程序员通过添加或删除变量上的类型注释来控制程序的一部分是在编译时还是在运行时进行类型检查，从而在单一语言中同时提供静态和动态检查的好处。几种面向对象的脚本语言正准备添加静态检查。为了支持这项工作，本文开发了一个面向对象语言的渐进式系统，扩展了Ob<； ：Abadi和Cardelli演算。我们的主要贡献是表明逐步类型化和子类型化是正交的，并且可以按原则组合在一起。我们还开发了一种小步语义，提供了类型安全的机器检查证明，并提高了高阶强制转换的空间效率。
Static and dynamic type systems have well-known strengths and weaknesses. In previous work we developed agradual type systemfor a functional calculus named. Gradual typing provides the benefits of both static and dynamic checking in a single language by allowing the programmer to control whether a portion of the program is type checked at compile-time or run-time by adding or removing type annotations on variables. Several object-oriented scripting languages are preparing to add static checking. To support that work this paper develops, a gradual type system for object-based languages, extending theOb< :calculus of Abadi and Cardelli. Our primary contribution is to show that gradual typing and subtyping are orthogonal and can be combined in a principled fashion. We also develop a small-step semantics, provide a machine-checked proof of type safety, and improve the space efficiency of higher-order casts.