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 paper-like 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, auto-generated 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 re-use 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 beginner-ish, Scala intermediate.

Scala 3 version used: 3.1.2

Updated code available at: https://github.com/jpablo/math-with-scala

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:

1. a set $O$ whose elements are called objects of $C$.

2. for every pair $(X,Y)$ of objects, a set $\mathrm{Hom}(X,Y)$ (called a hom-set), 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)$

3. 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

1. 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,

2. 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 hom-sets 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 “point-free” 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:

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:

1. Via subtyping
2. 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

1. $F_0: Ob(C)\rightarrow Ob(D)$

(instead of $F_0(X)$ it is common to just write $F_X$).

2. for every pair of objects $X, X'$ in $C$, a function

$$map_{X,X'}: C(X, X')\rightarrow D(F_X, F_{X'})$$

3. $F$ preserves composition

$$F(g f) = F(g) . F(f)$$

4. $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 (non-symmetric) 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.

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

m ◦ (e ⨂ id[M]) <-> id[M]

(flatten * (pure *: T)) <-> Nat.identity(T)

 m ◦ (id[M] ⨂ e) <-> id[M]

(flatten * (T :* pure)) <-> Nat.identity(T)

 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 usual classic.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.scala-lang.org/.

7. Changelog

• Jun 29, 2022: Scala 3 version 3.1.2
• Code repository added.