Framework for type inference with subtyping

Abstract

In type systems based on subtyping, type equality is replaced with subtyping, which is a less restrictive relationship. The idea is, if τ1 is a subtype of τ2, then a value of type τ1 can be transparently supplied whether a value of type τ2 is expected. Subtyping is used as a key concept to create formal type systems for object-oriented languages. These systems often require to be annotated with user-supplied type information. Being able to omit this information, or at least part of it, provides the programmer a greater degree of freedom, hence the desire arises to do type inference in the presence of subtyping.