5
$\begingroup$

Algebraic data types include two concepts with names that feel like they imply something clever, but that I can't for the life of me understand:

  • Sum type: This refers to tagged unions, like Rust's enums
  • Product type: This refers to collection types like tuples and structs

Why are these referred to using mathematical language? What makes the former more addition-like and the latter more product-like? It feels like these imply some sort of relationship and symmetry that's present in algebra, but I can't figure out what that would be.

$\endgroup$
5
  • 3
    $\begingroup$ Could someone please spell out what makes this question off-topic? The help center does not yet include a definition of the scope of programming-language design and implementation. $\endgroup$
    – Ben Kovitz
    Commented May 19, 2023 at 16:02
  • 2
    $\begingroup$ @BenKovitz Perhaps because it could've been answered by a simple Google search. It's already been asked on Stack Overflow. However, it's probably useful to have a question like this on PLDI too, I don't get the downvotes $\endgroup$
    – user
    Commented May 19, 2023 at 16:24
  • $\begingroup$ There is a similar question on another site: proofassistants.stackexchange.com/q/879/32 $\endgroup$
    – ice1000
    Commented May 19, 2023 at 19:23
  • $\begingroup$ One more funnily and unexplainedly downvoted question :) $\endgroup$
    – ice1000
    Commented May 19, 2023 at 19:25
  • $\begingroup$ Related code golf challenge. $\endgroup$
    – alephalpha
    Commented May 22, 2023 at 9:10

3 Answers 3

8
$\begingroup$

Category Theory

Those terms have meaning in category theory.

The direct product of two objects A and B in a category is an object P together with a pair of morphisms π₁ : P -> A and π₂ : P -> B called projections such that it is, in some sense, the smallest such object.

Precisely, the requirement is that if we have another candidate P' and morphisms π'₁ : P' -> A and π'₂ : P' -> B, then there must be a unique map f : P' -> P such that the following diagram commutes.

"Commutes" is just a fancy category theory term for "if there are multiple paths that go from one point to another, they must be equal". In this diagram, that means π₁∘f = π'₁ and π₂∘f = π'₂. That is, P is the "best" product in the sense that any other product is necessarily just "P with some extra".

In the category of types in a particular programming language, the categorical product of A and B is the type of tuples containing an A and a B, and the projection maps extract an A and a B from it respectively. Any other type which contains an A and a B must necessarily be isomorphic to "a tuple plus some extra".

Note that this representation is only unique up to isomorphism (up to a unique isomorphism, which is more powerful but in ways that aren't relevant here). (A, B) is a valid direct product of A and B. So is (B, A). And so is the structure

struct HelloThere {
  a: A,
  b: B,
}

All of these are distinct types but are isomorphic, and they are all valid products of the two input types.

Likewise, the direct sum or coproduct is the dual of the product, which means it's the above diagrams with all the arrows reversed. More precisely, the direct sum is an object I together with a pair of morphisms i₁ : A -> I and i₂ : B -> I.

Note that we've reversed the directions of our arrows. Instead of projections out of our type P, we have injections into I.

Again, we get a universal property, stating that I must be the best sum. So given I', i'₁ : A -> I', and i'₂ : B -> I', we must get an f : I -> I' with the following commutative diagram.

i.e., f∘i₁ = i'₁ and f∘i₂ = i'₂. It so happens that, in the category of types, this direct sum object manifests as the disjoint, or tagged, union (which Haskell calls Either).

You'll also sometimes hear function types called exponential types, which as a similar categorical relationship to the exponential object. I'll sometimes write A -> B and B^A (Note: The result type is the base of the exponent) interchangeably in what follows, when it makes sense for the explanation.

But why did we choose these names in category theory? Lots of reasons, actually!

First, we can make a cardinality argument. I'll borrow notation from set theory and write |A| to denote the cardinality of the set underlying our type. If you don't know what cardinality is, just think of it as "the number of possible distinct elements in your type". We have the following, for all types A and B.

  • |A + B| = |A| + |B|. The number of elements in the disjoint union is equal to the sum of the sizes of each type.
  • |A × B| = |A| × |B|. The number of elements in the tuple type is equal to the product of the sizes of each type.
  • |A ^ B| = |A| ^ |B|. The number of functions from B to A is equal to the size of A raised to the power of that of B.

So if all we care about is counting, then these operations match precisely our intuitive notions in ordinary arithmetic.

But there's more! These categorical objects behave a lot like ordinary arithmetic ones in more ways than just counting.

They're commutative.

  • A × B ≅ B × A
  • A + B ≅ B + A

They're associative.

  • (A × B) × C ≅ A × (B × C)
  • (A + B) + C ≅ A + (B + C)

and they even distribute.

  • (A + B) × C ≅ A × C + B × C
  • A × (B + C) ≅ A × C + A × C

The exponential (function) types are well behaved too. Take a moment to think about what these mean, as types, as these can be a bit less trivial to immediately see.

  • (A × B) ^ C ≅ A ^ C × B ^ C
  • A ^ (B + C) ≅ A ^ B × A ^ C
  • (A ^ B) ^ C ≅ A ^ (B × C)

We can go one step further. In category theory, we often denote the initial object of a category as 0 and the terminal object as 1. Under those definitions, in the category of types in our hypothetical language, the initial object 0 is Void, the empty type, and the terminal object 1 is Unit, the type having one value. These numbers also behave neatly in this model.

  • A + 0 ≅ 0 + A ≅ A
  • A × 1 ≅ 1 × A ≅ A
  • A × 0 ≅ 0 × A ≅ 0
  • A ^ 0 ≅ 1
  • 0 ^ A ≅ 0 (if A is nonempty)
  • 1 ^ A ≅ 1
  • A ^ 1 ≅ A

In summary, we call these types sums, products, exponentials, 0, and 1, because when we actually write down all of the nice arithmetic properties of addition, multiplication, powers, zero, and one, it turns out that these are the types that satisfy those properties.


Side note: You'll notice I switched from using = to halfway through. I use to denote isomorphism. It's true that (A × B) × C is not actually equal to A × (B × C), since the first looks like ((a, b), c) and the second looks like (a, (b, c)), but they store the same information. The notion of isomorphism makes that rigorous. In fact, all of the above isomorphisms are natural in their arguments, which means that the types are related in a uniform way that doesn't depend on the specific structure of the arguments.

$\endgroup$
1
  • 1
    $\begingroup$ While presenting the category theory model is interesting, it makes the concepts look more complicated than they are. The vocabulary of category theory comes from set theory and the set theory model is rather easier to understand. $\endgroup$ Commented May 20, 2023 at 22:11
7
$\begingroup$

For this example, we'll consider 2 datatypes: letters L abcdef and numbers 123456 N.

A sum type contains all elements in A or B

So L+N would be abcdef123456

This is a "Sum" because the number of items in the resulting type is the sum of the number of items in each subtype.

The sum of 0 types creates a never type, a type with no elements.

The union type

You didn't ask about the union type, but let me explain anyway. The union type, in typescript | or a untagged union, is like sum but duplicate items are counted only once. So L+L has 12 elements, each letter twice with a different tag, while L|L has only 6 elements: The letters themselves.

A product type contains all combinations of elements in A and B

The product of A*B would be [('a', '1'), ('a', '2'), ('a', '3'), ('a', '4'), ('a', '5'), ('a', '6'), ('b', '1'), ('b', '2'), ('b', '3'), ('b', '4'), ('b', '5'), ('b', '6'), ('c', '1'), ('c', '2'), ('c', '3'), ('c', '4'), ('c', '5'), ('c', '6'), ('d', '1'), ('d', '2'), ('d', '3'), ('d', '4'), ('d', '5'), ('d', '6'), ('e', '1'), ('e', '2'), ('e', '3'), ('e', '4'), ('e', '5'), ('e', '6'), ('f', '1'), ('f', '2'), ('f', '3'), ('f', '4'), ('f', '5'), ('f', '6')].

This is called a product, or Cartesian product, because its length is the product of the lengths of each of the types. Things get a bit more complex when types have infinite lengths.

The product of nothing is often defined to have one element, the unit type, as $0^0\ = 1$. This allows you to construct types from nothing by then summing bottom types.

$\endgroup$
12
  • $\begingroup$ Is the unit type considered to be bottom? I've always thought those were two veeeeery different things, at least in the Haskell world. $\endgroup$ Commented May 19, 2023 at 15:12
  • 2
    $\begingroup$ “0^0 = 1” — [citation needed] $\endgroup$
    – Bbrk24
    Commented May 19, 2023 at 15:33
  • $\begingroup$ @Bbrk24 In type theory yes $\endgroup$
    – mousetail
    Commented May 19, 2023 at 15:38
  • 1
    $\begingroup$ @UnrelatedString mousetail isn't saying unit is bottom, they're saying the product of nothing and nothing is unit. The unit type has one inhabitant, while the bottom type has none $\endgroup$
    – user
    Commented May 19, 2023 at 16:26
  • 1
    $\begingroup$ @user Well consider (a,b) is a tuple of 2 types, then () is a tuple containing no types. It has 1 element: The unit type $\endgroup$
    – mousetail
    Commented May 20, 2023 at 6:35
6
$\begingroup$

You count the number of distinct elements.

Let's forget about types with infinite many elements and only look at finite ones.

Suppose A have 5 instances, and B have 6 instances. The sum of A and B, which you know the definition of, has 11 instances in total. The product of A and B have 30 instances in total. Hence the names.

These are not the essential reasons, but this is an intuitive explanation I believe.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .