Type Inference for Record Concatenation and Multiple Inheritance

We show that the type inference problem for a lambda calculus with records, including a record concatenation operator, is decidable. We show that this calculus does not have principal types, but does have finite complete sets of types: that is, for any term M in the calculus, there exists an effectively generable finite set of type schemes such that every typing for M is an instance of one the schemes in the set. We show how a simple model of object-oriented programming, including hidden instance variables and multiple inheritance, may be coded in this calculus. We conclude that type inference is decidable for object-oriented programs, even with multiple inheritance and classes as first-class values. 1. Introduction A practical motivation for type inference is to ensure an operational safety property of programs that are well-typed: that is, when we execute a well-typed program, we are guaranteed that we will never get an error message such as "bad function nil." Our goal is to ext..