<p>For ordered enumeration instead of random generation you are getting into the realm of combinatorics. I don't know of any generic results, but this paper <a href="https://arxiv.org/abs/1210.2610" rel="nofollow noreferrer">Counting and Generating Lambda Terms</a> describes an enumeration of untyped terms and empirical data on the sieve approach to enumerating typed lambda terms. It looks like they use a hindley-milner type system so no annotations are needed.</p>

<p>On the other hand if you want to generate typed terms directly, there are libraries like SciFe (<a href="http://kaptoxic.github.io/SciFe/" rel="nofollow noreferrer">website</a>,<a href="http://dl.acm.org/citation.cfm?id=2814323" rel="nofollow noreferrer">paper</a>) and data/enumerate (<a href="https://docs.racket-lang.org/data/Enumerations.html" rel="nofollow noreferrer">docs</a>,<a href="https://github.com/maxsnew/Redex-Enum-Paper/blob/master/paper.pdf" rel="nofollow noreferrer">draft paper</a>) that support "dependent enumeration" where you enumerate one thing and then select what enumeration to use based on that (essentially enumeration of Sigma types), that is essential for enumerating typed terms in non-trivial languages.
Dependent enumeration isn't fast either, but it might be faster than a sieve.</p>

CC BY-SA 3.0
2017-03-21T23:27:33.540Z
The Grygiel / Lescanne paper uses the naive (=sieving) algorithm. I'm not familiar with dependent enumeration. I'll look into the the libraries.
Martin Berger
CC BY-SA 3.0
2017-03-22T09:48:48.943Z
I wonder how  "dependent enumeration" deals with really complicated enumeration, e.g. proofs of Fermat's Last Theorem.
Martin Berger
CC BY-SA 3.0
2017-03-22T14:33:05.153Z
Dependent enumeration is fastest when the dependent clause is always infinite (because you can do a diagonalization), if the dependent clause is finite it can be very slow, for instance if it is often empty it degenerates to a search procedure. This is detailed somewhat in the documentation for cons/de in data/enumerate, but there should probably be more. On the other hand, diagonalizing is fast, but doesn't give an ordering with a nice combinatorial interpretation.
Max New
CC BY-SA 3.0
2017-03-22T17:42:54.663Z
Is there a paper that describes dependent enumeration?
Martin Berger
CC BY-SA 3.0
2017-03-22T20:02:16.673Z
Yes, the papers for data/enumerate and SciFe both discuss it, I added links to my answer.
Max New
CC BY-SA 3.0
2017-03-21T18:53:36.653Z
2017-03-22T20:00:09.697Z
2017-03-22T20:00:09.697Z
Max New
<p>Two remarks first:</p>

<ol>
<li><p>I have used the "randomly generate terms and check that they are well-typed" approach (you mention that "untyped" terms are generated, you can also randomly generate terms in a Church-style grammar with explicit type annotations) and it worked very well in practice, it revealed all the bugs there was to find on this particular part of the project. For practical purposes I would recommend trying this first. (On the other hand, the generator was aware of scoping rules -- it maintained a set of currently bound variables for top-down generation, this is easy to implement.)</p></li>
<li><p>The choice of order depends <em>a lot</em> on the application you have in mind: two distinct applications will require different orders. For example, people that work on type-directed program synthesis are not usually interested in enumerating equivalent programs, so they will make simplification rules such as assuming that "any term of type A -> B can be chosen to start with a lambda-abstraction" -- in your framework, ordering lambda-terms before all terms at this type. This order is very bad for compiler testing: if you only generate programs that are in normal form, you are unlikely to exercise much of your optimization strategies or runtime semantics. So I believe that assuming an order to abstract away from the intended usage is not a good modeling choice: its choice is tightly coupled with the intended usage, and I would rather reason about the usage than the corresponding order.</p></li>
</ol>

<p>Now for some references.</p>

<p>For typed-term generation for testing purposes, you may be interested in "Making random judgments: Automatically generating well-typed terms from the definition of a type-system" by Burke Fetscher, Koen Claessen, Michał Pałka, John Hughes, and Robert Bruce Findler, 2015.</p>

<blockquote>
  <p>This paper presents a generic method for randomly generating well-
  typed expressions. It starts from a specification of a typing judgment in PLT Re-
  dex and uses a specialized solver that employs randomness to find many different
  valid derivations of the judgment form.<br>
  Our motivation for building these random terms is to more effectively falsify
  conjectures as part of the tool-support for semantics models specified in Redex.
  Accordingly, we evaluate the generator against the other available methods for
  Redex, as well as the best available custom well-typed term generator. Our results
  show that our new generator is much more effective than generation techniques
  that do not explicitly take types into account and is competitive with generation
  techniques that do, even though they are specialized to particular type-systems
  and ours is not.</p>
</blockquote>

<p>For typed term enumeration for program synthesis, two recent works that I know are <a href="http://www.cs.grinnell.edu/~osera/publications/frankle-popl-2016" rel="noreferrer">Example-Directed Synthesis: A Type-Theoretic Interpretation</a> by  Jonathan Frankle, Peter-Michael Osera, David Walker, and Steve Zdancewic, 2016, and <a href="http://people.csail.mit.edu/polikarn/publications/pldi16.pdf" rel="noreferrer">Program Synthesis from Polymorphic Refinement Types</a> by Nadia Polikarpova, Ivan Kuraj, and Armando Solar-Lezama, 2016. Note that both works use refinement types as a way to encode more desired properties of the searched program -- such as a testsuite that it should pass. These refinements often constrain the search space substantially more than just types, but they are also harder to invert -- interleave with search.</p>

CC BY-SA 3.0
2017-03-18T08:57:13.653Z
When you generate a-la-Church terms: do you generate type-annotations
randomly, or does the choice of type-annotation inform the generation
of the abstraction's body?
Martin Berger
CC BY-SA 3.0
2017-03-18T08:57:51.897Z
I was aware of the work on randomly generating programs such as Fetscher
et al. The key difference is that if you don't want a *uniform*
distribution (e.g. of programs of size $n$) you can just abandon a
search and backtrack if you are down a hopeless path. That's what
Fetscher et al do. But that's not possible in enumeration.
Martin Berger
CC BY-SA 3.0
2017-03-18T15:56:56.423Z
Re. random type-annotations generation, I just randomly generated annotations.
gasche
CC BY-SA 3.0
2017-03-18T16:05:39.140Z
One thing that I forgot to mention is the (natural) idea of writing an enumerator in a logic programming language. I am not sure that it would actually make it easier to push the type-system constraints into the generation (so it may be similar to naive random generation), but good Prolog implementation may support extra features to make it efficient, such as tabling. I have not tried myself.
gasche
CC BY-SA 3.0
2017-03-17T19:56:51.583Z
2017-03-17T19:56:51.583Z
gasche
<p> 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 <i>all</i> assembly programs are admissible.</p>
<p>  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, <i>most</i> 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.</p>
<p>
  Assume fixed an untyped programming language <span class="math-container">$L$</span> and a well-founded partial-order (or
  preorder) <span class="math-container">$\sqsubseteq$</span> on <span class="math-container">$L$</span> programs. We are also given a typing
  system for <span class="math-container">$L$</span>. We write <span class="math-container">$\Gamma \vdash P : \tau$</span> to indicate that
  program <span class="math-container">$P$</span> has type <span class="math-container">$\tau$</span> assuming <span class="math-container">$P$</span>'s free variables are typed
  as described in the typing environment <span class="math-container">$\Gamma$</span>. 
</p>
<p><b>Problem.</b>  Given a typing environment <span class="math-container">$\Gamma$</span>
  and a type <span class="math-container">$\tau$</span>, (lazily) enumerate (in increasing
  <span class="math-container">$\sqsubseteq$</span>-order) all programs <span class="math-container">$P$</span> such that <span class="math-container">$\Gamma \vdash P :
  \tau$</span>.
</p>
<p>
Note that my formulation of the problem has been deliberately vague,
  for it's likely that a lot depends on <span class="math-container">$\sqsubseteq$</span> and the typing
  system. Most orders <span class="math-container">$\sqsubseteq$</span> 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).
 </p>
<p><b>
    Question.</b> What is the state-of-the-art of research on efficient algorithms for
  such (and related) problems? 
</p>
<p><b>Update 23 June 2023.</b> 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:
<ul>
<li><a href="https://martinfriedrichberger.net/pldi2023.html" rel="nofollow noreferrer">Search-Based Regular Expression Inference on a GPU</a> (joint work with M. Valizadeh).</li>
</ul>
<p>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.</p>

CC BY-SA 3.0
2017-03-22T00:15:10.423Z
Come to the CLA 2017 workshop (https://cla.tcs.uj.edu.pl/) and find out! :-)
Noam Zeilberger
<reference-request><pl.programming-languages><type-systems><type-inference>
Efficiently ordering typed programs
Martin Berger
# Efficiently ordering typed programs

(Asked by: username_0 on 2017-03-17)

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](https://martinfriedrichberger.net/pldi2023.html) (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.

**Tags:** reference-request, pl.programming-languages, type-systems, type-inference
> **Comments:**
> **username_1**: Come to the CLA 2017 workshop (https://cla.tcs.uj.edu.pl/) and find out! :-)  

---

## 2 answers

### Answer by username_2 on 2017-03-21. Score: 6 | Accepted answer

For ordered enumeration instead of random generation you are getting into the realm of combinatorics. I don't know of any generic results, but this paper [Counting and Generating Lambda Terms](https://arxiv.org/abs/1210.2610) describes an enumeration of untyped terms and empirical data on the sieve approach to enumerating typed lambda terms. It looks like they use a hindley-milner type system so no annotations are needed.

On the other hand if you want to generate typed terms directly, there are libraries like SciFe ([website](http://kaptoxic.github.io/SciFe/),[paper](http://dl.acm.org/citation.cfm?id=2814323)) and data/enumerate ([docs](https://docs.racket-lang.org/data/Enumerations.html),[draft paper](https://github.com/maxsnew/Redex-Enum-Paper/blob/master/paper.pdf)) that support "dependent enumeration" where you enumerate one thing and then select what enumeration to use based on that (essentially enumeration of Sigma types), that is essential for enumerating typed terms in non-trivial languages.
Dependent enumeration isn't fast either, but it might be faster than a sieve.

> **Comments:**
> **username_0**: The Grygiel / Lescanne paper uses the naive (=sieving) algorithm. I'm not familiar with dependent enumeration. I'll look into the the libraries.  
> **username_0**: I wonder how  "dependent enumeration" deals with really complicated enumeration, e.g. proofs of Fermat's Last Theorem.  
> **username_2**: Dependent enumeration is fastest when the dependent clause is always infinite (because you can do a diagonalization), if the dependent clause is finite it can be very slow, for instance if it is often empty it degenerates to a search procedure. This is detailed somewhat in the documentation for cons/de in data/enumerate, but there should probably be more. On the other hand, diagonalizing is fast, but doesn't give an ordering with a nice combinatorial interpretation.  
> **username_0**: Is there a paper that describes dependent enumeration?  
> **username_2**: Yes, the papers for data/enumerate and SciFe both discuss it, I added links to my answer.  

---

### Answer by username_3 on 2017-03-17. Score: 6

Two remarks first:

1. I have used the "randomly generate terms and check that they are well-typed" approach (you mention that "untyped" terms are generated, you can also randomly generate terms in a Church-style grammar with explicit type annotations) and it worked very well in practice, it revealed all the bugs there was to find on this particular part of the project. For practical purposes I would recommend trying this first. (On the other hand, the generator was aware of scoping rules -- it maintained a set of currently bound variables for top-down generation, this is easy to implement.)
2. The choice of order depends *a lot* on the application you have in mind: two distinct applications will require different orders. For example, people that work on type-directed program synthesis are not usually interested in enumerating equivalent programs, so they will make simplification rules such as assuming that "any term of type A -> B can be chosen to start with a lambda-abstraction" -- in your framework, ordering lambda-terms before all terms at this type. This order is very bad for compiler testing: if you only generate programs that are in normal form, you are unlikely to exercise much of your optimization strategies or runtime semantics. So I believe that assuming an order to abstract away from the intended usage is not a good modeling choice: its choice is tightly coupled with the intended usage, and I would rather reason about the usage than the corresponding order.

Now for some references.

For typed-term generation for testing purposes, you may be interested in "Making random judgments: Automatically generating well-typed terms from the definition of a type-system" by Burke Fetscher, Koen Claessen, Michał Pałka, John Hughes, and Robert Bruce Findler, 2015.

> This paper presents a generic method for randomly generating well-
> typed expressions. It starts from a specification of a typing judgment in PLT Re-
> dex and uses a specialized solver that employs randomness to find many different
> valid derivations of the judgment form.  
> Our motivation for building these random terms is to more effectively falsify
> conjectures as part of the tool-support for semantics models specified in Redex.
> Accordingly, we evaluate the generator against the other available methods for
> Redex, as well as the best available custom well-typed term generator. Our results
> show that our new generator is much more effective than generation techniques
> that do not explicitly take types into account and is competitive with generation
> techniques that do, even though they are specialized to particular type-systems
> and ours is not.

For typed term enumeration for program synthesis, two recent works that I know are [Example-Directed Synthesis: A Type-Theoretic Interpretation](http://www.cs.grinnell.edu/~osera/publications/frankle-popl-2016) by Jonathan Frankle, Peter-Michael Osera, David Walker, and Steve Zdancewic, 2016, and [Program Synthesis from Polymorphic Refinement Types](http://people.csail.mit.edu/polikarn/publications/pldi16.pdf) by Nadia Polikarpova, Ivan Kuraj, and Armando Solar-Lezama, 2016. Note that both works use refinement types as a way to encode more desired properties of the searched program -- such as a testsuite that it should pass. These refinements often constrain the search space substantially more than just types, but they are also harder to invert -- interleave with search.

> **Comments:**
> **username_0**: When you generate a-la-Church terms: do you generate type-annotations randomly, or does the choice of type-annotation inform the generation of the abstraction's body?  
> **username_0**: I was aware of the work on randomly generating programs such as Fetscher et al. The key difference is that if you don't want a *uniform* distribution (e.g. of programs of size $n$) you can just abandon a search and backtrack if you are down a hopeless path. That's what Fetscher et al do. But that's not possible in enumeration.  
> **username_3**: Re. random type-annotations generation, I just randomly generated annotations.  
> **username_3**: One thing that I forgot to mention is the (natural) idea of writing an enumerator in a logic programming language. I am not sure that it would actually make it easier to push the type-system constraints into the generation (so it may be similar to naive random generation), but good Prolog implementation may support extra features to make it efficient, such as tabling. I have not tried myself.  

---

