3
$\begingroup$

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
$\endgroup$
  • 1
    $\begingroup$ 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). $\endgroup$ – Chai T. Rex Feb 20 '17 at 0:13
  • 5
    $\begingroup$ 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. $\endgroup$ – Derek Elkins left SE Feb 20 '17 at 0:41
  • $\begingroup$ @DerekElkins, OK, thanks. Time to rewatch it. $\endgroup$ – Chai T. Rex Feb 20 '17 at 18:20
  • 3
    $\begingroup$ 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. $\endgroup$ – chi Feb 20 '17 at 19:43
  • 1
    $\begingroup$ @chi, want to write that as an answer so we can upvote it, and the question can be treated as answered? $\endgroup$ – D.W. Feb 20 '17 at 22:46
4
$\begingroup$

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.

| cite | improve this answer | |
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.