Principality and type inference for intersection types using expansion variables

A. J. Kfoury, J. B. Wells

Research output: Contribution to journalArticle

46 Citations (Scopus)

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 ?-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. 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, ß-unification. © 2003 Elsevier B.V. All rights reserved.

Original languageEnglish
Pages (from-to)1-70
Number of pages70
JournalTheoretical Computer Science
Volume311
Issue number1-3
DOIs
Publication statusPublished - 23 Jan 2004

Fingerprint Dive into the research topics of 'Principality and type inference for intersection types using expansion variables'. Together they form a unique fingerprint.

  • Cite this