Posted on August 21, 2012.
A type system starts with some primitive types. Some examples include:
Int (the type of integers, perhaps limited to some range)
Real (the type of real numbers, perhaps represented as IEEE 754 floating-point numbers)
Char (the type of Unicode code points or ASCII character codes)
Any good programming language will let us construct compound types from simple ones like these. Let’s examine some of these operations, which are traditionally called type constructors.
Most programmers will be familiar with product types, but in programming they are more commonly called tuples (the name “tuple” is a generalization of “double”, “triple”, etc.). A product type is a compound type that is formed by a sequence of types, and is commonly denoted
(T1, T2, ..., Tn) or
T1 • T2 • ... • Tn. In set theory parlance, tuples correspond to cartesian products, and that is why they’re called “product types.”
As an example, we could represent a point in 3-space by a Cartesian triple:
(Real, Real, Real).
Most programming languages will allow the elements of a tuple to be named (rather than indexed). This has the same type theoretic meaning, but named tuples are often called records, structs, or classes, depending on the programming language and context.
Note: In type theory, we usually do not distinguish between a 1-tuple (called a “singleton”) and the type of its only element (however, most programming languages do make this distinction). This means that, for example,
(Int) is usually equivalent to
Int in the literature.
A special case of tuples is the 0-tuple, which is also called the unit type. The unit type can only hold one value (which means it stores zero information). It is sometimes called
Unit, and its value is often called
Common properties of the type product constructor:
- Closure: the product of two types is a type
(A • B) • C = A • (B • C)
- Identity element:
Depending on the type system, types and their constructors can form various algebraic structures, such as a monoid.
Sum types, also called tagged unions, disjoint unions, or variants, are used to describe values that could be of one of several types (the corresponding set theoretic operation is union of disjoint sets). We usually write sum types as
T1 + T2 + .. + Tn,
T1 | T2 | ... | Tn, or
T1 ∪ T2 ∪ ... ∪ Tn.
Many programmers often use sum types without knowing it. For example, what is the return type of the following Fython function?
return 5 if flag else "Hello"
It seems that
f could return an
int or a
str, so its type must be
int + str (or
int | str or
int ∪ str).
As a special case, if we take the sum of zero types, we get a special type called
⊥, which can take on no values. A function which does not return (i.e., does not halt) is said to have a return type of
Bottom. Likewise, the sum of all types is called
⊤, and it is sometimes called
General, because it can take on any value.
Note that, unlike product types, sum types can be defined inductively, as we shall see with lists and trees.
Common properties of the union constructor:
- Closure: the union of two types is a type
(A + B) + C = A + (B + C)
A + B = B + A
- Identity element:
You can see that types and the sum operation form a commutative monoid.
Algebraic Data Types
We can represent a number of different data structures using algebraic data types, which are simply sums of products of types. For example, we can represent a list of integers as
IntList = Unit + Int • IntList
where the product operation (
•) has a higher precedence than the sum operation (
Unit is the unit type (which represents an empty list here). In English, this means: a list of integers is either the empty list or an integer paired with a list of integers.
Using a nominative type system, we can also represent enumerated types as the union of disjoint unit types:
Clubs = Unit
Diamonds = Unit
Hearts = Unit
Spades = Unit
Suit = Clubs + Diamonds + Hearts + Spades
This only works in a nominative type system because, for example,
Diamonds need to be disjoint unit types or else the their union would still be the unit type (in type theory we talk about the unit type, but in practice we can have several unit types). In a structural type system, we would have
Suit = Clubs = Diamonds = Hearts = Spades, which is not what we want.
We might define a binary tree of integers like this:
IntTree = Unit + Int • IntTree • IntTree
This reads: a binary tree can be the empty tree or an integer and two subtrees.
Fun with Algebra
The title of this article suggests that we can manipulate expressions involving types algebraically, as we do with numbers. To make this easier, let’s adopt the following notation:
1 is the unit type
T is a primitive type
X + Y is the sum of two types
X • Y is the product of two types (which has a higher syntactic precedence than sum)
Additionally, we can use the rest of the natural numbers to mean sums of unit types (e.g.
2 = 1 + 1 = bool). Repeated products can be written as exponentials (e.g.
X • X • X = X^3). Now let’s describe some common data structures.
1 + T is a nullable type (also called an option type or a maybe type)
L = 1 + T • L is the type of lists
B = 1 + T • B • B is the type of binary trees, like
IntTree defined above
Take a look at that second one (lists). With a bit of hand-waving (treating type addition and multiplication like the corresponding operations on reals), we can solve for
L = 1 + T • L
L - T • L = 1
L • (1 - T) = 1
L = 1 / (1 - T)
L = 1 + T + T^2 + T^3 + ...
Interpreting that last line in set theoretic terms, we can translate it into English as: a list is either empty, or it contains one element, or two elements, or three elements, etc. Pretty cool, huh? If we’re treating these symbols as numbers, then they roughly correspond to the number of values that the corresponding types can take on (i.e. the sizes of the corresponding sets). For example, the unit type has 1 value, so in this notation, it becomes
1. The fact that
L = 1 + T + T^2 + T^3 + ... does not converge simply means that there are an infinite number of list topologies we can construct. In general, the algebraic forms of inductive datatypes do not converge.
I won’t go into detail, but I want to mention one more thing you can do with this notation. In 1997, a computer scientist named Gérard Huet suggested that we can also take derivatives of types in an unpublished work on zipper types. Oddly, the derivative laws look very much like their classical counterparts from differential calculus! The derivative of a type describes the “one-hole context” of a type, which is a data structure that represents a pointer to an item in a larger container type. For example, one-hole contexts can be used to mark the position of an item in a linked list or a binary tree and can be used to efficiently implement such containers in a purely functional fashion.