Module 2 · Lesson 4

Collections & Arrays

Lean provides two main sequential collections: List (linked lists) andArray (dynamic arrays). Knowing when to use each is crucial.

Lists

List is a singly-linked list—the default collection in functional programming:

lean

1-- Create lists with bracket syntax
2def nums : List Nat := [1, 2, 3, 4, 5]
3def empty : List String := []
4
5-- Prepend with :: (cons)
6def moreNums := 0 :: nums  -- [0, 1, 2, 3, 4, 5]
7
8-- Concatenate with ++
9def combined := [1, 2] ++ [3, 4]  -- [1, 2, 3, 4]
10
11-- Common operations
12#eval nums.length        -- 5
13#eval nums.head?         -- some 1
14#eval nums.tail?         -- some [2, 3, 4, 5]
15#eval nums.reverse       -- [5, 4, 3, 2, 1]
16#eval nums.take 3        -- [1, 2, 3]
17#eval nums.drop 2        -- [3, 4, 5]

Arrays

Array is a dynamic array with O(1) random access:

lean

1-- Create arrays with #[] syntax
2def nums : Array Nat := #[1, 2, 3, 4, 5]
3def empty : Array String := #[]
4
5-- Random access with []
6#eval nums[0]!   -- 1
7#eval nums[2]!   -- 3
8
9-- Safe access returns Option
10#eval nums[10]?  -- none
11
12-- Push elements (creates a new array)
13def moreNums := nums.push 6  -- #[1, 2, 3, 4, 5, 6]
14
15-- Common operations
16#eval nums.size          -- 5
17#eval nums.toList        -- [1, 2, 3, 4, 5]
18#eval nums.reverse       -- #[5, 4, 3, 2, 1]

When to Use Which?

Use Case	List	Array
Random access (index)	O(n) - slow	O(1) - fast
Prepend (add to front)	O(1) - fast	O(n) - slow
Append (add to end)	O(n) - slow	O(1)* - fast
Pattern matching	Natural	Less common
Proofs & reasoning	Preferred	More complex

Key Takeaway

Use List for pattern matching, proofs, and when building from the front. Use Array for computation, random access, and performance-critical code.

Transforming Collections

Both List and Array support similar transformation methods:

lean

1def nums := [1, 2, 3, 4, 5]
2
3-- Map: apply a function to each element
4#eval nums.map (· * 2)           -- [2, 4, 6, 8, 10]
5#eval nums.map toString          -- ["1", "2", "3", "4", "5"]
6
7-- Filter: keep elements matching a predicate
8#eval nums.filter (· > 2)        -- [3, 4, 5]
9#eval nums.filter (· % 2 == 0)   -- [2, 4]
10
11-- FilterMap: map and filter in one step
12#eval nums.filterMap (fun n => if n > 2 then some (n * 10) else none)
13-- [30, 40, 50]
14
15-- Find: first element matching a predicate
16#eval nums.find? (· > 3)         -- some 4

Folding and Reducing

Fold operations reduce a collection to a single value:

lean

1def nums := [1, 2, 3, 4, 5]
2
3-- foldl: fold from left to right
4#eval nums.foldl (· + ·) 0    -- 15 (sum)
5#eval nums.foldl (· * ·) 1    -- 120 (product)
6#eval nums.foldl max 0        -- 5 (maximum)
7
8-- Build a string
9#eval nums.foldl (fun acc n => acc ++ toString n) ""  -- "12345"
10
11-- foldr: fold from right to left
12#eval nums.foldr (· :: ·) []  -- [1, 2, 3, 4, 5] (copy)
13
14-- Specialized operations
15#eval nums.sum     -- 15 (requires Add instance)
16#eval nums.all (· > 0)  -- true
17#eval nums.any (· > 4)  -- true

Ranges

Create ranges of numbers with [start:stop] syntax:

lean

1-- Ranges (exclusive end)
2#eval [0:5]           -- [0, 1, 2, 3, 4]
3#eval [1:10:2]        -- [1, 3, 5, 7, 9] (step of 2)
4
5-- Convert range to List
6#eval (List.range 5)  -- [0, 1, 2, 3, 4]
7
8-- Useful for generating test data
9def squares := (List.range 10).map (fun n => n * n)
10#eval squares  -- [0, 1, 4, 9, 16, 25, 36, 49, 64, 81]

Deep Dive: Array Performance

Arrays in Lean use a clever optimization: when an array has only one reference, mutations happen in-place. This means code that looks functional can be as efficient as imperative code.

lean

1-- This is efficient because 'arr' is only referenced once
2def buildArray (n : Nat) : Array Nat := Id.run do
3  let mut arr := #[]
4  for i in [0:n] do
5    arr := arr.push i
6  return arr

The compiler detects single-ownership and optimizes accordingly.

Zipping Collections

Combine two collections element-wise:

lean

1def names := ["Alice", "Bob", "Carol"]
2def ages := [30, 25, 35]
3
4-- Zip into pairs
5#eval names.zip ages
6-- [("Alice", 30), ("Bob", 25), ("Carol", 35)]
7
8-- Zip with a function
9#eval names.zipWith ages (fun name age => s!"{name}: {age}")
10-- ["Alice: 30", "Bob: 25", "Carol: 35"]
11
12-- Enumerate: add indices
13#eval names.enum
14-- [(0, "Alice"), (1, "Bob"), (2, "Carol")]

Converting Between List and Array

lean

1def myList : List Nat := [1, 2, 3]
2def myArray : Array Nat := #[1, 2, 3]
3
4-- List to Array
5#eval myList.toArray   -- #[1, 2, 3]
6
7-- Array to List  
8#eval myArray.toList   -- [1, 2, 3]
9
10-- Chain operations
11#eval #[1, 2, 3].toList.reverse.toArray  -- #[3, 2, 1]

💡

When you need to do heavy computation, convert to Array. When you need to do pattern matching or prove properties, convert to List.

Recursive Data Next: Pattern Matching