Title: Principality and Decidable Type Inference
for Finite-Rank Intersection Types
Authors: A. J. Kfoury and J. B. Wells
Date: 6 November 1998
Abstract: Principality of typings is the property that for each
typable term, there is a typing from which all other typings are
obtained via some set of operations. Type inference is the problem
of finding a typing for a given term, if possible. We define an
intersection type system which has principal typings and types
exactly the strongly normalizable $\lambda$-terms. More interestingly,
every finite-rank restriction of this system (using Leivant's first
notion of rank) has principal typings and also has decidable type
inference. This is in contrast to System~F where the finite rank
restriction for every finite rank at 3 and above has neither principal
typings nor decidable type inference. This is also in contrast to
earlier presentations of intersection types where the status of these
properties is not known for the finite-rank restrictions at 3 and above.
Furthermore, the notion of principal typings for our system involves
only one operation, substitution, rather than several operations
(not all substitution-based) as in earlier presentations of
principality for intersection types (of unrestricted rank).
A unification-based type inference algorithm is presented using a
new form of unification, $\beta$-unification.