Relating Typability and Expressiveness in Finite-Rank Intersection Type Systems (Extended Abstract)

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 T1 A T2 to be used in some places at type T1 and in other places at type T2. A finite-rank intersection type system bounds how deeply the A 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+ l,n) =- 2^K(t,n); we prove that recognizing the pure A-terms of size n that are typable at rank k is complete for DTlME[K(k-1, n)]. We then consider the problem of deciding whether two A-terms typable at rank k have the same normal form,