# 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?

-
This is not a mathematical term. It's explained at Wikipedia: en.wikipedia.org/wiki/Algebraic_data_type. –  joriki Jul 8 '11 at 18:35
Discussion of the connection of algebraic data types to universal algebra in this Stackoverflow thread, Haskell's algebraic data types. The simple example given above doesn't demonstrate constructors, which can be related to functors in category theory. –  hardmath Jul 8 '11 at 20:08
@joriki I started reading the article on Wikipedia and I'll finish it before coming back to my question. Anyhow in the first line it says In computer programming, particularly functional programming and type theory, an algebraic data type [...] is..., in turn the article about type theory says In mathematics, logic and computer science, type theory is..., so it seems that algebraic data type has a definition in the field of type theory that has a definition in mathematics therefore is a mathematical term. ;) –  spaceCamel Jul 8 '11 at 20:29
The example you gave is really an example of a sum type, which is easy enough to explain in mathematical terms. There are more sophisticated algebraic datatypes, however. –  Zhen Lin Jul 8 '11 at 23:58
@hardmath: The simple example does demonstrate constructors, of type () -> Weekday. –  day Jan 6 '13 at 10:36

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.

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.

-
Typo: "... or it contains 2 elements ($X^3$) ...", the term in parentheses should be $X^2$. –  day Jan 6 '13 at 10:33
Thanks @plmday. Reading this answer again, I should probably edit to say something about exponential types ($Y^X$), which encode the type of functions $X\to Y$... –  Chris Taylor Jan 6 '13 at 18:50

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.

-