Polymorphic recursion and subtype qualifications: Polymorphic binding-time analysis in polynomial time

Abstract

The combination of parameter polymorphism, subtyping extended to qualified and polymorphic types, and polymorphic recursion is useful in standard type inference and gives expressive type-based program analyses, but raises difficult algorithmic problems. In a program analysis context we show how Mycroft's iterative method of computing principal types for a type system with polymorphic recursion can be generalized and adapted to work in a setting with subtyping. This does not only yield a proof of existence of principal types (most general properties), but also an algorithm for computing them. The punch-line of the development is that a very simple modification of the basic algorithm reduces its computational complexity from exponential time to polynomial time relative to the size of the given, explicitly typed program. This solves the open problem of finding an inference algorithm for polymorphic binding-time analysis [7].