Complete completion using types and weights

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.

References

1. A. Bove, P. Dybjer, and U. Norell. A brief overview of Agda - a functional language with dependent types. In TPHOLs, 2009.
2. V. Breazu-Tannen, T. Coquand, C. A. Gunter, and A. Scedrov. Inheritance as implicit coercion. Inf. Comput., 93: 172--221, July 1991. ISSN 0890--5401. 10.1016/0890--5401(91)90055--7.
3. M. Bruch, M. Monperrus, and M. Mezini. Learning from examples to improve code completion systems. In ESEC/SIGSOFT FSE, pages 213--222, 2009.
4. S. Chatterjee, S. Juvekar, and K. Sen. SNIFF: A search engine for java using free-form queries. FASE'09, pages 385--400, 2009.
5. D. Delahaye. Information retrieval in a Coq proof library using type isomorphisms. In TYPES, pages 131--147, 1999.
6. G. Dowek. Higher-order unification and matching. Handbook of automated reasoning, II: 1009--1062, 2001.
7. G. Dowek and Y. Jiang. Enumerating proofs of positive formulae. Comput. J., 52 (7): 799--807, Oct. 2009. ISSN 0010--4620.
8. Eclipse Code Recommenders. http://www.eclipse.org/recommenders/.
9. M. Ferrari, C. Fiorentini, and G. Fiorino. fCube: An efficient prover for intuitionistic propositional logic. In LPAR (Yogyakarta), 2010.
10. T. Gvero, V. Kuncak, and R. Piskac. Interactive synthesis of code snippets (tool demonstration). In 23rd Int. Conf. Computer Aided Verification, July 14--20, 2011.
11. T. Gvero, V. Kuncak, I. Kuraj, and R. Piskac. On complete completion using types and weights. Technical report, EPFL, December 2012.
12. Hayoo! API Search. http://holumbus.fh-wedel.de/hayoo/hayoo.html.
13. R. Holmes and G. C. Murphy. Using structural context to recommend source code examples. ICSE'05, pages 117--125, 2005.
14. Hoogle API Search. http://www.haskell.org/hoogle/.
15. IntelliJ IDEA website, 2011. URL http://www.jetbrains.com/idea/.
16. I. Kuraj. Interactive code generation. Master's thesis, EPFL, February 2013.
17. Z. Luo. Coercions in a polymorphic type system. phMathematical Structures in Computer Science, 18 (4): 729--751, 2008.
18. D. Mandelin, L. Xu, R. Bodík, and D. Kimelman. Jungloid mining: helping to navigate the api jungle. In phPLDI, 2005.
19. S. McLaughlin and F. Pfenning. Efficient intuitionistic theorem proving with the polarized inverse method. In CADE, 2009.
20. D. Perelman, S. Gulwani, T. Ball, and D. Grossman. Type-directed completion of partial expressions. In PLDI, pages 275--286, 2012.
21. J. C. Reynolds. Using category theory to design implicit conversions and generic operators. In Semantics-Directed Compiler Generation, pages 211--258, 1980.
22. N. Sahavechaphan and K. Claypool. Xsnippet: mining for sample code. In OOPSLA, 2006. ISBN 1--59593--348--4.
23. A. Solar-Lezama, G. Arnold, L. Tancau, R. Bodík, V. A. Saraswat, and S. A. Seshia. Sketching stencils. In PLDI, 2007.
24. R. Statman. Intuitionistic propositional logic is polynomial-space complete. Theoretical Computer Science, 9 (1): 67 -- 72, 1979.
25. heorem Prover()}DjinnThe Djinn Theorem Prover. http://www.augustsson.net/Darcs/Djinn/.
26. The Eclipse Foundation. http://www.eclipse.org/.
27. S. Thummalapenta and T. Xie. PARSEWeb: a programmer assistant for reusing open source code on the web. In ASE, 2007.
28. P. Urzyczyn. Inhabitation in typed lambda-calculi (a syntactic approach). In TLCA, 1997.
29. J. B. Wells and B. Yakobowski. Graph-based proof counting and enumeration with applications for program fragment synthesis. In LOPSTR, pages 262--277, 2004.

Index Terms

• Software and its engineering

  • Software notations and tools

    • Development frameworks and environments