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.
Maybe too simple.
In category theory, you call types "objects", and call functions "arrows".
id :: a -> a id x = x
compose :: (b -> c) -> (a -> b) -> (a -> c) compose g f = g . f
B, form the product
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