Logic in Computer Science (LICS 2002)

Paper: Efficient Type Inference for Record Concatenation and Subtyping (at LICS 2002)

Authors: Jens Palsberg Tian Zhao

Abstract

Record concatenation, multiple inheritance, and multiple-object cloning are closely related and part of various language designs. For example, in Cardelli's untyped Obliq language, a new object can be constructed from several existing objects by cloning followed by concatenation; an error is given in case of field name conflicts. Type systems for record concatenation have been studied by Wand, Harper and Pierce, Remy, and others; and type inference for the combination of record concatenation and subtyping has been studied by Sulzmann and by Pottier. In this paper we present the first polynomial-time type inference algorithm for record concatenation, subtyping, and recursive types. Our example language is the Abadi-Cardelli object calculus extended with a concatenation operator. The type inference algorithm runs in O(n^5) time where n is the size of the program. Our algorithm enables efficient type checking of Obliq programs without changing the programs at all.

BibTeX

  @InProceedings{PalsbergZhao-EfficientTypeInfere,
    author = 	 {Jens Palsberg and Tian Zhao},
    title = 	 {Efficient Type Inference for Record Concatenation and
    Subtyping},
    booktitle =  {Proceedings of the Seventeenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2002},
    year =	 2002,
    editor =	 {Gordon Plotkin},
    month =	 {July}, 
    location =   {Copenhagen, Denmark}, 
    publisher =	 {IEEE Computer Society Press}
  }