Complete completion using types and weights
- 16 June 2013
- conference paper
- conference paper
- Published by Association for Computing Machinery (ACM)
- Vol. 48 (6), 27-38
- https://doi.org/10.1145/2491956.2462192
Abstract
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.Keywords
This publication has 15 references indexed in Scilit:
- Learning from examples to improve code completion systemsPublished by Association for Computing Machinery (ACM) ,2009
- Efficient Intuitionistic Theorem Proving with the Polarized Inverse MethodPublished by Springer Science and Business Media LLC ,2009
- A Brief Overview of Agda – A Functional Language with Dependent TypesLecture Notes in Computer Science, 2009
- SNIFF: A Search Engine for Java Using Free-Form QueriesLecture Notes in Computer Science, 2009
- Enumerating Proofs of Positive FormulaeThe Computer Journal, 2008
- Coercions in a polymorphic type systemMathematical Structures in Computer Science, 2008
- ParsewebPublished by Association for Computing Machinery (ACM) ,2007
- Graph-Based Proof Counting and Enumeration with Applications for Program Fragment SynthesisLecture Notes in Computer Science, 2005
- Inheritance as implicit coercionInformation and Computation, 1991
- Intuitionistic propositional logic is polynomial-space completeTheoretical Computer Science, 1979