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.


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.

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.

Simplest possible introduction to category theory

Maybe too simple.

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

  1. The product

leaving off at 11:41