Type inference with simple selftypes is NP-complete

Reviewer: R. Clayton

Type inferencing accepts a program without explicit typing, and produces an equivalent, statically typed program in which all program entities are tagged by their type. Selftyping provides virtual return types for nonvirtual, inherited class methods. Without selftypes, an inherited method returns an instance of the method's defining class; with selftypes, the method returns an instance of the calling method's class. Selftyping eliminates the explicit downcasting that may be required when a child calls methods implemented in an ancestor. NP-complete problems are best solved by first guessing a solution, and then verifying the solution's correctness. NP completeness suggests that exact solutions are exponentially expensive, and that it may be better to consider approximate solutions that are not completely correct, but that can be computed more cheaply than an exact solution. The authors demonstrate that guessing and verifying is the best way to perform type inference on programs using selftyping. They do not speculate on approximate solutions, which, given the problem, is appropriate. They do offer the hope that type and selftyping systems less austere than the ones used in this paper may provide enough extra information to allow for more efficient type inferencing. Readers who know object-oriented languages will find enough detail in this paper to pick up type inference and selftyping. Readers must be previously familiar with complexity theory, however. In fact, an unquestioning predilection for complexity proofs will be helpful: the pragmatic and unintuitive translation between type inferencing and satisfiability will deny most of the laity the small pleasure that usually comes from seeing one problem unexpectedly and neatly transformed into another. Online Computing Reviews Service