Zulip Chat Archive

Stream: Lean Together 2021

Topic: Lean 4: An overview (Leo's talk)


view this post on Zulip Jason Rute (Jan 04 2021 at 17:08):

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.

view this post on Zulip Jason Rute (Jan 04 2021 at 17:10):

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

view this post on Zulip Kevin Lacker (Jan 04 2021 at 22:01):

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?

view this post on Zulip Jason Rute (Jan 04 2021 at 22:56):

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

view this post on Zulip Leonardo de Moura (Jan 04 2021 at 23:00):

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.

view this post on Zulip Huỳnh Trần Khanh (Jan 05 2021 at 00:27):

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

view this post on Zulip Leonardo de Moura (Jan 05 2021 at 00:36):

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 :)

view this post on Zulip Eric Wieser (Jan 05 2021 at 08:02):

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

view this post on Zulip Huỳnh Trần Khanh (Jan 05 2021 at 09:04):

set/map/multiset I guess

view this post on Zulip Kevin Lacker (Jan 05 2021 at 16:56):

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++?


Last updated: May 08 2021 at 22:13 UTC