Learning Lean 4 and Dependent Types
Dependent Types have been on my radar for a while. I had a bit of a struggle wrapping my head around them in Haskell, so finding them in Lean was a welcome surprise. I'm only a couple of weeks in with Lean, but I'm already sold — it scratches the itch I didn't quite manage to scratch in Haskell. Coming from Haskell also helps; the language feels familiar enough that the learning curve isn't too steep. In this short write-up, I compare two Word Puzzle solver implementations: one in Haskell, one in Lean 4 (the latter being my very green attempt). Here's what I found. Overview of the Problem I built both projects to solve an identical problem: given a pool of 4–9 lowercase letters and a mandatory letter, filter a dictionary file for words that can be spelt from the pool. My Haskell version uses pull-based streaming I/O with the io-streams library and applicative validation via Data.Validation . For my Lean 4 attempt, I used dependent types with compile-time...