Efficient generated code

Stream: lean4

[Arthur Paulino]

Are there general tips for writing Lean 4 code that generates efficient executables? (please write tips down if you know some :pray:)

[Wojciech Nawrocki]

Are you looking for quite detailed Lean 4 or general functional programming tips? Here are two general ones I could think of.

• If writing recursive functions, try to use tail-recursion. This is not so much about speed as it is about stack size limits - a function which is not tail-recursive can easily run out of stack space when executed on large inputs.
• Make sure you use persistent data structures when you expect them to be duplicated (i.e. multiple references will exist), and in-place data structures when linear use is possible (refcount never exceeds 1). This ties in with FBIP (this is the Koka tutorial but Lean also uses Perceus).

[Arthur Paulino]

I'm also interested in tips specific to Lean 4 :+1:

[Sebastian Ullrich]

See also this thread: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Metamath.20verifier.20in.20Lean.204

[Tomas Skrivan]

Once I got a big speed up by replacing product type A × B with a structure holding A and B.

[Sebastian Ullrich]

Wow, that is surprising to me. Unless either A or B were unboxed types.

[Tomas Skrivan]

Yes they were floats, probably should have mentioned that :)