# 📖Category Theory for Programmers

- authors
- Milewski, Bartosz
- year
- 2016
- url
- https://www.youtube.com/playlist?list=PLbgaMIhjbmEnaH_LTkxLI7FMa2HsnawM_

Category Theory 1.1: Motivation and Philosophy

Curry–Howard–Lambek correspondence

- Computation–Logic–Category theory are isomorphic

OOP is bad for concurrent programming because OOP hides data mutation and sharing (pointers). Mixing sharing and mutation is

*data race*.- this makes objects non-composable
- locks do not compose either

Template metaprogramming in C++ draws many ideas from Haskell. So you translate Haskell ideas into ugly C++ metaprogramming language.

- Haskell draws many ideas from Category Theory. So you translate concise Category Theory ideas into ugly Haskell language.

Category Theory unifies different branches of mathematics: type theory, logic, algebra, etc.

- Mathematics get philosophical: do mathematicians invent things or discover truth?

It might be that composition and this universal structure is not the property of the universe, but the property of human minds.

- It might be that humans evolved to work with abstraction and composition, and we don’t understand what we can’t explore using these tools.
- In that sense, Category Theory might be about human minds really and be closer to epistemology.

Category Theory 1.2: What is a category?

7.1: Functoriality, bifunctors

- Functors consist of functions and functions compose, so we can compose functors
- Identity functor is trivial
Cat = Category of functors

- Objects are categories
- Morphisms are functors
- It’s a category of small categories. For large categories, we need a more powerful mechanisms

- (Now, Haskell does not really allow composition of functors. If you have a
`Maybe [Int]`

(composition of two functors: Maybe and []), you have to use two fmaps instead of one.) - all algebraic data types are automatically functorial
bifunctor — is a functor from a product category (C×D → E)

- sum type is bifunctor as well

7.2: Monoidal Categories, Functoriality of ADTs, Profunctors

(cartesian) product (operator) + terminal object (Void) (a unit) is a monoidal category

terminal object is a unit of product

- by the same token, coproduct + initial object is a monoidal category
a monoidal category (or

*tensor category*)a bifunctor: $\otimes: C \times C \to C$ called a

*tensor product*- (e.g., product or coproduct)

- an object $I$ or $1$ called the
*unit object*or*identity object*.

Contravariant functor — is a functor defined on the opposite category (cofunctor? no)

haskelly-speaking

`class Contravariant f where contramap :: (a -> b) -> f b -> f a -- must satisfy: -- contramap id = id -- contramap f . contramap g = contramap (g . f)`

- (Strictly speaking, “cofunctor” is not the right name as the dual of a functor is a functor)
- you can think of Contravariant as an opposite of container. it does not contain As, but it requires As

function

`(->) a b`

is Contravariant in`a`

and Covariant in`b`

$C^{op} \times C \to C$

- that is called a
*Profunctor*

- that is called a
haskell

`class Profunctor p where dimap :: (a' -> a) -> (b -> b') -> p a b -> p a' b' instance Profunctor (->) where -- dimap :: (a' -> a) -> (b -> b') -> (a -> b) -> (a' -> b') dimap f g h = g . h . f`

- (how does that definition match to the Profunctor definition on wikipedia or nLab? $\phi: C \nrightarrow D \equiv \phi: D^{op}\times{}C \to Set$)

8.1: Function objects, exponentials

hom-set between two objects (if it’s a set), can be represented as an object in the same category

- “internal hom-set”

function objects:

pattern

`z`

is a function,`a`

is an argument type,`b`

—result type- the category must have products

universal construction

$\var{a \Rightarrow b} \text{ is a function object} \iff \forall z, \exists! h: z \to (a \Rightarrow b) \ni g = \var{eval} \circ (h \times id)$

- (this relies on that a morphism between two products can be constructed as a product of two morphisms ($h$ and $id$ here), and we know that that is a correct way to obtain $(a \Rightarrow b) \times a$ from $z \times a$ using $h: z \to (a \Rightarrow b)$)

in haskell, the next two are equivalent

`h :: z -> (a -> b) g :: (z, a) -> b`

(currying)

`curry :: ((a, b) -> c) -> (a -> (b -> c)) curry f = \a -> \b -> f (a, b) uncurry :: (a -> (b -> c)) -> ((a, b) -> c) uncurry f = \(a, b) -> f a b`

exponentials

- $a \Rightarrow b \equiv b^a$
e.g., $Bool \to Int \equiv (Int, Int) \equiv Int \times Int \equiv Int^2 \equiv Int^{Bool}$

- $1 = ()$
- $2 = Bool$

cartesian closed category (CCC)

- cartesian — has products
closed — has all exponentials $\forall{}a,b, \exists{}a^b$

- A category $C$ is closed if for any pair $a,b$ of objects the collection of morphisms from $a$ to $b$ can be regarded as forming itself an object of $C$.

- has a terminal object (0th power of an object)

Bicartesian closed category (BCCC)

- has products, co-products, exponentials, and initial and terminal objects
- bicartesian = both cartesian and cocartesian

- $a^0 = 1 \implies Void \to a \sim ()$ (
`absurd`

) - $1^a = 1 \implies a \to () \sim ()$
- $a^1 = a \implies () \to a \sim a$