Last September, Lean released a major update. My understanding is that this newest version of Lean is heavily focused on making the programming side of the theorem prover ergonomic enough that it’s worth the effort to use.
Having played around with it a bit, I’ve felt pretty impressed. Though I haven’t done nearly enough to be able to speak with any confidence about it, I’ve been appreciating the aesthetic of a single term-language (with universes) as apposed to Haskell’s terms, types, and kinds.
Though it hasn’t changed anything fundamental for me, Lean’s way of handling implicit parameters has made me look at Type Class resolution and dictionary passing in a different light.
Doing a little side project in Lean has been a fun adventure.
I’m curious if any other PureScript enthusiasts have found themselves impressed or if your experience has been qualitatively different.
2 Likes
I went through this book as well a couple months ago. I finished it in a couple days, which is very far from being enough time to get a decent understanding of a language. But overall I wasn’t particularly impressed. Elan the toolchain manager is nice, but why such a small language would need a “toolchain manager”? I think it’s better to design tools to be compatible, and IMO this is what PureScript follows to a great extent. The LSP was trivial to set up and it worked flawlessly, although it’s messages are very weird sometimes. Sadly there isn’t yet a package manager, nor, well, packages, other than maths packages. This isn’t at all an exaggeration there just really isn’t any. The standard library seems to be well-documented but the documentation could only be found in the source code (reaching which is, thankfully, only a matter of hitting goto definition). Another feature of the standard library is that it’s implemented as a single monolith: thousands LOC across just a few files, from primitives like syntax definitions to things like FAM typeclasses. Not saying it’s bad, but not what I’m used to or was expecting. One thing I really didn’t like is OCaml-ish syntax in match and lambdas and general lean towards some features more natural for imperative languages. In particular the method-call-like syntax arg1.function arg2 kills the order of arguments natural for use with binary operators, and what operators are there in Lean have their precedence messed up, so a lot of bread-and-butter FP idioms become awkward. Other syntax gripes aside (a lot of them TBH), compiler’s output seems to be decent — the binaries are perhaps too big for micro and one-off projects (5MB even for a hello world), but for small and mid-size apps it might be a worthy alternative to other compile-to-native FP languages.
1 Like
Ah, sounds like a fairly lackluster first impression for you. Totally fair 
I hadn’t really seen the method-call-like syntax as an issue, but I can definitely see where it might be a bit annoying. Though kind of like PS’s operator sections, creating functions using · notation as a placeholder is a fairly concise way to re-order parameters in many cases.
λ arg1 ↦ arg1.function arg2 can be written as function · arg2.
I don’t know if Lean’s ecosystem will ever be mature enough that you would want to use it in production for every-day programming tasks. I think that even simple tasks that might take a few hours to manage with Haskell/PureScript would take considerably longer with Lean as the libraries and such just don’t exist.