Document Open Access Logo

Hoogle⋆: Constants and λ-abstractions in Petri-net-based Synthesis using Symbolic Execution

Authors Henrique Botelho Guerra , João F. Ferreira , João Costa Seco

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2023.4.pdf
  • Filesize: 1.01 MB
  • 28 pages

Document Identifiers

Author Details

Henrique Botelho Guerra
  • INESC-ID and IST, University of Lisbon, Portugal
João F. Ferreira
  • INESC-ID and IST, University of Lisbon, Portugal
João Costa Seco
  • NOVA LINCS, NOVA School of Science and Technology, Caparica, Portugal

Funding

FCT UIDB/04516/2020, FCT UIDB/50021/2020, and ANI Lisboa-01-0247-Feder-045917.

Acknowledgements

We want to thank to the anonymous reviewers, for the constructive feedback.

Cite AsGet BibTex

Henrique Botelho Guerra, João F. Ferreira, and João Costa Seco. Hoogle⋆: Constants and λ-abstractions in Petri-net-based Synthesis using Symbolic Execution. In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 4:1-4:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ECOOP.2023.4

Abstract

Type-directed component-based program synthesis is the task of automatically building a function with applications of available components and whose type matches a given goal type. Existing approaches to component-based synthesis, based on classical proof search, cannot deal with large sets of components. Recently, Hoogle+, a component-based synthesizer for Haskell, overcomes this issue by reducing the search problem to a Petri-net reachability problem. However, Hoogle+ cannot synthesize constants nor λ-abstractions, which limits the problems that it can solve. We present Hoogle⋆, an extension to Hoogle+ that brings constants and λ-abstractions to the search space, in two independent steps. First, we introduce the notion of wildcard component, a component that matches all types. This enables the algorithm to produce incomplete functions, i.e., functions containing occurrences of the wildcard component. Second, we complete those functions, by replacing each occurrence with constants or custom-defined λ-abstractions. We have chosen to find constants by means of an inference algorithm: we present a new unification algorithm based on symbolic execution that uses the input-output examples supplied by the user to compute substitutions for the occurrences of the wildcard. When compared to Hoogle+, Hoogle⋆ can solve more kinds of problems, especially problems that require the generation of constants and λ-abstractions, without performance degradation.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Automatic programming
  • Theory of computation → Automated reasoning
Keywords
  • Type-directed
  • component-based
  • program synthesis
  • symbolic execution
  • unification
  • Haskell

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Lenart Augusstson. Djinn. URL: https://github.com/augustss/djinn.
  2. Franz Baader. Unification theory. In Klaus U. Schulz, editor, Word Equations and Related Topics, First International Workshop, IWWERT '90, Tübingen, Germany, October 1-3, 1990, Proceedings, volume 572 of Lecture Notes in Computer Science, pages 151-170. Springer, 1990. URL: https://doi.org/10.1007/3-540-55124-7_5.
  3. Roberto Baldoni, Emilio Coppa, Daniele Cono D'Elia, Camil Demetrescu, and Irene Finocchi. A survey of symbolic execution techniques. ACM Comput. Surv., 51(3):50:1-50:39, 2018. URL: https://doi.org/10.1145/3182657.
  4. João Costa Seco, Jonathan Aldrich, Luís Carvalho, Bernardo Toninho, and Carla Ferreira. Derivations with holes for concept-based program synthesis. In Proceedings of the 2022 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, Onward! 2022, pages 63-79, New York, NY, USA, 2022. Association for Computing Machinery. URL: https://doi.org/10.1145/3563835.3567658.
  5. Cristina David and Daniel Kroening. Program synthesis: challenges and opportunities. Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences, 375(2104):20150403, 2017. URL: https://doi.org/10.1098/rsta.2015.0403.
  6. Daniel J. Dougherty and Patricia Johann. An improved general e-unification method. J. Symb. Comput., 14(4):303-320, 1992. URL: https://doi.org/10.1016/0747-7171(92)90010-2.
  7. Yu Feng, Ruben Martins, Yuepeng Wang, Isil Dillig, and Thomas W. Reps. Component-based synthesis for complex apis. In Giuseppe Castagna and Andrew D. Gordon, editors, Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, pages 599-612. ACM, 2017. URL: https://doi.org/10.1145/3009837.3009851.
  8. Jean H. Gallier and Wayne Snyder. A general complete E-unification procedure. In Pierre Lescanne, editor, Rewriting Techniques and Applications, 2nd International Conference, RTA-87, Bordeaux, France, May 25-27, 1987, Proceedings, volume 256 of Lecture Notes in Computer Science, pages 216-227. Springer, 1987. URL: https://doi.org/10.1007/3-540-17220-3_19.
  9. Matthías Páll Gissurarson. Suggesting valid hole fits for typed-holes (experience report). In Nicolas Wu, editor, Proceedings of the 11th ACM SIGPLAN International Symposium on Haskell, Haskell@ICFP 2018, St. Louis, MO, USA, September 27-17, 2018, pages 179-185. ACM, 2018. URL: https://doi.org/10.1145/3242744.3242760.
  10. Matthías Páll Gissurarson, Leonhard Applis, Annibale Panichella, Arie van Deursen, and David Sands. PROPR: property-based automatic program repair. In 44th IEEE/ACM 44th International Conference on Software Engineering, ICSE 2022, Pittsburgh, PA, USA, May 25-27, 2022, pages 1768-1780. ACM, 2022. URL: https://doi.org/10.1145/3510003.3510620.
  11. Sumit Gulwani. Dimensions in program synthesis. In Temur Kutsia, Wolfgang Schreiner, and Maribel Fernández, editors, Proceedings of the 12th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, July 26-28, 2010, Hagenberg, Austria, pages 13-24. ACM, 2010. URL: https://doi.org/10.1145/1836089.1836091.
  12. Sumit Gulwani, Oleksandr Polozov, and Rishabh Singh. Program synthesis. Found. Trends Program. Lang., 4(1-2):1-119, 2017. URL: https://doi.org/10.1561/2500000010.
  13. Zheng Guo, David Cao, Davin Tjong, Jean Yang, Cole Schlesinger, and Nadia Polikarpova. Type-directed program synthesis for restful apis. In Ranjit Jhala and Isil Dillig, editors, PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13 - 17, 2022, pages 122-136. ACM, 2022. URL: https://doi.org/10.1145/3519939.3523450.
  14. Zheng Guo, Michael James, David Justo, Jiaxiao Zhou, Ziteng Wang, Ranjit Jhala, and Nadia Polikarpova. Program synthesis by type-guided abstraction refinement. Proc. ACM Program. Lang., 4(POPL):12:1-12:28, 2020. URL: https://doi.org/10.1145/3371080.
  15. Tihomir Gvero, Viktor Kuncak, Ivan Kuraj, and Ruzica Piskac. Complete completion using types and weights. In Hans-Juergen Boehm and Cormac Flanagan, editors, ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '13, Seattle, WA, USA, June 16-19, 2013, pages 27-38. ACM, 2013. URL: https://doi.org/10.1145/2491956.2462192.
  16. William T. Hallahan, Anton Xue, Maxwell Troy Bland, Ranjit Jhala, and Ruzica Piskac. Lazy counterfactual symbolic execution. In Kathryn S. McKinley and Kathleen Fisher, editors, Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2019, Phoenix, AZ, USA, June 22-26, 2019, pages 411-424. ACM, 2019. URL: https://doi.org/10.1145/3314221.3314618.
  17. William T. Hallahan, Anton Xue, and Ruzica Piskac. G2Q: haskell constraint solving. In Richard A. Eisenberg, editor, Proceedings of the 12th ACM SIGPLAN International Symposium on Haskell, Haskell@ICFP 2019, Berlin, Germany, August 18-23, 2019, pages 44-57. ACM, 2019. URL: https://doi.org/10.1145/3331545.3342590.
  18. Paul Hudak and Joseph H. Fasel. A gentle introduction to haskell. ACM SIGPLAN Notices, 27(5):1, 1992. URL: https://doi.org/10.1145/130697.130698.
  19. Gérard P. Huet. A unification algorithm for typed lambda-calculus. Theor. Comput. Sci., 1(1):27-57, 1975. URL: https://doi.org/10.1016/0304-3975(75)90011-0.
  20. Michael B. James, Zheng Guo, Ziteng Wang, Shivani Doshi, Hila Peleg, Ranjit Jhala, and Nadia Polikarpova. Digging for fold: synthesis-aided API discovery for haskell. Proc. ACM Program. Lang., 4(OOPSLA):205:1-205:27, 2020. URL: https://doi.org/10.1145/3428273.
  21. SL Peyton Jones, Cordy Hall, Kevin Hammond, Will Partain, and Philip Wadler. The glasgow haskell compiler: a technical overview. In Proc. UK Joint Framework for Information Technology (JFIT) Technical Conference, volume 93, 1993. Google Scholar
  22. John C. Kolesar, Ruzica Piskac, and William T. Hallahan. Checking equivalence in a non-strict language. Proc. ACM Program. Lang., 6(OOPSLA2):1469-1496, 2022. URL: https://doi.org/10.1145/3563340.
  23. James Koppel, Zheng Guo, Edsko de Vries, Armando Solar-Lezama, and Nadia Polikarpova. Searching entangled program spaces. Proc. ACM Program. Lang., 6(ICFP):23-51, 2022. URL: https://doi.org/10.1145/3547622.
  24. Justin Lubin, Nick Collins, Cyrus Omar, and Ravi Chugh. Program sketching with live bidirectional evaluation. Proc. ACM Program. Lang., 4(ICFP):109:1-109:29, 2020. URL: https://doi.org/10.1145/3408991.
  25. David Mandelin, Lin Xu, Rastislav Bodík, and Doug Kimelman. Jungloid mining: helping to navigate the API jungle. In Vivek Sarkar and Mary W. Hall, editors, Proceedings of the ACM SIGPLAN 2005 Conference on Programming Language Design and Implementation, Chicago, IL, USA, June 12-15, 2005, pages 48-61. ACM, 2005. URL: https://doi.org/10.1145/1065010.1065018.
  26. Neil Mitchel. Hoogle. URL: https://hoogle.haskell.org/.
  27. Niek Mulleners, Johan Jeuring, and Bastiaan Heeren. Program synthesis using example propagation. CoRR, abs/2210.13873, 2022. URL: https://doi.org/10.48550/arXiv.2210.13873.
  28. Niek Mulleners, Johan Jeuring, and Bastiaan Heeren. Scrybe. https://github.com/NiekM/scrybe, 2022.
  29. Phuc C. Nguyen, Sam Tobin-Hochstadt, and David Van Horn. Higher order symbolic execution for contract verification and refutation. J. Funct. Program., 27:e3, 2017. URL: https://doi.org/10.1017/S0956796816000216.
  30. Ulf Norell. Dependently typed programming in agda. In Pieter W. M. Koopman, Rinus Plasmeijer, and S. Doaitse Swierstra, editors, Advanced Functional Programming, 6th International School, AFP 2008, Heijen, The Netherlands, May 2008, Revised Lectures, volume 5832 of Lecture Notes in Computer Science, pages 230-266. Springer, 2008. URL: https://doi.org/10.1007/978-3-642-04652-0_5.
  31. Peter-Michael Osera and Steve Zdancewic. Type-and-example-directed program synthesis. In David Grove and Stephen M. Blackburn, editors, Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, June 15-17, 2015, pages 619-630. ACM, 2015. URL: https://doi.org/10.1145/2737924.2738007.
  32. Daniel Perelman, Sumit Gulwani, Thomas Ball, and Dan Grossman. Type-directed completion of partial expressions. In Jan Vitek, Haibo Lin, and Frank Tip, editors, ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '12, Beijing, China - June 11 - 16, 2012, pages 275-286. ACM, 2012. URL: https://doi.org/10.1145/2254064.2254098.
  33. John Peterson and Mark P. Jones. Implementing type classes. In Robert Cartwright, editor, Proceedings of the ACM SIGPLAN'93 Conference on Programming Language Design and Implementation (PLDI), Albuquerque, New Mexico, USA, June 23-25, 1993, pages 227-236. ACM, 1993. URL: https://doi.org/10.1145/155090.155112.
  34. Veselin Raychev, Martin T. Vechev, and Eran Yahav. Code completion with statistical language models. In Michael F. P. O'Boyle and Keshav Pingali, editors, ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '14, Edinburgh, United Kingdom - June 09 - 11, 2014, pages 419-428. ACM, 2014. URL: https://doi.org/10.1145/2594291.2594321.
  35. Jörg H. Siekmann. Unification theory. J. Symb. Comput., 7(3/4):207-274, 1989. URL: https://doi.org/10.1016/S0747-7171(89)80012-4.
  36. Armando Solar-Lezama. Program sketching. Int. J. Softw. Tools Technol. Transf., 15(5-6):475-495, 2013. URL: https://doi.org/10.1007/s10009-012-0249-7.
  37. Emina Torlak and Rastislav Bodík. Growing solver-aided languages with rosette. In Antony L. Hosking, Patrick Th. Eugster, and Robert Hirschfeld, editors, ACM Symposium on New Ideas in Programming and Reflections on Software, Onward! 2013, part of SPLASH '13, Indianapolis, IN, USA, October 26-31, 2013, pages 135-152. ACM, 2013. URL: https://doi.org/10.1145/2509578.2509586.
  38. Darya Verzhbinsky and Daniel Wang. Petsy: Polymorphic enumerative type-guided synthesis. POPL 2021 Student Research Competition, 2021. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact