# Notes: Categories for the Working Programmer

August 11, 2016

*These are my notes from Wadler's presentation Categories for the Working Programmer from Joy of Coding, 17 June 2016.*

## Background

Propositions as types is a really cool idea from th 1930s. It comes from the formalization of core ideas behind both logic and programming languages.

- In 1980 Howard publishes a paper showing that propositions and types are the same thing

This was the subject of Wadler's talk at Strange Loop.

## Premise

Propositions as types has deep connections to category theory.

The key idea behind category theory: Take some concept that some people know really well, and abstract it to the level where it becomes impossible to understand.

Things that you know well, made difficult.

## Simplest possible introduction to category theory

Maybe *too* simple.

- Category theory is object-oriented programming?
- It's got objects!
- Except "object" in category theory is the name of a type

- What are types good for?
- They describe functions
- A function has an argument of a given type and a result of a given type

In category theory, you call types "objects", and call functions "arrows".

Identity function:

```
id :: a -> a
id x = x
```

Function composition:

```
compose :: (b -> c) -> (a -> b) -> (a -> c)
compose g f = g . f
```

## The three most important structures in programming languages

- And how they arise in category theory
- They're also the three most important structures in logic
- Something something Curry-Howard

- The product
- Given the objects
`A`

and `B`

, form the product `AxB`

- In set theory, these are Cartesian products
In a programming language, these are *tuples* or *records*

```
data Object = A | B
type AxB = (A, B)
first :: AxB -> Object
first (a, _) = a
second :: AxB -> Object
second (_, b) = b
```

**leaving off at 11:41**