# 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
1. 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