By Chieri Saito and Atsushi Igarashi. In Proceedings of the 24th Annual ACM Symposium on Applied Computing (SAC2009), pages 1851-1858, Honolulu, HI, March 2009.
The notion of
ThisType has been proposed to promote type-safe
reuse of binary methods and recently extended to mutually recursive
definitions. It is well-known, however, that
ThisType does not
match with subtyping well. In the current type systems, type safety
is guaranteed by the sacrifice of subtyping, hence dynamic dispatch.
In this paper, we propose two mechanisms, namely, nonheritable
methods and local exactization to remedy the mismatch
ThisType and subtyping. We rigorously prove their
safety by modeling them in a small calculus.