License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ECOOP.2023.4
URN: urn:nbn:de:0030-drops-181974
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18197/
Go to the corresponding LIPIcs Volume Portal

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

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

pdf-format:
LIPIcs-ECOOP-2023-4.pdf (1 MB)

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.

BibTeX - Entry

@InProceedings{botelhoguerra_et_al:LIPIcs.ECOOP.2023.4,
  author =	{Botelho Guerra, Henrique and Ferreira, Jo\~{a}o F. and Costa Seco, Jo\~{a}o},
  title =	{{Hoogle⋆: Constants and \lambda-abstractions in Petri-net-based Synthesis using Symbolic Execution}},
  booktitle =	{37th European Conference on Object-Oriented Programming (ECOOP 2023)},
  pages =	{4:1--4:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-281-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{263},
  editor =	{Ali, Karim and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2023/18197},
  URN =		{urn:nbn:de:0030-drops-181974},
  doi =		{10.4230/LIPIcs.ECOOP.2023.4},
  annote =	{Keywords: Type-directed, component-based, program synthesis, symbolic execution, unification, Haskell}
}

Keywords: Type-directed, component-based, program synthesis, symbolic execution, unification, Haskell
Collection: 37th European Conference on Object-Oriented Programming (ECOOP 2023)
Issue Date: 2023
Date of publication: 11.07.2023
Supplementary Material: Software (ECOOP 2023 Artifact Evaluation approved artifact): https://doi.org/10.4230/DARTS.9.2.20

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI