Type Inference For Recursive Definitions
Date
2000-03-06
DOI
Authors
Kfoury, Assaf J.
Pericas-Geertsen, Santiago M.
Version
OA Version
Citation
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]
Abstract
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.