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

Complexity Tips

A quick mental model: Lists are great for building up results and pattern matching, while Arrays are great for indexing and bulk computation. When performance matters, convert to the structure that matches the dominant operation.

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]

HashMap and HashSet

For efficient key-value storage and membership testing, use Std.HashMap andStd.HashSet:

lean

1import Std.Data.HashMap
2import Std.Data.HashSet
3
4open Std
5
6-- Create a HashMap
7def ages : HashMap String Nat := HashMap.empty
8  |>.insert "Alice" 30
9  |>.insert "Bob" 25
10
11-- Lookup
12#eval ages.find? "Alice"     -- some 30
13#eval ages.find? "Unknown"   -- none
14
15-- Check membership
16#eval ages.contains "Bob"    -- true
17
18-- HashSet for unique values
19def seen : HashSet String := HashSet.empty
20  |>.insert "a"
21  |>.insert "b" 
22  |>.insert "a"  -- Duplicate, ignored
23
24#eval seen.size              -- 2
25#eval seen.contains "a"      -- true

ℹ

HashMap and HashSet require BEq and Hashable instances for the key type. Most standard types already have these.

Strings as Collections

Strings can be treated as collections of characters:

lean

1-- Iterate over characters
2#eval "hello".toList           -- ['h', 'e', 'l', 'l', 'o']
3#eval "hello".data             -- Same thing
4
5-- Map over characters  
6#eval "hello".map Char.toUpper -- "HELLO"
7
8-- Filter characters
9#eval "he11o".filter Char.isAlpha  -- "heo"
10
11-- Fold characters
12#eval "hello".foldl (fun acc c => acc ++ toString c ++ "-") ""
13-- "h-e-l-l-o-"
14
15-- Check all/any
16#eval "HELLO".all Char.isUpper     -- true
17#eval "Hello".any Char.isLower     -- true

💡

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

Exercise: Transform an Array

Convert an Array to a List, filter even numbers, and convert back to an array.

lean

1def nums : Array Nat := #[1, 2, 3, 4, 5, 6]
2
3def evens : Array Nat :=
4  nums.toList.filter (· % 2 == 0) |>.toArray
5
6#eval evens  -- #[2, 4, 6]

Recursive Data Next: Pattern Matching