guest0x0 / normalization-bench Goto Github PK

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.

It would be worth to set runtime options: https://v2.ocaml.org/manual/runtime.html#s%3Aocamlrun-options I have found that GC options have a very significant effect on overall performance in normalization/conversion checking. We'd also want to use tuned GC settings in real-world implementations, so it's more realistic IMO to benchmark with them. I used export OCAMLRUNPARAM="v=0x400,s=100000000,i=100000000" to significant effect, your mileage may vary.