Lean 4: An overview (Leo's talk)

Stream: Lean Together 2021

[Jason Rute]

Leo: I tried some of the advent of code exercises in Lean4 and it was very pleasant to program in. I really like the foo (<- bar) notation. It eliminates the need for a lot of monadic combinators.

[Jason Rute]

Question about persistent data structures: When you compare persistent data structures in C++ and Lean 4, do you use them persistently?

[Kevin Lacker]

i missed the zoom chat about porting mathlib to lean 4. did anyone conclude or plan anything, can someone share a TLDR of the conversation?

[Jason Rute]

I didn’t happen on Zoom in the end (I think due to time).

[Leonardo de Moura]

When you compare persistent data structures in C++ and Lean 4, do you use them persistently?

No. The comparison I was referring to was on a benchmark where the tree was being used linearly.
In benchmarks where persistency matter, the Lean 4 version is several orders of magnitude faster than the C++ std version since we have to keep copying the whole tree in C++.
We believe the Lean and Koka implementations are faster than the C++ version because of two ingredients: "counting immutable beans" paper and mimalloc.

[Huỳnh Trần Khanh]

Binary trees in the STL are known to be slow right? So Lean 4 being faster on that front isn't really surprising.

[Leonardo de Moura]

It was surprising to me and my colleagues. The STL version is performing destructive updates, and our version is pure. Our version is also much faster than Haskell. It was surprising to Simon PJ. He conjectured that we would only be faster when the trees were being updated linearly. However, when we tried nonlinear benchmarks, the Lean version was even faster.
BTW, when we reported our results, many were skeptical and doubted our experimental results were correct. Now, they were reproduced in Koka, this kind of doubt is gone.
The Lean version is also much faster than the persistent red-black tree used in Lean 3 and implemented in C++. I implemented both versions :)

[Eric Wieser]

To be clear, which C++ STL "tree" container are we comparing to here?

[Huỳnh Trần Khanh]

set/map/multiset I guess

[Kevin Lacker]

so if I just have an STL map<string, int> and I insert a million entries into it and do a million random reads, I should expect the equivalent to be faster in Lean 4 than in C++?