Module 3 · Lesson 4

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-- Each · is a SEPARATE parameter, filled left to right.
11-- So (· + ·) is (fun a b => a + b) — a two-argument function.
12#eval [1, 2, 3].foldl (· + ·) 0    -- 6
13
14-- Which means this does NOT work on pairs: (·.1 + ·.2) is
15-- (fun a b => a.1 + b.2), and map wants a one-argument function.
16-- #eval [(1, 2), (3, 4)].map (·.1 + ·.2)   -- error
17
18-- Destructure with fun instead
19#eval [(1, 2), (3, 4)].map (fun (a, b) => a + b)  -- [3, 7]
20
21-- ...or use one dot and project inside it
22#eval [(1, 2), (3, 4)].map (fun p => p.1 + p.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

The mapfunction applies a transformation to every element in a collection, producing a new collection of the same shape. This is one of the most commonly used higher-order functions because it cleanly separates "what to do" from "how to iterate".

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

The filter function keeps only elements that satisfy a predicate. Unlike map, the output may be shorter than the input. The order of remaining elements is preserved.

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

The foldl (fold-left) function reduces a list to a single value by combining elements from left to right. It takes an initial accumulator value and a combining function that merges each element into the accumulator.

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

The foldr (fold-right) function works like foldlbut processes elements from right to left. For associative operations like addition this gives the same result, but for non-associative operations the order matters.

lean

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

ℹ

Note the argument order flips: foldl takes (acc, x) and foldr takes (x, acc). In both cases the accumulator sits on the side the fold comes from. Getting this backwards is the usual cause of a baffling type error when switching between the two.

💡

Which to reach for: foldl for reductions to a scalar (sum, max, count) — it is tail recursive and the left-to-right order matches how you would write a loop. foldr for rebuilding a structure, because it lines up with :: — xs.foldr (· :: ·) [] is the identity on lists, and map and filter are both one-line foldrs.

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

Predicates as Functions

A predicate is just a function returning Bool. This makes it easy to reuse filtering logic.

lean

1def isEven (n : Nat) : Bool := n % 2 == 0
2def isLarge (n : Nat) : Bool := n >= 10
3
4#eval [1, 2, 10, 12].filter isEven  -- [2, 10, 12]
5#eval [1, 2, 10, 12].filter isLarge -- [10, 12]

Function Composition

Compose functions with ∘ (typed \circ or \o). Unlike Haskell, Lean does not use . for composition — x.f is namespace-resolved method syntax, which is a completely different thing.

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

The Same Functions, Other Containers

map is not a list function — it is a shape-preserving transformation, and it exists for anything with a hole in it. Recognising this saves you writing a lot of pattern matches.

lean

1-- map on Option: apply the function if there is a value
2#eval (some 3).map (· * 2)          -- some 6
3#eval (none : Option Nat).map (· * 2)  -- none
4
5-- map on Array, on Except, on Prod's second component...
6#eval #[1, 2, 3].map (· * 2)                    -- #[2, 4, 6]
7#eval (Except.ok 3 : Except String Nat).map (· * 2)  -- Except.ok 6
8
9-- filterMap: map and drop the failures in one pass
10#eval ["1", "x", "3"].filterMap String.toNat?   -- [1, 3]
11
12-- flatMap: map to lists and concatenate ("for each x, produce several")
13#eval [1, 2, 3].flatMap (fun n => [n, n * 10])  -- [1, 10, 2, 20, 3, 30]
14
15-- any / all: fold to a Bool, short-circuiting
16#eval [1, 2, 3].any (· > 2)   -- true
17#eval [1, 2, 3].all (· > 0)   -- true

💡

filterMap is underused and deserves a mention on its own. Whenever you find yourself writing xs.map f |>.filter (· != none) |>.map Option.get!, the answer is xs.filterMap f — one pass, no partial functions, no get!.

Effectful Higher-Order Functions

When the function you want to map is itself effectful — it reads a file, or can fail — the plain versions do not typecheck. The M-suffixed variants are what you want:

lean

1-- mapM: map with an effect, collecting the results
2#eval do
3  let results ← [1, 2, 3].mapM (fun n => do
4    IO.println s!"processing {n}"
5    return n * 2)
6  return results
7-- processing 1 / processing 2 / processing 3 / [2, 4, 6]
8
9-- forM: same, but you do not care about the results
10#eval [1, 2, 3].forM (fun n => IO.println s!"saw {n}")
11
12-- foldlM: fold where the step function is effectful
13#eval [1, 2, 3].foldlM (fun acc n => do
14  IO.println s!"acc={acc}"
15  return acc + n) 0

ℹ

The pattern generalises: nearly every list function has an M sibling (mapM, filterM, foldlM, anyM, forM). They work in any monad, not just IO — including Option and Except, where mapMmeans "apply to all, and fail the whole thing if any one fails". Module 5 covers monads properly.

Exercise: Reusable Filter

Define a function that filters a list using a predicate and then maps a function over the result.

lean

1def filterMap' (p : α → Bool) (f : α → β) (xs : List α) : List β :=
2  xs.filter p |>.map f
3
4#eval filterMap' (· > 2) (· * 10) [1, 2, 3, 4]  -- [30, 40]

Tail Recursion Next: Error Handling