Complexity of kernel Fun subtype checking

System kernel Fun is an abstract version of the system Fun defined by Cardelli's and Wegner's seminal paper [CW85], and is strictly related to system F≤. Extensions of these two systems are currently the basis of most proposals for strong type systems for object-oriented languages. We study here the problem of subtype checking for system kernel Fun, presenting the following results. We show that the standard kernel Fun subtype checking algorithm has an exponential complexity, and generates an exponential number of different subproblems. We then present a new subtype checking algorithm which has a polynomial complexity. In the process we study how variable names can be managed by a kernel Fun subtype checker which is not based on the De Bruijn encoding, and we show how to perform kernel Fun subtype checking with a `constraint generating' technique. The algorithm we give is described by a set of type rules, which we prove to be equivalent to the standard one. This new presentation of kernel Fun type system is characterized by a `multiplicative' behaviour, and it may open the way to new presentations for system F≤ as well.