August 11, 2016

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

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.

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.

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
```

- 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`

- Given the objects

**leaving off at 11:41**