002: Types do the driving

2026-07-31

Post 001 was parser tricks – records, notation, macros, commands. Cheap thrills. This time the type system earns its keep: sum types with payloads, typeclasses that infer meaning instead of just overloading names, notation that exists only where you open it, and – I am not making this up – a user-definable offside rule. Layout, as a library feature. The fine manuals are the Lean language reference and Metaprogramming in Lean 4; links below point into both. RTFM as needed, that’s what it’s for.

Lesson 1: sums with payloads, and the expression problem

Inductive constructors carry data. Film at 11 – it’s your ordinary sum type, except the arms take named fields:

inductive Ref where
  | name (n : Lean.Name)
  | date (d : Std.Time.PlainDate)
deriving Repr, BEq

.date d builds one where a Ref is expected (the expected-type dot trick), fun | .name n => ... | .date d => ... takes one apart. A ToString in one line, anonymous constructor plus \case:

instance : ToString Ref :=
  ⟨fun | .name n => n.toString | .date d => toString d⟩

Zero new mechanics. The design question is the old expression problem, and here’s the two-line version for the impatient. Closed sum: new operations cheap (another total match), new cases expensive – every match in the tree breaks. Which is not a bug: the compiler just handed you a grep-quality todo list, with line numbers. Open typeclass: new cases cheap (one more instance), new operations expensive. Neither wins; they answer different questions, and one program can answer differently per axis – close the axis where operations breed, open the one where cases do. Lean ships open existentials if you insist (Lean.Dynamic, keyed by TypeName), but reach for the closed sum first. Exhaustiveness checking is the best navigation tool ever shipped; followups to /dev/null.

Lesson 2: a date the compiler reads

The stdlib ships a clock. import Std.Time, and you get PlainDate – a calendar date, no time, no zone, no nonsense – plus a literal that’s validated during elaboration:

import Std.Time
open Std.Time

def deadline : PlainDate := date("2026-08-15")

def oops : PlainDate := date("2026-02-30")   -- BUILD ERROR: invalid date

February 30 bounces at compile time. For contrast, Haskell’s time library takes fromGregorian 2026 2 30 and silently clamps it to February 28, and you get to learn this from a pager, at 3am, in production. Or you write the TH splice yourself, again. Here it’s just a macro (001, lesson 3) running the validator at elaboration time – same move as #eval-as-assertion (001, lesson 6), packaged as a term.

Comparisons: PlainDate has no LT instance, on purpose, so < is a non-starter. You go through Ord:

def isDue (today d : PlainDate) : Bool := (compare d today).isLE

compare : α → α → Ordering, and Ordering carries its own predicates (.isLE, .isLT, == .eq) so you rarely bother matching on it. One class, one total order, derived once – and none of the Ord-implies-Eq-what-about-Double flamewar. Wall clock is PlainDate.now : IO PlainDate, honestly stamped IO like the effect it is.

Lesson 3: typeclasses that infer meaning

A typeclass member doesn’t have to mention the class parameter at all:

class Shipped (α : Type) where
  weight  : α → Nat
  carrier : String        -- no α in sight

A Haskell class member whose type doesn’t pin the instance means a trip through the extension soup – AllowAmbiguousTypes, TypeApplications, or the Proxy of shame. In Lean it’s a non-event, because every argument, implicit and instance-implicit included, can be passed by name:

instance : Shipped Book where
  weight  := fun b => b.pages * 2
  carrier := "media mail"

#eval Shipped.carrier (α := Book)   -- "media mail"

(α := Book) pins the implicit; instance search does the rest. Now the payoff. Default argument values (001, lesson 1) are arbitrary terms elaborated at the call site – so a default can itself fire instance resolution:

def shipLabel [Shipped α] (x : α)
    (via : String := Shipped.carrier (α := α)) : String :=
  s!"{via}: {Shipped.weight x}g"

#eval shipLabel book                           -- "media mail: 642g"
#eval shipLabel book (via := "carrier pigeon") -- override at will

Read that signature twice. The caller passes a value; the type of that value picks the default for an argument they never wrote. That’s “infer meaning from types” as a service – the same judgment the elaborator makes inferring types from terms, now yours at the domain level. A new inferrable meaning is a new instance: no new syntax, no elaborator surgery, open by construction (lesson 1’s other axis).

Lesson 4: an offside rule of your own

Haskell’s layout rule comes down from the Report on stone tablets: the committee defines it, GHC implements it, you receive it. In Lean, whitespace sensitivity is library code – do-notation’s layout is built from parser combinators sitting right there in the box. The primitives, from the syntax toolbox: withPosition(p) parses p and pins its start column; colGe/colGt/colEq succeed only if the current token sits at-or-right-of / strictly-right-of / exactly-at the pin. Add a self-recursive syntax category and indentation is the grammar:

declare_syntax_cat branch
syntax atomic(colGe "- ") withPosition("branch " ident branch*) : branch
syntax withPosition("tree " ident branch*) : command

which parses

tree animals
  - branch mammals
    - branch cats
  - branch birds

with cats under mammals, not under animals. No braces, no separators, no yacc. Mechanics: every withPosition re-pins at its own branch keyword; a child’s - must pass colGe against the innermost pin, so indented lines attach to the nearest block, and a dedented line flunks the inner check, falls out, and gets picked up by an outer one. atomic keeps the flunk clean – backtrack past the whole - attempt instead of dying mid-token. That’s the entire offside rule. Three combinators. (Semantics is 001, lesson 4: elab_rules, match quotations of your category, recurse.)

Two landmines, paid for in core dumps so you don’t have to:

Command dispatch is token-indexed. The parser picks a command rule by hashing the literal leading token. Hide your keyword behind a category reference (syntax myThing : command where myThing starts with "tree ") and dispatch never finds it – the keyword string must sit in the command rule itself.
colGt geometry. “Strictly right of” sounds correct for children until a grandchild lands in the same column as an anchor two levels up and silently reattaches to the wrong parent. Draw the columns on graph paper. colGe against the right anchor beats colGt against the wrong one.

Lesson 5: notation that stays in its lane

001, lesson 2’s infixl grabs its operator globally – every importer eats it, like it or not. The scoped modifier makes notation lie dormant until its namespace gets opened:

namespace Frobnicate
scoped infixl:65 " <+> " => Nat.add
end Frobnicate

-- #eval 1 <+> 2        -- unknown token; notation's asleep
open Frobnicate in
#eval 1 <+> 2           -- 3

open ... in wakes it for exactly one declaration. Haskell can hide an operator behind an import list; it cannot make grammar blink in and out of existence. In Lean whole sublanguages ship this way. Exhibit A: Verso, the Lean documentation engine, exposes an HTML template language as scoped syntax over its Html type:

open Verso.Output.Html in
def hello (who : String) : Html :=
  {{ <ul> <li> "greetings, " {{ (who : Html) }} </li> </ul> }}

Under the open, {{ ... }} quotes honest-to-parser HTML; outside it, your {{ braces mean whatever they meant before. Splicing rides on coercions: Coe String Html inserts escaped text – injection-safe unless you ask otherwise – and a List Html coercion drops a .map straight into a template. Two literals round out the kit, both in the string chapter: interpolation s!"{via}: {weight}g" you’ve seen; raw r!"..." keeps CSS brace soup unescaped.

Logistics footnote that makes “just depend on Verso” a cheap call: lake builds by import closure, not by package. Import one module, compile that module’s transitive imports, done – however big the repo around it is. Dependencies bill per-module, not per-tarball.

Lesson 6: everything is an endofunction

Cheapest abstraction in the book: abbrev, a definition marked reducible so elaboration and instance search see straight through it. Ideal for naming a function type:

abbrev Cleanup := List Nat → List Nat

def dropZeros : Cleanup := List.filter (· != 0)
def ascending : Cleanup := (List.mergeSort · (· ≤ ·))

#eval (ascending ∘ dropZeros) [3, 0, 1]   -- [1, 3]
#eval [3, 0, 1] |> dropZeros |> ascending -- same thing, pipe order

Transformations as plain values of α → α, composed with ∘, piped with |>, identity is id. For the category theory crowd that’s an endomorphism monoid; for everyone else it’s function composition, no DSL, no interpreter, no Free, no ceremony. The host language’s function space is the algebra. List.mergeSort takes an explicit le : α → α → Bool and is stable – which is what makes single-key sorts compose: sort by one key, ties keep the order they arrived in.

One more pair: mutual and partial. Lean is a proof assistant; recursive definitions must visibly terminate – structurally or by well-founded measure – or the logic goes to lunch. Walking data that might contain cycles, no such proof exists, and partial is the honest opt-out:

mutual
  partial def walk (g : Graph) (n : Node) : Nat := 1 + visit g (next g n)
  partial def visit (g : Graph) (ns : List Node) : Nat :=
    ns.foldl (fun acc n => acc + walk g n) 0
end

mutual ... end admits mutual recursion. partial tells the kernel: compile it, run it, prove nothing about it – the return type must be Inhabited so the logic stays consistent while looking the other way. It’s a trade, not a defeat: pay in reasoning power, or pay in fuel parameters and a termination proof. For rendering code, partial is the right price. YMMV.

Queries now compose over the graph and one renderer draws it; the obvious next moves are more of both. Sooner or later some property will be worth proving instead of #eval-checking, and that’s rung 2 of 001’s ladder: the tactic language. Bring coffee.