Matching MyType to subtyping

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.