Code Completion using Quantitative Type Inhabitation
Tihomir Gvero, Viktor Kunčak, Ružica Piskač · Infoscience (Ecole Polytechnique Fédérale de Lausanne) · 2011
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. The technique generates expressions by taking into account 1) polymorphic type constraints of the values in scope, 2) the API usage patterns in a corpus of code, and 3) any available test cases. It supports polymorphic type declarations and can synthe-size expressions containing methods with any number of arguments and any depth. Our synthesis approach is based on a quantitative generalization of the type inhabitation problem with weighted type assignments. Weights indicate preferences to certain type bind-ings; they guide the search and enable the ranking of solutions. We present a new polynomial-time algorithm for a restricted ver-sion of quantitative type inhabitation, as well as a complete semi-decision procedure for the general case of generic types. We iden-tify a simple method to handle subtyping by introducing coercion functions and then erasing them in the final expressions. We have implemented our technique and evaluated it on over 100 examples taken from the Web. The system was remarkably effective in re-inventing the erased expressions from the (previously unprocessed) code and ranking these expressions among the top suggestions for the developer. Our overall experience indicates that this approach to synthesizing and suggesting code fragments goes beyond cur-rently available techniques and is a useful functionality of software development environments. 1.