In Philip Wadler's presentation, "Category Theory for the Working Hacker", something confused me. At about 30:52, he says:
We need this additional construct which is called distributivity. Here it is, right? It just says "given a choice of an A or a C and a choice of a B or a C, we can get a choice of an A or a B and a C."
This is shown on the slide as:
$$ (A + C)\times(B + C) \cong (A + B) \times C $$
Is this correct? I have the following doubts about it:
- I think that, in Boolean algebra, the distributive property would give $ (A + C)\times(B + C) = (A \times B) + C $.
- Given a choice of an A or a C and a choice of a B or a C, we might choose C both times, giving us only a C and a C. For example, in Haskell:
data AorC = ACA A | ACC C -- sum type data BorC = BCB B | BCC C -- sum type data Prod = Prod AorC BorC -- product type cAndC = Prod (ACC c1) (BCC c2) -- choose type C both times