Understanding the diagrams of Product and Coproduct

Question

I am trying to understand the Product and Coproduct corresponding to the following picture:

Product:

Coproduct:

As I understand, a Product type in Haskell is for example:

data Pair = P Int Double

and a Sumtype is:

data Pair = I Int | D Double 

How to understand the images in relation with Sum and Product type?

The images are from http://blog.higher-order.com/blog/2014/03/19/monoid-morphisms-products-coproducts/.

Answer 1

So as far as I can tell, the idea behind these diagrams is that you are given:

• types A, B and Z
• function f and g of the indicated types (in the first diagram, f :: Z -> A and g :: Z -> B, in the second the arrows go "the other way", so f :: A -> Z and g :: B -> Z).

I'll concentrate on the first diagram for now, so that I don't have to say everything twice with slight variations.

Anyway, given the above, the idea is that there is a type M together with functions fst :: M -> A, snd :: M -> B, and h :: Z -> M such that, as the mathematicians say, the diagram "commutes". By that is simply meant that, given any two points in the diagram, if you follow the arrows in any way from one to the other, the resulting functions are the same. That is, f is the same as fst . h and g is the same as snd . h

It is easy to see that, no matter what Z is, the pair type (A, B), together with the usual Haskell functions fst and snd, satisfies this - together with an appropriate choice of h, which is:

h z = (f z, g z)

which trivially satisfies the two required identities for the diagram to commute.

That's a basic explanation of the diagram. But you may be slightly confused about the role of Z in all this. That arises because what's actually being stated is rather stronger. It is that, given A, B, f and g, there is an M together with functions fst and snd, that you can construct such a diagram for any type Z (which means supplying a function h :: Z -> M as well). And further that there is only one function h which satisfies the required properties.

It's pretty clear, once you play with it and understand the various requirements, that the pair (A, B), and various other types isomorphic to it (which basically means MyPair A B where you've defined data MyPair a b = MyPair a b), are the only things which satisfy this. And that there are other types M which would also work, but which would give various different hs - eg. take M to be a triple (A, B, Int), with fst and snd extracting ("projecting to" in mathematical terminology) the first and second components, and then h z = (f z, g z, x) is such a function for any x :: Int that you care to name.

It's been too long since I studied mathematics, and category theory in particular, to be able to prove that the pair (A, B) is the only type that satisfies the "universal property" we're talking about - but rest assured that it is, and you really don't need to understand that (or really any of this) in order to be able to program with product and sum types in Haskell.

The second diagram is more or less the same, but with all the arrows reversed. In this case the "coproduct" or "sum" M of A and B turns out to be Either a b (or something isomoprhic to it), and h :: M -> Z will be defined as:

h (Left a) = f a
h (Right b) = g b