Yeah yeah I know the title is definitely clickbait, but Lean is basically the Ali’s of programming languages. The moment I stepped foot inside Ali’s, I knew this was the perfect restaurant for me that I needed all my life. Same for Lean. IT’S SO LIFE-CHANGING TRUST ME YOU HAVE TO TRY IT.
Kublai: Lean? Isn’t that a proof assistant?
That’s right, Lean is primarily used as a proof assistant, especially for formal math. But it’s also an amazing, highly extensible functional programming language for automating proofs, and even for general-purpose programming! Think of it as the best parts of Haskell and Dafny and Rust combined together, plus lots more fun stuff like dependent types and a giant math library and massive Unicode abuse. Lean even runs on my phone! Honestly I don’t think I can go back to coding in other languages after trying Lean, other than Python for short scripts and Rust for performance-important stuff.
Sadly so far I haven’t convinced any of my friends to try Lean, but you, yes you right there, should give it a try! If you want something easy to start with, check out the Natural Number Game or this anime walkthrough of that game (warning: it uses the older Lean 3 instead of Lean 4).
Kublai: Talk is cheap. Show me some Lean code!
Sure, let’s dive right in! To test the waters, here’s a port of the lazy infinite power series code that I previously wrote in Python and Nix.
Lean uses eager evaluation by default instead of lazy evaluation like Haskell, but it has a thunk feature for being lazy. Let’s try implementing a lazy list and some helper functions.
inductive LazyList (α : Type u) where
| nil
| cons : α → Thunk (LazyList α) → LazyList α
def LazyList.take : Nat → LazyList α → List α
| 0, _ => .nil
| _, nil => .nil
| n + 1, cons x xs => .cons x <| xs.get.take n
def LazyList.map (f: α → β) : LazyList α → LazyList β
| nil => nil
| cons x xs => cons (f x) <| xs.get.map f
def LazyList.zipWith (f: α → β → γ) : LazyList α → LazyList β → LazyList γ
| nil, _ => nil
| _, nil => nil
| cons x xs, cons y ys => cons (f x y) <| zipWith f xs.get ys.get
Now time for the self-reference! Here’s an infinite list of integers:
def ints := LazyList.cons 1.0 <| ints.map (· + 1)
Oops! Lean doesn’t like that at all!
fail to show termination for
ints
with errors
failed to infer structural recursion:
no parameters suitable for structural recursion
well-founded recursion cannot be used, 'ints' does not take any (non-fixed) arguments
Infinite recursion is really bad for theorem provers. Why? Because it just completely breaks them. For instance, here’s one way to abuse infinite recursion to prove false in Dafny:
method prove_false()
decreases *
ensures false
{
prove_false();
}
However, we know here that because of lazy evaluation, we won’t actually loop infinitely. I’m still a beginner at Lean so I haven’t figured out how to prove that to Lean, so as a cop-out we’ll just use unsafe. It’s like unsafe Rust, kind of.
unsafe def ints := LazyList.cons 1.0 <| ints.map (· + 1)
#eval ints.take 10
-- [1.000000, 2.000000, 3.000000, 4.000000, 5.000000, 6.000000, 7.000000, 8.000000, 9.000000, 10.000000]
Yay, now it works! (If any Lean experts reading this have a solution for not using unsafe here, I’d love to hear it.) I’d also like to point out here that #eval combined with the Lean VSCode extension gives amazing live interactivity and it’s so much better than Jupyter notebooks since pure functional programming just sidesteps the Jupyter hidden state problem completely.
Anyways, back to our program. One downside of unsafe is that it infects everything it touches, so we’ll have to make our integration function unsafe as well.
unsafe def integrate s (c : Float) := LazyList.cons c <| LazyList.zipWith (· / ·) s ints
unsafe def expSeries := expSeries integrate 1.0
#eval expSeries.take 10
-- Lean server printed an error: libc++abi: terminating due to uncaught exception of type lean::throwable: deep recursion was detected at 'interpreter' (potential solution: increase stack space in your system) interpreter stacktrace: #1 expSeries #2 expSeries #3 expSeries #4 expSeries #5 expSeries #6 expSeries #7 expSeries #8 expSeries #9 expSeries #10 expSeries #11 expSeries #12 expSeries #13 expSeries #14 expSeries #15 expSeries #16 expSeries #17 expSeries #18 expSeries #19 expSeries #20 expSeries #21 expSeries #22 expSeries #23 expSeries #24 expSeries #25 expSeries #26 expSeries #27 expSeries #28 expSeries #29 expSeries #30
Oh no! Lean crashed this time! Welp that’s the risk of using unsafe. I’m not really sure why Lean crashes here but I figured out we can avoid it by using a macro instead of a function for integrate.
notation s "integrate" c => LazyList.cons c <| LazyList.zipWith (· / ·) s ints
unsafe def expSeries := expSeries integrate 1.0
#eval expSeries.take 10
-- [1.000000, 1.000000, 0.500000, 0.166667, 0.041667, 0.008333, 0.001389, 0.000198, 0.000025, 0.000003]
Yay, no more crashes!
And now, for the grand finale:
def evalAt n (s : LazyList Float) x := (s.take n).foldr (λ a acc => a + acc * x) 0
mutual
unsafe def sine := cosine integrate 0.0
unsafe def cosine := (sine integrate -1.0).map (-·)
end
#eval sine.take 10
-- [0.000000, 1.000000, -0.000000, -0.166667, 0.000000, 0.008333, -0.000000, -0.000198, 0.000000, 0.000003]
#eval evalAt 100 sine 2.0
-- 0.909297
#eval 2.0.sin
-- 0.909297
And… they match! We did it!
You’ve probably noticed Lean syntax is kind of weird sometimes, such as (-·) for the negate function or 2.0.sin for the sine of 2. Trust me, it’ll all make sense after a while.
I’d say the main takeaway of this is that lazy infinite lists are pretty terrible in Lean and I wouldn’t ever recommend using them unlike in Haskell, but hey, I’d call this experiment a success!
Using partial functions instead of unsafe
Locria Cyber pointed out that we can avoid unsafe using a neat trick: partial functions. Here’s the code:
inductive LazyList (α : Type u)
| nil
| cons : α → Thunk (LazyList α) → LazyList α
deriving Inhabited
def LazyList.take : Nat → LazyList α → List α
| 0, _ => .nil
| _, nil => .nil
| n + 1, cons x xs => .cons x <| xs.get.take n
def LazyList.map (f: α → β) : LazyList α → LazyList β
| nil => nil
| cons x xs => cons (f x) <| xs.get.map f
def LazyList.zipWith (f: α → β → γ) : LazyList α → LazyList β → LazyList γ
| nil, _ => nil
| _, nil => nil
| cons x xs, cons y ys => cons (f x y) <| zipWith f xs.get ys.get
partial def ints _ := LazyList.cons 1.0 <| (ints ()).map (· + 1)
#eval (ints ()).take 10
def integrate (s : Unit → LazyList Float) (c : Float) := LazyList.cons c <| LazyList.zipWith (· / ·) (s ()) (ints ())
partial def expSeries _ := integrate expSeries 1.0
#eval (expSeries ()).take 10
def evalAt n (s : LazyList Float) x := (s.take n).foldr (λ a acc => a + acc * x) 0
mutual
partial def sine _ := integrate cosine 0.0
partial def cosine _ := (integrate sine (-1.0)).map (-·)
end
#eval (sine ()).take 10
#eval evalAt 1000 (sine ()) 2.0
#eval 2.0.sin