0. Introduction
Learning math can be hard for several reasons, but one of them is that the language used by authors tends to be optimized for specialists:
 symbols and identifiers are heavily overloaded
 math writers abhor boilerplate
 a lot of the context of a given expression is assumed to be available to the reader, etc.
In addition to that, most math is written in plain paper or paperlike mediums such as PDF.
(If you look at this practice from the perspective of a programmer this is a bit strange: it’s similar as if programs were written primarily using the plain text editor “Notepad”, and without any help from the type checker)
But probably the main difficulty is just abstraction itself. One can spend a lot of time trying to come up with a good mental representation of new concepts.
As it turns out, we can use Scala (or other programming languages) to encode many mathematical definitions and ideas, and get some immediate wins:
 The typechecker can point out many errors.
 We get access to all the tools available when using a modern IDE, such as code completion, navigate to definition, inline documentation, autogenerated code, etc.
 A lot of the ambiguity is removed since we’re forced to write every single definition in painful detail.
And crucially, we can reuse our existing programming intuition to help develop a purely abstract math intuition.
Of course we’ll have to make some compromises in generality, but the reality is that most people don’t learn (or do) math at the maximum possible level of generality (in part because that level is not fixed: it normally increases over time). All this is to say that for the ideas that can be expressed in our programming language, we are doing real math.
Now while Scala can be used to automate some theorem proofs (a topic for a different post), it is not a theorem prover such as Lean, or Agda. If you’re seriously interested in doing math on your computer at the maximum generality then an automated theorem prover is the best tool.
In this article we’ll explore how we can encode several definitions from the book Category Theory and Applications by Marco Grandis and translate them into Scala 3 (Dotty).
Quoted text like this we’ll be reserved for quotes from this book.
We’ll end up by stating and proving the Yoneda lemma and explaining the (in) famous phrase “Monads are just monoids in the category of endofunctors”.
Note 1: This article focuses mostly on the process of encoding Algebraic concepts into Scala, and is not meant to be a full tutorial on Categories.
Note 2: If you’re not familiar with type functions then I recommend perusing Illustrated guide to Types, Sets and Values.
Audience: Math beginnerish, Scala intermediate.
Scala 3 version used: 3.1.2
Updated code available at: https://github.com/jpablo/mathwithscala
1. Categories
Informally, a category is a special kind of directed graph with an operation similar to path concatenation defined on the edges.
A Category $C$ consists of the following data:
a set $O$ whose elements are called objects of $C$.
for every pair $(X,Y)$ of objects, a set $\mathrm{Hom}(X,Y)$ (called a homset), whose elements are called morphisms (or maps, or arrows) of $C$ from $X$ to $Y$ and denoted as $f: X \rightarrow Y$,
The set $\mathrm{Hom}(X, Y)$ is also written as $C(X, Y)$
 for every triple $X, Y, Z$ of objects on $C$, a mapping or composition
$\begin{matrix} \mathrm{Hom}(X, Y) \times \mathrm{Hom}(Y,Z) & \rightarrow & \mathrm{Hom}(X, Z) \\ (f, g) & \mapsto & g ◦ f \end{matrix}$These data must satisfy the following axioms
Associativity. Given three consecutive arrows $f:X \to Y$, $g:Y \to Z$, and $h:Z \to W$, the equation $h◦(g◦f)=(h◦g)◦f$ holds,
Identities. Given an object $X$, there exists and endomorphism $e: X \to X$ which acts as an identity whenever composition makes sense; in other words if $f: X' \to X$ and $g:X \to X''$, one has $e ◦ f = f$ and $g ◦ e = g$.
$e$ is called the identity of $X$ and written as $1_X$ or id$X$.
1.1 Categories over the set of all types 𝕋
Our approach will be to represents objects as types (i.e. elements of the set $\mathbb{T}$ of all types), and homsets as type functions $\mathbb{T} \times \mathbb{T} \to \mathbb{T}$.
trait Category[Hom[_, _]]:
type ~>[A, B] = Hom[A, B]
extension [A, B, C] (g: B ~> C)
def ◦ (f: A ~> B): A ~> C = f >>> g
extension [A, B, C] (f: A ~> B)
def >>> (g: B ~> C): A ~> C
def id[A]: A ~> A
@Law
def associativity[A, B, C, D](
f: A ~> B,
g: B ~> C,
h: C ~> D
) =
h ◦ (g ◦ f) <> (h ◦ g) ◦ f
@Law
def identityR[A, B](f: A ~> B) = f ◦ id[A] <> f
@Law
def identityL[A, B](f: A ~> B) = id[B] ◦ f <> f
Laws are usually expressed as functions that return an instance of the case class IsEq(lhs, rhs)
, (the operator <>
is provided by Cats, it simply creates a new IsEq
), which is then used in conjunction with the library discipline and Scalacheck to generate random values and try to find counterexamples.
(Here’s a fully developed example using these laws)
Some of the types involved in this definition are:
with composition:
Notation can get heavy pretty fast, so the arrow notation A ~> B
is very convenient as long as we remember that arrows are not necessarily functions (and as a reminder of this I decided to use Hom[_, _]
for the parameter name).
In particular notice that there’s no evaluation function defined on arrows, which means that everything needs to be done “pointfree” when using the Category
trait.
Example: Pure Scala functions and types
Probably one of the most elementary categories in math is the Set category of sets and functions.
Arguably the Scala category (with types as objects and pure functions as arrows) defined below plays a similar role, in the sense that it is the “base” language on top of which everything else is built.
type Scala[A, B] = A => B
given Scala: Category[Scala] with
def id[A]: A => A = identity[A]
extension [A, B, C]
(g: B => C) def ◦ (f: A => B) = g compose f
// This satisfies the category laws but
// only for pure functions :)
From now on we’ll refer to this category simply as Scala.
(Dotty feature: given instances).
Implicit or explicit?
There’s no requirement to make the Scala category instance an implicit value (I mean… given). But in most cases we’ll be using only one category instance C
for a given hom function Hom[_,_]
. In this situation it’s very convenient to be able to just pass the hom function and have the corresponding category instance be looked up by the compiler (and we can always use an explicit instance when needed).
Here’s a summary of how we translated the definition into Scala:
Math  Scala 

Algebraic definition  Trait with some abstract members 
Axioms / Laws  Test suite 
Concrete Category  Lawful implementation of the Category trait 
Objects $O$ of the category $C$  All types (for now) 
$\mathrm{Hom}(X,Y)$ (morphisms between $X$ and $Y$)  Values of type Hom[X, Y] 
Function $\mathrm{Hom}:O \times O \to \mathrm{Sets}$  Type Function Hom[_,_] 
Composition operator  Family of binary functions ◦[A, B, C] , one for each triple $A, B, C \in\mathbb{T}$ 
Identity morphism $1_X$ for each object $X$  A value of type id[X] for each type X 
Function family $X \mapsto 1_X \in \mathrm{Hom}(X,X)$  Polymorphic function [X] =>> id[X]: Hom[X,X] 
The textbook definition allows for the objects $O$ of the category $C$ to be an arbitrary set, whereas in our Category
trait we have no way to restrict the arguments for Hom
, which means that instances of this trait have a fixed set of objects O
: the set of all types!
In order to create more general categories we need to find a way to restrict objects to be members of different sets of types.
There are two main ways in which we can specify subsets of types in Scala:
 Via subtyping
 Via type classes
Long story short, we’ll have to create slightly different Category
definitions to express different kind of constraints over the arguments of Hom
. We’ll use our original definition when possible though, because other definitions add some boilerplate.
Type arguments vs type members
Another encoding choice would be to use an abstract type member like so:
trait Category
type Hom[A, B]
def id[A]: Hom[A, A]
def [A, B, C] (g: Hom[B, C]) ◦ (f: Hom[A, B]): Hom[A, C]
I find this approach more cumbersome to deal, mainly due to the fact that it can be easy to get the types wrong, and harder to fix. Also you end up having to use things like the Aux[_]
pattern frequently to reduce boilerplate and prevent errors.
Example: Category of types and subtyping relationships
We know that types in Scala form a lattice under subtyping:
A natural category to consider would be one with all types as objects and a single morphism between A
and B
if A <: B
(and no morphisms otherwise).
(This is called the Liskov category in scalaz)
Scala provides a data type (<:<[A, B]
) that encodes the fact that type A
is a subtype of B
given Subtypes: Category[<:<] with
def id[A] = <:<.refl
extension [A, B, C]
(g: B <:< C) def ◦ (f: A <:< B): A <:< C =
g compose f
For each pair of types A <: B
there is only one arrow, the unique value of type A <:< B
that can be obtained using summon
(and none otherwise):
trait A
trait B extends A
trait C extends B
Subtypes.id[A] == summon[A <:< A]
import Subtypes.~>
val f: C ~> B = summon[C <:< B]
val g: B ~> A = summon[B <:< A]
val h: C ~> A = summon[C <:< A]
g ◦ f == h
Example: Product category
If $C$ and $D$ are categories, one defines the product category $C \times D$.
An object is a pair $(X, Y)$ where $X \in C$ and $Y \in D$. A morphism is a pair of morphisms
$(f, g): (X, Y) \to (X', Y')$for $f\in C(X, X')$ and $g \in D(Y, Y')$.
Thus for us objects will be types of the form (A, B)
and arrows tuples of arrows (C[A1, A2], D[B1, B2])
.
First we use match types to define two functions that can only be applied to types of tuples, and can extract the first and second arguments (i.e. the first or second type):
type _1[X] = X match {
case (a, _) => a
}
type _2[X] = X match {
case (_, b) => b
}
Morphisms are tuples of morphisms:
type ×[~>[_, _], >[_, _]] = [A, B] =>>
( _1[A] ~> _1[B],
_2[A] > _2[B] )
The operator ×
constructs the product category:
// C × D
extension [C[_, _], D[_, _]]
(C: Category[C]) def × (D: Category[D]): Category[C × D] =
import C.{extension_◦ => ++}
import D.{extension_◦ => +}
new Category[C × D]:
def id[A]: A ~> A =
( C.id[Fst[A]],
D.id[Snd[A]] )
extension [A, B, C]
(g: B ~> C) def ◦ (f: A ~> B): A ~> C =
( g._1 ++ f._1,
g._2 + f._2 )
Example:
val Scala2 = Scala × Scala
val (f, g) = Scala2.id[(Int, Char)]
// f == identity[Int]
// g == identity[Char]
1.2 Other encodings
Example: Monoids as a categories
As an example of a category where the arrows are not functions, consider a category with only one (arbitrary) element *
and whose morphisms are Ints
.
The previous Category
definition won’t work here because the Hom
function accepts arguments of any type.
One way to restrict the arguments is to add a common upper bound everywhere:
trait CategoryS[U, Hom[_ <: U, _ <: U]]
type ~> = Hom
def id[A <: U]: A ~> A
def [A <: U, B <: U, C <: U] (g: B ~> C) ◦ (f: A ~> B): A ~> C
// Category laws modified accordingly
Now we can choose an arbitrary value (say '*'
) and use its singleton type as the upper bound U
:
// The singleton type of the String "Singleton".
// Any other singleton type will work
// since our goal is to use a type
// with only one inhabitant.
type ● = "Singleton"
type ConstantHom[A] = [_ <: ●, _ <: ●] =>> A
object IntCategory extends CategoryS[●, ConstantHom[Int]]:
def id[A <: ●] = 0
extension [A <: ●, B <: ●, C <: ●] (g: Int) def ◦ (f: Int) =
g + f
now we can use the category composition operator ◦
on Ints
:
import IntCategory.◦
assert(1 ◦ 2 == 3)
The above definition can be generalized to any zio.prelude.classic.Monoid
instance:
// create a new category instance given a zio.prelude.classic.Monoid instance
import zio.prelude.classic
def fromMonoid[M](M: classic.Monoid[M]) =
new CategoryS[●, ConstantHom[M]]:
def id[A <: ●]: M = M.identity
extension [A <: ●, B <: ●, C <: ●]
(g: M) def ◦ (f: M) = M.combine(g, f)
// usage:
given StringMonoidCat: CategoryS[●, ConstantHom[String]] =
fromMonoid(zio.prelude.Identity[String])
assert( StringMonoidCat.id == "" )
assert( "a" ◦ "b" == "ab" )
This construction justifies the following:
A single monoid $M$ can be viewed as a category with one formal object $*$.
The morphisms $x: * \to *$ are the elements of $M$, composed by the multiplication $x y$ of the monoid, with identity $id(*) = 1$, the unit of the monoid.
Grandis, pp 17.
Example: Category of Groups
Some of the classic examples of categories are those where the objects are sets with some algebraic structure and the arrows are homomorphisms preserving the algebraic structure.
As an example let’s define Grp, the category of Groups (i.e. classic.Group
)
For this we’ll have to add a type class constraint P[_]
to our types:
trait CategoryTC[P[_], Hom[_, _]]:
type ~>[A, B] = Hom[A, B]
def id[A: P]: A ~> A
extension [A: P, B: P, C: P]
(g: B ~> C) def ◦ (f: A ~> B): A ~> C
In order to represent group homomorphisms we’ll have to cheat: a group homomorphism will be just a regular function between groups.
Ideally we would have at least a smart constructor that verifies the given function satisfies the homomorphism property; alas this would be totally impractical, so we’ll leave it to the user to verify this either in a test suite or just manually.
import zio.prelude.*
case class GroupHom[A: classic.Group, B: classic.Group](f: A => B) extends (A => B):
def apply(a: A) = f(a)
object GroupHomLaws:
def multiplication[A: classic.Group, B: classic.Group](
f: GroupHom[A, B], x: A, y: A
) =
f(x <> y) == (f(x) <> f(y))
Now we can create Grp:
given Grp: CategoryTC[classic.Group, classic.Group]:
def id[A: classic.Group] = GroupHom(identity)
extension [A: classic.Group, B: classic.Group, C: classic.Group]
(g: B ~> C) def ◦ (f: A ~> B): A ~> C =
GroupHom(g compose f)
2. Functors
Functors are graph mappings that preserve arrow composition.
If $C$, $D$ are categories, then a (covariant) functor $F$ from $C$ to $D$ is a tuple $(F_0, map)$ where
 $F_0: Ob(C)\rightarrow Ob(D)$
(instead of $F_0(X)$ it is common to just write $F_X$).
 for every pair of objects $X, X'$ in $C$, a function
$map_{X,X'}: C(X, X')\rightarrow D(F_X, F_{X'})$
 $F$ preserves composition
$F(g f) = F(g) . F(f)$
 $F$ preserves identity morphisms
$F(id_X) = id_{F_X}$
A functor is a data structure that contains a type function F[_]
and a regular function map
.
Since now there are two categories involved we’re going to use C[_,_]
for the types of arrows.
trait Functor[
F[_], Source[_, _], Target[_, _]
](
using
S: Category[Source],
T: Category[Target]
):
// symbolic aliases
type ~>[A, B] = Source[A, B]
type ~>>[A, B] = Target[A, B]
def map[A, B](f: A ~> B): F[A] ~>> F[B]
// helper method to be able to do F(f)
def apply[A, B](f: A ~> B) = map(f)
@Law
def composition[X, Y, Z](f: X ~> Y, g: Y ~> Z) =
map(g ◦ f) <> map(g) ◦ map(f)
@Law
def identities[X] =
map(S.id[X]) <> T.id[F[X]]
On notation
Since dotty supports curried type functions an alternative alias for functors could be
type >[From[_, _], To[_, _]] =
[F[_]] =>> Functor[F, From, To]
To be used like so:
// endofunctors
(C > C)[F]
// Bifunctor
(C1 × C2 > D)[F]
// etc
The downside is that it could be hard to keep track of all different kind of arrows.
2.1 The identity functor on a category C
type Id[A] = A
object Functor:
def identity[C[_, _]: Category]: (C > C) [Id] =
new Functor { def map[X, Y](f: C[X, Y]) = f }
2.2 Endofunctors
A Functor from a category $C$ to itself.
type Endofunctor[F[_], C[_, _]] = (C > C) [F]
Later we’ll use the following given to create Scala
endofunctors from zio.prelude
instances.
import zio.prelude.*
given [F[+_]](using F: classic.Functor[F]): Endofunctor[F, Scala] with
def map[A, B](f: A => B) = F.map(f)
// uses classic.Functor[List] to create our Endofunctor instance
summon[Endofunctor[List, Scala]]
2.3 Bifunctors
A bifunctor is a functor whose domain is the product category
type Bifunctor[F[_, _], Prod[_, _], D[_, _]] =
Functor[[A] =>> F[Fst[A], Snd[A]], Prod, D]
alternatively:
trait Bifunctor2[F[_, _], C1[_, _], C2[_, _], D[_, _]](
given Category[C1 × C2], Category[D]
) extends
Functor[[A] =>> F[Fst[A], Snd[A]], C1 × C2, D]
2.4 The Hom functor
Given a fixed object $X_0$ in a category $C$, the $\mathrm{Hom}$ functor $C \to \mathbb{T}$ sends $A \mapsto \mathrm{Hom}(X_0, A)$.
type Hom[C[_, _], X0] = [A] =>> C[X0, A]
def homFunctor[C[_, _]: Category, X0]: (C > Scala)[C[X0, *]] =
new Functor:
def map[A, B](f: C[A, B]): C[X0, A] => C[X0, B] = f ◦ _
2.5 Functor composition
type ⊙[G[_], F[_]] = [A] =>> G[F[A]]
// G ⊙ F
extension [F[_], G[_], C[_, _], D[_, _], E[_, _]] (
G: (D > E) [G]) def ⊙ (
F: (C > D) [F]
)(using
Category[C],
Category[D],
Category[E]
): (C > E) [G ⊙ F] =
new Functor:
def map[X, Y](f: C[X, Y]) = G(F(f))
3. Natural Transformations
A natural transformation is a family of morphisms between the images of two functors:
Given two functors $F, G: C \to D$ between the same categories, a natural transformation $\varphi: F \to G$ consists of the following data:
For each object $X$ of $C$ a morphism $\varphi X: FX \to GX$ in $D$ so that, for every arrow $f: X \to X'$ in $C$, we have a commutative square in $D$ (naturality condition of $\varphi$ on $f$)
i.e.
$\varphi X'.F(f)= G(f). \varphi X$
trait Nat[From[_], To[_], C[_, _], D[_, _]](
using
Category[C],
Category[D]
) { self =>
val from: (C > D) [From]
val to : (C > D) [To]
type ~>[A, B] = D[A, B]
def apply[X]: From[X] ~> To[X]
@Law
def naturality[X, Y](
F: (C > D) [From],
G: (C > D) [To],
φ: (From ==> To) [C, D],
f: C[X, Y]
) =
φ[Y] ◦ F(f) <> G(f) ◦ φ[X]
}
One could also define an alias (double fat arrow)
type ==>[F[_], G[_]] =
[C[_, _], D[_, _]] =>> Nat[F, G, C, D]
and use it like so
(F ==> G)[C, D]
but same caveats apply regarding “way too many arrows” (TM)
3.1 The identity transformation
object Nat:
def identity[F[_], C[_, _], D[_, _]](
F: (C > D)[F]
)(using
C: Category[C],
D: Category[D]): (F ==> F)[C, D] =
new Nat:
val from = F
val to = F
def apply[X] = D.id[F[X]]
3.2 Vertical composition
Two natural transformations $\varphi: F \to G$ and $\psi: G \to H$ have a vertical composition $\psi\varphi: F \to H$ (also written $\psi.\varphi$)
$(\psi\varphi)(X)=\psi(X).\varphi(X): FX \to HX$
// vertical composition:
// ψ * φ: F ==> H
extension [
F[_],G[_],H[_],
C[_, _],
D[_, _]
] (ψ: (G ==> H)[C, D]) def * (
φ: (F ==> G)[C, D] )
(using
Category[C],
Category[D]): (F ==> H)[C, D]
=
new Nat:
val from = φ.from
val to = ψ.to
def apply[X] = ψ[X] ◦ φ[X]
3.3 Whisker composition
Moreover there is a whisker composition of natural transformations with functors, or reduced horizontal composition, written as $K \varphi H$
$K \varphi H: K F H \to K G H \\ (K \varphi H)(X) = K(\varphi(H X)$
// whisker(K, φ, H): K ⊙ F ⊙ H ==> K ⊙ G ⊙ H
def whisker[
H[_], F[_], G[_], K[_],
Cp[_, _], C[_, _],
D[_, _], Dp[_, _]
](
K: (D > Dp)[K],
φ: (F ==> G )[C, D],
H: (Cp > C )[H],
)(using
Category[Cp],
Category[C],
Category[D],
Category[Dp],
): (K ⊙ F ⊙ H ==> K ⊙ G ⊙ H)[Cp, Dp] =
val F = φ.from
val G = φ.to
new Nat:
val from = K ⊙ F ⊙ H
val to = K ⊙ G ⊙ H
def apply[X] = K(φ[H[X]])
The binary operations $\varphi H$ and $K \varphi$ are also called whisker compositions (obtained by inserting identity functors in the ternary operation)
// (φ *: H): F * H ==> G * H
extension [
H[_], F[_], G[_],
Cp[_, _], C[_, _], D[_, _]
](
φ: (F ==> G)[C, D]) def *: (
H: (Cp > C)[H]
)(using
Category[Cp],
Category[C],
Category[D]
): (F ⊙ H ==> G ⊙ H) [Cp, D] =
whisker(Functor.identity[D], φ, H)
// (K :* φ): K * F ==> K * G
extension [
F[_], G[_], K[_],
C[_, _], D[_, _], Dp[_, _]
](
K: (D > Dp)[K]) def :* (
φ: (F ==> G)[C, D]
)(using
Category[C],
Category[D],
Category[Dp]
): (K ⊙ F ==> K ⊙ G) [C, Dp] =
whisker(K, φ, Functor.identity[C])
We’ve chosen φ *: H
and K :* φ
to have a visual clue of which side is the natural transformation and which side is the functor.
A natural transformation between two functors in Scala ((F ==> G)[Scala, Scala]
) is just a polymorphic function that is capable of transforming one data structure / context into another, without looking at the concrete type argument.
We could say that a functor transforms the contents of a data structure from one type into another:
F[A] > F[B]
whereas a natural transformation performs a structural/context transformation:
F[A] > G[A]
4. Monads
A monad in the category $X$ is a triple $(T, \eta, \mu)$ where $T: X\rightarrow X$ is an endofunctor, while $\eta: 1\rightarrow T$ and $\mu: T^2 \rightarrow T$ are natural transformations (called the unit and multiplication of the monad) which make the following diagrams commute:
(Grandis, p133)
trait Monad[T[_], X[_, _]: Category]:
// redefine ==> locally (for endofunctors)
type ==>[H[_], G[_]] = Nat[H, G, X, X]
def T : Endofunctor[T, X]
def pure : Id ==> T // 𝜂: 1 ==> T
def flatten : (T ⊙ T) ==> T // 𝜇: T² ==> T
@Law
def unitarity1 =
(flatten * (pure *: T)) <> Nat.identity(T)
@Law
def unitarity2 =
(flatten * (T :* pure)) <> Nat.identity(T)
@Law
def associativity =
flatten * (T :* flatten) <> flatten * (flatten *: T)
4.1 Monoids in the category of endofunctors
In fact, a monad on the category $X$ is an internal monoid in the category $C = \mathrm{End}(X)$ of endofunctors of $X$ and their natural transformations, equipped with the strict (nonsymmetric) monoidal structure given by the composition of endofunctors.
Let’s unpack this remark.
4.1.1 Monoidal categories and internal monoids
A (strict) monoidal category $(C, \otimes, E)$ is a category $C$ equipped with a a bifunctor
$\otimes: C \times C \to C$that is associative, and an object $E$ called the unit satisfying
$E \otimes A = A \\ A \otimes E = A \\$
trait Monoidal[C[_, _]] extends Category[C]
type ⨂[_, _]
type E
def tensor: Bifunctor[⨂, C × C, C]
// tensor gives rise to the canonical function
// f ⨂ g:
extension [A1, B1, A2, B2]
( f: A1 ~> B1) def ⨂ (
g: A2 ~> B2): (A1 ⨂ A2) ~> (B1 ⨂ B2) =
tensor[(A1, A2), (B1, B2)]((f, g))
@Law
def unitLeft[A]:
(E ⨂ A) =:= A
@Law
def unitRight[A]:
(A ⨂ E) =:= A
@Law
def associativity[A, B, C]:
(A ⨂ (B ⨂ C)) =:= ((A ⨂ B) ⨂ C)
An internal monoid in $C$ is a triple $(M, e, m)$, consisting of an object $M$ and two arrows $e: E \to M$, $m: M \otimes M \to M$ of $C$, called the unit and multiplication, satisfying:
trait InternalMonoid[C[_, _]](given val C: Monoidal[C]):
import C.{~>, E, ⨂, id}
type M
val e: E ~> M
val m: M ⨂ M ~> M
// laws
@Law
def unitarity1 =
m ◦ (e ⨂ id[M]) <> id[M]
@Law
def unitarity2 =
m ◦ (id[M] ⨂ e) <> id[M]
@Law
def associativity =
m ◦ (m ⨂ id[M]) <> m ◦ (id[M] ⨂ m)
4.1.2 The category of endofunctors and natural transformations
In order to describe this category we’ll need a higher order version of CategoryTC
(that we used to create the category of groups).
// A category of type functions with some constraint P
trait CategoryTC1[P[F[_]], Hom[F[_], G[_]]]:
type ~>[F[_], G[_]] = Hom[F, G]
def id[F[_]](using P[F]): F ~> F
extension [F[_]: P, G[_]: P, H[_]: P]
(m: G ~> H) def ◦ (n: F ~> G): F ~> H
This means objects will be type functions $\mathbb{T} \to \mathbb{T}$ with some constraint represented by P[_[_]]
and Hom
is a function $(\mathbb{T} \to \mathbb{T}, \mathbb{T} \to \mathbb{T}) \to \mathbb{T}$.
// Given a Category[X] creates the category whose objects are
// endofunctors of X and whose morphisms are the natural
// transformations between them.
def endo[X[_, _]: Category] =
type Hom[H[_], G[_]] = (H ==> G)[X, X]
type EndoX[F[_]] = Endofunctor[F, X]
new CategoryTC1[EndoX, Hom]:
def id[F[_]](using f: EndoX[F]): F ~> F =
Nat.identity(f)
extension [F[_]: EndoX, G[_]: EndoX, H[_]: EndoX]
(m: G ~> H) def ◦ (n: F ~> G): F ~> H =
m * n
For example, this is identity natural transformation for List
in the category of endofunctors in Scala:
endo[Scala].id[List]
And this is the category of endofunctors for the Kleisli
category of functions A => Option[B]
:
val optionKleisliEndo = endo[[A, B] =>> Kleisli[Option, A, B]]
4.1.3 Monoids in the category of endofunctors
In fact, a monad on the category $X$ is an internal monoid in the category $C = End(X)$ of endofunctors of $X$ and their natural transformations, equipped with the strict monoidal structure given by the composition of endofunctors.
I won’t rewrite all the definitions needed here in terms of CategoryTC1
, but instead I’ll just ask the reader to compare the structure of InternalMonoid
vs Monad
.
Internal Monoid  Monad 

trait InternalMonoid[C[_, _]] (using val C: Monoidal[C]): import C.{~>, E, ⨂, id} // // type M val e: E ~> M val m: M ⨂ M ~> M 
trait Monad[T[_], X[_, _]]: (using Category[X]) type ==>[F[_], G[_]] = Nat[F, G, X, X] // def T : Endofunctor[T, X] def pure : Id ==> T def flatten : (T * T) ==> T 
unitarity1  
m ◦ (e ⨂ id[M]) <> id[M] 
(flatten * (pure *: T)) <> Nat.identity(T) 
unitarity2  
m ◦ (id[M] ⨂ e) <> id[M] 
(flatten * (T :* pure)) <> Nat.identity(T) 
associativity  
m ◦ (m ⨂ id[M]) <> m ◦ (id[M] ⨂ m) 
flatten * (flatten *: T) <> flatten * (T :* flatten) 
4.2 Monads in Scala
If we set the category to be Scala
(of types and functions) several things happen:

Endofunctor
becomes the usualclassic.Functor

Natural transformations become:
trait Nat[F[_]: classic.Functor, G[_]: classic.Functor]:
def apply[A]: F[A] => G[A]
 Our specialized monad becomes:
trait Monad[T[_]: classic.Functor]:
def pure : Nat[Id, T]
def flatten: Nat[T◦T, T]
 Simplifying even more by inlining the
apply
method of both transformations:
import zio.prelude.*
trait Monad[T[_]: classic.Functor]:
def pure [A]: A => T[A]
def flatten[A]: T[T[A]] => T[A]
def flatMap[A, B](a: T[A])(f: A => T[B]): T[B] =
flatten(Covariant[T].map(f)(a))
voila!
5. The Yoneda lemma
Let $F, G:C\rightarrow Set$ be two functors, with $F=C(X_0, \_)$. The canonical mapping
$\begin{matrix} y: & Nat(F,G) & \rightarrow & G_{X_0} \\ & \varphi & \mapsto & \varphi_{X_0}(id_{X_0}) \end{matrix}$from the set of natural transformations $\varphi:F \rightarrow G$ to the set $G(X_0)$ is a bijection.
The inverse mapping is given by
$\begin{matrix} y': & G_{X_0} & \rightarrow & Nat(Hom(X_0,\_),G) \\ & z & \mapsto & y'(z)_X f:=G_f(z) \ \ \forall X \\ & & & _{f: C(X_0, X)} \end{matrix}$(pp 44)
A bijection between two types A
and B
can be naturally expressed as a instance of the following type
case class Biyection[A, B](
from: A => B,
to : B => A
):
// satisfying laws
@Law
def IdB = (from ◦ to) <> identity[B]
@Law
def IdA = (to ◦ from) <> identity[A]
type ≅[A, B] = Biyection[A, B]
Since our base category is Scala (instead of Set) then both $F, G$ will be functors from $C$ to Scala.
def yonedaLemma[C[_, _], G[_], X0](G: (C > Scala)[G])
(using C: Category[C] ) =
import C.id
val F: (C > Scala)[C[X0, *]] = homFunctor[C, X0]
// at this point we know that F, G are functors
// and C is a category, so we can simplify a bit
// by working with the natural transformation as a
// polymorhic function instead of the wrapper type Nat:
type ==>[F[_], G[_]] =
[X] => F[X] => G[X]
// 
// The Yoneda lemma
// 
// the canonical mapping:
val y : (C[X0, *] ==> G) => G[X0] =
φ => φ[X0]( id[X0] )
// is a bijection with inverse:
val yp: G[X0] => (C[X0, *] ==> G) =
z => ([X] => (f: C[X0, X]) => G(f)(z))
// i.e.
// y ◦ yp <> identity[G[X0]]
// yp ◦ y <> identity[CX0 ==> G]
// Or more concisely:
val yoneda: (C[X0, *] ==> G) ≅ G[X0] =
Bijection(y, yp)
Proof:
// a) yp(y(𝜑)) == 𝜑
def proofPart1(φ: CX0 ==> G) =
// by definition of y:
yp(y(φ)) == yp( φ[X0] { id[X0] } )
// by definition of yp:
yp(y(φ)) == ( [X] => (f: C[X0, X]) => G(f) { φ[X0] { id[X0] } } )
// which in Scala is the same as:
yp(y(φ)) == ( [X] => (f: C[X0, X]) => (G(f) ◦ φ[X0]) { id[X0] } )
// by the naturality condition: G(f) ◦ φ[X0] === φ[X] ◦ F(f)
yp(y(φ)) == ( [X] => (f: C[X0, X]) => (φ[X] ◦ F(f)) { id[X0] } )
yp(y(φ)) == ( [X] => (f: C[X0, X]) => φ[X] { F(f) { id[X0] } } )
// by definition of homFunctor: F(f)( id[X0] ) == f ◦ id[X0]
// and by definition of composition: f ◦ id[X0] == f
yp(y(φ)) == ( [X] => (f: C[X0, X]) => φ[X] { f } )
// applying eta reduction two times:
// yp(y(φ)) == ( [X] => φ[X] ) == φ
yp(y(φ)) == φ
// b) y(yp(z)) == z
def proofPart2(z: G[X0]) =
// by definition of yp:
y(yp(z)) == y( [X] => (f: C[X0, X]) => G(f)(z) )
// by definition of y:
y(yp(z)) == ( [X] => (f: C[X0, X]) => G(f)(z) ) { id[X0] }
// evaluating the right hand side
y(yp(z)) == G(id[X0])(z)
// Since G maps identities to identities:
// G(id[X0]) == Scala.id[G[X0]] == identity[G[X0]] = x => x
y(yp(z)) == z
// Q.E.D
This is pretty much what one would write on paper, except that it is more verbose. The other difference is that the compiler will help us ensure that expressions at least typecheck.
6. Bibliography
 M. Grandis, Category Theory And Applications: A Textbook For Beginners, World Scientific, 2018.
 W. Lawvere, Conceptual Mathematics: A First Introduction to Categories, Cambridge University Press; 2 edition, 2009.
 Scala 3 documentation: https://docs.scalalang.org/.
7. Changelog
 Jun 29, 2022: Scala 3 version 3.1.2
 Code repository added.