Complete Completion using Types and Weights

Developing modern software 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 inhabitation for lambda calculus terms in long normal form. We introduce a succinct representation for type judgements that merges types into equivalence classes to reduce the search space, then reconstructs any desired number of solutions on demand. Furthermore, we introduce a method to rank solutions based on weights derived from a corpus of code. We implemented the algorithm and deployed it as a plugin for the Eclipse IDE for Scala. We show that the techniques we incorporated greatly increase the effectiveness of the approach. Our evaluation benchmarks are code examples from programming practice; we make them available for future comparisons.

Published in:
PLDI 2013, 27-38
Presented at:
34th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)', u'34th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI)
New York, ACM

 Record created 2013-10-01, last modified 2018-03-17

Download fulltext

Rate this document:

Rate this document:
(Not yet reviewed)