Module 2 · Lesson 3

Recursive Data

Inductive types can refer to themselves, enabling powerful data structures like linked lists and trees.

Building a Linked List

Let's implement a generic linked list from scratch to understand how recursion works in data types:

lean

1inductive MyList (α : Type) where
2  | nil : MyList α                        -- Empty list
3  | cons : α → MyList α → MyList α        -- Element + rest of list
4  deriving Repr
5
6-- Create some lists
7def empty : MyList Nat := MyList.nil
8def oneItem : MyList Nat := MyList.cons 1 MyList.nil
9def threeItems : MyList Nat := 
10  MyList.cons 1 (MyList.cons 2 (MyList.cons 3 MyList.nil))
11
12#eval threeItems  -- MyList.cons 1 (MyList.cons 2 (MyList.cons 3 MyList.nil))

The key insight: cons takes an element and another MyList. This self-reference is what makes the type recursive.

Functions on Recursive Types

Functions on recursive types are typically recursive themselves:

lean

1inductive MyList (α : Type) where
2  | nil : MyList α
3  | cons : α → MyList α → MyList α
4  deriving Repr
5
6-- Length of a list
7def MyList.length : MyList α → Nat
8  | nil => 0
9  | cons _ tail => 1 + tail.length
10
11-- Sum of a list of Nats
12def MyList.sum : MyList Nat → Nat
13  | nil => 0
14  | cons head tail => head + tail.sum
15
16def nums : MyList Nat := MyList.cons 1 (MyList.cons 2 (MyList.cons 3 MyList.nil))
17
18#eval nums.length  -- 3
19#eval nums.sum     -- 6

💡

A small choice with large consequences: write tail.length + 1 rather than 1 + tail.length. Both compute the same number, but n + 1 is definitionally Nat.succ n, so later proofs by induction, rfl, and simp line up without an extra Nat.add_comm step. The standard library writes it this way throughout, and matching that convention makes your lemmas compose with theirs.

Structural Recursion

Lean enforces termination by requiring recursive calls on smaller pieces of data. This is called structural recursion.

lean

1inductive MyList (α : Type) where
2  | nil : MyList α
3  | cons : α → MyList α → MyList α
4
5def MyList.last? : MyList α → Option α
6  | nil => none
7  | cons x nil => some x
8  | cons _ xs => xs.last?

Key Takeaway

The recursive structure of the type guides the recursive structure of functions. Base case (nil) → base result. Recursive case (cons) → recursive call on the tail.

Binary Trees

Trees are another classic recursive structure:

lean

1inductive BinaryTree (α : Type) where
2  | leaf : BinaryTree α
3  | node : α → BinaryTree α → BinaryTree α → BinaryTree α
4  deriving Repr
5
6open BinaryTree
7
8--     2
9--    / \
10--   1   3
11def myTree : BinaryTree Nat :=
12  node 2 (node 1 leaf leaf) (node 3 leaf leaf)
13
14-- Count nodes in a tree
15def BinaryTree.size : BinaryTree α → Nat
16  | leaf => 0
17  | node _ left right => 1 + left.size + right.size
18
19-- Calculate depth/height
20def BinaryTree.depth : BinaryTree α → Nat
21  | leaf => 0
22  | node _ left right => 1 + max left.depth right.depth
23
24#eval myTree.size   -- 3
25#eval myTree.depth  -- 2

Mapping Over Recursive Structures

A common operation is applying a function to every element:

lean

1inductive MyList (α : Type) where
2  | nil : MyList α
3  | cons : α → MyList α → MyList α
4  deriving Repr
5
6def MyList.map (f : α → β) : MyList α → MyList β
7  | nil => nil
8  | cons head tail => cons (f head) (tail.map f)
9
10def nums := MyList.cons 1 (MyList.cons 2 (MyList.cons 3 MyList.nil))
11
12#eval nums.map (· * 2)  -- MyList.cons 2 (MyList.cons 4 (MyList.cons 6 MyList.nil))
13#eval nums.map toString -- MyList.cons "1" (MyList.cons "2" (MyList.cons "3" MyList.nil))

Expression Trees

Recursive types are perfect for representing expressions:

lean

1inductive Expr where
2  | num : Int → Expr
3  | add : Expr → Expr → Expr
4  | mul : Expr → Expr → Expr
5  | neg : Expr → Expr
6  deriving Repr
7
8open Expr
9
10-- Represent: -(2 + 3) * 4
11def myExpr : Expr := mul (neg (add (num 2) (num 3))) (num 4)
12
13-- Evaluate the expression
14def Expr.eval : Expr → Int
15  | num n => n
16  | add a b => a.eval + b.eval
17  | mul a b => a.eval * b.eval
18  | neg e => -e.eval
19
20#eval myExpr.eval  -- -20
21
22-- Pretty print
23def Expr.toString : Expr → String
24  | num n => s!"{n}"
25  | add a b => s!"({a.toString} + {b.toString})"
26  | mul a b => s!"({a.toString} * {b.toString})"
27  | neg e => s!"-{e.toString}"
28
29#eval myExpr.toString  -- "(-(2 + 3) * 4)"

💡

This four-line evaluator is the whole idea behind interpreters, symbolic differentiation, and compilers: represent the program as data, then recurse over it. Adding a new operation means adding a constructor and one line to each function — and Lean's exhaustiveness check will point at every function you forgot to update.

Nested Recursion

A constructor can hold a List of the type being defined. This is a nested inductive type, and it is how you model trees with an arbitrary number of children.

lean

1inductive Rose (α : Type) where
2  | node : α → List (Rose α) → Rose α
3  deriving Repr
4
5def Rose.size : Rose α → Nat
6  | .node _ children => 1 + (children.map Rose.size).sum
7
8#eval (Rose.node 1 [Rose.node 2 [], Rose.node 3 []]).size   -- 3

ℹ

Note that Rose.size recurses through List.map — the recursive call is not on a direct sub-argument, but on an element buried inside a list. Lean handles this, but it is doing real work: it must see that List.map only ever applies the function to elements of its argument. If Lean cannot see it, you will get a termination error and need termination_by — covered in the Termination lesson.

Deep Dive: Mutual Recursion

Sometimes you need types that refer to each other. Lean supports this withmutual:

lean

1mutual
2  inductive Even where
3    | zero : Even
4    | succOdd : Odd → Even
5
6  inductive Odd where
7    | succEven : Even → Odd
8end

This is advanced and rarely needed, but it's available when required.

Folding Recursive Structures

fold collapses a recursive structure into a single value:

lean

1inductive MyList (α : Type) where
2  | nil : MyList α
3  | cons : α → MyList α → MyList α
4
5-- Right fold: process from end to beginning
6def MyList.foldr (f : α → β → β) (init : β) : MyList α → β
7  | nil => init
8  | cons head tail => f head (tail.foldr f init)
9
10def nums := MyList.cons 1 (MyList.cons 2 (MyList.cons 3 MyList.nil))
11
12-- Sum using fold
13#eval nums.foldr (· + ·) 0  -- 6
14
15-- Build a string
16#eval nums.foldr (fun n s => toString n ++ s) ""  -- "123"

The Built-in List Type

Lean's built-in List works exactly like our MyList, but with syntax sugar:

lean

1-- These are equivalent:
2def list1 : List Nat := [1, 2, 3]
3def list2 : List Nat := 1 :: 2 :: 3 :: []
4def list3 : List Nat := List.cons 1 (List.cons 2 (List.cons 3 List.nil))
5
6-- :: is infix for List.cons
7-- [] is List.nil
8
9-- Pattern matching works the same way
10def head? : List α → Option α
11  | [] => none
12  | x :: _ => some x
13
14#eval head? [1, 2, 3]  -- some 1

Exercise: Count Leaves

Write a function that counts the number of leaves in a binary tree.

lean

1inductive BinaryTree (α : Type) where
2  | leaf : BinaryTree α
3  | node : α → BinaryTree α → BinaryTree α → BinaryTree α
4
5open BinaryTree
6
7def leafCount : BinaryTree α → Nat
8  | leaf => 1
9  | node _ left right => leafCount left + leafCount right
10
11#eval leafCount (node 1 leaf (node 2 leaf leaf))  -- 3

Inductive Types Next: Collections & Arrays