Principal Types and Unification for Simple Intersection Type Systems

In this paper we introduce a decidable restriction of the intersection type discipline. The restriction is based on a uniform principle rather than on a notion of rank. For this system we give a type checking algorithm that we prove to be sound and complete. An extended language of types with labelled intersections and intersection schemes is needed to describe the principal type of terms which turns out to be unique module a set of equations between labels. The unification algorithm far labelled types, that extends first order unification, could be used as a basis to define inference algorithms for other (more powerful) systems with intersection.