On Fast Code Completion using Type Inhabitation

Developing modern software applications typically involves composing functionality from existing libraries. This task is difficult because libraries may expose many methods to the developer. To help developers in such scenarios, we present a technique that synthesizes and suggests valid expressions of a given type at a given program point. As the basis of our technique we use type reconstruction for lambda calculus with subtyping. We show that the inhabitation problem in the presence of subtyping remains PSPACE-complete. We introduce a succinct representation for type judgements that merges types into equivalence classes to reduce the search space. We introduce a proof rule on this succinct representation of types and show that it is sound and complete for inhabitation. We implemented the resulting algorithm and deployed it as a plugin for the Eclipse IDE for Scala.