Assaf Kfoury, Harry Mairson, Franklyn Turbak, and J.B. Wells. Relating Typability and Expressiveness in Finite-Rank Intersection Type Systems. International Conference on Functional Programming (ICFP '99). ACM, 1999.

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 KK(0,n)=n and KK(t+1,n)=2^KK(t,n); we prove that recognizing the pure λ-terms of size n that are typable at rank k is complete for DTIME[KK(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[KK(KK(k-1,n),2)]-complete. This relationship between the complexity of typability and expressiveness is identical in well-known 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 T is a predicative type system where typability has complexity t(n) and expressiveness has complexity e(n), then t(n)=Ω(log^*(e(n))).

[PS] [PDF]