Abstract
Type systems in object-oriented systems are useful tools to ensure correctness, safety, and integration of programs. This thesis studies the matching of recursive interface types for the purpose of software-system integration and type inference for object types to help reduce bulky type information for programs with flexible type systems.
We explore the problem of equality and subtyping of recursive types. Potential applications include automatic generation of bridge code for multi-language systems and type-based retrieval of software modules from libraries. We present efficient decision procedures for a notion of type equality that includes unfolding of recursive types, and associativity and commutativity of product types. Advocated by Auerbach, Barton, and Raghavachari, these properties enable flexible matching of recursive types.
We also present results on type inference for object-oriented languages with flexible type systems including features such as read-only field and record concatenation.
Read-only fields are useful in object calculi, pi calculi, and statically-typed intermediate languages because they admit covariant subtyping, unlike updateable fields. For example, Glew's translation of classes and objects to an intermediate calculus places the method tables of classes into read-only fields; covariant subtyping on the method tables is required to ensure that subclasses are translated to subtypes. In programs that use updateable fields, read-only fields can be either specified or discovered. For both cases, we will show that type inference is equivalent to solving type constraints and computable in polynomial time.
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. We will present a 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. Our algorithm enables efficient type checking of Obliq programs without changing the programs at all.
