Matching MyType to subtyping
Matching MyType to subtyping
复制标题
DOI：
10.1016/j.scico.2012.12.010
复制
发表时间：
2013-07
期刊：
影响因子：
--
通讯作者：
C. Saito;Atsushi Igarashi
中科院分区：
文献类型：
--
作者：
C. Saito;Atsushi Igarashi
MyType的概念是为了促进二进制方法的类型安全重用而提出的，最近扩展到了相互递归的定义。然而，众所周知，MyType并不能很好地匹配子类型。在当前的类型系统中，类型安全是以牺牲子类型以及动态调度为代价的。在本文中，我们提出了两种机制，即非遗传方法和精确语句来弥补MyType和子类型之间的不匹配。我们通过在一个小微积分中对它们进行建模，严格地证明了它们的安全性。
The notion of MyType has been proposed to promote type-safe reuse of binary methods and recently extended to mutually recursive definitions. It is well known, however, that MyType does not match with subtyping well. In current type systems, type safety is guaranteed at the expense of subtyping, and hence dynamic dispatch. In this article, we propose two mechanisms, namely, nonheritable methods and exactstatements to remedy the mismatch between MyType and subtyping. We rigorously prove their safety by modeling them in a small calculus.