Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Example-Based Reasoning about the Realizability of Polymorphic Programs

Niek Mulleners, Johan Jeuring, Bastiaan Heeren

TL;DR

This work presents a pipeline to automatically decide the realizability of polymorphic programs specified by types, input-output examples, and sketches. It leverages parametricity by translating polymorphic functions into container morphisms, then encodes the resulting shape and position constraints into SMT for decision procedures. The approach is instantiated for map and foldr to demonstrate how example propagation and trace information can support reasoning about higher-order combinators and recursion schemes, including a notion of shape completeness to ensure decidability. Empirically, the method shows favorable running times on many cases and highlights the importance of efficient container representations for practical synthesis pruning and analysis. The work lays a foundation for integrating unrealizability reasoning into synthesis pipelines and sketches future extensions to richer data types and sketching languages.

Abstract

Parametricity states that polymorphic functions behave the same regardless of how they are instantiated. When developing polymorphic programs, Wadler's free theorems can serve as free specifications, which can turn otherwise partial specifications into total ones, and can make otherwise realizable specifications unrealizable. This is of particular interest to the field of program synthesis, where the unrealizability of a specification can be used to prune the search space. In this paper, we focus on the interaction between parametricity, input-output examples, and sketches. Unfortunately, free theorems introduce universally quantified functions that make automated reasoning difficult. Container morphisms provide an alternative representation for polymorphic functions that captures parametricity in a more manageable way. By using a translation to the container setting, we show how reasoning about the realizability of polymorphic programs with input-output examples can be automated.

Example-Based Reasoning about the Realizability of Polymorphic Programs

TL;DR

This work presents a pipeline to automatically decide the realizability of polymorphic programs specified by types, input-output examples, and sketches. It leverages parametricity by translating polymorphic functions into container morphisms, then encodes the resulting shape and position constraints into SMT for decision procedures. The approach is instantiated for map and foldr to demonstrate how example propagation and trace information can support reasoning about higher-order combinators and recursion schemes, including a notion of shape completeness to ensure decidability. Empirically, the method shows favorable running times on many cases and highlights the importance of efficient container representations for practical synthesis pruning and analysis. The work lays a foundation for integrating unrealizability reasoning into synthesis pipelines and sketches future extensions to richer data types and sketching languages.

Abstract

Parametricity states that polymorphic functions behave the same regardless of how they are instantiated. When developing polymorphic programs, Wadler's free theorems can serve as free specifications, which can turn otherwise partial specifications into total ones, and can make otherwise realizable specifications unrealizable. This is of particular interest to the field of program synthesis, where the unrealizability of a specification can be used to prune the search space. In this paper, we focus on the interaction between parametricity, input-output examples, and sketches. Unfortunately, free theorems introduce universally quantified functions that make automated reasoning difficult. Container morphisms provide an alternative representation for polymorphic functions that captures parametricity in a more manageable way. By using a translation to the container setting, we show how reasoning about the realizability of polymorphic programs with input-output examples can be automated.
Paper Structure (30 sections, 23 equations, 5 figures, 1 table)

This paper contains 30 sections, 23 equations, 5 figures, 1 table.

Table of Contents

  1. Introduction
  2. Background: Containers
  3. Constructing Containers
  4. Container Morphisms
  5. Small Containers
  6. Realizability of Input-Output Examples with Polymorphic Types
  7. Translating a Single Example
  8. Example: Reverse as Map
  9. Translating Multiple Examples
  10. Sketching with Map
  11. Reasoning About Recursion Schemes
  12. Realizability of Tail
  13. Sketching with Foldr
  14. A Note on Scoping
  15. Evaluation
  16. ...and 15 more sections

Figures (5)

  • Figure 1: A specification for the function reverse.
  • Figure 2: $\mathcal{T}$ is the set of programs of type $\tau$. $\mathcal{E}$ is the set of programs implementing the examples $\varepsilon$. $\mathcal{S}$ is the set of programs refining the sketch $\varsigma$.
  • Figure 3: Specifications that are unrealizable.
  • Figure 4: The pipeline for computing the realizability of a polymorphic program defined as a map with a single input-output example.
  • Figure 5: The pipeline for computing the realizability of a polymorphic program defined as a fold with a single input-output example.

Theorems & Definitions (3)

  • Definition 1
  • Definition 2
  • Definition 3