# 📖Category Theory for Programmers

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

## 1.1 Motivation and Philosophy

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.

## 1.2 What is a category?

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*

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 typethe 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$

## 8.2 Type algebra, Curry-Howard-Lambek isomorphism

$a^{b+c} = a^b \times a^c$