Rank 2 Type Systems and Recursive Definitions
Trevor Jim · DSpace@MIT (Massachusetts Institute of Technology) · 1995
We demonstrate an equivalence between the rank 2 fragments of the polymorphic lambda calculus (System F) and the intersection type discipline: exactly the same terms are typable in each system. An immediate consequence is that typability in the rank 2 intersection system is DEXPTIME-complete. We introduce a rank 2 system combining intersections and polymorphism, and prove that it types exactly the same terms as the other rank 2 systems. The combined system suggests a new rule for typing recursive definitions. The result is a rank 2 type system with decidable type inference that can type many examples of polymorphic recursion. Finally,we discuss some applications of the type system in data representation optimizations suchas unboxing and overloading.