On Fast Code Completion using Type Inhabitation
Tihomir Gvero, Viktor Kunčak, Ivan Kuraj, Ružica Piskač · Infoscience (Ecole Polytechnique Fédérale de Lausanne) · 2012
Developing modern software applications typically involves com-posing 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 syn-thesizes and suggests valid expressions of a given type at a given program point. As the basis of our technique we use type recon-struction for lambda calculus with subtyping. We show that the in-habitation problem in the presence of subtyping remains PSPACE-complete. We introduce a succinct representation for type judge-ments that merges types into equivalence classes to reduce the search space. We introduce a proof rule on this succinct represen-tation of types and show that it is sound and complete for inhabita-tion. We implemented the resulting algorithm and deployed it as a plugin for the Eclipse IDE for Scala. 1.