Control Flow and Structures

Most languages let you lie to the compiler. Lean does not. There are no statements, only expressions. Every if produces a value. Every match is exhaustive or the compiler complains. Every recursive function must terminate or you must convince the system otherwise. Where imperative languages let you wave your hands, Lean demands you show your work.

Conditionals

Lean’s if-then-else is an expression, not a statement. Every branch must produce a value of the same type, and the entire expression evaluates to that value. There is no void, no implicit fall-through, no forgetting to return. The ternary operator that other languages treat as a curiosity is simply how conditionals work here.

-- If-then-else expressions
def absolute (x : Int) : Int :=
  if x < 0 then -x else x

#eval absolute (-5)   -- 5
#eval absolute 3      -- 3

-- Nested conditionals
def classifyNumber (n : Int) : String :=
  if n < 0 then "negative"
  else if n == 0 then "zero"
  else "positive"

#eval classifyNumber (-10)  -- "negative"
#eval classifyNumber 0      -- "zero"
#eval classifyNumber 42     -- "positive"

-- Conditionals are expressions, not statements
def minValue (a b : Nat) : Nat :=
  if a < b then a else b

#eval minValue 3 7  -- 3

Pattern Matching

Pattern matching with match expressions lets you destructure data and handle cases exhaustively. The compiler verifies you have covered every possibility, which eliminates an entire category of bugs that haunt languages where the default case is “do nothing and hope for the best.” You can match on constructors, literals, and multiple values simultaneously.

-- Pattern matching with match
def describeList {α : Type} (xs : List α) : String :=
  match xs with
  | [] => "empty"
  | [_] => "singleton"
  | [_, _] => "pair"
  | _ => "many elements"

#eval describeList ([] : List Nat)     -- "empty"
#eval describeList [1]                  -- "singleton"
#eval describeList [1, 2]               -- "pair"
#eval describeList [1, 2, 3, 4]         -- "many elements"

-- Matching on multiple values
def fizzbuzz (n : Nat) : String :=
  match n % 3, n % 5 with
  | 0, 0 => "FizzBuzz"
  | 0, _ => "Fizz"
  | _, 0 => "Buzz"
  | _, _ => toString n

#eval (List.range 16).map fizzbuzz
-- ["FizzBuzz", "1", "2", "Fizz", "4", "Buzz", ...]

-- Guards in pattern matching
def classifyAge (age : Nat) : String :=
  match age with
  | 0 => "infant"
  | n => if n < 13 then "child"
         else if n < 20 then "teenager"
         else "adult"

#eval classifyAge 5   -- "child"
#eval classifyAge 15  -- "teenager"
#eval classifyAge 30  -- "adult"

Simple Recursion

Recursive functions are fundamental to functional programming. A function processing a list works through elements one by one, patient and systematic, eventually reaching the empty case and returning upstream with its catch. In Lean, functions that call themselves must be shown to terminate. For simple structural recursion on inductive types like Nat or List, Lean can automatically verify termination.

-- Simple recursion on natural numbers
def factorial : Nat → Nat
  | 0 => 1
  | n + 1 => (n + 1) * factorial n

#eval factorial 5   -- 120
#eval factorial 10  -- 3628800

-- Recursion on lists
def sum : List Nat → Nat
  | [] => 0
  | x :: xs => x + sum xs

#eval sum [1, 2, 3, 4, 5]  -- 15

-- Computing the length of a list
def length {α : Type} : List α → Nat
  | [] => 0
  | _ :: xs => 1 + length xs

#eval length [1, 2, 3]  -- 3

Tail Recursion

Naive recursion can overflow the stack for large inputs because each recursive call adds a frame. Tail recursion solves this by restructuring the computation so the recursive call is the last operation, allowing the compiler to optimize it into a loop. Scheme mandated tail call optimization in 1975. Most other languages did not, which is why stack traces exist.

-- Naive recursion can overflow the stack for large inputs
-- Tail recursion uses an accumulator to avoid this

-- Tail-recursive factorial
def factorialTR (n : Nat) : Nat :=
  let rec go (acc : Nat) : Nat → Nat
    | 0 => acc
    | k + 1 => go (acc * (k + 1)) k
  go 1 n

#eval factorialTR 20  -- 2432902008176640000

-- Tail-recursive sum
def sumTR (xs : List Nat) : Nat :=
  let rec go (acc : Nat) : List Nat → Nat
    | [] => acc
    | x :: rest => go (acc + x) rest
  go 0 xs

#eval sumTR (List.range 1000)  -- Sum of 0..999

-- Tail-recursive reverse
def reverseTR {α : Type} (xs : List α) : List α :=
  let rec go (acc : List α) : List α → List α
    | [] => acc
    | x :: rest => go (x :: acc) rest
  go [] xs

#eval reverseTR [1, 2, 3, 4, 5]  -- [5, 4, 3, 2, 1]

Structural Recursion

Lean requires all recursive functions to terminate, which prevents you from accidentally writing infinite loops and passing them off as proofs. For simple cases where the recursive argument structurally decreases, Lean verifies termination automatically. For more complex cases, you must provide termination hints, essentially explaining to the compiler why your clever recursion scheme actually finishes. The termination checker is not easily fooled.

-- Lean requires recursion to be well-founded
-- Structural recursion on decreasing arguments is automatic

-- Merge two sorted lists into one sorted list
def merge : List Nat → List Nat → List Nat
  | [], ys => ys
  | xs, [] => xs
  | x :: xs, y :: ys =>
    if x ≤ y then x :: merge xs (y :: ys)
    else y :: merge (x :: xs) ys

-- Full merge sort: split at midpoint, recurse, merge
def mergeSort (xs : List Nat) : List Nat :=
  if h : xs.length < 2 then xs
  else
    let mid := xs.length / 2
    let left := xs.take mid
    let right := xs.drop mid
    have hl : left.length < xs.length := by
      have h1 : mid < xs.length := Nat.div_lt_self (by omega) (by omega)
      have h2 : left.length ≤ mid := List.length_take_le mid xs
      omega
    have hr : right.length < xs.length := by
      simp only [List.length_drop, right, mid]
      have : mid > 0 := Nat.div_pos (by omega) (by omega)
      omega
    merge (mergeSort left) (mergeSort right)
termination_by xs.length

#eval mergeSort [3, 1, 4, 1, 5, 9, 2, 6]  -- [1, 1, 2, 3, 4, 5, 6, 9]

The merge function is structurally recursive: each call operates on a smaller list. The mergeSort function is trickier. It splits the list at the midpoint and recurses on both halves. Lean cannot immediately see that take and drop produce shorter lists, so we provide have clauses that prove the lengths decrease. The termination_by xs.length annotation tells Lean to measure termination by list length rather than structural decrease.

Escape Hatches: partial and do

Sometimes you just want to compute something. The termination checker is a feature, not a prison. When proving termination would require more ceremony than the problem warrants, Lean provides escape hatches.

The partial keyword marks a function that might not terminate. Lean skips the termination proof and trusts you. The tradeoff: partial functions cannot be used in proofs since a non-terminating function could “prove” anything. For computation, this is often acceptable.

-- When termination is hard to prove, partial lets you skip the proof
partial def findFixpoint (f : Nat → Nat) (x : Nat) : Nat :=
  let y := f x
  if y == x then x else findFixpoint f y

#eval findFixpoint (· / 2 + 1) 100  -- 2

-- Sum even Fibonacci numbers below a bound (Project Euler #2)
partial def sumEvenFibsBelow (bound : Nat) : Nat := Id.run do
  let mut a := 0
  let mut b := 1
  let mut sum := 0
  while b < bound do
    if b % 2 == 0 then
      sum := sum + b
    let next := a + b
    a := b
    b := next
  return sum

#eval sumEvenFibsBelow 4000000  -- 4613732

The second example uses Id.run do to write imperative-looking code in a pure context. The Id monad is the identity monad, and Id.run extracts the final value. The mut keyword introduces mutable bindings; := reassigns them. Lean compiles this into pure functional operations. The resulting code is referentially transparent, but the syntax is familiar to programmers from imperative backgrounds.

This style shines for algorithms where the functional version would be contorted. Consider Project Euler Problem 2: sum even Fibonacci numbers below four million. The imperative version is direct. The pure functional version would thread accumulators through recursive calls, which is correct but harder to read.

Use partial when exploring, prototyping, or when the termination argument would distract from the actual logic. When you need to prove properties about the function, you will need to establish termination. But not everything needs to be a theorem. Sometimes you just want an answer.

Unless

The unless keyword is syntactic sugar for if not. When you find yourself writing if !condition then ..., the negation can obscure intent. With unless, the code reads closer to how you would describe it in English: “unless this is valid, bail out early.”

def validatePositive (n : Int) : IO (Option Int) := do
  unless n > 0 do
    return none
  return some n

#eval validatePositive 5    -- some 5
#eval validatePositive (-3) -- none

def processIfValid (values : List Int) : IO Unit := do
  for v in values do
    unless v >= 0 do
      continue
    IO.println s!"Processing: {v}"

The unless keyword works in do blocks as a guard clause. Combined with continue, it provides a clean way to skip iterations that fail some condition without nesting the rest of the loop body inside an if.

For Loops

For loops iterate over anything with a ForIn instance. Lists, arrays, ranges, and custom types all work uniformly. The syntax for x in collection do binds x to each element in turn.

def sumList (xs : List Nat) : Nat := Id.run do
  let mut total := 0
  for x in xs do
    total := total + x
  return total

#eval sumList [1, 2, 3, 4, 5]  -- 15

def sumRange (n : Nat) : Nat := Id.run do
  let mut total := 0
  for i in [0:n] do
    total := total + i
  return total

#eval sumRange 10  -- 45

def sumEvens (n : Nat) : Nat := Id.run do
  let mut total := 0
  for i in [0:n:2] do
    total := total + i
  return total

#eval sumEvens 10  -- 20

def findMax (arr : Array Int) : Option Int := Id.run do
  if arr.isEmpty then return none
  let mut maxVal := arr[0]!
  for x in arr do
    if x > maxVal then maxVal := x
  return some maxVal

#eval findMax #[3, 1, 4, 1, 5, 9, 2, 6]  -- some 9

The range syntax [start:stop] generates numbers from start up to but not including stop. Add a third component [start:stop:step] to control the increment. Unlike Python slices, these are exclusive on the right. Unlike C loops, there is no opportunity to mess up the bounds.

While Loops

While loops repeat until their condition becomes false. They work within do blocks using Id.run do for pure computation or directly in IO for effectful operations.

def countdownFrom (n : Nat) : List Nat := Id.run do
  let mut result : List Nat := []
  let mut i := n
  while i > 0 do
    result := i :: result
    i := i - 1
  return result.reverse

#eval countdownFrom 5  -- [5, 4, 3, 2, 1]

def gcd (a b : Nat) : Nat := Id.run do
  let mut x := a
  let mut y := b
  while y != 0 do
    let temp := y
    y := x % y
    x := temp
  return x

#eval gcd 48 18  -- 6
#eval gcd 17 13  -- 1

The while true do pattern with early return handles cases where the exit condition is easier to express as “stop when” rather than “continue while.” The GCD example uses the standard Euclidean algorithm, which terminates because the remainder strictly decreases.

Break and Continue

Lean’s continue skips to the next iteration; early return serves as break by exiting the entire function. There is no dedicated break keyword because the do notation’s early return provides the same control flow with clearer semantics.

def findFirst (xs : List Nat) (pred : Nat → Bool) : Option Nat := Id.run do
  for x in xs do
    if pred x then return some x
  return none

#eval findFirst [1, 2, 3, 4, 5] (· > 3)  -- some 4

def sumPositives (xs : List Int) : Int := Id.run do
  let mut total : Int := 0
  for x in xs do
    if x <= 0 then continue
    total := total + x
  return total

#eval sumPositives [1, -2, 3, -4, 5]  -- 9

def findInMatrix (m : List (List Nat)) (target : Nat) : Option (Nat × Nat) := Id.run do
  let mut i := 0
  for row in m do
    let mut j := 0
    for val in row do
      if val == target then return some (i, j)
      j := j + 1
    i := i + 1
  return none

#eval findInMatrix [[1,2,3], [4,5,6], [7,8,9]] 5  -- some (1, 1)

In nested loops, early return exits all the way out, which is usually what you want when searching. If you need to break only the inner loop while continuing the outer, restructure into separate functions.

Mutable State

The let mut syntax introduces mutable bindings within do blocks. Assignment uses :=, and the compiler tracks that mutations happen only within the do block’s scope. Under the hood, Lean transforms this into pure functional code by threading state through the computation.

def imperative_factorial (n : Nat) : Nat := Id.run do
  let mut result := 1
  let mut i := n
  while i > 0 do
    result := result * i
    i := i - 1
  return result

#eval imperative_factorial 5  -- 120

def fibPair (n : Nat) : Nat × Nat := Id.run do
  let mut a := 0
  let mut b := 1
  for _ in [0:n] do
    let temp := a + b
    a := b
    b := temp
  return (a, b)

#eval fibPair 10  -- (55, 89)

def buildReversed {α : Type} (xs : List α) : List α := Id.run do
  let mut result : List α := []
  for x in xs do
    result := x :: result
  return result

#eval buildReversed [1, 2, 3, 4]  -- [4, 3, 2, 1]

def demonstrate_assignment : Nat := Id.run do
  let mut x := 10
  x := x + 5
  x := x * 2
  return x

#eval demonstrate_assignment  -- 30

The Id.run do wrapper extracts the pure result from what looks like imperative code. The Id monad is the identity monad: it adds no effects, just provides the syntax. This pattern shines when the algorithm is naturally stateful but the result is pure.

Structures

Structures group related data with named fields. If you have used records in ML, structs in Rust, or data classes in Kotlin, the concept is familiar. Unlike C structs, Lean structures come with automatically generated accessor functions, projection notation, and none of the memory layout anxiety.

-- Structures group related data with named fields
structure Point where
  x : Float
  y : Float
  deriving Repr

-- Creating structure instances
def origin : Point := { x := 0.0, y := 0.0 }
def point1 : Point := Point.mk 3.0 4.0
def point2 : Point := ⟨1.0, 2.0⟩

-- Accessing fields
#eval point1.x  -- 3.0
#eval point1.y  -- 4.0

-- Functions on structures
def distance (p : Point) : Float :=
  Float.sqrt (p.x * p.x + p.y * p.y)

#eval distance point1  -- 5.0

The deriving Repr clause automatically generates a Repr instance, which lets #eval display the structure’s contents. Without it, Lean would not know how to print a Point. Other commonly derived instances include BEq for equality comparison with ==, Hashable for use in hash maps, and DecidableEq for propositional equality that can be checked at runtime. You can derive multiple instances by listing them: deriving Repr, BEq, Hashable. The Polymorphism article covers this in more detail.

Updating Structures

Rather than modifying structures in place, Lean provides the with syntax for creating new structures based on existing ones with some fields changed. This functional update pattern means you never have to wonder whether some other part of the code is holding a reference to your data and will be surprised by your mutations.

-- Updating structures with "with" syntax
def moveRight (p : Point) (dx : Float) : Point :=
  { p with x := p.x + dx }

def moveUp (p : Point) (dy : Float) : Point :=
  { p with y := p.y + dy }

#eval moveRight origin 5.0  -- { x := 5.0, y := 0.0 }

-- Multiple field updates
def translate (p : Point) (dx dy : Float) : Point :=
  { p with x := p.x + dx, y := p.y + dy }

#eval translate origin 3.0 4.0  -- { x := 3.0, y := 4.0 }

Nested Structures

Structures can contain other structures, allowing you to build complex data hierarchies. Lean’s projection notation makes accessing nested fields readable: person.address.city works as you would hope, without the verbose getter chains of enterprise Java.

-- Nested structures
structure Rectangle where
  topLeft : Point
  bottomRight : Point
  deriving Repr

def myRect : Rectangle := {
  topLeft := { x := 0.0, y := 10.0 },
  bottomRight := { x := 10.0, y := 0.0 }
}

def width (r : Rectangle) : Float :=
  r.bottomRight.x - r.topLeft.x

def height (r : Rectangle) : Float :=
  r.topLeft.y - r.bottomRight.y

def area (r : Rectangle) : Float :=
  width r * height r

#eval area myRect  -- 100.0

Default Values

Structures can have default values for their fields, making it easy to create instances with sensible defaults while overriding only specific fields.

-- Structures with default values
structure Config where
  host : String := "localhost"
  port : Nat := 8080
  debug : Bool := false
  deriving Repr

-- Use defaults
def defaultConfig : Config := {}

-- Override some defaults
def prodConfig : Config := { host := "api.example.com", port := 443 }

#eval defaultConfig  -- { host := "localhost", port := 8080, debug := false }
#eval prodConfig     -- { host := "api.example.com", port := 443, debug := false }

Inductive Types: Enumerations

Inductive types let you define custom data types by specifying their constructors. This is the core mechanism that makes Lean’s type system expressive: natural numbers, lists, trees, and abstract syntax all emerge from the same primitive. Simple enumerations have constructors with no arguments; more complex types carry data in each variant. Like Starfleet’s ship classification system, each variant is distinct and the compiler ensures you handle them all.

-- Simple enumerations
inductive Direction where
  | north
  | south
  | east
  | west
  deriving Repr, DecidableEq

def opposite : Direction → Direction
  | .north => .south
  | .south => .north
  | .east => .west
  | .west => .east

#eval opposite Direction.north  -- Direction.south

-- Starfleet vessel classes
inductive StarshipClass where
  | galaxy      -- Galaxy-class (Enterprise-D)
  | sovereign   -- Sovereign-class (Enterprise-E)
  | defiant     -- Defiant-class (compact warship)
  | intrepid    -- Intrepid-class (Voyager)
  | constitution -- Constitution-class (original Enterprise)
  deriving Repr, DecidableEq

def crewComplement : StarshipClass → Nat
  | .galaxy => 1014       -- Families welcome
  | .sovereign => 855     -- More tactical
  | .defiant => 50        -- Tough little ship
  | .intrepid => 141      -- Long-range science
  | .constitution => 430  -- The classic

#eval crewComplement StarshipClass.defiant  -- 50

-- Enums with associated data (MTG spell types)
inductive Spell where
  | creature (power : Nat) (toughness : Nat) (manaCost : Nat)
  | instant (manaCost : Nat)
  | sorcery (manaCost : Nat)
  | enchantment (manaCost : Nat) (isAura : Bool)
  deriving Repr

def manaCost : Spell → Nat
  | .creature _ _ cost => cost
  | .instant cost => cost
  | .sorcery cost => cost
  | .enchantment cost _ => cost

def canBlock : Spell → Bool
  | .creature _ toughness _ => toughness > 0
  | _ => false

#eval manaCost (Spell.creature 3 3 4)        -- 4 (e.g., a 3/3 for 4 mana)
#eval manaCost (Spell.instant 2)              -- 2 (e.g., Counterspell)
#eval canBlock (Spell.creature 2 1 1)         -- true
#eval canBlock (Spell.enchantment 3 true)     -- false

Recursive Inductive Types

Inductive types can be recursive, allowing you to define trees, linked lists, and other self-referential structures. This is where inductive types earn their name: you define larger values in terms of smaller ones, and the recursion has a base case that grounds the whole edifice.

-- Recursive inductive types
inductive BinaryTree (α : Type) where
  | leaf : BinaryTree α
  | node : α → BinaryTree α → BinaryTree α → BinaryTree α
  deriving Repr

-- Building trees
def exampleTree : BinaryTree Nat :=
  .node 1
    (.node 2 .leaf .leaf)
    (.node 3
      (.node 4 .leaf .leaf)
      .leaf)

-- Counting nodes
def BinaryTree.size {α : Type} : BinaryTree α → Nat
  | .leaf => 0
  | .node _ left right => 1 + left.size + right.size

#eval exampleTree.size  -- 4

-- Computing depth
def BinaryTree.depth {α : Type} : BinaryTree α → Nat
  | .leaf => 0
  | .node _ left right => 1 + max left.depth right.depth

#eval exampleTree.depth  -- 3

-- In-order traversal
def BinaryTree.inorder {α : Type} : BinaryTree α → List α
  | .leaf => []
  | .node x left right => left.inorder ++ [x] ++ right.inorder

#eval exampleTree.inorder  -- [2, 1, 4, 3]

Reading constructor type signatures takes practice. The node constructor has type α → BinaryTree α → BinaryTree α → BinaryTree α. In any arrow chain A → B → C → D, the last type is the return type; everything before is an input. So node takes a value of type α, a left subtree, a right subtree, and produces a tree. The leaf constructor takes no arguments and represents an empty position where the tree ends.

Parameterized Types

Inductive types can be parameterized, making them generic over the types they contain. This is how you write a List α that works for any element type, or an expression tree parameterized by its literal type. One definition, infinitely many instantiations.

-- Expression trees parameterized by the literal type
inductive Expr (α : Type) where
  | lit : α → Expr α
  | add : Expr α → Expr α → Expr α
  | mul : Expr α → Expr α → Expr α
  deriving Repr

-- Evaluate for any type with Add and Mul instances
def Expr.eval {α : Type} [Add α] [Mul α] : Expr α → α
  | .lit n => n
  | .add e1 e2 => e1.eval + e2.eval
  | .mul e1 e2 => e1.eval * e2.eval

-- Integer expression: (2 + 3) * 4
def intExpr : Expr Int := .mul (.add (.lit 2) (.lit 3)) (.lit 4)
#eval intExpr.eval  -- 20

-- Float expression: (1.5 + 2.5) * 3.0
def floatExpr : Expr Float := .mul (.add (.lit 1.5) (.lit 2.5)) (.lit 3.0)
#eval floatExpr.eval  -- 12.0

-- Map a function over all literals
def Expr.map {α β : Type} (f : α → β) : Expr α → Expr β
  | .lit n => .lit (f n)
  | .add e1 e2 => .add (e1.map f) (e2.map f)
  | .mul e1 e2 => .mul (e1.map f) (e2.map f)

-- Convert int expression to float
def floatFromInt : Expr Float := intExpr.map (fun n => Float.ofInt n)
#eval floatFromInt.eval  -- 20.0

Mutual Recursion

Sometimes you need multiple definitions that refer to each other, like even and odd functions that call each other, or a parser and its sub-parsers. Lean supports mutually recursive definitions within a mutual block. The termination checker handles these jointly, so your circular definitions must still demonstrably finish.

-- Mutually recursive definitions
mutual
  def isEven : Nat → Bool
    | 0 => true
    | n + 1 => isOdd n

  def isOdd : Nat → Bool
    | 0 => false
    | n + 1 => isEven n
end

#eval isEven 10  -- true
#eval isOdd 7    -- true

-- Mutually recursive types
mutual
  inductive Tree (α : Type) where
    | node : α → Forest α → Tree α

  inductive Forest (α : Type) where
    | nil : Forest α
    | cons : Tree α → Forest α → Forest α
end

-- Example forest
def exampleForest : Forest Nat :=
  .cons (.node 1 .nil)
    (.cons (.node 2 (.cons (.node 3 .nil) .nil))
      .nil)

FizzBuzz

FizzBuzz is the canonical “can you actually program” interview question, famous for filtering candidates who cannot write a loop. Pattern matching on multiple conditions makes it elegant: match on whether divisible by 3, whether divisible by 5, and the four cases fall out naturally.

def fizzbuzz' (n : Nat) : String :=
  match n % 3 == 0, n % 5 == 0 with
  | true,  true  => "FizzBuzz"
  | true,  false => "Fizz"
  | false, true  => "Buzz"
  | false, false => toString n

def runFizzbuzz (limit : Nat) : List String :=
  (List.range limit).map fun i => fizzbuzz' (i + 1)

#eval runFizzbuzz 15

Tip

Run from the repository: lake exe fizzbuzz 20

The Collatz Conjecture

The Collatz conjecture states that repeatedly applying a simple rule (halve if even, triple and add one if odd) eventually reaches 1 for any positive starting integer. Proposed in 1937, it remains unproven. Mathematicians have verified it for numbers up to \(2^{68}\), yet no one can prove it always works. Erdos said “Mathematics is not yet ready for such problems.”

The recursion here needs fuel (a maximum step count) because we cannot prove termination. If we could, we would have solved a famous open problem.

/-- The Collatz conjecture: every positive integer eventually reaches 1.
    Unproven since 1937, but we can at least watch the journey. -/
def collatzStep (n : Nat) : Nat :=
  if n % 2 == 0 then n / 2 else 3 * n + 1

def collatzSequence (n : Nat) (fuel : Nat := 1000) : List Nat :=
  match fuel with
  | 0 => [n]  -- give up, though Collatz would be disappointed
  | fuel' + 1 =>
    if n <= 1 then [n]
    else n :: collatzSequence (collatzStep n) fuel'

def collatzLength (n : Nat) : Nat :=
  (collatzSequence n).length

-- The famous 27: takes 111 steps and peaks at 9232
#eval collatzSequence 27
#eval collatzLength 27

-- Find the longest sequence for starting values 1 to n
def longestCollatz (n : Nat) : Nat × Nat :=
  (List.range n).map (· + 1)
    |>.map (fun k => (k, collatzLength k))
    |>.foldl (fun acc pair => if pair.2 > acc.2 then pair else acc) (1, 1)

#eval longestCollatz 100  -- (97, 119)

Tip

Run from the repository: lake exe collatz 27

Role Playing Game Example

The constructs above combine naturally in larger programs. What better way to demonstrate this than modeling the “real world”? We will build a Dungeons & Dragons character generator. D&D is a tabletop role-playing game where players create characters with ability scores, races, and classes, then embark on adventures guided by dice rolls and a referee called the Dungeon Master. The game has been running since 1974, which makes it older than most programming languages and considerably more fun than COBOL.

Structures hold character data, inductive types represent races and classes, pattern matching computes racial bonuses, and recursion drives the dice-rolling simulation.

We start by defining the data types that model our domain. The AbilityScores structure bundles the six core abilities. Inductive types enumerate races, classes, and backgrounds. The Character structure ties everything together:

structure AbilityScores where
  strength : Nat
  dexterity : Nat
  constitution : Nat
  intelligence : Nat
  wisdom : Nat
  charisma : Nat
  deriving Repr

inductive Race where
  | human
  | elf
  | dwarf
  | halfling
  | dragonborn
  | tiefling
  deriving Repr, DecidableEq

inductive CharClass where
  | fighter   -- d10 hit die
  | wizard    -- d6 hit die
  | rogue     -- d8 hit die
  | cleric    -- d8 hit die
  | barbarian -- d12 hit die
  | bard      -- d8 hit die
  deriving Repr, DecidableEq

inductive Background where
  | soldier
  | sage
  | criminal
  | noble
  | hermit
  | entertainer
  deriving Repr, DecidableEq

structure Character where
  name : String
  race : Race
  charClass : CharClass
  background : Background
  level : Nat
  abilities : AbilityScores
  hitPoints : Nat
  deriving Repr

Racial bonuses modify ability scores based on the character’s race. Pattern matching maps each race to its specific bonuses. Humans get +1 to everything; elves favor dexterity and intelligence; dwarves are sturdy:

def racialBonuses (r : Race) : AbilityScores :=
  match r with
  | .human      => { strength := 1, dexterity := 1, constitution := 1,
                     intelligence := 1, wisdom := 1, charisma := 1 }
  | .elf        => { strength := 0, dexterity := 2, constitution := 0,
                     intelligence := 1, wisdom := 0, charisma := 0 }
  | .dwarf      => { strength := 0, dexterity := 0, constitution := 2,
                     intelligence := 0, wisdom := 1, charisma := 0 }
  | .halfling   => { strength := 0, dexterity := 2, constitution := 0,
                     intelligence := 0, wisdom := 0, charisma := 1 }
  | .dragonborn => { strength := 2, dexterity := 0, constitution := 0,
                     intelligence := 0, wisdom := 0, charisma := 1 }
  | .tiefling   => { strength := 0, dexterity := 0, constitution := 0,
                     intelligence := 1, wisdom := 0, charisma := 2 }

Each character class has a different hit die, representing how much health they gain per level. Wizards are fragile with a d6, while barbarians are tanks with a d12:

def hitDie (c : CharClass) : Nat :=
  match c with
  | .wizard    => 6
  | .rogue     => 8
  | .bard      => 8
  | .cleric    => 8
  | .fighter   => 10
  | .barbarian => 12

Random character generation needs randomness. A linear congruential generator provides deterministic pseudo-random numbers, which means the same seed produces the same character:

structure RNG where
  state : Nat
  deriving Repr

def RNG.next (rng : RNG) : RNG × Nat :=
  let newState := (rng.state * 1103515245 + 12345) % (2^31)
  (⟨newState⟩, newState)

def RNG.range (rng : RNG) (lo hi : Nat) : RNG × Nat :=
  let (rng', n) := rng.next
  let range := hi - lo + 1
  (rng', lo + n % range)

D&D ability scores use 4d6-drop-lowest: roll four six-sided dice and discard the lowest. This generates scores between 3 and 18, heavily weighted toward the middle. We thread the RNG state through each dice roll to maintain determinism:

def roll4d6DropLowest (rng : RNG) : RNG × Nat :=
  let (rng1, d1) := rng.range 1 6
  let (rng2, d2) := rng1.range 1 6
  let (rng3, d3) := rng2.range 1 6
  let (rng4, d4) := rng3.range 1 6
  let dice := [d1, d2, d3, d4]
  let sorted := dice.toArray.qsort (· < ·) |>.toList
  let top3 := sorted.drop 1
  (rng4, top3.foldl (· + ·) 0)

def rollAbilityScores (rng : RNG) : RNG × AbilityScores :=
  let (rng1, str) := roll4d6DropLowest rng
  let (rng2, dex) := roll4d6DropLowest rng1
  let (rng3, con) := roll4d6DropLowest rng2
  let (rng4, int) := roll4d6DropLowest rng3
  let (rng5, wis) := roll4d6DropLowest rng4
  let (rng6, cha) := roll4d6DropLowest rng5
  (rng6, { strength := str, dexterity := dex, constitution := con,
           intelligence := int, wisdom := wis, charisma := cha })

Character generation threads the RNG through multiple operations: pick a name, race, class, and background, roll ability scores, apply racial bonuses, and calculate starting hit points:

def applyRacialBonuses (base : AbilityScores) (race : Race) : AbilityScores :=
  let bonus := racialBonuses race
  { strength := base.strength + bonus.strength
    dexterity := base.dexterity + bonus.dexterity
    constitution := base.constitution + bonus.constitution
    intelligence := base.intelligence + bonus.intelligence
    wisdom := base.wisdom + bonus.wisdom
    charisma := base.charisma + bonus.charisma }

def abilityModifier (score : Nat) : Int :=
  (score : Int) / 2 - 5

def startingHP (con : Nat) (c : CharClass) : Nat :=
  let conMod := abilityModifier con
  let baseHP := hitDie c
  if conMod < 0 && baseHP < conMod.natAbs then 1
  else (baseHP : Int) + conMod |>.toNat

def pickRandom {α : Type} (rng : RNG) (xs : List α) (default : α) : RNG × α :=
  match xs with
  | [] => (rng, default)
  | _ =>
    let (rng', idx) := rng.range 0 (xs.length - 1)
    (rng', xs[idx]?.getD default)

def allRaces : List Race := [.human, .elf, .dwarf, .halfling, .dragonborn, .tiefling]
def allClasses : List CharClass := [.fighter, .wizard, .rogue, .cleric, .barbarian, .bard]
def allBackgrounds : List Background := [.soldier, .sage, .criminal, .noble, .hermit, .entertainer]

-- Names that would make sense at both a D&D table and a PL theory conference
def fantasyNames : List String := [
  "Alonzo the Untyped",     -- Church, lambda calculus
  "Haskell the Memory Guzzler", -- I didn't choose the thunk life, the thunk life chose me
  "Dana the Continuous",    -- Scott, domain theory
  "Thorin Typechecker",     -- Tolkien meets compilation
  "Edsger the Structured",  -- Dijkstra, structured programming
  "Kurt the Incomplete"     -- Gödel, incompleteness theorems
]

def generateCharacter (seed : Nat) : Character :=
  let rng : RNG := ⟨seed⟩
  let (rng1, name) := pickRandom rng fantasyNames "Adventurer"
  let (rng2, race) := pickRandom rng1 allRaces .human
  let (rng3, charClass) := pickRandom rng2 allClasses .fighter
  let (rng4, background) := pickRandom rng3 allBackgrounds .soldier
  let (_, baseAbilities) := rollAbilityScores rng4
  let abilities := applyRacialBonuses baseAbilities race
  let hp := startingHP abilities.constitution charClass
  { name := name
    race := race
    charClass := charClass
    background := background
    level := 1
    abilities := abilities
    hitPoints := hp }

Display functions convert internal representations to human-readable strings. The modifier calculation implements D&D’s (score / 2 - 5) formula:

def raceName : Race → String
  | .human => "Human"
  | .elf => "Elf"
  | .dwarf => "Dwarf"
  | .halfling => "Halfling"
  | .dragonborn => "Dragonborn"
  | .tiefling => "Tiefling"

def className : CharClass → String
  | .fighter => "Fighter"
  | .wizard => "Wizard"
  | .rogue => "Rogue"
  | .cleric => "Cleric"
  | .barbarian => "Barbarian"
  | .bard => "Bard"

def backgroundName : Background → String
  | .soldier => "Soldier"
  | .sage => "Sage"
  | .criminal => "Criminal"
  | .noble => "Noble"
  | .hermit => "Hermit"
  | .entertainer => "Entertainer"

def formatModifier (score : Nat) : String :=
  let m := abilityModifier score
  if m >= 0 then s!"+{m}" else s!"{m}"

def printCharacter (c : Character) : IO Unit := do
  IO.println "======================================"
  IO.println s!"  {c.name}"
  IO.println "======================================"
  IO.println s!"  Level {c.level} {raceName c.race} {className c.charClass}"
  IO.println s!"  Background: {backgroundName c.background}"
  IO.println ""
  IO.println "  ABILITY SCORES"
  IO.println "  --------------"
  IO.println s!"  STR: {c.abilities.strength} ({formatModifier c.abilities.strength})"
  IO.println s!"  DEX: {c.abilities.dexterity} ({formatModifier c.abilities.dexterity})"
  IO.println s!"  CON: {c.abilities.constitution} ({formatModifier c.abilities.constitution})"
  IO.println s!"  INT: {c.abilities.intelligence} ({formatModifier c.abilities.intelligence})"
  IO.println s!"  WIS: {c.abilities.wisdom} ({formatModifier c.abilities.wisdom})"
  IO.println s!"  CHA: {c.abilities.charisma} ({formatModifier c.abilities.charisma})"
  IO.println ""
  IO.println s!"  Hit Points: {c.hitPoints}"
  IO.println s!"  Hit Die: d{hitDie c.charClass}"
  IO.println "======================================"

The main function reads a seed from command-line arguments (defaulting to 42), generates a character, and prints it in a formatted sheet:

def main (args : List String) : IO Unit := do
  let seed := match args.head? >>= String.toNat? with
    | some n => n
    | none => 42

  IO.println ""
  IO.println "  D&D CHARACTER GENERATOR"
  IO.println "  Type-Safe Adventures Await!"
  IO.println ""

  let character := generateCharacter seed

  printCharacter character

  IO.println ""
  IO.println "Your adventure begins..."
  IO.println "(Use a different seed for a different character: lake exe dnd <seed>)"

Try different seeds to generate different characters. The generator uses a deterministic pseudo-random number generator, so the same seed always produces the same character.

Tip

Run from the repository: lake exe dnd 42. The full source is on GitHub.

Toward Abstraction

With structures and inductive types, you can model complex domains. But real programs need abstraction over types themselves. Polymorphism and type classes let you write code that works for any type satisfying certain constraints. This is how you build generic libraries without sacrificing type safety.