Typista.org

Notes on Category Theory in Scala 3 (Dotty)

December 23, 2019

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.0.0-M1

1. Categories

Informally, a category is a special kind of directed graph with an operation similar to path concatenation defined on the edges.

categories50

A Category CC consists of the following data:

  1. a set OO whose elements are called objects of CC.
  2. for every pair (X,Y)(X,Y) of objects, a set Hom(X,Y)\mathrm{Hom}(X,Y) (called a hom-set), whose elements are called morphisms (or maps, or arrows) of CC from XX to YY and denoted as f:X→Yf: X \rightarrow Y,

The set Hom(X,Y)\mathrm{Hom}(X, Y) is also written as C(X,Y)C(X, Y)

  1. for every triple X,Y,ZX, Y, Z of objects on CC, a mapping or composition
Hom(X,Y)Γ—Hom(Y,Z)β†’Hom(X,Z)(f,g)↦gβ—¦f\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→Yf:X \to Y, g:Y→Zg:Y \to Z, and h:Z→Wh:Z \to W, the equation h◦(g◦f)=(h◦g)◦fh◦(g◦f)=(h◦g)◦f holds,
  2. Identities. Given an object XX, there exists and endomorphism e:X→Xe: X \to X which acts as an identity whenever composition makes sense; in other words if f:X′→Xf: X' \to X and g:X→X′′g:X \to X'', one has e◦f=fe ◦ f = f and g◦e=gg ◦ e = g.

ee is called the identity of XX and written as 1X1_X or idXX.

1.1 Categories over the set of all types 𝕋

Our approach will be to represents objects as types (i.e. elements of the set T\mathbb{T} of all types), and hom-sets as type functions T×T→T\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:

categories

with composition:

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 as Category[Scala]:
  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 OO of the category CC All types (for now)
Hom(X,Y)\mathrm{Hom}(X,Y) (morphisms between XX and YY) Values of type Hom[X, Y]
Function Hom:O×O→Sets\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∈TA, B, C \in\mathbb{T}
Identity morphism 1X1_X for each object XX A value of type id[X] for each type X
Function family X↦1X∈Hom(X,X)X \mapsto 1_X \in \mathrm{Hom}(X,X) Polymorphic function [X] =>> id[X]: Hom[X,X]

The textbook definition allows for the objects OO of the category CC 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:

structure1

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 as Category[<:<]:
  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 CC and DD are categories, one defines the product category CΓ—DC \times D.

An object is a pair (X,Y)(X, Y) where X∈CX \in C and Y∈DY \in D. A morphism is a pair of morphisms

(f,g):(X,Y)β†’(Xβ€²,Yβ€²)(f, g): (X, Y) \to (X', Y')

for f∈C(X,Xβ€²)f\in C(X, X') and g∈D(Y,Yβ€²)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 Fst[X] = X match { 
  case (a, _) => a 
}

type Snd[X] = X match { 
  case (_, b) => b 
}

Morphisms are tuples of morphisms:

type Γ—[~>[_, _], ->[_, _]] = [A, B] =>>
  ( Fst[A] ~> Fst[B],
    Snd[A] -> Snd[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.

monoid

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 CategorySub[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 CategorySub[●,  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 cats.Monoid instance:

// create a new category instance given a cats.Monoid instance
def fromMonoid[M](M: cats.Monoid[M]) = 
  new CategorySub[●, ConstantHom[M]]:
    def id[A <: ●]: M = M.empty
    extension [A <: ●, B <: ●, C <: ●] 
      (g: M) def β—¦ (f: M) = M.combine(g, f)

// usage:
import cats.implicits._

type H[_ <: *, _ <: *] = String

given StringMonoidCat as CategoryS[●, ConstantHom[String]] =
  fromMonoid(cats.Monoid[String])

assert( StringMonoidCat.id == "" )
assert( "a" β—¦ "b" == "ab" )

This construction justifies the following:

A single monoid MM can be viewed as a category with one formal object βˆ—*.

The morphisms x:βˆ—β†’βˆ—x: * \to * are the elements of MM, composed by the multiplication xyx y of the monoid, with identity id(βˆ—)=1id(*) = 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. cats.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 cats.Group
import cats.implicits._
import scala.language.implicitConversions

case class GroupHom[A: Group, B: Group](f: A => B) extends (A => B)
  def apply(a: A) = f(a)

object GroupHomLaws:
  def multiplication[A: Group, B: Group](
    f: GroupHom[A, B], x: A, y: A
  ) = 
    f(x |+| y) <-> f(x) |+| f(y)

Now we can create Grp:

given Grp as CategoryTC[Group, GroupHom]:

  def id[A: Group] = GroupHom(identity)

  extension [A: Group, B: Group, C: Group] 
		(g: B ~> C) def β—¦ (f: A ~> B): A ~> C =
    GroupHom(g compose f)

2. Functors

Functors are graph mappings that preserve arrow composition.

monoid

If CC, DD are categories, then a (covariant) functor FF from CC to DD is a tuple (F0,map)(F_0, map) where

  1. F0:Ob(C)β†’Ob(D)F_0: Ob(C)\rightarrow Ob(D)

(instead of F0(X)F_0(X) it is common to just write FXF_X).

  1. for every pair of objects X,Xβ€²X, X' in CC, a function
mapX,Xβ€²:C(X,Xβ€²)β†’D(FX,FXβ€²)map_{X,X'}: C(X, X')\rightarrow D(F_X, F_{X'})
  1. FF preserves composition
F(gf)=F(g).F(f)F(g f) = F(g) . F(f)
  1. FF preserves identity morphisms
F(idX)=idFXF(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 CC to itself.

type Endofunctor[F[_], C[_, _]] = (C --> C) [F]

Later we’ll use the following given to create Scala endofunctors from cats instances.

import scala.language.implicitConversions

given [F[_]](using F: cats.Functor[F]) as Endofunctor[F, Scala]:
  def map[A, B](f: A => B) = F.lift(f)

import cats.implicits._
// uses cats.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 X0X_0 in a category CC, the Hom\mathrm{Hom} functor Cβ†’TC \to \mathbb{T} sends A↦Hom(X0,A)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:

monoid

Given two functors F,G:C→DF, G: C \to D between the same categories, a natural transformation φ:F→G\varphi: F \to G consists of the following data:

For each object XX of CC a morphism φX:FX→GX\varphi X: FX \to GX in DD so that, for every arrow f:X→X′f: X \to X' in CC, we have a commutative square in DD (naturality condition of φ\varphi on ff)

nat-diagram

i.e.

Ο†Xβ€².F(f)=G(f).Ο†X\varphi X'.F(f)= G(f). \varphi X

​

natural transformations1
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 Ο†:Fβ†’G\varphi: F \to G and ψ:Gβ†’H\psi: G \to H have a vertical composition ΟˆΟ†:Fβ†’H\psi\varphi: F \to H (also written ψ.Ο†\psi.\varphi)

(ΟˆΟ†)(X)=ψ(X).Ο†(X):FXβ†’HX(\psi\varphi)(X)=\psi(X).\varphi(X): FX \to HX
natural transformations composition
// 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φHK \varphi H

KφH:KFH→KGH(KφH)(X)=K(φ(HX)K \varphi H: K F H \to K G H \\ (K \varphi H)(X) = K(\varphi(H X)

monoid

// 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 φH\varphi H and Kφ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 XX is a triple (T,η,μ)(T, \eta, \mu) where T:X→XT: X\rightarrow X is an endofunctor, while η:1→T\eta: 1\rightarrow T and μ:T2→T\mu: T^2 \rightarrow T are natural transformations (called the unit and multiplication of the monad) which make the following diagrams commute:

image-20190923221121457

(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 XX is an internal monoid in the category C=End(X)C = \mathrm{End}(X) of endofunctors of XX 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,βŠ—,E)(C, \otimes, E) is a category CC equipped with a a bifunctor

βŠ—:CΓ—Cβ†’C\otimes: C \times C \to C

that is associative, and an object EE called the unit satisfying

EβŠ—A=AAβŠ—E=AE \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 CC is a triple (M,e,m)(M, e, m), consisting of an object MM and two arrows e:Eβ†’Me: E \to M, m:MβŠ—Mβ†’Mm: M \otimes M \to M of CC, called the unit and multiplication, satisfying:

internal monoid
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 T→T\mathbb{T} \to \mathbb{T} with some constraint represented by P[_[_]] and Hom is a function (T→T,T→T)→T(\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 XX is an internal monoid in the category C=End(X)C = End(X) of endofunctors of XX 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 usual cats.Functor
  • Natural transformations become:
trait Nat[F[_]: cats.Functor, G[_]: cats.Functor]:
  def apply[A]: F[A] => G[A]
  • Our specialized monad becomes:
trait Monad[T[_]: cats.Functor]:
  def pure   : Nat[Id,  T]
  def flatten: Nat[Tβ—¦T, T]
  • Simplifying even more by inlining the apply method of both transformations:
trait Monad[T[_]: cats.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(cats.Functor[T].map(a)(f))

voila!

5. The Yoneda lemma

Let F,G:C→SetF, G:C\rightarrow Set be two functors, with F=C(X0,_)F=C(X_0, \_). The canonical mapping

y:Nat(F,G)β†’GX0φ↦φX0(idX0)\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 φ:F→G\varphi:F \rightarrow G to the set G(X0)G(X_0) is a bijection.

The inverse mapping is given by

yβ€²:GX0β†’Nat(Hom(X0,_),G)z↦yβ€²(z)Xf:=Gf(z)Β Β βˆ€Xf:C(X0,X)\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,GF, G will be functors from CC 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.
  • Dotty 0.20.0-RC1 documentation: https://dotty.epfl.ch/docs.

7. Changelog

Nov 19, 2020: Scala 3 version 3.0.0-M1