Sometimes it is useful to enumerate in increasing order programs that have a given type. A simple example is test generation for compilers: we want to test a new optimising phase and are interested in generating programs that trigger that phase (we use types for this purpose). Since we want to find 'minimal' examples exhibiting bugs in the new optimising phase, it makes sense to start with the smallest programs as test cases first. Another (somewhat trivial) example is superoptimising compilation where we enumerate all possible assembly programs by increasing length. The typing system is trivial in the sense that all assembly programs are admissible.
There is a trivial algorithm solving this problem: lazily enumerate all untyped programs and do type inference on each, reject those that fail to type. The trivial algorithm is unlikely to be efficient since for reasonable typing systems, most programs don't have the target type. Surely one can do better by interspersing typing and enumeration. Let's express this problem in a more abstract setting.
Assume fixed an untyped programming language $L$ and a well-founded partial-order (or preorder) $\sqsubseteq$ on $L$ programs. We are also given a typing system for $L$. We write $\Gamma \vdash P : \tau$ to indicate that program $P$ has type $\tau$ assuming $P$'s free variables are typed as described in the typing environment $\Gamma$.
Problem. Given a typing environment $\Gamma$ and a type $\tau$, (lazily) enumerate (in increasing $\sqsubseteq$-order) all programs $P$ such that $\Gamma \vdash P : \tau$.
Note that my formulation of the problem has been deliberately vague, for it's likely that a lot depends on $\sqsubseteq$ and the typing system. Most orders $\sqsubseteq$ will be too complicated to admit efficient algorithms, I imagine. The orders I have in mind are program size, or weighted program size (some program constructors are 'heavier' than others).
Question. What is the state-of-the-art of research on efficient algorithms for such (and related) problems?
Update 23 June 2023. Following up on the answers to this question here and CLA 2017, which I enjoyed a great deal, I have looked into this problem much more and recently, we have been able to do program enumeration to GPUs, currently only for regular expressions, but the technique generalises:
- Search-Based Regular Expression Inference on a GPU (joint work with M. Valizadeh).
This does not change any asymptotic bounds, but, in practise, allows us to synthesise several orders of magnitude faster. This might be of interest for experimentation.