Prefer input terms which could have been hand-written

[AndrasKovacs]

Looking at the benchmark code, I see that large numerals are being inlined to benchmark input. Instead, I think it's better to have input terms which are realistic as hand-written source code, because most of the time we execute user source code in practical settings (with some exceptions, like bloat generated by tactics).

Large numerals and insufficient code structure could be a reason why compiled code is not doing well in the benchmarks, especially in Church multiplication. In my old benchmarks I did find that compiled HOAS in GHC was significantly faster than interpretation. Perhaps OCaml compilation is that much worse than GHC, but I don't find that likely; I would expect that compiled Church multiplication is significantly faster than the interpreted one.

For compiled code it would be good to have primitive let-definitions in terms which can be translated to actual OCaml let-s. Using beta-redexes to emulate let is possible of course, but that's also highly unrealistic as input to the OCaml compiler and it would be probably handled worse.

[Guest0x0]

Indeed, large literal terms are not realistic in hand-written code. My understanding of "realworld code" is that, most of the time there is little normalization work (e.g. when writing inductive functions, each case only requires one level of calculation), except for some proof-by-refl applications. In the current benchmarks, I think church-add and self-interp are most "realworld" in the sense that they require O(init_term_size) steps to normalize.

Using native let in compiled impls to avoid large literal term in generated code is definitely a good idea I missed, I'll (soonish) try this out when I've got time (currently I am playing with hash-consing impls)

In terms of the effect of large input term size on compiled impls, I think the exponential and parigot-add benchmarks are worth investigating, as they have very small input term size. I may also add a benchmark that repeatedly do some trivial calculation for a large, binary-encoded number of times, which also require exponential computation steps (proportional to input term size), but also have very small result term size.

[AndrasKovacs]

To make my emphasis more precise, I did not mean that benchmarks should be reflective of real-world typechecking workload, I meant that whatever computation we benchmark, the source code for that should be realistic. It certainly makes sense to both have synthetic and real-world-ish benchmarks.

[Guest0x0]

If the compiled normalizer is a part of a complete compiler, then the unrealistic large numerals are part of the input to this complete compiler, and all the normalizers accept this same input. Take the church multiplication as an example, I am not really comparing the performance of normalizing church multiplication, but the performance of processing a source program of multiplying two large church numerals, so the unrealistic-ness is part of the benchmark design: that's why I thought you were talking about the benchmark itself.

IMO when talking about "compiled NBE", there are several different approaches:

1. write source program directly in target language (as in your benchmark)
2. reuse an existing compiler from text level (as in my current setting)
3. use MetaOCaml/TemplateHaskell or similar
4. reuse some intermediate language/backend of an existing compiler, such as Coq's bytecode VM

For 1 I have no idea how it should be implemented. 3 and 4 are probably more interesting/practical, I implement 2 first simply because it is the simplest.

[AndrasKovacs]

There's not much difference between 1 and 2. I wrote the HOAS sources manually because the translation from a given term language to HOAS source was not very interesting for benchmarking. We can assume that the exact same sources can be obtained as the output of a straightforward translation.

My background assumption when using OCaml or GHC for compiled NbE, is that they are too slow for real time usage during elaboration or interaction, and that the way of using them would be ahead-of-time module compilation or perhaps compilation as a background task. So I don't care a lot about how long it takes to compile with OCaml or GHC. I would be more interested in compilation speed where there's a reasonable chance that it's fast enough for interactive usage.

[Guest0x0]

Indeed the normalizers should receive the same input. For the church-mul benchmark here, unrealistic input code with large literals is part of the benchmark design and applies equally to all normalizers. It is not intended for testing the performance of actually performing church multiplication with hand-written code (in that case, hand-written-ish input with let is definitely more accurate), but just yet another workload with a quadratic computation complexity w.r.t. init code size. For workloads with smaller code size and higher complexity, my current setting has exponential and parigot-add. I think hand-written church multiplication would behave more like these two.

I totally agree with you on that OCaml/GHC based compiled NBE is not suitable for interactive use. In my tests compilation time dominates normalization time for even modest initial code size.