Comment by auggierose
3 months ago
Yes, factorial_10_hardcoded convinces me that RUNTIME is not a good idea, although it works actually as RUNTIME is supposed to work: Hardcoding the computed value for a given input is the ultimate optimisation.
Not sure about the factorial_hardcoded_a_b example, because you still need to get rid of the existential somehow, maybe via skolemisation b[n], but that does not really matter in light of factorial_10_hardcoded.
The typing rules for RUNTIME would have been simply that if f has type a_1 => ... => a_n => b for n >= 1, and x_i has type a_i, then RUNTIME f x_1 ... x_n has type b.
That would exclude the clearly problematic case RUNTIME x for n = 0, but it seems to me hardcoding is basically how you can get that case back in via extensionality.
Although, I am starting to wonder how bad the constant hardcoding case really is.
As I said before, it is to be expected: Providing a precomputed value is a very fast implementation!
I am not entirely convinced yet that it would damage what RUNTIME can say about variable inputs, so I guess a complete analysis of your hardcoded_a_b example is necessary after all.