Module 3 · Lesson 4

Higher-Order Functions

A higher-order function takes a function as an argument or returns one. map, filter and foldl are the ones you will use most.

Functions as Values

In Lean, functions are values. You can store them, pass them and return them like any other value:

lean

Try it

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

Try it

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

Try it

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 map function 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

Try it

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

Try it

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

Try it

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

Try it

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

Try it

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

Try it

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

Try it

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

Try it

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

Try it

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

Try it

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

Try it

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

Try it

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 mapM means "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

Try it

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