Comparing Lean 4 with Haskell
I've been curious about dependent types for some time. After wrestling with them in Haskell , discovering Lean felt like a small revelation. Two weeks in, Lean's proofs-as-values and tighter types already feel like the missing piece I couldn't quite get in Haskell. My Haskell background helps; the language still feels familiar enough that the learning curve is manageable. In this post I compare two Word Puzzle solvers I implemented: one in Haskell and my first program in Lean 4 . Below I list the differences I noticed and why they mattered for design, validation and I/O. 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...