Lists and Monoids
In this chapter, we explore the foundational concept of monoids and their deep connection to lists, one of the most fundamental data structures in both mathematics and computer science. We begin by examining lists as sequences of elements drawn from a type α, highlighting their structure and operations such as concatenation and the empty list. Building on this, we introduce monoids—algebraic structures consisting of a list equipped with an associative binary operation and an identity element.
We will see that addition and multiplication over the natural numbers naturally form monoids. We then introduce the free monoid over a type α and examine its defining properties. A central focus of the chapter is the universal property of the free monoid, which characterizes it as the most general monoid generated by a type of elements.
We conclude the theoretical discussion by applying the universal property to define the length of a list as a monoid homomorphism into the natural numbers with addition. This example showcases the practical utility of the abstract theory. Finally, the chapter ends with a set of exercises designed to reinforce the concepts presented in this chapter.
Lists
In functional programming and formal systems like Lean, a list is a fundamental data structure that represents a sequence of elements of a given type.
If we #print List, Lean returns:
inductive List.{u} : Type u → Type u
number of parameters: 1
constructors:
List.nil : {α : Type u} → List α
List.cons : {α : Type u} → α → List α → List αThe List type is defined as an inductive type. List is a parametric type that takes one type parameter—say, α—and produces the type List α, representing lists of elements of type α. This definition includes two constructors. The first, List.nil, represents the empty list, also written [], meaning it can construct an empty list for any type α. The second constructor, List.cons, builds a nonempty list by taking an element of type α, say x, and a list of elements of type α, say xs, returning a new list of type List α, List.cons x xs, also written x :: xs. This new list will have x as its head and the list xs as its tail. This construction makes lists easy to process recursively, as each list is either empty or built by adding an element to the front of another list.
For example, in List N, the expression [] represents the empty list, z :: [] is a list containing a single element—namely [z], and z :: s z :: [] constructs a list with two elements, written as [z, s z].
Using the List.cons constructor we can define the concatenation operation, List.append, which takes two lists l1 and l2 of type List α and returns a new list List.append l1 l2, also written l1 ++ l2, which appends the two lists together. For example, for the lists [z, s z] and [z] in List N, [z, s z] ++ [z] returns the list [z, s z, z].
Monoids
The following Lean code defines the algebraic structure of a monoid and monoid homomorphisms as structure types in Lean.
Monoids.lean
-- A monoid
@[ext] structure Monoid.{u} where
base : Type u
mul : base → base → base
one : base
assoc : ∀ {a b c : base}, mul a (mul b c) = mul (mul a b) c
idl : ∀ {a : base}, mul one a = a
idr : ∀ {a : base}, mul a one = a
-- A monoid homomorphism
@[ext] structure MonoidHom (M N : Monoid) where
map : M.base → N.base
map_mul : ∀ {a b : M.base}, map (M.mul a b) = N.mul (map a) (map b)
map_one : map M.one = N.oneThe first structure, Monoid, represents a monoid as a type base equipped with a binary operation mul (interpreted as multiplication), an identity element one, and three axioms. The associativity axiom (assoc) asserts that multiplication is associative: for all elements a, b, and c, we have mul a (mul b c) = mul (mul a b) c. The left identity (idl) and right identity (idr) laws state that the element one behaves as left and right identity for multiplication: mul one a = a and mul a one = a, respectively. The attribute @[ext] enables Lean to automatically generate extensionality lemmas for these structures, making it easier to prove equalities between instances.
The second structure, MonoidHom, formalizes monoid homomorphisms between two monoids M and N. A homomorphism consists of a function map between the underlying sets of M and N, which preserves the monoid operations: it satisfies map (M.mul a b) = N.mul (map a) (map b) for all a, b, and also maps the identity element of M to that of N, i.e., map M.one = N.one. Together, these definitions provide a foundation for reasoning formally about monoids and their structure-preserving maps within Lean’s type theory framework.
Examples of monoids
We present two examples of monoid structures defined over the natural numbers. In the first example, the binary operation is addition, with 0 serving as the identity element. In the second example, the operation is multiplication, and the identity element is 1. Both structures satisfy the monoid axioms.
Monoids.lean
The free monoid over type α
For any type α, the free monoid over α is given by the type List α, equipped with list concatenation (++) as the binary operation and the empty list [] as the identity element. This structure forms a monoid because concatenation is associative and the empty list acts as a neutral element for concatenation on both sides.
FreeMonoid.lean
-- (List α, ++, []) is a monoid for any type α
def FreeMonoid {α : Type u} : Monoid where
base := List α
mul := List.append
one := []
assoc := by
intro a b c
induction a with
| nil => simp [List.append]
| cons x xs ih => simp [List.append, ih]
idl := by
intro a
induction a with
| nil => simp [List.append]
| cons x xs ih => simp [List.append, ih]
idr := by
intro a
induction a with
| nil => simp [List.append]
| cons x xs ih => simp [List.append, ih]The universal property
The following Lean code defines the canonical insertion of generators function η from a type α into List α.
FreeMonoid.lean
The function η takes an element a : α and returns the singleton list [a], implemented here as List.cons a []. This reflects the standard way of embedding generators into a free monoid: each element of α is mapped to a list containing just that element.
The universal property of the FreeMonoid α states that for any monoid M and any function f : α → M.base, there exists a unique monoid homomorphism Lift f : FreeMonoid α → M such that Lift f ∘ η = f. This means that Lift f extends f in a way that respects the monoid structure, making FreeMonoid α the most general monoid generated freely by the elements of α.
The definition of Lift f is defined recursively on lists, as follows:
FreeMonoid.lean
The base case corresponds to the empty list: Lift f [] = M.one, ensuring the identity element of the monoid is preserved. For non-empty lists, Lift f applies the homomorphism recursively to the tail of the list and then combines it with the image of the head element using the monoid multiplication M.mul. Specifically, for a list x::xs', we have Lift f (x::xs) = M.mul (f x) (Lift f xs).
This construction guarantees that Lift f is a monoid homomorphism, mapping the empty list to the identity element and preserving the monoid operation, as we can prove below.
FreeMonoid.lean
-- The function `Lift f` is a monoid homomorphism from the free monoid to the monoid `M`
def LiftMonoidHom {α : Type u} {M : Monoid} (f : α → M.base) : MonoidHom (@FreeMonoid α) M where
map := Lift f
map_mul := by
intro a b
induction a with
| nil => calc
Lift f (FreeMonoid.mul [] b) = Lift f b := rfl
_ = M.mul (M.one) (Lift f b) := M.idl.symm
_ = M.mul (Lift f []) (Lift f b) := congrArg (fun x => M.mul x (Lift f b)) rfl
| cons x xs ih => calc
Lift f (FreeMonoid.mul (x::xs) b) = Lift f (x :: (FreeMonoid.mul xs b)) := rfl
_ = M.mul (f x) (Lift f (FreeMonoid.mul xs b)) := rfl
_ = M.mul (f x) (M.mul (Lift f xs) (Lift f b)) := congrArg (fun y => M.mul (f x) y) ih
_ = M.mul (M.mul (f x) (Lift f xs)) (Lift f b) := M.assoc
_ = M.mul (Lift f (x::xs)) (Lift f b) := congrArg (fun y => M.mul y (Lift f b)) rfl
map_one := rflFurthermore, Lift f extends f in the sense that for each element a : α, it satisfies Lift f (η a) = f a, where η is the insertion map that sends a to the singleton list [a]. This is proven in the theorem below.
FreeMonoid.lean
Finally, we can prove that the function Lift f is the unique monoid homomorphism from the free monoid FreeMonoid α to any monoid M that satisfies the property Lift f ∘ η = f. This is proven in the theorem below.
FreeMonoid.lean
theorem LiftUnique {α : Type u} {M : Monoid} (f : α → M.base)
(g : MonoidHom (@FreeMonoid α) M) : g.map ∘ η = f → g = LiftMonoidHom f := by
intro h
apply MonoidHom.ext
funext a
induction a with
| nil => calc
g.map [] = M.one := g.map_one
_ = (LiftMonoidHom f).map [] := (LiftMonoidHom f).map_one
| cons x xs ih => calc
g.map (x::xs) = g.map (FreeMonoid.mul (η x) xs) := rfl
_ = M.mul (g.map (η x)) (g.map xs) := g.map_mul
_ = M.mul (f x) (g.map xs) := congrArg (fun y => M.mul y (g.map xs)) (congrFun h x)
_ = M.mul ((LiftMonoidHom f).map (η x)) (g.map xs) := congrArg (fun y => M.mul y (g.map xs)) (congrFun (LiftEta f).symm x)
_ = M.mul ((LiftMonoidHom f).map (η x)) ((LiftMonoidHom f).map xs) := congrArg (fun y => M.mul ((LiftMonoidHom f).map (η x)) y) ih
_ = (LiftMonoidHom f).map (FreeMonoid.mul (η x) xs) := (LiftMonoidHom f).map_mul.symm
_ = (LiftMonoidHom f).map (x::xs) := rflThe length of a list
As an application of the universal property of the free monoid, we define a function Length that computes the length of a list. First, we define Len : α → N, a function that maps each element of type α to the natural number 1, representing the fact that each element in a list contributes exactly one to the length.
Using the universal property of the free monoid, we extend Len to a monoid homomorphism Length : (List α,++,[]) → (N,+,0) by applying the Lift function.
This guarantees that Length satisfies the required monoid homomorphism properties: it maps the empty list to 0 (the identity in (N,+,0)), and for any two lists, the length of their concatenation is the sum of their individual lengths. Thus, Length is a monoid homomorphism that respects the structure of the free monoid and computes the number of elements in a list. This example highlights how the universal property of the free monoid enables the definition of homomorphisms that extend functions from the generators to any target monoid.
Exercises
Exercises.lean