Module 3 · Lesson 3

Higher-Order Functions

Functions that take or return other functions are called higher-order functions. They're the backbone of functional programming.

Functions as Values

In Lean, functions are first-class citizens—they can be stored, passed, and returned like any other value:

lean

1-- Store a function in a variable
2def addOne : Nat → Nat := fun x => x + 1
3
4-- Pass a function to another function
5#eval [1, 2, 3].map addOne  -- [2, 3, 4]
6
7-- Return a function from a function
8def makeAdder (n : Nat) : Nat → Nat :=
9  fun x => x + n
10
11def addFive := makeAdder 5
12#eval addFive 10  -- 15

Lambda Expressions

Create inline anonymous functions with fun:

lean

1-- Full syntax
2#eval [1, 2, 3].map (fun x => x * 2)  -- [2, 4, 6]
3
4-- With type annotation
5#eval [1, 2, 3].map (fun (x : Nat) => x * 2)
6
7-- Multiple parameters
8#eval [(1, 2), (3, 4)].map (fun (a, b) => a + b)  -- [3, 7]
9
10-- Unicode lambda (stylistic choice)
11#eval [1, 2, 3].map (λ x => x * 2)  -- [2, 4, 6]

Shorthand Syntax with ·

The dot · creates concise lambdas:

lean

1-- (· + 1) means (fun x => x + 1)
2#eval [1, 2, 3].map (· + 1)      -- [2, 3, 4]
3
4-- (· * 2) means (fun x => x * 2)
5#eval [1, 2, 3].map (· * 2)      -- [2, 4, 6]
6
7-- (· > 2) means (fun x => x > 2)
8#eval [1, 2, 3, 4].filter (· > 2)  -- [3, 4]
9
10-- Multiple dots for multiple arguments
11#eval [(1, 2), (3, 4)].map (·.1 + ·.2)  -- [3, 7]

Key Takeaway

The · syntax is perfect for simple transformations. Use fullfun syntax for complex logic or when you need to name parameters.

Standard Higher-Order Functions

map: Transform Each Element

lean

1#eval [1, 2, 3].map (· * 10)           -- [10, 20, 30]
2#eval ["a", "b"].map String.toUpper     -- ["A", "B"]
3#eval [1, 2, 3].map toString            -- ["1", "2", "3"]

filter: Keep Matching Elements

lean

1#eval [1, 2, 3, 4, 5].filter (· > 3)   -- [4, 5]
2#eval [1, 2, 3, 4, 5].filter (· % 2 == 0)  -- [2, 4]
3#eval ["", "a", "", "b"].filter (· != "")  -- ["a", "b"]

foldl: Accumulate Left to Right

lean

1-- Sum: start with 0, add each element
2#eval [1, 2, 3, 4].foldl (· + ·) 0     -- 10
3
4-- Product: start with 1, multiply each
5#eval [1, 2, 3, 4].foldl (· * ·) 1     -- 24
6
7-- Build a string: start with "", append each
8#eval [1, 2, 3].foldl (fun s n => s ++ toString n) ""  -- "123"
9
10-- Find maximum: start with 0, take max
11#eval [3, 1, 4, 1, 5].foldl max 0      -- 5

foldr: Accumulate Right to Left

lean

1-- Different order than foldl
2#eval [1, 2, 3].foldl (fun acc x => s!"({acc} + {x})") "0"
3-- "((0 + 1) + 2) + 3)"
4
5#eval [1, 2, 3].foldr (fun x acc => s!"({x} + {acc})") "0"
6-- "(1 + (2 + (3 + 0)))"

The Pipe Operator

Chain operations with |> for readable data pipelines:

lean

1-- Without pipes (nested, hard to read)
2#eval String.length (String.toUpper "hello")
3
4-- With pipes (flows left to right)
5#eval "hello" |> String.toUpper |> String.length  -- 5
6
7-- Complex pipeline
8def processNumbers (nums : List Nat) : Nat :=
9  nums
10  |> List.filter (· > 0)      -- Keep positives
11  |> List.map (· * 2)          -- Double them
12  |> List.foldl (· + ·) 0      -- Sum them
13
14#eval processNumbers [0, 1, 2, 3]  -- 12

💡

Pipes make data transformation pipelines read like English: "Take nums, filter positives, map double, fold sum."

Function Composition

Compose functions with ∘ (or . in some contexts):

lean

1def addOne (x : Nat) : Nat := x + 1
2def double (x : Nat) : Nat := x * 2
3
4-- Compose: (double ∘ addOne) means "first addOne, then double"
5def addOneThenDouble := double ∘ addOne
6
7#eval addOneThenDouble 5  -- 12 (5 + 1 = 6, 6 * 2 = 12)
8
9-- Use in pipelines
10#eval [1, 2, 3].map (double ∘ addOne)  -- [4, 6, 8]

Partial Application

Fix some arguments to create a new function:

lean

1def add (x y : Nat) : Nat := x + y
2
3-- Partially apply: fix first argument
4def add10 := add 10
5
6#eval add10 5   -- 15
7#eval add10 20  -- 30
8
9-- Useful with higher-order functions
10#eval [1, 2, 3].map (add 100)  -- [101, 102, 103]
11
12-- Works with operators too
13#eval [1, 2, 3].map (· + 100)  -- Same thing

Deep Dive: Currying

All multi-parameter functions in Lean are "curried"—they take one argument at a time and return a function for the rest:

lean

1-- These are equivalent
2def add (x y : Nat) : Nat := x + y
3def add' (x : Nat) : Nat → Nat := fun y => x + y
4def add'' : Nat → Nat → Nat := fun x y => x + y
5
6-- add 1 returns a function Nat → Nat
7#check add 1  -- Nat → Nat

This is why partial application works so naturally in Lean.

Building Custom Higher-Order Functions

lean

1-- Apply a function n times
2def iterate (n : Nat) (f : α → α) (x : α) : α :=
3  match n with
4  | 0 => x
5  | n + 1 => iterate n f (f x)
6
7#eval iterate 3 (· + 1) 0   -- 3
8#eval iterate 5 (· * 2) 1   -- 32
9
10-- Find first element matching predicate
11def findFirst (p : α → Bool) : List α → Option α
12  | [] => none
13  | x :: xs => if p x then some x else findFirst p xs
14
15#eval findFirst (· > 5) [1, 3, 7, 2, 8]  -- some 7

Recursion Next: Error Handling