~/tend/blog $ // learn lean 4 by building a task manager

001: Six Lean lessons for the recovering Haskeller

2026-07-26

The repo grew real code this cycle; this post teaches the Lean that code is made of – records, notation, macros, commands, the compiler’s environment, compile-time checks – as a standalone tutorial. Read it cold, or with the commit diff open in the next tty. Two references to keep handy: the Lean language reference and Metaprogramming in Lean 4; we link into both throughout.

Lesson 1: data types, but with namespaces

A structure is your single-constructor data with record syntax, minus twenty years of accumulated regret:

structure Point where
  x : Float
  y : Float
  z : Float := 0
deriving Repr, BEq

Things to notice, in decreasing order of envy:

The headline difference is what happens to functions. There is no field namespace problem and no pointNorm prefixing convention, because functions live in namespaces and dot-call resolves through them:

def Point.norm (p : Point) : Float :=
  Float.sqrt (p.x^2 + p.y^2 + p.z^2)

#eval ({ x := 3, y := 4 : Point }).norm   -- 5.000000

Naming it Point.norm is what makes p.norm work. That’s the entire mechanism – namespace resolution on the type of the receiver, no typeclass, no dictionary. It’s what OverloadedRecordDot wants to be when it grows up, and it works for every function whose first explicit argument is the receiver’s type: xs.filter, xs.any, g.nodes – all just names.

The same convention runs in reverse for constructors: .sqrt above, or (.ok 3 : Except String Nat) – a leading dot means “resolve this name in the namespace of the expected type.”

extends: record inheritance, no lenses required

structure Particle extends Point where
  mass : Float := 1

A Particle has x, y, z, mass – parent fields flattened in – plus a generated projection Particle.toPoint. Record update crosses the boundary without comment:

def bump (p : Particle) : Particle := { p with x := p.x + 1 }

{ p with ... } is your record-update syntax; combined with field punning ({ p with mass } picks up a local named mass) it dissolves most of what Haskell needed lenses for. Not all of it – deep nested update is still wordy – but the everyday 90%.

«in»: when your identifier is a keyword

in is a Lean keyword (for x in xs, let ... in). Want it as a constructor name anyway? Guillemets un-keyword anything:

inductive Rel where
  | «in»
  | blocks
deriving Repr, BEq

Haskell makes you write in_ and feel bad; Lean makes you type «» and feel fancy. While we’re here, a one-line typeclass instance via the anonymous constructor ⟨...⟩ and a pattern-matching lambda:

instance : ToString Rel := ⟨fun | .«in» => "in" | .blocks => "blocks"⟩

fun | ... => ... is \case. ⟨f⟩ builds the instance record positionally – ToString has one method, so one component.

Lesson 2: notation is a library feature

In Haskell, (<+>) is the function. Lean splits the atom: functions get boring names, and notation is a separate declaration pointing at one:

def Point.add (a b : Point) : Point :=
  { x := a.x + b.x, y := a.y + b.y, z := a.z + b.z }

infixl:65 " ⊞ " => Point.add

infixl:65 – left-associative, precedence 65, declared where the operator is born instead of in a fixity declaration orbiting nearby. a ⊞ b ⊞ c folds left. Any unicode you can type is fair game (editors take TeX-style abbreviations: \oplus, \-->, …). infixl and friends are the entry-level tier of the notation system; lessons 3 and 4 are the heavier tiers.

Lesson 3: quotations, and a macro that knows where it is

Lean metaprograms manipulate typed syntax trees, written in quotations that use the language’s own grammar – no [d| ... |] bracket dialect:

`(1 + $x)        -- a term with an antiquoted hole
`(def foo := 3)  -- a whole command

$x splices a TSyntax in; the quotation is checked against the real parser at compile time. Macros are rewrites from syntax to syntax, hygienic by default, expanded during elaboration at the use site – which means they can see context. The star witness is decl_name%, a core macro that elaborates to the name of the enclosing declaration:

def whereAmI : Lean.Name := decl_name%

#eval whereAmI   -- `whereAmI

Anything your macro expands to can use it: generate f decl_name% and every call site quietly passes its own name to f. Template Haskell has no cheap equivalent – a splice can’t ask “which binding am I the body of?”. Note the payload type: Lean.Name, the compiler’s own hierarchical name type, available in the prelude. Your program’s identifiers can be first-class data of the same type the elaborator uses.

Lesson 4: the grammar is open

The heaviest tier: add a top-level declaration form to the language. This is a library-level act in Lean – the thing Haskell reserves for GHC proposals:

syntax (docComment)? "greet " ident : command

Read it as BNF: optional doc comment, keyword, identifier, producing a command. (The metaprogramming book’s Syntax chapter maps this territory.) Then attach semantics with elab_rules:

open Lean Elab Command in
elab_rules : command
  | `($[$doc?:docComment]? greet $x) => do
    elabCommand (← `($[$doc?:docComment]? def $x : String := "hello"))

The pattern is a quotation too; $[...]? threads the optional doc comment from pattern to template ($[...]* does repetitions). elabCommand hands the synthesized def back to the elaborator as if you’d typed it – so greet fred defines fred : String, hover documentation included, and go-to-definition works on generated code. Whole DSLs are built this way (chapter 8).

One landmine, learned empirically: a string literal in syntax reserves that token globally – every file importing yours loses greet as an identifier, including field names whose dot-access will mysteriously die. There’s &"greet" for “non-reserved keyword”, but it does not dispatch at the head of a command, so in practice: reserve, and pick DSL keywords the way you’d pick a Unix signal name. You only get so many.

Lesson 5: the compiler is a database

Lean exposes its own environment – the map from names to declarations that elaboration builds up – as something libraries read, extend, and persist. Three faces of this:

One: libraries can hang state off the environment.

initialize favorites : SimplePersistentEnvExtension Lean.Name (Array Lean.Name) ←
  registerSimplePersistentEnvExtension {
    addEntryFn := Array.push
    addImportedFn := fun arrs => arrs.flatten
  }

An environment extension is typed, ordered, module-local state that survives into .olean files and merges across imports – think TH’s qPutQ/qGetQ upgraded to interface files. A command (lesson 4) can modifyEnv (favorites.addEntry · name); any later command can favorites.getState (← getEnv) and see every entry, including imported ones, in declaration order.

Two: doc comments are data. /-- like this -/ isn’t trivia for a doc generator; it’s stored in the environment next to the declaration’s type and value, and findDocString? env name hands it back to any metaprogram. Documentation, hover text, and queryable data are one artifact.

Three: generate references, not values. When a metaprogram wants to emit a list of previously-registered things, it doesn’t evaluate anything – it splices identifiers (mkIdent name) into a quotation and lets ordinary elaboration resolve, type-check, and compile the result. Code generation stays honest: the output is plain Lean that could have been handwritten. (For turning runtime values into syntax the other way, there’s quote.)

Lesson 6: compile-time checks by just running code

#eval expr evaluates during elaboration and prints the result – the REPL, inverted: instead of loading code into GHCi, you drop the prompt into the file, and the language server evaluates it live in your editor. It runs IO too. Which yields the cheapest possible compile-time enforcement: run a checker that throws.

def assertNonEmpty (xs : List Nat) : IO Unit :=
  if xs.isEmpty then throw <| .userError "empty!" else pure ()

#eval assertNonEmpty []   -- BUILD ERROR: empty!

A failing #eval fails the build, with your error message, at that line. It’s TH’s runIO minus the song and dance. And it’s rung one of a ladder:

  1. Run a check (#eval + throw). Five lines, great error messages.
  2. Prove a theorem. State the property as a Prop, give it a Decidable instance, and theorem ok : P := by decide – now the fact is a kernel-checked proof object downstream code can consume. (Tactic proofs start here.)
  3. Make illegal states unrepresentable. Index your types so the bad value can’t be constructed. Maximum guarantee, maximum ceremony.

Rung 1 buys ~90% of the value for ~2% of the cost, and unlike decide, its error can name the offender. Climb only when something downstream needs the fact, not the check.

Next

More of the standard library in anger – List combinators, Option, folds with effects – as the code grows the functions that interpret data instead of merely declaring it.