Skip to content

Latest commit

 

History

History
263 lines (191 loc) · 6.89 KB

algebraofalgebra.org

File metadata and controls

263 lines (191 loc) · 6.89 KB
Raw

The Categorical Perspective

Haskell and Category Theory

./dk-hask.png

What is Category Theory?

Introduction

Sometime called the Algebra of Algebra by Thorsten Altenkirch or “abstract nonsense” – anon mathematician.

Category Theory grew out of the fields of abstract algebra and algebraic topology and was introduced in the seminal work of Saunders Mac Lane, “Categories for the Working Mathematician” [cite: @maclane]. It’s goal is to provide a unified and (essentially) abstract view of mathematical structure across multiple fields.

References

An excellent introduction for working programmers drawing examples in C++ and Haskell is given by Bartosz Milewski in his online Category Theory for Programmers and printed volume [cite:@milewski]

A more mathematically orientend introduction can be found in An Introduction to Category Theory by Harold Simmons [cite:@simmons]; which is accompanied by downloadable solutions to exercises making it suitable for self study.

A more comprehensive approach can be followed in Steve Awodey’s - Category Theory [cite:@awodey].

Basic Concepts

Category

Objects (could be only one)

\begin{equation*} \resizebox{10cm}{!}{% \begin{tikzpicture} \node (A) {$A$}; \node (B) [right of=A] {$B$}; \end{tikzpicture} } \end{equation*}

Arrows/morphisms

\begin{equation*} \resizebox{10cm}{!}{% \begin{tikzpicture} \node (A) {$A$}; \node (B) [right of=B] {$B$}; \draw [->] (A) to node {$$} (B); \end{tikzpicture} } \end{equation*}

Identity arrows

\begin{equation*} \resizebox{10cm}{!}{% \begin{tikzpicture}[every edge quotes/.append style = {font=\tiny}] \node (A) {$A$}; \node (B) [below of=A] {$B$}; \path[->] (B) edge [out=210, in=150, loop, “${\tiny id_B}$”] (B); \path[->] (A) edge [out=210, in=150, looseness=5, loop, “$id_A$”] (A); \end{tikzpicture} } \end{equation*}

Associative composition of arrows

\begin{equation*} \resizebox{7cm}{!}{% \begin{tikzpicture}[node distance=3cm, auto] \node (A) {$A$}; \node (B) [below of=A] {$B$}; \node (C) [right of=B] {$C$}; \draw [->] (A) to node {$g ˆ f$} (C); \draw [->] (A) to node {$f$} (B); \draw [->] (B) to node {$g$} (C); \end{tikzpicture} } \end{equation*}

Such that the diagram “commutes”

In Haskell

{-# LANGUAGE NoImplicitPrelude #-}
class Category cat where
  id :: cat a a
  (.) :: cat b c -> cat a b -> cat a c

Category Hask?

Types are the objects in the category Hask

And pure functions are the morphisms in Hask

We also have: id : ∀ a. a -> a

But none of this is true really!

-------

CBut if we ignore ⊥ inhabiting every type
Haskand handwave a bit…

-------

We have a useful fiction

import qualified GHC.Base as Base (id, (.))

instance Category (->) where
  id = Base.id
  (.) = (Base..)

Monoid

Not strictly a concept from category theory but from abstract algebra and probably the most fundamental structure in computation (even mathematics).

  1. A Set with an associative binary operator:

    (x ⊕ y) ⊕ z ≡ x ⊕ (y ⊕ z)

  2. And an identity element:

    e ⊕ x ≡ x x ⊕ e ≡ x

Examples of monoids

  • Basic arithmetic over the set of natural numbers (ℕ) (ℕ,+,0) and (ℕ,*,1)
  • String concatenation (String, ++, “”)

Monoid as a category

A general monoid (M,*,𝟙) is a single object category the set M

equipt with a binary operation: * : M x M -> M

the arrows are the elements of the set {x, y, z...} ∈ M

With a unit element 𝟙

such that: x * (y * z) ≡ (x * y) * z and 𝟙 * x ≡ x ≡ x * 𝟙

The composition of the arrows is the binary operation: x * y

Monoid abstractly

class Monoid m where
  μ :: (m, m) -> m    -- "multiplication"
  η :: () -> m        -- identity (unit of "multiplication")

Functor

Is morphism (arrow) between categories: F(A) -> F(B)

An endofunctor is a functor where the source and target are the same category: F(C) -> F(C)

Functors map objects and arrows in such a way as to preserve structure (composition, diagrams and identities). Functoriality conditions: F(g . f) == F(g) . F(f)

F(id) = id F

Natural Transformations

Natural transformations are morphisms between functors

In Hask the natural transformations between functors are (polymorphic) functions between Functors:

α : f a -> g a

head :: List a -> Maybe a

Category of functors

Of course these form a category of functors (a.k.a. 2-categories)

\begin{equation*} \resizebox{10cm}{!}{%} \begin{tikzpicture}[node distance=3cm, auto] \node (FC) {$F(C)$}; \node (FD) [right of=FC] {$F(D)$}; \node (GC) [below of=FC] {$G(C)$}; \node (GD) [right of=GC] {$G(D)$}; \draw [->] (FC) to node {$F(f)$} (FD); \draw [->] (GC) to node {$G(f)$} (GD); \draw [->] (FC) to node {$α_C$} (GC); \draw [->] (FD) to node {$α_D$} (GD); \end{tikzpicture} } \end{equation*}

Where the morphisms are natural tranformations and the objects are functors.

(C D : Cat; F G : Functor; f is a morphism in its category)

It’s n-categories all the way down…

✓ Category theory for programmers - Bartosz Milewski

⚙ Monads made difficult - Stephen Diehl

⚙ A categorical view of computational effects - Emily Riehl (Lambda world 2019)

🤯n-Category Café

🌻nlab