Product and Sum in Category Theory

Even if you are not a functional programmer, the notion of product type should be familiar to you, e.g.,

Pair<A, B>

in Java is a product type of

A

and

B

. But the definition in category theory is not that easy to comprehend. Here is how it is defined on Wikipedia:


Why is it defined that way and how do we interpret it? Let me translate it into something that Java programmers can understand. The definition actually says, if

X1 x X2

is a product type of

X1

and

X2

with two functions

π1 : X -> X1

and

π2 : X -> X2

, there must be a unique function

f : Y -> X1 × X2

which satisfies the property: for any value

y

of type

Y

, function

f1 : Y -> X1

and a function

f2 : Y -> X2

, the equations

π1(f(y)) == f1(y)

and

π2(f(y)) == f2(y)

must always be true.

In other words, if I define my product type as usual like:

// Java
class Pair<X1, X2> {
private final X1 x1;
private final X2 x2;

public Pair(X1 x1, X2 x2) {
this.x1 = x1;
this.x2 = x2;
}

public X1 getX1() {
return x1;
}

public X2 getX2() {
return x2;
}
}

There must be a unique

f

which is constructed by:

// Java
Function<Y, Pair<X1, X2>> makeF(Function<Y, X1> f1, Function<Y, X2> f2) {
return (Y y) -> new Pair(f1.apply(y), f2.apply(y));
}

In other words, product type guarantees that if you have a function of type

Y -> X1

and a function of type

Y -> X2

, you must have a unique function of type

Y -> X1 x X2

satisfying the property. The property can be expressed programatically as: for any

y

,

f1

and

f2

, the following test must pass.

// Java
void testProductType(Y y, Function<Y, X1> f1, Function<Y, X2> f2) {
Function<Y, Pair<X1, X2>> f = makeF(f1, f2);
assert(f.apply(y).getX1() == f1.apply(y));
assert(f.apply(y).getX2() == f2.apply(y));
}

So what could be a counterexample? Here is:

// Java
class Pair<X1, X2> {
private final X1 x1;
private final X2 x2;

public Pair(X1 x1, X2 x2) {
this.x1 = x1;
this.x2 = x2;
}

public X1 getX1() {
return 1;
}

public X2 getX2() {
return 2;
}
}

With this wrong definition of product type, you cannot possibly construct such a

f

which satisfies the universal property, i.e., there are always some cases which can make the test fail.

If you think it is done, here comes the tricky part, is the type below a product type?

// Java
class Pair<X1, X2> {
private final X1 x1;
private final X2 x2;

public Pair(T x1, U x2) {
this.x1 = x1;
this.x2 = x2;
}

public T getX1() {
return x1 + 1;
}

public T getX2() {
return x2 + 2;
}
}

Intuition may tell you it is not a product type, but by definition of product type in the category theory, it actually is. Why? Because you can define a unique

f

satisfying the property:

// Java
Function<Y, Pair<X, Y>> makeF(Function<Y, X1> f1, Function<Y, X2> f2) {
return (Y y) -> new Pair(f1.apply(y) - 1, f2.apply(y) - 2);
}

What this means is that, the two product types are equivalent in category theory. This is because category theory defines equivalence by structure, if two things have the same structure, they are considered the same thing.

Then, what about sum type (a.k.a coproduct type)? The definition in category theory is:


From program perspective, the definition says, if

X1 ∐ X2

is a sum type of

X1

and

X2

with two functions

i1 : X1 -> X1 ∐ X2

and

i2 : X2 → X1 ∐ X2

, there must be a unique function

f : X1 ∐ X2 -> Y

which satisfies the property: for any value

y : Y

, function

f1 : X1 -> Y

and function

f2 : X2 -> Y

, the equations

f(i1(y)) == f1(y)

and

f(i2(y)) == f2(y)

must always be true.

If I define sum type as below:

// Java
class Either<X1, X2> {
private final Optional<X1> x1;
private final Optional<X2> x2;

private Either(Optional<X1> x1, Optional<X2> x2) {
this.x1 = x1;
this.x2 = x2;
}

public static Either<X1, X2> left(X1 x1) {
return new Either(Optional.of(x1), Optional.absent());
}

public static Either<X1, X2> right(X2 x2) {
return new Either(Optional.absent(), Optional.of(x2));
}

public Optional<T> getX1() {
return x1;
}

public Optional<U> getX2() {
return x2;
}
}

There must be a unique

f

which is constructed by:

// Java
Function<Either<X1, X2>, Y> makeF(Function<X1, Y> f1, Function<X2, Y> f2) {
return (Either<X1, X2> e) -> e.getX1().isPresent() ? f1.apply(e.getX1().get()) : f2.apply(e.getX2().get());
}

In other words, sum type guarantees that if you have a function of type

X1 -> Y

and a function of type

X2 -> Y

, you must have a unique function of type

X1 ∐ X2 -> Y

satisfying the property. The property can be verified programatically as: for any

x1

,

x2

,

f1

,

f2

the following tests must pass.

// Java
void testSumType(X1 x1, X2 x2, Function<X1, Y> f1, Function<X2, Y> f2) {
assert(f.apply(Either.left(x1)) == f1.apply(x1));
assert(f.apply(Either.left(x2)) == f2.apply(x2));
}

To sum up, category theory defines product and sum type by requiring them to be able to construct such a function which satisfies a universal property.