Category Theory for Programmers
- redraw pictures of ƒ(A)=B so that the morphisms look like • and the objects look like →. Hey, why not?
- string diagrams (process networks) are just as good as algebraic symbology
- tensor products
switch( switch( • )) ≠ •, then* you’ve got a braided category, which is described by the algebra of knots. “I’m not sure why you would want your programming language to include the algebra of knots at a basic level, but … you could.” I think braided code totally makes sense … in a visualising-a-big-system-of-code kind of way.
*Technically speaking: in Haskell it’s always true for every
• input that
switch( switch( • )) ≠ • . If we were talking about a language where
switch( switch( • )) ≠ • is not always true — sometimes or possibly not true — then that language would be a braided category.
∃x | ¬ p(x) = ¬∀x p(x) — all symbols spoken in the subjunctive.