Currently, I haven't learned about a functional language that can achieve the same performance as C/C++. And I have learned that some languages that favor functional programming to imperative programming, such as Scala and Rust, use imperative ways to implement their library functions for better efficiency.
So here comes my question, on today's comptuters that execute imperative instructions, is this a limitation of the compiler or functional programming itself? For every imperative function with no side effects, either in a language without GC such as C/C++/Rust/assembly or one with GC such as Java, is there a pure functional counterpart in Haskell, Scala, etc. that can be compiled to run with identical performance in time and space (not just asymptotic but exactly the same) or even to the same instructions, with an optimal functional compiler that utilizes all modern and even undiscovered optimization techniques such as tail recursion, laziness, static analysis, formal verification, and so on which I don't know about?
I am aware of the equivalence between λ-computable and Turing computable, but but I couldn't find an answer to this question online. If there is, please share a compiler example or a proof. If not, please explain why and show a counter-example. Or is this a non-trivial open question?
Supplementary edits as suggested by Andrej Bauer:
To be more specific, here are 2 examples that led into thinking about this question.
For example, tail recursion and accumulators can improve the performance of some recursive functions to be identical to an imperative implementation using
for. In some cases they might even have the same instructions.
Another example is about laziness in Haskell. Laziness can help avoid unnecessary copying of data structures and make performance better. However, laziness leaves wrappings, closures, etc. in the runtime and still can't make the program as fast as an imperative implementation where there are no such things. So I am wondering whether such things can be statically removed before runtime during compilation.
Supplementary edits as suggested by Nearoo:
The question can also be stated in this way: is there a language that supports both pure functional programming and imperative programming, paired with an optimized compiler, in which every function with no side effects implemented imperatively can be replaced with one implemented purely functionally, at no cost of performance or even compiled to the same instructions?