Code Completion using Quantitative 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. 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 synthesize 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 bindings; they guide the search and enable the ranking of solutions. We present a new polynomial-time algorithm for a restricted version of quantitative type inhabitation, as well as a complete semidecision procedure for the general case of generic types. We identify 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 reinventing 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 currently available techniques and is a useful functionality of software development environments.