Categories for the working hacker

https://www.youtube.com/watch?v=gui_SE8rJUM

Another banger by Philip Wadler (the guy who added generics to Java). Though the essence of the talk is:

• Basic (loose) category definition
• Product category
  • Actually, from what I understood, this is about extending a category to include some new object $A\times B$ given objects $A,B$ in the existing category, and the minimum extra morphisms you'd need to add (namely $fst:A\times B\to A$ and $snd:A\times B\to B$) so that the extended object class (collection) still forms a category; even if you include a new arbitrary morphism from some other object $C$, ie $f:C\to A\times B$, then as long as you have $fst$, you can still compose them like $(fst\circ f):C\to A$ and $(snd\circ f):C\to B$.
  • Technically, a product of categories is a construction where the objects class satisfies $\mathrm{\forall }A\in obj(C),\mathrm{\forall }B\in obj(D),(A,B)\in obj(C\times D)$ . This is not the same as adding the product of a particular pair of objects in an existing category to that category's object class.
• Sum category. Analogous to above; not really the sum category, but an extension of an existing category.
• Correspondences between categories, programming and logic
  • There is a correspondence between extending a category to include products of objects, and proving logical conjunction. I think this correspondence is saying that "proving $(fst\circ f):C\to A$ is in a category is the same as proving $(C⟹A\wedge B)⟹A$". Or rather, it is equivalent to say:
    1. If $f:C\to A\times B$ and $fst:A\times B\to A$ are in $\text{mor}(\mathcal{C})$ and $\mathcal{C}$ is a category then $(fst\circ f):C\to A$ is also in $\text{mor}(\mathcal{C})$.
    2. If $C⟹A\wedge B$ then $C⟹A$, which can be read as: "if (if C then A and B) then (if C then A)"
  • Similarly there is a correspondence between extending a category to include sums of objects and proving logical disjunction.
  • There is a correspondence between categories and types; categories including products of objects correspond to product types; ditto for categories including sums and union (aka sum) types.
  • Conjunction and disjunction are opposites of each other (De Morgan's law); product extensions and sum extensions are dual categories of each other.
  • By the Curry-Howard correspondence, simple categories with products and sums correspond to the simply typed lambda calculus, "System $F$".
• Some blockchain companies are using basic category theory as the foundation for definitions of smart contracts. Others (including Philip's at the time, I think) are using "System $F\omega$ ", which is basically "typed lambda calculus with type constructors (like List, Maybe)", aka Elm!.

Questions

1. Why can't the compiler permit arbitrarily big tuples by generating functions for them? If $A\times (B\times C)\cong (A\times B)\times C$ then why can't we just parse tuple definitions like x : (a,b,c) instead as x : (a,(b,c)) and take f: (a,b,c) -> d to mean g : (a,(b,c)) -> d where f (a,b,c) = g (a,(b,c)). Then if we write (a,b,c) we can take fst : (a,b,c) -> a to mean fst : (a,(b,c)) -> a, and snd : (a,b,c) -> b to mean snd : (a(b,c,)) -> b where snd abc = snd . snd $ abc. Generically, we can generate get_i : (a,b,...,n) -> t_i where t_1 = a, t_2 = b, ..., t_n = n and the compiler can yell at you if you don't satisfy $1\le i<n$ ?
   1. You can encode these yourself of course. Also, probably, 27 (as is the case in Haskell) is probably practically enough. However, it hurts only a little bit that the compiler doesn't recognise this. Perhaps with a preprocessor, this would be perfectly fine.

data Product a b =
	Pair { fst :: a, snd :: b}

-- shorthand
-- (a,b) = Product a b

-- Generated by compiler when it sees (a,b,c)
module T3 (..) where
to_pair_3 : (a,b,c) -> (a,(b,c))
to_pair_3 (a,b,c) = (a,(b,c))

get_1 : (a,b,c) -> a
get_1 = fst . to_pair_3

get_2 : (a,b,c) -> b
get_2 = fst . snd . to_pair_3

get_3 : (a,b,c) -> c
get_3 = snd . snd . to_pair_3

-- Generated by compiler when it sees (a,b,c,d)
module T4 (..) where

to_pair_4 : (a,b,c,d) -> (a,(b,(c,d)))
to_pair_4 (a,b,c,d) = (a,(b,(c,d)))

get_1 : (a,b,c,d) -> a
get_1 = fst . to_pair_4

get_2 : (a,b,c,d) -> b
get_2 = fst . snd . to_pair_4

get_3 : (a,b,c,d) -> c
get_3 = fst . snd . snd . to_pair_4

get_4 : (a,b,c,d) -> d
get_4 = snd . snd . snd . to_pair_4