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

d Abstract) Assaf J. Kfoury∗ Boston University http://www.cs.bu.edu/˜kfoury Harry G. Mairson† Brandeis University http://www.cs.brandeis.edu/˜mairson Franklyn A. Turbak‡ Wellesley College http://www.wellesley.edu/CS/fturbak.html J. B. Wells § Heriot-Watt University http://www.cee.hw.ac.uk/˜jbw 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 τ1 ∧ τ2 to be used in some places at type τ1 and in other places at type τ2. 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 polymorph...

• Type: Conference
• Year: 1999
• Where: ICFP
• Authors: Assaf J. Kfoury, Harry G. Mairson, Franklyn A. Turbak, J. B. Wells
• Keywords: ICFP 1999, Intersection Type, Programming Languages, Type Inference, Type System