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 characters)
Any good programming language will let us construct compound types from simple ones like these. Let’s examine some of these operations, which are 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 the terms “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 element (however, most programming languages do make this distinction). This means that, for example,
(Int)is usually equivalent to
Intin 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
- Associativity (sometimes):
(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 Python function?
def f(flag): return 5 if flag else "Hello"
It seems that
fcould return an
str, so its type must be
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.
Properties of the union constructor:
- Closure: the union of two types is a type
- Associativity (sometimes):
(A + B) + C = A + (B + C)
A + B = B + A
- Identity element:
You can see that types and the sum operation might form a commutative monoid, depending on whether
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 (
Unitis 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,
Diamondsneed 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 a nominative type system 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:
1is the unit type
Tis a primitive type
X + Yis the sum of two types
X × Yis the product of two types (which has a higher syntactic precedence than sum)
Additionally, we can let the rest of the natural numbers represent 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 + Tis a nullable type (also called an option type or a maybe type)
L = 1 + T × Lis the type of lists
B = 1 + T × B × Bis the type of binary trees, like
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 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 possible 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 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.