# Distributive property with sum types and product types

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

• That's where I'm getting stuck. Why can't you choose $C$ both times? I'm getting my intuition, which is probably wrong, from Haskell, where if I have data AorC = ACA A | ACC C; data BorC = BCB B | BCC C; data Prod = Prod AorC BorC, where AorC and BorC are sum types and Prod is a product of the two sum types, and you can choose C in both with Prod (ACC c1) (BCC c2). – Chai T. Rex Feb 20 '17 at 0:13
• You can tell from the explicit definition of the isomorphism on that slide that it is definitely a "typo", which would've been my expectation without looking at the slide. – Derek Elkins left SE Feb 20 '17 at 0:41
• @DerekElkins, OK, thanks. Time to rewatch it. – Chai T. Rex Feb 20 '17 at 18:20
• Polynomial types form a commutative semiring. Roughly, all the basic arithmetic laws for plus and times hold as expected, up to iso. It probably should be $(A\times C) + (B \times C) \simeq (A+B)\times C$, I guess. – chi Feb 20 '17 at 19:43
• @chi, want to write that as an answer so we can upvote it, and the question can be treated as answered? – D.W. Feb 20 '17 at 22:46

Polynomial types (those obtained through $+,\times,0,1$ and type variables) form a commutative semiring.
Basically, all the elementary arithmetic laws for $+$ and $\times$ hold as expected, up to (natural) isomorphism. These include commutativity, associativity, and distributivity of $\times$ over $+$.
More concretely, the distributive law is $$(A\times C)+(B\times C) \simeq (A+B)\times C$$ and I think this was the law that Philip Wadler meant to show.