Type Inference For Recursive Definitions
Data(s) |
20/10/2011
20/10/2011
06/03/2000
|
---|---|
Resumo |
We consider type systems that combine universal types, recursive types, and object types. We study type inference in these systems under a rank restriction, following Leivant's notion of rank. To motivate our work, we present several examples showing how our systems can be used to type programs encountered in practice. We show that type inference in the rank-k system is decidable for k ≤ 2 and undecidable for k ≥ 3. (Similar results based on different techniques are known to hold for System F, without recursive types and object types.) Our undecidability result is obtained by a reduction from a particular adaptation (which we call "regular") of the semi-unification problem and whose undecidability is, interestingly, obtained by methods totally different from those used in the case of standard (or finite) semi-unification. National Science Foundation (CCR-9417382, EIA-9806745) |
Identificador |
Kfoury, Assaf; Pericas-Geertsen, Santiago M.. "Type Inference For Recursive Definitions", Technical Report BUCS-2000-007, Computer Science Department, Boston University, March 6, 2000. [Available from: http://hdl.handle.net/2144/1801] |
Idioma(s) |
en_US |
Publicador |
Boston University Computer Science Department |
Relação |
BUCS Technical Reports;BUCS-TR-2000-007 |
Palavras-Chave | #Type systems #Type inference #Lambda calculus #Unification #Software specification |
Tipo |
Technical Report |