Unifiable Subtyping

Abstract. Key longstanding difficulties associated with subtyping can be avoided by using type unification instead of subtyping on function argument types. In particular, the types of method specialisations need only be unifiable subtypes of the method’s default type. Now methods can be viewed as pattern-matching functions in the recently defined higher-order pattern calculus, a small calculus that supports polymorphism with respect to data, structures, paths, patterns and now subtyping.