Polymorphic record calculi have recently attracted much attention as a typed foundation for object-oriented programming. Recent studies have established techniques to develop an ML-style type inference algorithm for such a polymorphic type system. Ohori established a method to compile ML-style polymorphic record calculus into an efficient code. But most of the prior studies are based on polymorhpic record calculi that lack the record concatenation operation which is essential to analyse multiple inheritence of object-oriented programming.
We define a polymorphic record calculus with the record concatenation operation as an extension of Damas and Milner's proof system for ML. For the efficient execution of our polymorphic record calculus, we extend Ohori's implementation calculus. In our implementation calculus, as in Ohori's, records are presented as arrays of values, and field selection is performed by direct indexing. We then develop an algorithm to translate the polymorphic record calculus into the implementation calculus; it simultaneously computes a principal type scheme in the polymorphic record calculus and a correct implementation term in the implementation calculus. The type inference is shown to be sound and complete.
