Paper: Type Inference for Recursive Definitions (at LICS 1999)

Authors: Assaf J. Kfoury Santiago M. Pericás-Geertsen

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 \mathand undecidable for \math. (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.

BibTeX

  @InProceedings{KfouryPericsGeertse-TypeInferenceforRec,
    author = 	 {Assaf J. Kfoury and Santiago M. Pericás-Geertsen},
    title = 	 {Type Inference for Recursive Definitions},
    booktitle =  {Proceedings of the Fourteenth Annual IEEE Symposium on Logic in Computer Science (LICS 1999)},
    year =	 {1999},
    month =	 {July}, 
    pages =      {119--128},
    location =   {Trento, Italy}, 
    publisher =	 {IEEE Computer Society Press}
  }