Chamelean synthesizes slow generator for well-typed STLC terms.

[dsainati1]

In Test/DeriveArbitrarySuchThat/DeriveSTLCGenerator.lean, if we inspect the generator synthesized by #derive_generator (fun (e : term) => typing G e t) we can see that the function application case is handled by the following code:

do
  let e2 ← Plausible.Arbitrary.arbitrary;
  do
    let τ1 ← ArbitrarySizedSuchThat.arbitrarySizedST (fun τ1 => typing G_1 e2 τ1) initSize;
    do
      let e1 ← aux_arb initSize size' G_1 (type.Fun τ1 t_1);
      return term.App e1 e2

Essentially, Chamelean is choosing an arbitrary term for the function argument e2, then attempts to produce a type τ1 that checks it. Only after successfully doing this will it attempt to synthesize the function e1 from τ1 to the goal type. This is essentially just generate-and-test, which is slow. It is also not the behavior of QuickChick, which instead generates an arbitrary type for the argument, then attempts to synthesize a term of that type for the argument, and then generates the function.

I.e., something like

do
  let τ1 ← Plausible.Arbitrary.arbitrary;
  let e1 ← aux_arb initSize size' G_1 (type.Fun τ1 t_1);
  let e2 ← aux_arb initSize size' G_1 τ1;
  return term.App e1 e2

Manually changing Chamelean's generator in this case to use the latter approach improves the performance by over 90%. Is it possible to change Chamelean's synthesis strategy to more closely match QuickChick's output in this case?

[ngernest]

Thanks for pointing this out, good point! I remember trying to debug this summer. I believe this is because the current implementation finds a naive generator schedule, i.e. after doing a depth-first enumeration of all possible schedules (ordered according to some heuristics, e.g. shorter schedules come first), it just picks the first well-formed schedule. (See the comments for the dfs function in DeriveSchedules.lean.)

To get Chamelean's synthesis strategy to match QuickChick, we would need to implement the entirety of the generator derivation algorithm from Testing Theorems, Fully Automatically (Elazar-Mittleman et al 2025, under submission), which includes optimizing generator schedules & pruning bad ones (i.e. "generate-and-check" schedules). The first author @segevm is currently interning at AWS and working on extending/improving Chamelean in another fork (https://github.com/codyroux/plausible), so maybe that fork will match QuickChick's behavior more closely!