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 τ₁ Λ τ₂ to be used in some places at type τ₁ and in other places at type τ₂. A finite-rank intersection type system bounds how deeply the Λ 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 λ-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 λ-terms typable at rank k have the same normal form, generalizing a well-known result of Statman from simple types to finite-rank intersection types. We show that the equivalence problem is DTIME[K(K(k − 1, n), 2)]-complete. This relationship between the complexity of typability and expressiveness is identical in wellknown decidable type systems such as simple types and Hindley-Milner types, but seems to fail for System F and its generalizations. The correspondence gives rise to a conjecture that if Τ is a predicative type system where typability has complexity t(n) and expressiveness has complexity e(n), then t(n) = Ω(log* e(n)).