Not an expert, but I've played with these languages. The short answer is yes this is possible, but it is also possible already in non-dependently typed language

Not an expert, but I've played with these languages. The short answer is yes this is possible, but it is also possible already in non-dependently typed languages to do so. Moreover in practice it's not very common to actually evaluate your functions on large literal inputs at compile time. Indeed it's not very common to evaluate the function on a single value as such at all. Instead it is better to think of your functions as abstract rewrite rules, that allow you to substitute one side with the other. Unlike at runtime, recursive functions do not always need to recurse until their base case. Therefore it's not actually very common to e.g. have a recursive function recurse many times at compile time. However, when it does happen, yeah your compile times can shoot up, but it's usually fairly obvious what's causing it. Even then, in absolute terms the quantity of calculations involved generally isn't astronomical, it's rather the case that the compiler is far more inefficient at executing your code at compile time than your runtime system is at executing the compiled code. That being said, dependently typed languages on the whole do tend to have abysmal compile times, but this seems like an implementation issue rather than a fundamental limitation. Efforts like https://github.com/AndrasKovacs/smalltt/blob/master/README.md https://github.com/AndrasKovacs/smalltt/blob/master/README.m... make me hopeful this is something that can be solved.