Paper Info
Title
Principality and decidable type inference for finite-rank intersection types
Abstract
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.
Year
DOI
Venue
1999
10.1145/292540.292556
POPL
Keywords
Field
DocType
finite rank restriction,type inference,finite rank,unification-based type inference algorithm,decidable type inference,finite-rank intersection types,principal typing,finite-rank intersection type,intersection type system,intersection type,finite-rank restriction,earlier presentation,java,continuations,subroutines,technical report
Programming language,Subroutine,Computer science,Unification,System F,Decidability,Type inference,Polymorphic recursion,Bytecode,Undecidable problem
Conference
ISBN
Citations 
PageRank 
1-58113-095-3
42
1.61
References 
Authors
15
2
Name
Order
Citations
PageRank
A. J. Kfoury146147.34
J. B. Wells239825.09