0. Functional Programming in Lean

No knowledge of category theory is assumed.

These lectures use Lean 4 to build a theorem prover. Lean 4 is itself both a functional programming language and a theorem prover. The dual role is the central theme of the course: chapter 1 and chapter 2 construct a parser and a type checker by hand; chapter 3 and chapter 4 discuss the same machinery inside Lean; chapter 5 joins the two; chapter 6 proves some properties of the object language; and chapter 7 unfolds the hand-built evaluator into the abstract machine it secretly was. This chapter introduces some of the functional programming concepts needed to build the theorem prover: inductive types and pattern matching, failure as a value, input and output, recursion that provably terminates, and the monad, which is the interface organizing all of it.

The number guessing game

The program picks a secret number between 1 and 100; the player types guesses; the program answers too small, too large, or correct. The player gets seven guesses. Three small problems must be solved: reading a guess, comparing it against the secret, and looping.

The player's input arrives as a String, and turning text into a number is the first place something can go wrong, since the player may type anything. Lean's standard library answers with String.toNat?:

#check String.toNat?

#guard "42".toNat? == some 42
#guard "42x".toNat? == none
#guard "".toNat? == none

The return type Option Nat is an inductive type: a type whose values are exactly what its constructors build. Its two constructors are none and some n, so a function returning Option Nat announces in its type that failure is possible, and the type checker forces callers to say what happens in both cases. No exceptions, no null: failure is an ordinary value. And String.toNat? is also, in a modest sense, the first parser in these lectures: it consumes text and either produces a value or refuses, and chapter 1 grows this seed into a parser for a full language.

A remark on the #guard lines, which appear throughout these lectures: each one checks a proposition when the file is compiled, and compilation fails if the check does. They are not comments. Every piece of Lean on these pages is extracted from a checked build; what you read is what the compiler accepted.

#help command "#guard"

Comparing two numbers is the second problem; the standard library answers again, this time with an inductive type made to be consumed.

#guard compare 3 7 == Ordering.lt
#guard compare 7 7 == Ordering.eq
#guard compare 9 7 == Ordering.gt

Where a mathematician states a trichotomy, a functional programmer defines an inductive type. The function compare returns an Ordering, whose three constructors are lt, eq, and gt; the match in judge below handles each constructor exactly once, and the compiler checks that none is forgotten. We will define and match on inductive types constantly. The abstract syntax trees of chapter 1 are nothing else.

A guess can be wrong three ways: not a number at all, too small, too large; and the game as a whole can run out of guesses. The type Option could only say that something failed. An error is a value too, and an inductive type of errors can say which failure:

inductive GuessError where
  | notANumber
  | tooSmall
  | tooLarge
  | outOfFuel
deriving Repr, BEq

def describe : GuessError -> String
  | .notANumber => "Not a number."
  | .tooSmall => "Too small."
  | .tooLarge => "Too large."
  | .outOfFuel => "Out of guesses."

Judging a guess needs no keyboard and no screen, so it should not get them. We give the judgment a type that says exactly what it can do: succeed, or fail with a GuessError.

inductive Result (err a : Type) where
  | ok (x : a)
  | error (e : err)
deriving Repr, BEq

def Result.bind : Result err a -> (a -> Result err b) -> Result err b
  | .ok x, k => k x
  | .error e, _ => .error e

instance : Monad (Result err) where
  pure := .ok
  bind := .bind

Read Result err a as: a value of a, or an error of err. Its bind runs the rest of a computation only on success and passes an error through untouched, so an error, once raised, is thrown past everything that follows. The Monad instance hands this bind to do-notation; the class is the subject of the next section. The judgment is then three small functions:

def parseGuess (line : String) : Result GuessError Nat :=
  match line.trimAscii.toNat? with
  | none => .error .notANumber
  | some n => .ok n

def judge (secret guess : Nat) : Result GuessError Unit :=
  match compare guess secret with
  | .lt => .error .tooSmall
  | .gt => .error .tooLarge
  | .eq => .ok ()

def checkLine (secret : Nat) (line : String) : Result GuessError Unit := do
  let guess <- parseGuess line
  judge secret guess

#guard checkLine 42 "42" == .ok ()
#guard checkLine 42 "41" == .error .tooSmall
#guard checkLine 42 "100" == .error .tooLarge
#guard checkLine 42 "forty-two" == .error .notANumber

Two details are worth a pause. First, the success type of judge and checkLine is Unit, the type with exactly one value, written (). Success carries no news here; every bit of information rides in the error channel, and a correct guess is the absence of a complaint. The one-valued type returns as part of the object language in chapter 2. Second, checkLine is do-notation over Result GuessError, not over IO: when parseGuess fails, judge never runs, exactly as none short-circuited before, except the reason survives. And because all of this is pure, its behavior is checked at compile time: the #guard lines are the game's specification.

Only the loop touches the world:

def play (secret : Nat) : (fuel : Nat) -> IO Unit
  | 0 => IO.println (describe .outOfFuel ++ s!" It was {secret}.")
  | fuel + 1 => do
    IO.print "> "
    let line <- (<- IO.getStdin).getLine
    match checkLine secret line with
    | .ok () => IO.println "Correct."
    | .error e =>
      IO.println (describe e)
      play secret fuel

Read the type: play takes the secret and an amount of fuel, and returns an IO Unit. That value is not "nothing": it is a description of an interaction with the world which, when run, produces the uninformative (). Pure functions cannot read stdin; a value of type IO a is how Lean keeps effects inside the type discipline. The do block sequences such actions, one per line, and <- runs an action and binds its result; here it reads a line from standard input. The division of labor is exact: checkLine decides, IO reports.

The loop is the recursion: every wrong verdict prints its description and calls play secret fuel again. Lean does not accept recursive definitions on faith. It insists on a proof of termination, and recursion on fuel provides one silently: the match splits the fuel into 0 or fuel + 1, every recursive call uses the strictly smaller fuel, and when the fuel is spent the game ends and reveals the secret. The compiler produced and checked a termination proof without ceremony. It is the first theorem in these lectures, and nobody had to state it. Nor does the bound cost the player anything: binary search halves the interval 1..100 in at most seven steps, since $2^7 = 128 > 100$, so a careful player always wins. Lean does provide an escape hatch, partial def, for functions whose termination it cannot see, or that may truly run forever. The game needs no hatch; chapter 1 meets a loop where partiality is the honest answer, and takes it.

def guesses : Nat := 7

def main : IO Unit := do
  IO.println s!"I picked a number between 1 and 100. \
    You have {guesses} guesses."
  let secret <- IO.rand 1 100
  play secret guesses

Here IO.rand draws the secret, an action again: a pure function could hardly return a different number each run. Two small idioms round the program off. The fuel bound lives in one constant, guesses, so the greeting and the loop cannot drift apart; and the greeting is an interpolated string: inside s!"...", braces splice any printable value into the text, as the loop's farewell already did with the secret. And main itself is an ordinary definition of type IO Unit. The whole program is a value.

Monads: pure, map, join

The type Option carried failure; Result carried reasons; IO carried interaction. All three were used through the same two gestures: wrap a plain value, and sequence a step with what depends on its result. The shared structure has a name, and stating it needs nothing beyond Lean itself: a monad is a function on types equipped with three operations.

structure MonadOps (m : Type -> Type) where
  pure : {a : Type} -> (x : a) -> m a
  map : {a b : Type} -> (f : a -> b) -> (xs : m a) -> m b
  join : {a : Type} -> (xss : m (m a)) -> m a

Here m : Type -> Type is a function from types to types, such as List, Option, or Result GuessError; the braces mark arguments Lean fills in by itself. The lowercase m says it is a variable ranging over such functions, not any concrete one of them, and Lean's own Monad class spells it the same way. The field pure wraps a value; map applies an ordinary function underneath m; join collapses two layers of m into one.

The arrow associates to the right, so the type of map can be read as (a -> b) -> (m a -> m b): a function that turns an ordinary function into a function between containers, one level up. Functions taking or returning functions are called higher-order, and they are the daily bread of everything that follows. Two more conventions keep the parentheses away: application associates to the left, so Result err a reads (Result err) a, and application binds tighter than the arrow, which is why m a -> m b needs no parentheses to mean (m a) -> (m b). In symbols, the readings at a glance:

The three conventions return as grammar decisions in chapter 1. The standard library already has map for every container in sight:

#check @List.map
#check @Option.map

For lists, the other two operations are old friends: pure builds a one-element list, and join is concatenation.

def pure (x : a) : List a := [x]

def join : List (List a) -> List a
  | [] => []
  | xs :: xss => xs ++ join xss

#guard join [[1, 2], [], [3]] == [1, 2, 3]

The three operations obey laws, and the laws can be stated in Lean, as propositions; #check confirms each is a well-formed Prop:

section
variable {a : Type}

#check ∀ xs : List a, join [xs] = xs
#check ∀ xs : List a, join (xs.map pure) = xs
#check ∀ xsss : List (List (List a)), join (join xsss) = join (xsss.map join)

end

Read them aloud: joining a one-element list gives the element back; wrapping every element and then joining changes nothing; and when three layers collapse to one, it does not matter which two collapse first. A mathematician will recognize the shape at once: two unit laws and an associativity law, exactly as for a monoid. Making that recognition precise is the business of category theory, which these lectures do not use; the nLab entry under Further reading tells that story for whoever wants it. We state the laws and move on. That they can also be proved here, and what proving them costs, is the aside closing this chapter. The same two operations exist for Option, where join collapses nested partiality: a computation that may fail to produce a computation that may fail is just a computation that may fail.

def pure (x : a) : Option a := some x

def join : Option (Option a) -> Option a
  | some (some x) => some x
  | _ => none

#guard join (some (some 5)) == some 5
#guard join (some (none : Option Nat)) == none
#guard join (none : Option (Option Nat)) == none

Programs rarely apply join directly. The everyday operation is bind, which feeds each result of a first computation into a second, and it is a derived notion:

def bind (xs : List a) (k : a -> List b) : List b :=
  join (xs.map k)

#guard bind [1, 2, 3] (fun n => List.replicate n n) == [1, 2, 2, 3, 3, 3]
#guard bind [1, 2, 3] (fun n => List.replicate n n)
    == [1, 2, 3].flatMap (fun n => List.replicate n n)

def bind (x : Option a) (k : a -> Option b) : Option b :=
  join (x.map k)

#guard bind (some 4) (fun n => if n % 2 == 0 then some (n / 2) else none) == some 2
#guard bind (some 3) (fun n => if n % 2 == 0 then some (n / 2) else none) == none
#guard bind none (fun n => some (n + 1)) == none

For Option, bind reads: if the first step failed, fail; otherwise run the second on its result. That is exactly the short-circuiting that Result.bind performed in the game.

The binder names follow a convention these lectures keep from here on: a plain function of type a -> b, such as the one map takes, is called f, while a function of type a -> m b, such as the one bind takes, is called k, for continuation: the rest of the computation.

The derivation runs backwards too. Given bind and pure, both map and join are one-liners:

def mapViaBind [Monad m] (f : a -> b) (x : m a) : m b :=
  x >>= fun y => pure (f y)

def joinViaBind [Monad m] (x : m (m a)) : m a :=
  x >>= id

#guard mapViaBind (· + 1) (some 2) == some 3
#guard joinViaBind (some (some 5)) == some 5

The whole dictionary fits in one table: join and map define bind, and bind, with pure, defines both map and join:

So (pure, map, join) and (pure, bind) present the same structure, and which is primitive is a matter of interface, not substance. Lean chose bind: the Monad type class provides pure and bind, written infix as >>=, and do-notation is sugar over them. Join is the concept; bind is the interface.

Lean's core library ships no Monad List instance: it was removed for performance issues, discussed in the Zulip thread under Further reading, and that is why this chapter defined the list operations by hand.

The wrapping operation is called $\operatorname{unit}$ in mathematics, pure in Lean, and return in Haskell. The Haskell name is famously unfortunate, suggesting a jump out of the function that never happens. Lean does keep a return for exactly that intuition, but as a piece of do-notation rather than a function: a macro that makes its argument the result of the enclosing do block. The function is pure.

Do-notation

To see that do-notation is nothing but bind, one computation is written three ways: parse two strings, then divide the first number by the second, refusing division by zero.

def div? (m n : Nat) : Option Nat :=
  if n == 0 then none else some (m / n)

First, with bind spelled out:

def ratioBind (s t : String) : Option Nat :=
  s.toNat?.bind fun m =>
    t.toNat?.bind fun n =>
      div? m n

Each fun is the rest of the computation, waiting for the previous step's result; a none anywhere short-circuits the whole chain. Second, the same definition with the infix operator:

def ratioInfix (s t : String) : Option Nat :=
  s.toNat? >>= fun m =>
    t.toNat? >>= fun n =>
      div? m n

Third, in do-notation:

def ratioDo (s t : String) : Option Nat := do
  let m <- s.toNat?
  let n <- t.toNat?
  div? m n

This is not a third semantics: do is notation the compiler expands into exactly the binds above. In most languages such a claim would be a remark about the compiler; here it is checked, and the checking introduces the most important word in these lectures:

#guard ratioDo "10" "4" == some 2
#guard ratioDo "10" "0" == none
#guard ratioDo "1o" "4" == none

example : ratioBind = ratioInfix := rfl
example : ratioInfix = ratioDo := rfl

An example ... := rfl states an equality and proves it by reflexivity: rfl succeeds precisely when both sides compute to the same normal form. Equality by computation is called definitional equality, and it is the load-bearing notion of chapter 2, where our type checker must decide it for the object language. Here it quietly certifies that three spellings are one definition.

A two-step chain hardly shows what the notation buys, so chase indices through a list, five lookups deep, each hop starting from the result of the previous one and each allowed to fall off the end:

def hop (xs : List Nat) (i : Nat) : Option Nat :=
  xs[i]?

def chaseBind (xs : List Nat) (start : Nat) : Option Nat :=
  (hop xs start).bind fun a =>
    (hop xs a).bind fun b =>
      (hop xs b).bind fun c =>
        (hop xs c).bind fun d =>
          hop xs d

Written with bind, the chain is a staircase. Every step indents one level deeper than the last, and each new name appears at the end of its line, behind the operation that produces it. In do-notation the same chain is flat:

• one step per line, all at the same depth;
• each new name stands first on its line, where a reader scanning the left margin will find it.

Nothing changes but the spelling, as the rfl confirms:

def chaseDo (xs : List Nat) (start : Nat) : Option Nat := do
  let a <- hop xs start
  let b <- hop xs a
  let c <- hop xs b
  let d <- hop xs c
  hop xs d

example : chaseBind = chaseDo := rfl

#guard chaseDo [1, 2, 3, 4, 5, 0] 0 == some 5
#guard chaseDo [9] 0 == none

Lists and the left fold

Lists have already surfaced twice: the index chase hopped through one, and the list monad's join concatenated them. The type itself deserves a look, and #print shows it to be an inductive type like the others, with two constructors: nil, the empty list, written []; and cons, an element in front of a shorter list, written infix as ::. The bracket literals are sugar for a chain of conses:

#print List

#guard [1, 2, 3] == 1 :: 2 :: 3 :: []

Functions over lists will be structural recursions, the same gesture that consumed fuel and Ordering above; before writing them, it pays to know that such recursions come in two shapes. The classic exhibit is a pair of factorials, and it opens section 1.2.1 of Abelson and Sussman's Structure and Interpretation of Computer Programs. The first factorial multiplies after its recursive call returns:

def factorial : Nat -> Nat
  | 0 => 1
  | n + 1 => (n + 1) * factorial n

#guard factorial 4 == 24

Unfolding a call by hand shows the shape the book names a linear recursive process: a growing wedge of deferred multiplications, expanding until the base case arrives and only then collapsing:

The second factorial keeps a running product and finishes each multiplication before it recurses, so nothing is ever deferred:

def factIter (product : Nat) : Nat -> Nat
  | 0 => product
  | n + 1 => factIter (product * (n + 1)) n

#guard factIter 1 4 == 24

The same unfolding now stays flat. Every line is a complete summary of where the computation stands, and the last call already holds the answer; the book names this shape a linear iterative process. The extra argument that makes it possible has a standard name of its own, the accumulator:

A left fold is the iterative shape, packaged. The function foldl takes a step function, a starting accumulator, and a list, and pushes the accumulator through the list from the left; the factorial loop falls out as the special case where the list holds the counters:

def foldl (step : b -> a -> b) (acc : b) : List a -> b
  | [] => acc
  | x :: xs => foldl step (step acc x) xs

#guard foldl (fun product n => product * n) 1 [1, 2, 3, 4] == 24

Four everyday list functions, written first the way this chapter has written everything so far, one match apiece with recursion doing the looping: len counts, concat stitches two lists into one, rev reverses by sending each head to the far end, and filter keeps the elements that pass a test:

def len : List a -> Nat
  | [] => 0
  | _ :: xs => len xs + 1

def concat : List a -> List a -> List a
  | [], ys => ys
  | x :: xs, ys => x :: concat xs ys

def rev : List a -> List a
  | [] => []
  | x :: xs => concat (rev xs) [x]

def filter (p : a -> Bool) : List a -> List a
  | [] => []
  | x :: xs => if p x then x :: filter p xs else filter p xs

#guard len ["a", "b", "c"] == 3
#guard concat [1, 2] [3, 4] == [1, 2, 3, 4]
#guard rev [1, 2, 3] == [3, 2, 1]
#guard filter (fun n => n % 2 == 0) [1, 2, 3, 4, 5, 6] == [2, 4, 6]

The same four again, this time as folds. Two are a perfect fit: lenFold pushes a counter down the list, and revFold is the accumulator trick in its purest form, consing each element onto the answer so far, which also makes it one linear pass where rev above walks its entire result once per element. The other two must lean on reversal: a left fold hands over elements in list order but builds its result front-first, so concatFold pours a reversed copy of the first list onto the second, and filterFold reverses its harvest at the end. The comparison is the lesson: match spells a recursion out and follows the list's own shape, while foldl names a loop shape and commits to it, a perfect fit for some functions and a visible contortion for others.

def lenFold (xs : List a) : Nat :=
  foldl (fun n _ => n + 1) 0 xs

def revFold (xs : List a) : List a :=
  foldl (fun acc x => x :: acc) [] xs

def concatFold (xs ys : List a) : List a :=
  foldl (fun acc x => x :: acc) ys (revFold xs)

def filterFold (p : a -> Bool) (xs : List a) : List a :=
  revFold (foldl (fun acc x => if p x then x :: acc else acc) [] xs)

#guard lenFold ["a", "b", "c"] == 3
#guard revFold [1, 2, 3] == [3, 2, 1]
#guard concatFold [1, 2] [3, 4] == [1, 2, 3, 4]
#guard filterFold (fun n => n % 2 == 0) [1, 2, 3, 4, 5, 6] == [2, 4, 6]

Comprehending monads, literally

Set-builder notation is everyday mathematics: a set like $\{\, x \cdot y \mid x \in A,\; y \in B \,\}$. Its programming twin is the list comprehension, everyday Python: [x * y for x in xs for y in ys]. Wadler's Comprehending monads earned its title by showing that the shared notation is monad notation in disguise.

Lean does not ship a comprehension syntax, so these lectures conjure one: a fresh syntax category and a handful of productions and macro rules; building notation is the subject of chapter 3, and nothing below depends on how the notation is implemented. For present purposes, it suffices to examine the comprehension syntax examples below.

The desugaring is nothing but the bind and pure of this chapter, so the notation works for every monad at once, and the list instance it needs is exactly the one this chapter already built by hand.

declare_syntax_cat compClause

syntax ident " in " term : compClause

syntax "[" term " | " compClause,+ "]" : term

macro_rules
  | `([$e | $x:ident in $xs]) => `(($xs) >>= fun $x => pure $e)
  | `([$e | $x:ident in $xs, $cs,*]) => `(($xs) >>= fun $x => [$e | $cs,*])

#guard [x + y | x in some 1, y in some 2] == some 3
#guard [x + 1 | x in (none : Option Nat)] == none

instance : Monad List where
  pure := ListMonad.pure
  bind := ListMonad.bind

#guard [x * y | x in [1, 2, 3], y in [10, 20]]
    == [10, 20, 20, 40, 30, 60]

A guard clause joins the grammar: a condition prunes the results, and pruning means the empty list, so this one clause is list-specific where the generators work for any monad; Wadler's paper does it generally, with a monadic zero.

syntax "if " term : compClause

macro_rules
  | `([$e | if $c]) => `(if $c then pure $e else [])
  | `([$e | if $c, $cs,*]) => `(if $c then [$e | $cs,*] else [])

A truth table. The set comprehends over every valuation of three propositional letters and records the verdict of $(p \land q) \to r$ beside each:

Spelled out as the table it is:

The program is the same three generators, and the pinned list is that table, row by row, all eight falsifying none but the one where the antecedent holds and the consequent fails:

def bools : List Bool := [true, false]

#guard [(p, q, r, !(p && q) || r) | p in bools, q in bools, r in bools]
    == [(true, true, true, true), (true, true, false, false),
        (true, false, true, true), (true, false, false, true),
        (false, true, true, true), (false, true, false, true),
        (false, false, true, true), (false, false, false, true)]

The diagonal of the x-y integer plane, cut to a finite window. The set has two descriptions, a filter over the square and a direct image of the axis:

On the board, with rows reading $y$ downward and columns $x$ rightward over the window $A = \{-2, \dots, 2\}$, the diagonal is the rising line it ought to be:

The comprehensions transcribe both sides, and the two #guards check each against the diagonal written out and against each other:

def axis : List Int := [-2, -1, 0, 1, 2]

#guard [(x, y) | x in axis, y in axis, if x == y]
    == [(-2, -2), (-1, -1), (0, 0), (1, 1), (2, 2)]

#guard [(x, y) | x in axis, y in axis, if x == y]
    == [(x, x) | x in axis]

Lawful monads

A mathematician will have noticed the sleight of hand: we exhibited a structure with unit-and-associativity laws and never imposed them. The objection deserves a direct answer, and Lean's answer is characteristic: the operations and the laws are separate interfaces: Monad is the programming interface, and the laws live in a second class:

#check @LawfulMonad

The class LawfulMonad is a structure whose fields are propositions: the unit and associativity laws, stated in the same language as the programs they govern. This is the first sighting of the central fact of these lectures. In a dependently typed language, statements are types, so an algebraic structure can carry its own axioms. Down the road, chapter 6 states theorems about our object language exactly the way these laws are stated about bind.

Why does the programming interface not require the laws?

• Proving them is possible but not free. For this chapter's monads the proofs are case splits, and the standard library in fact proves them for the instances it ships, Option among them. But laws about function-valued types need function extensionality, transformer stacks (chapter 4) turn the proofs into boilerplate that scales badly, and for IO the equations miss the point: what matters is the effect on the world, which equality between values does not see.
• Some monads are unlawful by design. QuickCheck-style random generators split the random seed at each bind, so that generation parallelizes and shrinking is reproducible; Plausible is the Lean incarnation of the idea. Seed-splitting breaks associativity of bind on the nose, and everyone involved considers the trade excellent. Parser libraries in the megaparsec tradition likewise tune their choice operator for the quality of error messages rather than for the algebraic laws of choice, and chapter 1 makes the same trade and will name it when it does.
• Many such structures are lawful up to observational equivalence, just not up to the strict equality that propositions default to. A mathematician knows this distinction from strict versus non-strict structures; declining to track the coherence is a legitimate engineering stance.

Propositions as types

The aside above pointed at the central fact once; it deserves its own three lines:

• propositions as types: a statement is the type of its evidence;
• proofs as programs: to prove a proposition is to construct a value of that type;
• simplification of proofs as evaluation of programs: the computation that ran the guessing game is the same mechanism that turns a roundabout proof into a direct one, which is why the rfl proofs earlier in this chapter could decide equalities by computing.

The correspondence has a century of history and several independent discoverers, and one canonical modern telling, Wadler's Propositions as Types, under Further reading. These lectures walk the programming side of the bridge; the proving side is the same bridge.

The symmetry is concrete enough to walk in both directions. Here is a theorem, the commutativity of addition, proved by pure terms and no tactics: each proof is a recursive function, its induction spelled as the same structural recursion the game used, with congrArg playing "apply successor to both sides". The declarations say def rather than theorem to make the point bluntly, and their names follow the lemma convention, snake_case for mathematics where programs are lowerCamel. The proofs also debut the low-precedence application operator $: everything to its right is one argument, so chains of lemma applications shed their parentheses. Taken to its limit, composing away the arguments themselves is a whole aesthetic called point-free style, and pointfree.io, under Further reading, converts expressions to it for amusement and occasional enlightenment.

def zero_add : (n : Nat) -> 0 + n = n
  | 0 => rfl
  | n + 1 => congrArg (· + 1) $ zero_add n

def succ_add : (m n : Nat) -> (m + 1) + n = (m + n) + 1
  | _, 0 => rfl
  | m, n + 1 => congrArg (· + 1) $ succ_add m n

def add_comm : (m n : Nat) -> m + n = n + m
  | m, 0 => .symm $ zero_add m
  | m, n + 1 =>
    Eq.trans (congrArg (· + 1) $ add_comm m n) $ .symm $ succ_add n m

And here is a program built by tactics, the language Lean users normally reserve for proving: intro receives the pair, constructor splits the goal in two, and each exact supplies a component. The goal was never a proposition, and the tactics did not care, because underneath there is only one activity: producing a term of a type.

def swapPair : Int × Int -> Int × Int := by
  intro p
  constructor
  · exact p.2
  · exact p.1

#guard swapPair (1, -2) == (-2, 1)

Could the definition be a theorem instead? Lean refuses, and the refusal is informative: the theorem keyword polices the bridge, demanding a proposition. The two vocabularies elaborate the same way; the words record intent, and one practical difference rides on them, since proofs never need to run while programs do.

/--
error: type of theorem `Course.Chapter0_FunctionalProgramming.swapPairThm` is not a proposition
  Int × Int → Int × Int
-/
#guard_msgs in
theorem swapPairThm : Int × Int -> Int × Int := by
  intro p
  constructor
  · exact p.2
  · exact p.1

Wrapped in the chapter's usual IO edge, the tactic-built function reads two integers split by a space, swaps them, and prints. Each refutable let pattern either matches or falls to its vertical-bar alternative, an early exit that keeps the happy path flat, the same virtue the chaseDo example claimed for do-notation:

def swapMain : IO Unit := do
  let line <- (<- IO.getStdin).getLine
  let [a, b] := line.trimAscii.toString.splitOn " "
    | IO.println "expected two integers"
  let some m := a.toInt?
    | IO.println s!"{a} is not an integer"
  let some n := b.toInt?
    | IO.println s!"{b} is not an integer"
  let (x, y) := swapPair (m, n)
  IO.println s!"{x} {y}"

List theorems

The addition lemmas were a demonstration; the same craft can earn its keep on this chapter's own definitions. Two facts about concat deserve the name of theorem: concatenation adds lengths, and concatenation is associative. Each proof is again a recursive function whose recursion is the induction, this time on a list, one arm per constructor, and the length theorem consumes zero_add and succ_add from a moment ago as its lemmas:

def len_concat : (xs ys : List a) -> len xs + len ys = len (concat xs ys)
  | [], ys => zero_add (len ys)
  | _ :: xs, ys =>
    Eq.trans (succ_add (len xs) (len ys)) $
      congrArg (· + 1) $ len_concat xs ys

Associativity needs no helper lemmas at all: the nil case is rfl, and the cons case is congrArg again, "cons x to both sides of the induction hypothesis". The statement itself should look familiar: it is the associativity underneath the join law stated for lists earlier, one of the laws the section on lawful monads priced as provable but not free. That associativity, at least, is proved outright:

def concat_assoc : (xs ys zs : List a) ->
    concat (concat xs ys) zs = concat xs (concat ys zs)
  | [], _, _ => rfl
  | x :: xs, ys, zs => congrArg (x :: ·) $ concat_assoc xs ys zs

A dependently typed language offers one more move: rather than prove the length equation after the fact, carry it in the type. The inductive family Vec a n makes the length an index: the types say that nil has length zero, that cons adds one, and that appending must therefore announce a sum. The theorem len_concat has moved into a signature, checked by the elaborator at every use instead of proved once:

inductive Vec (a : Type) : Nat -> Type where
  | nil : Vec a 0
  | cons : a -> Vec a n -> Vec a (n + 1)

def Vec.append : Vec a m -> Vec a n -> Vec a (n + m)
  | .nil, ys => ys
  | .cons x xs, ys => .cons x (append xs ys)

example :
    Vec.append (.cons 1 .nil) (.cons 2 (.cons 3 .nil))
      = .cons 1 (.cons 2 (.cons 3 .nil)) := rfl

One detail rewards a second look: the result index reads n + m, the second length first. Addition on Nat recurses on its right argument, so n + 0 and n + (m + 1) unfold by definition exactly where the two match arms need them to, while the prettier m + n would need add_comm spliced into the definition. Indices make definitional equality a daily concern, the notion chapter 2 must decide for the object language; and the intrinsically typed terms of chapter 6 are this vector's idea grown up, a syntax tree indexed by its own type.

More monads

The state monad threads one updatable value through a computation, and its definition here is an inductive type, deliberately: get and put are the commands of a tiny language, pure and bind are its glue, and a stateful program is a tree built from the four. The inductive definition gives the syntax:

inductive State (s : Type) : Type -> Type 1 where
  | get : State s s
  | put : s -> State s Unit
  | pure : a -> State s a
  | bind : State s a -> (a -> State s b) -> State s b

instance : Monad (State s) where
  pure := .pure
  bind := .bind

A tree does nothing on its own, which is a sentence this chapter has said before: an IO action, too, was a description waiting for a runner. What acts is the interpreter. The function runState takes an initial state and a program and returns the program's answer paired with the state left behind; each command's meaning is one line, and the bind arm is exactly the threading that do-notation has been hiding all along. The inductive definition gave the syntax; the function that executes it gives the interpreter:

def runState (init : s) : State s a -> a × s
  | .get => (init, init)
  | .put st => ((), st)
  | .pure x => (x, init)
  | .bind xs k =>
    let (x, st) := runState init xs
    runState st (k x)

Do-notation comes for free with the Monad instance, and the classic use of state is a supply of fresh numbers: each call to fresh answers with the current count and advances it. Running the program from zero shows both answers and the final state:

def fresh : State Nat Nat := do
  let n <- State.get
  State.put (n + 1)
  pure n

#guard runState 0 (do
    let x <- fresh
    let y <- fresh
    pure (x, y))
  == ((0, 1), 2)

The section on lawful monads mentioned structures lawful only up to observational equivalence, and this State is the cleanest specimen on the page. As trees, State.bind (State.pure x) k and k x are plainly different values, one of them having a bind at its root, so the first unit law fails on the nose. Interpret them, and the difference is gone, by rfl, for every k:

example (init : s) (x : a) (k : a -> State s b) :
    runState init (State.bind (State.pure x) k) = runState init (k x) := rfl

Lean's own state monad, which chapter 4 reaches through the transformer story, keeps no tree: there a computation is the function from initial state to answer-and-final-state, every program already interpreted. The tree form is the one worth remembering, because its two halves are the working shape of everything ahead: an inductive type for the syntax and a function for its meaning is chapter 1 building trees, chapter 2 evaluating them, and chapter 7 turning that evaluator into a machine.

The identity monad is the opposite bookend, the monad that adds nothing: wrapping a value does nothing, and binding is application with the arguments reversed. Do-notation over it is plain sequencing, every step an ordinary definition; it is what remains of a monad when the effect is taken away, and its interpreter has nothing to do. Lean ships the same monad as Id, its runIdentity spelled Id.run; the header Id.run do is everyday Lean for a pure function that wants do-notation's flat sequencing, and chapter 4's transformer stacks bottom out on the same monad:

def Identity (a : Type) : Type := a

instance : Monad Identity where
  pure x := x
  bind x k := k x

def runIdentity (x : Identity a) : a := x

#guard runIdentity (do
    let x <- pure 2
    let y <- pure (x * 10)
    pure (y + 1))
  == 21

#check @Id.run

Functional pearls

Functional programming has a literature of short papers written to be read for pleasure, which the community calls functional pearls, and these lectures will point at a few as they go. Three to start with, introduced no further, because their abstracts speak for themselves:

• Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire
• Data types à la carte
• Use and abuse of instance parameters in the Lean mathematical library
• ...... ......

Further reading

• Functional Programming in Lean. <- back
• Abelson and Sussman, Structure and Interpretation of Computer Programs: the linked section 1.2.1, Linear Recursion and Iteration, is the two-factorials comparison this chapter replays on lists. <- back
• Comprehending monads: the link is Wadler's collected page on monads, which includes this paper. <- back
• monad in the nLab: the category-theoretic account, where the monoid shape of the three operations and their laws is made precise. Nothing in these lectures depends on it. <- back
• Wadler, Propositions as Types: the correspondence in full, with its history. <- back
• pointfree.io. <- back
• Nederpelt and Geuvers, Type Theory and Formal Proof: An Introduction: a gentle, step-by-step introduction to type theory and lambda calculus. <- back
• Programming Language Foundations in Agda. <- back
• Brady, Type-Driven Development with Idris: note that the language has since moved on; the current version is Idris 2. <- back
• Meijer, Fokkinga, and Paterson, Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire. <- back
• optics: the Haskell library for lenses. <- back
• Swierstra, Data types à la carte. <- back
• Baanen, Use and abuse of instance parameters in the Lean mathematical library. <- back
• Option do notation regression?. <- back
• Purification: the Idris pull request deprecating return in favor of pure. <- back
• Rydeheard and Burstall, Computational Category Theory. <- back