pith. sign in

arxiv: 1907.03105 · v1 · pith:IEK24TXJnew · submitted 2019-07-06 · 💻 cs.PL

Constraint-Based Type-Directed Program Synthesis

Peter-Michael Osera This is my paper

Pith reviewed 2026-05-25 01:39 UTC · model grok-4.3

classification 💻 cs.PL
keywords type-directed program synthesisconstraint-based type inferencepolymorphismGADTsHaskellprogram synthesis
0
0 comments X

The pith

Rooting type-directed synthesis in constraint-based type inference allows more efficient synthesis of polymorphic code and support for GADTs.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper sets out to show that constraint-based type inference methods can be used as the foundation for type-directed program synthesis. This would let synthesis tools produce polymorphic programs more efficiently while also handling advanced type features such as GADTs. A reader would care because most current synthesis approaches either avoid polymorphism or scale poorly when types grow complex, limiting their use in languages like Haskell.

Core claim

The paper claims that by adapting the constraint generation and solving steps from ordinary type inference to the task of searching for program terms, type-directed synthesis can handle polymorphic code more efficiently and can be extended to features like GADTs that depend on polymorphism, with the approach realized in the Scythe prototype for Haskell.

What carries the argument

Constraint-based type inference techniques, which generate and solve type constraints to infer types, repurposed to direct the search for well-typed terms during synthesis.

If this is right

  • Polymorphic functions can be synthesized without the usual blow-up in search space.
  • GADTs and other polymorphism-dependent features become reachable targets for synthesis.
  • A live programming tool for Haskell can incorporate these techniques directly.
  • The same constraint machinery used by the type checker can guide term construction.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same constraint adaptation might be tried in other languages whose type systems already rely on constraint solvers.
  • Integration with existing type checkers could reduce duplication between checking and synthesis.
  • The approach might scale to larger programs if the constraint solver is already optimized for the language.

Load-bearing premise

That the same constraint techniques used for type inference can be transferred to synthesis without creating new soundness problems or losing the efficiency gains when polymorphism and GADTs are involved.

What would settle it

A concrete polymorphic program or GADT-using example that the constraint-based synthesizer either cannot produce or produces more slowly than a non-constraint synthesis method.

Figures

Figures reproduced from arXiv: 1907.03105 by Peter-Michael Osera.

Figure 1
Figure 1. Figure 1: Basic syntax of the object language. Current systems that handle polymorphic synthesis simply enumerate and explore all the possible types that can be created from the context. However, this may lead to an excessive exploration of type combinations that do not work, e.g., choosing a to be Int but not having any functions of type Int -> Bool available in the context. Furthermore, it may lead to repeated che… view at source ↗
Figure 2
Figure 2. Figure 2: Type inference system. Polymorphic types interact with the inference system in two ways. The first is let-generalization which occurs at top-level bindings f = e. After generating constraints C for the body of the binding, we solve them using a standard unification algorithm to find a type substitution θ for each of the unification variables found in C (infer-bind). Those unification variables with no subs… view at source ↗
Figure 3
Figure 3. Figure 3: Syntactic extensions for type-and-example-directed program synthesis. [PITH_FULL_IMAGE:figures/full_fig_p006_3.png] view at source ↗
Figure 4
Figure 4. Figure 4: Type-and-example program synthesis rules. [PITH_FULL_IMAGE:figures/full_fig_p007_4.png] view at source ↗
Figure 5
Figure 5. Figure 5: Auxiliary definitions for the synthesis system. [PITH_FULL_IMAGE:figures/full_fig_p008_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Example generation derivation of map. to a choice of a complete instantiation of a type scheme upfront (which requires us to systematically search the space of possible types), we infer the instantiation as we generate the complete term. If type-and-example-directed program synthesis captures the idea of “evaluating during enumera￾tion” [19], then our approach of integrating type inference into the term ge… view at source ↗
Figure 7
Figure 7. Figure 7: Syntactic extensions for GADT synthesis. [PITH_FULL_IMAGE:figures/full_fig_p012_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Extensions to synthesis system for GADTs. [PITH_FULL_IMAGE:figures/full_fig_p013_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: Example Scythe runs for stutter and append contrast to the shallower search that GHC’s hole-filling mechanism conducts which only suggests s1 as a valid completion.6 It might be the case that some polymorphic function of interest is too complicated to be specified with examples. This example shows that synthesis techniques like those used by Scythe still have the potential to provide meaningful feedback, e… view at source ↗
Figure 10
Figure 10. Figure 10: The complete system: syntax. e ≡β v iff e −→∗ v λx:τ . e ≡β v ⇒ χ iff (λx:τ . e) v ≡β χ . W | K e = {S → χ ∈ W | Se −→∗ K v1 · · · vk } unify(C) = θ (standard unification algorithm) C ⊨ C ′ iff ∀τ ∼ τ ′ ∈ C ′ . θτ = θτ ′whereunify(C) = θ . consistent(C) iff ∃θ . unify(C) = θ [PITH_FULL_IMAGE:figures/full_fig_p025_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: The complete system: auxiliary synthesis definitions. [PITH_FULL_IMAGE:figures/full_fig_p025_11.png] view at source ↗
Figure 12
Figure 12. Figure 12: The complete system: typechecking [PITH_FULL_IMAGE:figures/full_fig_p026_12.png] view at source ↗
Figure 13
Figure 13. Figure 13: The complete system: synthesis semantics. [PITH_FULL_IMAGE:figures/full_fig_p027_13.png] view at source ↗
read the original abstract

We explore an approach to type-directed program synthesis rooted in constraint-based type inference techniques. By doing this, we aim to more efficiently synthesize polymorphic code while also tackling advanced typing features such as GADTs that build upon polymorphism. Along the way, we also present an implementation of these techniques in Scythe, a prototype live, type-directed programming tool for the Haskell programming language and reflect on our initial experience with the tool.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper explores rooting type-directed program synthesis in constraint-based type inference (e.g., HM(X)-style solvers) to more efficiently synthesize polymorphic code and support advanced features such as GADTs. It presents a prototype implementation of these ideas in Scythe, a live type-directed programming tool for Haskell, together with reflections on initial experience using the tool.

Significance. If the transfer of constraint techniques succeeds in practice, the work could improve the scalability of type-directed synthesis for languages with rich polymorphism and GADTs by reusing existing, optimized solvers rather than building custom ones. The concrete Scythe artifact and experience report provide a useful starting point for tool builders, though the absence of formal transfer theorems or controlled experiments limits the strength of the efficiency claims.

major comments (2)
  1. [§4, §5] §4 (Implementation) and §5 (Experience): the central efficiency claim for polymorphic synthesis is not supported by any quantitative measurements, timing data, or comparisons against prior synthesizers; without such data the claim that constraint-based inference yields efficiency gains remains untested in the manuscript.
  2. [§3] §3 (Approach): while the text describes adapting constraint generation and solving for synthesis, no soundness or completeness argument is supplied for the GADT case; the manuscript therefore does not establish that the adaptation preserves the guarantees needed for the claimed feature support.
minor comments (2)
  1. [Abstract, §1] The abstract and introduction use the phrase 'more efficiently' without defining a baseline; a short paragraph clarifying the intended comparison (e.g., to unification-based synthesis) would help readers.
  2. [§3] Notation for the constraint language is introduced informally; adding a small table or grammar fragment would improve readability for readers unfamiliar with HM(X).

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their constructive feedback on our manuscript. We address the two major comments below, acknowledging the points raised regarding evaluation and formal arguments.

read point-by-point responses

  1. Referee: [§4, §5] §4 (Implementation) and §5 (Experience): the central efficiency claim for polymorphic synthesis is not supported by any quantitative measurements, timing data, or comparisons against prior synthesizers; without such data the claim that constraint-based inference yields efficiency gains remains untested in the manuscript.

    Authors: We agree that no quantitative data is presented to support efficiency gains. The paper's focus is on the approach and the Scythe prototype as an experience report. The efficiency benefit is argued at a high level by reusing existing solvers. We will revise the manuscript to clarify that efficiency claims are preliminary and not empirically validated in this work, and discuss this as a direction for future evaluation. revision: partial

  2. Referee: [§3] §3 (Approach): while the text describes adapting constraint generation and solving for synthesis, no soundness or completeness argument is supplied for the GADT case; the manuscript therefore does not establish that the adaptation preserves the guarantees needed for the claimed feature support.

    Authors: We acknowledge the absence of a formal soundness or completeness argument for the GADT extension. The description in §3 adapts standard techniques from constraint-based type inference for GADTs, but without providing proofs specific to the synthesis context. In a revised version, we will update §3 to explicitly note the lack of formal guarantees and position this as an area for further theoretical development. revision: yes

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper is an exploratory description of adapting constraint-based type inference (HM(X)-style) to type-directed synthesis, implemented in the Scythe prototype for Haskell. It presents no equations, fitted parameters, predictions, or formal derivation chain that could reduce to self-definition or self-citation. The central contribution is a practical implementation approach and experience reflection rather than a theorem or quantitative claim whose validity depends on internal fitting or prior self-citations. No load-bearing steps match any of the enumerated circularity patterns.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

No technical details, equations, or assumptions are supplied in the abstract, so the ledger cannot enumerate specific free parameters, axioms, or invented entities.

pith-pipeline@v0.9.0 · 5574 in / 1098 out tokens · 21312 ms · 2026-05-25T01:39:47.457645+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

26 extracted references · 26 canonical work pages

  1. [1]

    Lennart Augustsson. 2004. [Haskell] Announcing Djinn, Version 2004-12-11, a Coding Wizard

    work page 2004

  2. [2]

    Frédéric Bour, Thomas Refis, and Gabriel Scherer. 2018. Merlin: A Language Server for OCaml (Experience Report). Proceedings of the ACM on Programming Languages 2, ICFP (July 2018), 103:1–103:15. https://doi.org/10.1145/3236798

    work page doi:10.1145/3236798 2018

  3. [3]

    Sheng Chen and Martin Erwig. 2016. Principal Type Inference for GADTs. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016) . ACM Press, St. Petersburg, FL, USA, 416–428. https://doi.org/10.1145/2837614.2837665

    work page doi:10.1145/2837614.2837665 2016

  4. [4]

    Yu Feng, Ruben Martins, Yuepeng Wang, Isil Dillig, and Thomas W. Reps. 2017. Component-Based Synthesis for Complex APIs. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017). ACM Press, Paris, France, 599–612. https://doi.org/10.1145/3009837.3009851

    work page doi:10.1145/3009837.3009851 2017

  5. [5]

    Feser, Swarat Chaudhuri, and Isil Dillig

    John K. Feser, Swarat Chaudhuri, and Isil Dillig. 2015. Synthesizing Data Structure Transformations from Input-Output Examples. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2015). ACM Press, Portland, OR, USA, 229–239. https://doi.org/10.1145/2737924.2737977

    work page doi:10.1145/2737924.2737977 2015

  6. [6]

    Jonathan Frankle, Peter-Michael Osera, David Walker, and Steve Zdancewic. 2016. Example-Directed Synthesis: A Type-Theoretic Interpretation. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016) . ACM, St. Petersburg, FL, USA. https://doi.org/10.1145/2914770.2837629 20 Peter-Michael Osera

    work page doi:10.1145/2914770.2837629 2016

  7. [7]

    Matthías Páll Gissurarson. 2018. Suggesting Valid Hole Fits for Typed-Holes (Experience Report). In Proceedings of the 11th ACM SIGPLAN International Symposium on Haskell (Haskell 2018) . ACM Press, St. Louis, MO, USA, 179–185. https://doi.org/10.1145/3242744.3242760

    work page doi:10.1145/3242744.3242760 2018

  8. [8]

    Sumit Gulwani, Oleksandr Polozov, and Rishabh Singh. 2017. Program Synthesis. Foundations and Trends in Program- ming Languages 4, 1-2 (2017), 1–119. https://doi.org/10.1561/2500000010

    work page doi:10.1561/2500000010 2017

  9. [9]

    Tihomir Gvero, Viktor Kuncak, Ivan Kuraj, and Ruzica Piskac. 2013. Complete Completion Using Types and Weights. In Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2013) , Vol. 48. ACM Press, New York, NY, USA, 27–38. https://doi.org/10.1145/2499370.2462192

    work page doi:10.1145/2499370.2462192 2013

  10. [10]

    Mark P. Jones. 1995. Functional Programming with Overloading and Higher-Order Polymorphism. In Advanced Functional Programming, First International Spring School on Advanced Functional Programming Techniques-Tutorial Text. Springer-Verlag, Berlin, Heidelberg, 97–136

    work page 1995

  11. [11]

    Georgios Karachalias, Tom Schrijvers, Dimitrios Vytiniotis, and Simon Peyton Jones. 2015. GADTs Meet Their Match: Pattern-Matching Warnings That Account for GADTs, Guards, and Laziness. InProceedings of the 20th ACM SIGPLAN International Conference on Functional Programming (ICFP 2015). ACM Press, Vancouver, BC, Canada, 424–436. https://doi.org/10.1145/27...

    work page doi:10.1145/2784731.2784748 2015

  12. [12]

    Susumu Katayama. 2012. An Analytical Inductive Functional Programming System That Avoids Unintended Programs. In Proceedings of the ACM SIGPLAN 2012 Workshop on Partial Evaluation and Program Manipulation (PEPM 2012) . ACM Press, Philadelphia, Pennsylvania, USA, 43. https://doi.org/10.1145/2103746.2103758

    work page doi:10.1145/2103746.2103758 2012

  13. [13]

    Gabriela Moreira, Cristiano Vasconcellos, and Rodrigo Ribeiro. 2018. Type Inference for GADTs, Outsidein and Anti-Unification. In Proceedings of the XXII Brazilian Symposium on Programming Languages (SBLP 2018) . ACM Press, Sao Carlos, Brazil, 51–58. https://doi.org/10.1145/3264637.3264644

    work page doi:10.1145/3264637.3264644 2018

  14. [14]

    Martin Odersky, Martin Sulzmann, and Martin Wehr. 1999. Type Inference with Constrained Types.Theory and Practice of Object Systems 5, 1 (Jan. 1999), 35–55. https://doi.org/10.1002/(SICI)1096-9942(199901/03)5:1<35::AID-TAPO4>3.0. CO;2-4

    work page doi:10.1002/(sici)1096-9942(199901/03)5:1 1999

  15. [15]

    Cyrus Omar, Ian Voysey, Ravi Chugh, and Matthew A. Hammer. 2019. Live Functional Programming with Typed Holes. Proceedings of the ACM on Programming Languages 3, POPL (Jan. 2019), 1–32. https://doi.org/10.1145/3290327

    work page doi:10.1145/3290327 2019

  16. [16]

    Cyrus Omar, Ian Voysey, Michael Hilton, Jonathan Aldrich, and Matthew A. Hammer. 2017. Hazelnut: A Bidirectionally Typed Structure Editor Calculus. In Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2017). ACM Press, Paris, France, 86–99. https://doi.org/10.1145/3009837.3009900

    work page doi:10.1145/3009837.3009900 2017

  17. [17]

    Peter-Michael Osera. 2015. Program Synthesis with Types. PhD Thesis. University of Pennsylvania, Philadelphia, PA

    work page 2015

  18. [18]

    Peter-Michael Osera. 2019. Constraint-Based Type-Directed Program Synthesis. In The 4th Workshop on Type-Driven Development (TyDe 2019). ACM Press, Berlin, Germany

    work page 2019

  19. [19]

    Peter-Michael Osera and Steve Zdancewic. 2015. Type-and-Example-Directed Program Synthesis. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2015) . ACM Press, Portland, OR, USA, 619–630. https://doi.org/10.1145/2737924.2738007

    work page doi:10.1145/2737924.2738007 2015

  20. [20]

    Benjamin C. Pierce. 2002. Types and Programming Languages. MIT Press, Cambridge, MA

    work page 2002

  21. [21]

    Pierce and David N

    Benjamin C. Pierce and David N. Turner. 2000. Local Type Inference. ACM Transactions on Programming Languages and Systems 22, 1 (Jan. 2000), 1–44. https://doi.org/10.1145/345099.345100

    work page doi:10.1145/345099.345100 2000

  22. [22]

    Nadia Polikarpova, Ivan Kuraj, and Armando Solar-Lezama. 2016. Program Synthesis from Polymorphic Refinement Types. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2016). ACM Press, Santa Barbara, CA, USA, 522–538. https://doi.org/10.1145/2908080.2908093

    work page doi:10.1145/2908080.2908093 2016

  23. [23]

    Tom Schrijvers, Simon Peyton Jones, Martin Sulzmann, and Dimitrios Vytiniotis. 2009. Complete and Decidable Type Inference for GADTs. In Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming (ICFP 2009). ACM Press, Edinburgh, Scotland, 341. https://doi.org/10.1145/1596550.1596599

    work page doi:10.1145/1596550.1596599 2009

  24. [24]

    Vincent Simonet and François Pottier. 2007. A Constraint-Based Approach to Guarded Algebraic Data Types. ACM Transactions on Programming Languages and Systems 29, 1 (Jan. 2007), 1–es. https://doi.org/10.1145/1180475.1180476

    work page doi:10.1145/1180475.1180476 2007

  25. [25]

    Dimitrios Vytiniotis, Simon Peyton Jones, Tom Schrijvers, and Martin Sulzmann. 2011. OutsideIn(X) Modular Type Inference with Local Assumptions. Journal of Functional Programming 21, 4-5 (Sept. 2011), 333–412. https://doi.org/ 10.1017/S0956796811000098

    work page doi:10.1017/s0956796811000098 2011

  26. [26]

    Philip Wadler. 1989. Theorems for Free!. InProceedings of the Fourth International Conference on Functional Programming Languages and Computer Architecture (FPCA 1989) . ACM Press, Imperial College, London, United Kingdom, 347–359. https://doi.org/10.1145/99370.99404 Constraint-Based Type-Directed Program Synthesis 21 A THE FORMALISM A.1 The System We giv...

    work page doi:10.1145/99370.99404 1989