# Type Inference for Intersection Types with Expansion Variables

Joe Wells Department of Computing and Electrical Engineering Heriot-Watt University 4pm Wednesday 21 April 1999 Room 2511, JCMB, King's Buildings

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 (decidable or undecidable) of these properties is unknown
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 (without rank restrictions). In our system the
earlier notion of *expansion* is integrated in the form of
*expansion variables*, which are subject to substitution as
are ordinary variables. A unification-based type inference
algorithm is presented using a new form of unification,
beta-unification.