[tines]

This seems really cool, but can someone who knows both Lean and Haskell (the former is probably just a subset of the latter, lol) explain how this is materially different from a Haskell implementation of the same algorithm? I don't know where to look for the cool dependently-typed parts.

[kmill]

I did this to see how it was as a practical functional programming language, and I find I like the syntax and typeclass system more than Haskell's. One neat feature is that do notation had mut variables and for loops that get compiled to folds automatically. It also has Idris-style arrow notation for binding inside pure expressions. (It's also really easy to compile to C!)

The Lean runtime implements the Perseus algorithm for functional in-place updating when possible. It's a very clever reimagining of reference counting from basic principles. The loop that combines all the results from all the threads takes advantage of this and doesn't allocate intermediate arrays.

[haskellandchill]

This doesn't have any cool dependent typed parts. Lean 4 lets you program like Haskell if you don't make any claims to prove anything.