What's the meaning of algebraic data type?

I'm reading a book about Haskell, a programming language, and I came across a construct defined "algebraic data type" that looks like

data WeekDay = Mon | Tue | Wed | Thu | Fri | Sat | Sun

That simply declares what are the possible values for the type WeekDay.

My question is what is the meaning of algebraic data type (for a mathematician) and how that maps to the programming language construct?

Think of an algebraic data type as a type composed of simpler types, where the allowable compositions operators are AND (written $\cdot$, often referred to as product types) and OR (written $+$, referred to as union types or sum types).

We also have the unit type $1$ (representing a null type) and the basic type $X$ (representing a type holding one piece of data - this could be of a primitive type, or another algebraic type).

We also tend to use $2X$ to mean $X+X$ and $X^2$ to mean $X\cdot X$, etc.

For example, the Haskell type

data List a = Nil | Cons a (List a)

tells you that the data type List a (a list of elements of type a) is either Nil, or it is the Cons of a basic type and another lists. Algebraically, we could write

$$L = 1 + X \cdot L$$

This isn't just pretty notation - it encodes useful information. We can rearrange to get

$$L \cdot (1 - X) = 1$$

and hence

$$L = \frac{1}{1-X} = 1 + X + X^2 + X^3 + \cdot$$

which tells us that a list is either empty ($1$), or it contains 1 element ($X$), or it contains 2 elements ($X^2$), or it contains 3 elements, or...

For a more complicated example, consider the binary tree data type:

data Tree a = Nil | Branch a (Tree a) (Tree a)

Here a tree $T$ is either nil, or it is a Branch consisting of a piece of data and two other trees. Algebraically

$$T = 1 + X\cdot T^2$$

which we can rearrange to give

$$T = \frac{1}{2X} \left( 1 - \sqrt{1-4X} \right) = 1 + X + 2X^2 + 5X^3 + 14X^4 + 42X^5 + \cdots$$

where I have chosen the negative square root so that the equation makes sense (i.e. so that there are no negative powers of $X$, which are meaningless in this theory).

This tells us that a binary tree can be nil ($1$), that there is one binary tree with one datum (i.e. the tree which is a branch containing two empty trees), that there are two binary trees with two datums (the second datum is either in the left or the right branch), that there are 5 trees containing three datums (you might like to draw them all) etc.

I don't know who coined the term, but as far as I know the name “algebraic data type” comes from the fact that such types are solutions of an algebraic equation (or a set thereof):

$$ \begin{gather*} T_1 = P_1(T_1,\dots,T_n) \\ \dots \\ T_n = P_n(T_1,\dots,T_n) \\ \end{gather*} $$

The $P_k$ are polynomials, built upon the disjoint union operation (addition) and the cross product operation (multiplication).

For example, given a type of integers int, the type int_list of lists of integers is given by the equation

$$\verb|int_list| = 1 + \verb|int| \times \verb|int_list|$$

Programming languages introduce a few concepts that complicate the underlying mathematics.

• These operations only have nice properties (associativity, commutativity, neutral element) when you consider types up to isomorphisms. For example, programming languages typically distinguish a product of one element (a 1-tuple) from that element (under the hood, the product of one element would be represented as a pointer to that element).

• Most programming languages give distinct names to the operands in a disjoint union. Most programming languages also offer to give distinct names to the operands in a cross-product, though not necessarily in the same type declaration. Mathematically, one way to model named unions in a set-theoretical semantics is to include the constructor name as part of the mathematical structure:

  $$\verb|left|(A) + \verb|right|(B) = (\{\verb|left|\} \times A) \cup (\{\verb|right|\} \times B)$$

• Most programming languages have some form of type generativity: if you declare two types as solutions of the same equation, they are distinct types. This addresses a common concern in programming, where you usually don't want two types to be considered identical just because the underlying data is represented in the same way. (However, there are cases where generativity is not desired. Most functional languages provide non-generative definitions of product types; a few provide non-generative definitions of sum types as well.)

The example you give is special case with no recursion ($P_1$ is constant) and where all the products are trivial:

$$\verb|WeekDay| = 1 + 1 + 1 + 1 + 1 + 1 + 1$$

Furthermore, the terms in this sum are given names, from Mon to Sun.