Fold

Folding Lists

foldl (fold left) reduces a list to a single value by applying a function repeatedly:

#eval [1, 2, 3, 4, 5].foldl (fun acc x => acc + x) 0
-- 15

Reading this: start with accumulator 0, then for each element x, compute the new accumulator acc + x.

foldl is the basis for many computations:

-- Sum
def mySum (xs : List Nat) : Nat := xs.foldl (fun acc x => acc + x) 0

-- Product
def myProduct (xs : List Nat) : Nat := xs.foldl (fun acc x => acc * x) 1

-- Maximum (given non-empty list)
def myMax (xs : List Nat) : Nat := xs.foldl (fun acc x => if x > acc then x else acc) 0

Your Turn

Define countEvens that counts how many even numbers are in a list using foldl.

Hint: The accumulator starts at 0, and for each element you add 1 if it's even, 0 otherwise.