Type inference for record concatenation and subtyping

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 a type inference algorithm for record concatenation, subtyping, and recursive types. Our example language is the Abadi–Cardelli object calculus extended with a concatenation operator. Our algorithm enables type checking of Obliq programs without changing the programs at all. We prove that the type inference problem is NP-complete.

Authors

• Jens Palsberg
• Tian Zhao

Keywords

• Types
• Objects
• Complexity