[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.