Understanding Category Theory Using Agda - Part 1

6 minute read

Published:

After a long silence, I decided to blog again. Now, I’ll start a series on implementing Category Theory using Agda.

My focus on this post series will be presenting the main definitions of category theory, implement them in Agda, show some examples of these definitions and prove some basic results. A good introduction to category theory are the posts by Bartosz Milewski. If you don’t know anything about Agda, I recommend this tutorial.

What’s so special about category theory?

Everyone that starts to use functional programming languages, like Haskell, would hear something about category theory (that’s happened to me). Usually, people talk about category theory with some mistery or fear, due to its abstract content. But, essentially, category theory is about structure preserving transformations and how such transformations can be composed. Since, composition is essential to software design, category theory can be a great source of inspiration for ideas in programming.

Before talking about formal definitions of categories and how to code them in Agda, in this post, we will focus on monoids, that are a very useful algebraic structure that shares some similarities with categories.

Monoids - A brief, but useful interlude

Before give a definition of what is a category, it’s useful to consider what is a monoid, since categories can be seen as a generalization of monoids.

A monoid consists of a set \(A\), a binary operation \(\circ : A \times A \to A\) and an element \(\epsilon \in A\) which satisfies the following properties:

  • \(\forall x.\forall y. \forall z. x \circ (y \circ z) = (x \circ y) \circ z \).
  • \(x \circ \epsilon = x = \epsilon \circ x \)

In Agda, we can define a record definition to code a monoid and its properties:

record IsMonoid {l}{A : Set l}(ε : A)(_∘_ : A → A → A) : Set l where
    field
      left-id : ∀ {x : A} → ε ∘ x ≡ x
      right-id : ∀ {x : A} → x ∘ ε ≡ x
      assoc : ∀ {x y z : A} → x ∘ (y ∘ z) ≡ (x ∘ y) ∘ z

record Monoid {l}(A : Set l) : Set (lsuc l) where
    field
      ε : A
      _∘_ : A → A → A
      isMonoid : IsMonoid ε _∘_

We represent both the requirements for and the algebraic structure of monoid using records. In Agda, records can be opened into scope like modules and it is a nice way to enforce some sort of information hiding, when implement algebraic structures.

Several well known structures are monoids. Addition and multiplication over natural numbers, multiplication over matrices are some examples. Below, we show how addition over natural numbers forms a monoid.

data Nat : Set where
   zero : Nat
   suc  : Nat → Nat

_+_ : Nat → Nat → Nat
zero + m = m
(suc n) + m = suc (n + m)

+zero-r : ∀ (n : Nat) → n + 0 ≡ n
+zero-r zero = refl
+zero-r (suc n) = cong suc (+zero-r n)

+assoc : ∀ (n m p : Nat) → n + (m + p) ≡ (n + m) + p
+assoc zero m p = refl
+assoc (suc n) m p = cong suc (+assoc n m p)


natMonoid : Monoid Nat
natMonoid
= record {
          ε = zero
		  ; _∘_ = _+_
		  isMonoid
		  = record {
 		           left-id = refl
				;  right-id = +zero-r
				;  assoc = +assoc
		     }
		 }

The previous source code piece declares a data type of natural numbers, Nat, its addition operation and some lemmas stating that addition is associative and zero is left and right unit element for it.

Lists and their concatenation operation are other example that forms a monoid. Such monoid is known as free-generated monoid.

Freely generated monoids

Formally, given a set \(S\), a list over \(S\) is a pair \( (n,f) \), where \(n \in\mathbb{N}\) and \(f : {1,…,n}\to S\) is a function such that \(f(i)\) denotes the i-th list element, \(i\in{1,…,n}\).

The empty list is represented by \([ ]\) and it is the unique list \( (n,f) \) such that \( n = 0 \).

Given two lists, \( L = (n,f) \) and \( L’ = (n’,f’) \), we define their concatenation, \( L ++ L’ \) to be the list \( (n + n’,g) \), where function \( g \) is defined as:

  • \(g(i) = f(i)\); if \(1 \leq i \leq n\)
  • \(g(i) = f’(i - n)\); if \(n + 1 \leq i \leq n + n’ \)

The monoid freely generated by a set \(S \) is given by the triple \( (List\,S, [], ++) \), where \(List\,S\) is the set of lists of elements in S, \([] \in List\,S\), and \(++\) is the list concatenation operation.

Agda list data type and its concatenation function forms a monoid, in the sense of the previous record definition. The next source code piece proves the monoid properties for lists and their concatenation.

  data List {l}(A : Set l) : Set l where
    [] : List A
    _::_ : A → List A → List A

  _++_ : ∀ {l}{A : Set l} → List A → List A → List A
  [] ++ ys = ys
  (x :: xs) ++ ys = x :: (xs ++ ys)

  ++right-r : ∀ {l}{A : Set l}(xs : List A) → xs ++ [] ≡ xs
  ++right-r [] = refl
  ++right-r (x :: xs) = cong (_::_ x) (++right-r xs)

  ++assoc : ∀ {l}{A : Set l}(xs ys zs : List A) → xs ++ (ys ++ zs) ≡ (xs ++ ys) ++ zs
  ++assoc [] ys zs = refl
  ++assoc (x :: xs) ys zs = cong (_::_ x) (++assoc xs ys zs)
  free : ∀ {l}{A : Set l} → Monoid (List A)
  free = record {
               ε = []
               ; _∘_ = _++_
			   ; isMonoid = record {
			          left-id = refl
					; right-id = λ {xs} → ++right-r xs
					; assoc = λ {xs}{ys}{zs} → ++assoc xs ys zs } }

Freely generated structures are almost everywhere in abstract algebra. In next post, we will talk about categories, their definition and how they can be freely generated.