Subtyping functional+nonempty record types

Abstract

Solving systems of subtype constraints (or subtype inequalities) is in the core of efficient type reconstruction in modern object-oriented languages with subtyping and inheritance, two problems known polynomial time equivalent. It is important to know how different combinations of type constructors influence the complexity of the problem. We show the NP-hardness of the satisfiability problem for subtype inequalities between object types built by using simultaneously both the functional and the nonempty record type constructors, but without any atomic types and atomic subtyping. The class of constraints we address is intermediate with respect to known classes. For pure functional types with atomic subtyping of a special non-lattice (crown) form solving subtype constraints is PSPACE-complete [Tiuryn 92, Frey97]. On the other hand, if there are no atomic types and subtyping on them, but the largest T type is included, then both pure functional and pure record (separately) subtype constraints are polynomial time solvable, which is mainly due to the lattice type structure. We show that combining the functional and nonempty record constructors yields NP-hardness without any atomic subtyping, and the same is true for just a single type constant with a nonempty record constructor.