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

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)"

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

Inductive Types Next: Collections & Arrays