Good practices to write fast code

Stream: lean4

[Aatman Supkar]

As an example, let's say in C++, people prefer to write iterations over recursions because they grant better speed. Similarly, do we know guidelines on how to write Lean4 code that runs fast (as in, they're algorithmically the same thing, but the internal workings speed one up more than the other)?

I am interested in Lean4 as a programming language, and am interested in wanting to write highly optimiseed code as well.

[Mario Carneiro]

you generally want to write tail recursive functions if you are concerned about performance. The monad sugar like for desugars to function calls to tail recursive functions that get inlined into your function, but the let mut handling causes unnecessary allocations on each iteration of the loop which you can avoid by writing the tail recursive function yourself

[Mario Carneiro]

This is a bit of a micro optimization though, it's probably not worth doing unless it shows up in profiles

[Mario Carneiro]

Another thing to watch out for in performance sensitive code is that you design your mutable data structures to be used linearly (i.e. values to mutate have one active reference when performing the mutation, so that an expensive copy is avoided), and you make sure that they are in fact used linearly where you expect. This is very difficult to predict in advance because the current compiler has a tendency to break linearity though optimizations, you just have to either look at the IR, test with dbgTraceIfShared, or profile and notice a lot of time is being spent in the "garbage collector" lean_dec_ref_cold.

[Aatman Supkar]

Not quite sure what you mean by the thing about mutable structures being used linearly because optimisation might break it. I understand I don't want to make unnecessary copies, yes.