Relating typability and expressiveness in finite-rank intersection type systems

We investigate finite-rank intersection type systems, analyzing the complexity of their type inference problems and their relation to the problem of recognizing semantically equivalent terms. Intersection types allow something of type tau(1) boolean AND tau 2 to be used in some places at type tau 1 and in other places at type tau 2. A finite-rant intersection type system bounds how deeply the boolean AND can appear in type expressions. Such type systems enjoy strong normalization, subject reduction, and computable type inference, and they support a pragmatics for implementing parametric polymorphism. As a consequence, they provide a conceptually simple and tractable alternative to the impredicative polymorphism of System F and its extensions, while typing many more programs than the Hindley-Milner type system found in ML and Haskell. While type inference is computable at every rank, we show that its complexity grows exponentially as rank increases. Let K(0, n) = n and K(t + 1, n) = 2(K(t.n)) we prove that recognizing the pure X-terms of size n that are typable at rank k is complete for DTIME[K(k - 1,n)]. We then consider the problem of deciding whether two X-terms typable at rank k have the same normal form.