“Category Theory for Programmers”

July 14, 2020 in Languages, Math by hundalhh | 1 comment

I’ve been reading “Category Theory for Programmers” which was suggested to me by Mark Ettinger.  This book presents many examples in C++ and Haskell.  It teaches you some Haskell as you read the book.  It uses almost zero upper level mathematics and it skips almost all of the mathematical formalities.  If you decide that you want to read it, then you might want to read the first six chapters of “Learn You a Haskell for Great Good!” and write a few small Haskell programs first.  (I also would suggest trying to solve the first three problems in Project Euler https://projecteuler.net/archives  using Haskell.)

I find the book to be easy to read and informative.  When the author makes a statement like   A*(B+C) = A*B + A*C where * means categorical product, + means coproduct, and = means isomorphic, I find myself trying to figure out the categories where the statement is true and the categories for which it is false.  (It is true for the Category of Set and the Category Hask.  The book is mostly about those categories.) That type of thinking improves my understanding of category theory.  The book is also reawakening the parts of my brain that had forgotten parts of category theory and Haskell.

Interestingly, in category theory, $A*(B+C) = A*B + A*C$ can be translated into the following theorems :

  1.  A*(B+C) = A*B + A*C  is true for all positive integers A,B, and C,
  2. max(A, min(B,C)) = min( max(A,B), max(A,C))  for all real numbers A, B, and C,
  3. lcm(A, gcd(B,C)) = gcd( lcm(A,B), lcm(A,C) )   where  lcm means least common multiple and gcd means greatest common denominator, and
  4. intersection(A, union(B,C)) = union( intersection(A,B), intersection(A, C)).
If you don’t believe the four theorems, here is some Mathematica Code which tests each theorem:
Unprotect[C];
test[ funcRandChoose_, prod_, sum_, i_] := Tally[ Table[ 
     A = funcRandChoose[];
     B = funcRandChoose[];
     C = funcRandChoose[];
      prod[ A, sum[B, C]] == sum[ prod[A, B] , prod[A, C]], 
 {i}]];

test[ RandomInteger[{1, 1000}] &, Times, Plus, 100]
test[ RandomInteger[{-1000, 1000}] &, Max, Min, 100]
test[ RandomInteger[{-1000, 1000}] &, LCM, GCD, 100]
test[ RandomSample[ Subsets[ Range[5]]] &, Intersection, Union, 100]

1 comment

  1. hundalhh’s avatar

    hundalhh on July 14, 2020 at 10:20 am

    On reddit, someone pointed out that you can always find an arrow from (A*B)+(A*C) to A*(B+C). Here is a proof.

    Def: If X+Y is the coproduct of X and Y, let inj(X, X+Y) and inj(Y,X+Y) be the associated injection arrows.

    Def: If X*Y is the product of X and Y, let pro(X*Y,X) and pro(X*Y, Y) be the associated projection arrows.

    Def: If aXY is an arrow from X to Y and aYZ is an arrow from Y to Z, then let

    comp(aYZ, aXY)

    be the composition of aYZ and aXY. comp(aYZ, aXY) is an arrow from X to Z.

    Notation: If you have two arrows f:Z->X, and g:Z->Y, the let be the unique arrow from Z to X*Y such that

    comp( pro(X*Y,X) , ) = f and
    comp( pro(X*Y,Y) ,     ) = g. (The existence of comes from the definition of X*Y.)

    Notation: If you have two arrows f:X->Z, and g:Y->Z, the let [f,g] be the unique arrow from X+Y to Z such that

    comp( [f,g], inj(X,X+Y) ) = f and
    comp( [f,g], inj(Y,X+Y) ) = g. (The existence of [f,g] comes from the definition of X+Y.)

    1) Let a_1 = comp( inj(B, B+C), pro(A*B, B). a_1: A*B -> B+C.
    2) Let a_2 = comp( inj(B, B+C), pro(A*C, C). a_2: A*C -> B+C.
    3) Let a_3 = [a_1, a_2]. a_3:(A*B)+(A*C) -> B+C.
    4) Let a_4 = [pro(A*B,A), pro(A*C,A)]. a_4:(A*B)+(A*C) -> A.
    5) Let a_5 = . a_5:(A*B)+(A*C) -> A*(B+C).

    a_5 is jagr2808’s arrow.

    (I am not a category theorist, so this notation may be totally non-standard, or maybe I saw it somewhere.)

Comments are now closed.