Kinded type inference for parameteric overloading

Parameteric overloading refers to the combination of parameteric polymorphism and overloading of polymorphic operators. The formal basis for parametric overloading, proposed by Kaes and extended by Wadler and Blott, is based on type predicates. In this paper another approach to type-checking for parameteric overloading is proposed. The resulting type system loosens some of the restrictions required of overload instance types for type-checking, while also providing fresh insight into type-checking for parameteric overloading. In this system, the kind for a type variable characterizes the set of closed type expressions which may be substituted for that variable. A theory of equality and subkinding for this system is presented, and algorithms for emptiness-checking, subkinding and intersection are provided. This kind system is used as the basis for an extension of Milner's W algorithm for ML-style type inference to kinded type inference. Finally the kinded type system is verified to be sound and complete with respect to the system of type predicates proposed by Wadler and Blott.