| | | | | |
- Emacs Major Mode — there are also extensions for Neovim and VS Code.
- Functional Programming in Lean
- The Lean Language Reference
- Zulip Forum?
It's fairly straightforward, but you need to be careful with package names. In Homebrew, points to the old Lean 3 package. What you actually want now is:
❯ brew install elan
Similarly, for the Emacs extension, Doom Emacs already includes Lean in its init.el (just uncomment the lean line):
lean ; for folks with too much to prove
However, you will encounter this error:
> Regenerating envvars file
✓ Generated ~/.config/emacs/.local/env
x There was an unexpected runtime error
Message: Could not find package company-lean. Updating recipe repositories:
(org-elpa melpa nongnu-elpa gnu-elpa-mirror el-get emacsmirror-mirror) with
‘straight-pull-recipe-repositories’ may fix this
It turns out was removed from MELPA a few months ago. Upgrading fixed the original error for me but led to a new one:
lean get info: (json-readtable-error 108).
Digging into an issue from 2023, I found a solution. I removed from my and installed the Lean 4 mode manually:
(package! lean4-mode :recipe
(:host github
:repo "leanprover/lean4-mode"
:files ("*.el" "data")))
To begin, I tried a basic snippet from the Lean docs to read a file:
def main (args : List String) : IO Unit := do
match args with
| [] =>
IO.println "Usage: please provide the filename as an argument."
| filename :: _ =>
let content ← IO.FS.readFile filename
IO.println content
That worked, but I wanted to read the file line by line. I went digging through and discovered IO.FS.getLine. It turns out it’s basically an FFI call under the hood, which reads until a line break and returns an empty string on EOF. The details are burried in the Lean 4 source code:
Soon, however, I realized Lean’s syntax has some peculiarities, and I needed to go back to the language reference. My attempts at writing a recursive function with do blocks were failing because I hadn’t fully absorbed how Lean’s do syntax actually works.
/--
Read text up to (including) the next line break from the handle.
If the returned string is empty, an end-of-file marker has been reached.
Note that EOF does not actually close a handle, so further reads may block and return more data.
-/
@[extern "lean_io_prim_handle_get_line"] opaque getLine (h : @& Handle) : IO String
From there, I realized that Lean’s syntax can feel unfamiliar if you’re not fully used to it. I kept stumbling over small details, and I began to suspect I was missing fundamental knowledge about Lean. The tipping point was when I tried something like:
def processFile (filename: String) : IO Unit := do
let content ← IO.FS.lines filename
let rec processGraph (lines: Array String) (index Nat): IO Unit := do
match index with
| Nat.zero => return
| idx => do
IO.println s!"Line does not contain |: {line}; returning"
process_graph lines (idx - 1)
processGraph content content.size
return
This code snippet threw errors on and also on . I will later discover why, but it turns out is not just line up instructions in imperative style and using recursion with it can be tricky unless you get the function signatures and scoping exactly right. At that point, it became impossible to keep sweeping my confusion under the rug: I really needed to read the language reference properly, at least the relevant chapters. (I skimmed four entire chapters of the Lean manual to rush into this solution)
So, I got humble and restarted from the ground up, going through basic Lean examples:
Screenshot by author.
LƎⱯN in Emacs
One fascinating aspect is that functions can behave like methods if you place them within the namespace of the type. For example:
def String.x (_: String) :=
10
#eval "test".x
-- 10
This returns 10. So you can extend a type in Lean by creating a function in the String namespace.
Polymorphism in Lean also reminds me a lot of Zig. Generics take a type parameter, which is a first-class citizen:
structure Point (α : Type) where
x : α
y : α
deriving Repr
#eval ({ x := Nat.zero, y := Nat.zero } : Point Nat)
In Lean, functions are curried by default, meaning a function with multiple arguments conceptually becomes a chain of one-argument functions:
def replace (α : Type) (point : Point α) (xx : α) (yy : α) : Point α :=
{ point with x := xx, y := yy }
#check (replace)
replace : (α : Type) → Point α → α → α → Point α
Currying was named after an american mathematician, logician and computer scientist - Haskell Brooks Curry
You can see it’s not just in a single call, but actually . If you partially apply it -- say, omit the last parameter -- you get back a function waiting on that parameter:
def add (a : Nat) (b : Nat) : Nat :=
a + b
#eval add 10
-- Could not synthetize a 'Repr' or 'ToString' instance of type
-- Nat → Nat
Another awesome feature is that Lean treats types as first-class citizens. You can do things like write a function that returns different types based on an inductive constructor:
inductive Sign where
| pos
| neg
def direction (s : Sign) : match s with | Sign.pos => Nat | Sign.neg => Int :=
match s with
| Sign.pos => (1 : Nat)
| Sign.neg => (-1 : Int)
To me, that’s pretty mind-blowing. This kind of type-level computation is powerful and elegantly integrated.
Another thing to notice is that pairs in Lean are , while is akin to in C++, so you have:
def sevens : String × (Int × Nat) := ("VII", (7, 4 + 3)) - para
def Weird : Type := String ⊕ Int
def weird : List Weird :=
[Sum.inl "S", Sum.inr 10, Sum.inl "F", Sum.inl "R", Sum.inr 20]
Pattern matching is central to Lean, so to define, say, a function that returns the last element of a list:
def List.last {α : Type} (xs : List α) : Option α :=
match list with
| [] => none
| x :: [] => some x
| _ :: rest => last rest
#eval [1, 2, 3].last
Or to find the first element matching a predicate:
def List.findFirst {α : Type} (xs : List α) (predicate : α -> Bool) : Option α :=
match xs with
| [] => none
| x :: rest => if predicate x then some x else List.findFirst rest predicate
def is2 (x : Nat) : Bool :=
match x with
| 2 => true
| _ => false
#eval [1, 2, 3].findFirst is2
Pattern matching is so central to Lean that there is a dedicated shortcut for the most common scenario: when your first line of code matches on the function parameter. As a result, the example shown above can be rewritten as follows:
def List.findFirst : List α → (α → Bool) → Option α
| [], _ => none
| x :: rest, pred => if pred x then some x else List.findFirst rest pred
def is2 : Nat → Bool
| 2 => true
| _ => false
#eval [1, 2, 3].findFirst is2
Lean also has couple more interesting tricks like simulatnous matching, which is matching a pattern of many variables at once. Lean also can deduce most of the types for us, and sometimes defining a type is completly unnecessary. Combine that with anonymous functions and you can rewrite the above as:
def List.findFirst : List α → (α → Bool) → Option α
| [], _ => none
| x :: rest, pred => if pred x then some x else List.findFirst rest pred
#eval [1, 2, 3].findFirst (· = 2)
Or shorten the predicate to , which is the same as . You’ll also see a lot of Unicode in Lean code (, , , etc.). Emacs Lean mode provides a long list of very handy shortcuts (e.g., → , → , etc.) that make it straightforward to type these symbols.
Finally, there’s Lean’s notation. This is not just an imperative style, but more accurately a domain-specific language for monadic composition. If you’re coming from Haskell, it’ll feel familiar. If you’re from an imperative language, the syntax looks welcoming, but the semantics are different—each line returns a result that’s passed along in a monadic context.
Now, enough with the theory: let’s tackle the Advent of Code 2024 Day 5 puzzle. The problem deals with a directed graph of page references: Page X must come before Page Y. Then we’re given sequences to check whether the order is valid, and we also need a topological ordering for part two.
def parseLines (lines : List String) : List String :=
match lines with
| [] => []
| line :: rest => match line.posOf '|' with
| false => rest
| true => parseLines rest
#eval parseLines ["a|r", "k|a"]
Nope :)
Messages below:
27:6:
type mismatch
false
has type
Bool : Type
but is expected to have type
String.Pos : Type
30:0:
aborting evaluation since the expression depends on the 'sorry' axiom, which can lead to runtime instability and crashes.
To attempt to evaluate anyway despite the risks, use the '#eval!' command.
That failed because returns a position (a ), not a . I also got an error about the sorry axiom, which Lean uses to stub out missing proofs.
theorem my_theorem : 2 + 2 = 4 :=
sorry
That’s not relevant for finished code, but it’s interesting to see how Lean explicitly requires proofs for certain conditions like termination or safety. In older Lean versions, could run code with unsolved proofs, but that’s no longer allowed by default.
I refactored my approach after more reading. My new idea was: gather all lines containing , split them, convert to , and store them in a graph. Something like:
def parsePageRules (lines : List String) (graph : HashMap Nat (List Nat)) : (List String × HashMap Nat (List Nat)) :=
match lines with
| [] => ([], graph)
| line :: rest =>
match line.contains '|' with
| false => (rest, graph)
| true =>
let parts := line.split (· = '|')
if parts.length != 2 then
(rest, graph)
else
match parts with
| [l, r] =>
match (l.trim.toNat?, r.trim.toNat?) with
| (some left, some right) =>
let successors := graph.getD left []
let graph' := graph.insert left (right :: successors)
parsePageRules rest graph'
| _ => (rest, graph)
| _ => (rest, graph)
But to simplify, I ended up deciding to fold over all lines and skip those without . For example:
def skipToPageRules (lines : List String) :=
match lines with
| [] => []
| "" :: rest => rest
| _ :: rest => skipToPageRules rest
def parsePageRules (lines : List String) :=
lines.foldl (fun arr line =>
if line.contains '|' then
((line.split (. = '|')
|>.map (fun x => x.trim)
|>.map (fun x => x.toNat!))
:: arr)
else
arr
) ([] : List (List Nat))
def createRulesGraph (page_rules : List (List Nat)) :=
page_rules.foldl (fun g rule =>
match rule with
| [x, y] =>
let successors := g.getD x []
let g' := g.insert x (y :: successors)
if g'.contains y then g' else g'.insert y []
| _ => g) (HashMap.empty)
Having built the graph, the next step was to check if a page sequence is correctly ordered -- i.e., does each page appear before all of its successors? One straightforward way is to transform your list of pages into an index map (page -> its position), and then verify the condition index(page) < index(successor):
def ordered? (pages : List Nat) (rules : HashMap Nat (List Nat)) :=
let indexMap := pages.enum.foldl (fun m (i, p) => m.insert p i) (HashMap.empty)
pages.all (fun page =>
let idx := indexMap.getD page 0
let successors := rules.getD page []
successors.all (fun s =>
if indexMap.contains s then
let idxS := indexMap.getD s 0
idx < idxS
else
true
)
)
Testing that with:
❯ lean --run day05.lean example.txt
Part 1 Result: 143
That worked great. Then for part two, we want a topological sort of the pages:
def processPages (inDegree : HashMap Nat Nat) (localRulesMap : HashMap Nat (List Nat)) (queue : List Nat) (pages : List Nat) (sorted : List Nat) :=
match queue with
| [] => sorted
| el :: _ =>
let sorted' := sorted ++ [el]
let successors := localRulesMap.getD el []
let inDegree' := successors.foldl reduce inDegree
let pages' := pages.erase el
let queue' := pages'.filter (fun p => inDegree.getD p 0 = 0)
processPages inDegree' localRulesMap queue' pages' sorted'
At first, Lean refused to compile, complaining about not being able to prove termination.
fail to show termination for
processPages
with errors
failed to infer structural recursion:
Cannot use parameter inDegree:
the type HashMap Nat Nat does not have a `.brecOn` recursor
Cannot use parameter localRulesMap:
the type HashMap Nat (List Nat) does not have a `.brecOn` recursor
Cannot use parameter queue:
failed to eliminate recursive application
processPages inDegree' localRulesMap queue' pages' sorted'
Cannot use parameter pages:
failed to eliminate recursive application
processPages inDegree' localRulesMap queue' pages' sorted'
Cannot use parameter sorted:
failed to eliminate recursive application
processPages inDegree' localRulesMap queue' pages' sorted'
Could not find a decreasing measure.
The arguments relate at each recursive call as follows:
(<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted)
queue pages #1
1) 95:4-55 ? ? ?
#1: sorted
Please use `termination_by` to specify a decreasing measure.
When Lean compiles a recursive function, it requires a proof that the recursion terminates (unless you mark it partial). My recursion doesn’t obviously shrink just from the function arguments, because I’m mutating a and scanning a in each step. Also, doesn’t provide a built-in structural measure for the compiler.
I tried messing with and but got stuck. Then I realized Lean was actually helping me find a logical bug. I used to bypass the termination check and inserted debugging:
set_option diagnostics true
set_option diagnostics.threshold 255
partial def processPages (inDegree : HashMap Nat Nat) (localRulesMap : HashMap Nat (List Nat)) (queue : List Nat) (pages : List Nat) (sorted : List Nat) :=
match queue with
| [] => sorted
| el :: _ =>
let sorted' := sorted ++ [el]
let successors := localRulesMap.getD el []
let inDegree' := successors.foldl reduce inDegree
let pages' := pages.erase el
let queue' := pages'.filter (fun p => inDegree.getD p 0 = 0)
dbg_trace s!"pages={pages'}, queue={queue'}"
processPages inDegree' localRulesMap queue' pages' sorted'
It turned out I was filtering the queue with the old instead of . Correcting that:
let queue' := pages'.filter (fun p => inDegree'.getD p 0 = 0)
solved my logical error. And indeed:
❯ lean --run day05.lean input.txt
Part 1 Result: 143
Part 2 Result: 123
Victory! Lean’s termination system was right to be suspicious. After I fixed the bug, I could have tried again to provide a proper termination metric, but partial was enough for my immediate puzzle solution.
With that, I cleaned up and pushed everything to Codeberg.
Next week, I’m solving another Advent of Code puzzle in fish to learn how it differs from Bash. See you later!