Programmers in typed languages with higher order functions and algebraic data types are already comfortable with most of the basic constructions of set/type theory. In categorical terms, those programmers are familiar with finite products and coproducts and (monoidal/cartesian) closed structure. The main omissions are subset types (equalizers/pullbacks) and quotient types (coequalizers/pushouts) which would round out limits and colimits. Not having a good grasp on either of these constructions dramatically shrinks the world of mathematics that is understandable, but while subset types are fairly straightforward, quotient types are quite a bit less intuitive.
See this StackOverflow answer by me which provides a more software engineering perspective.
In my opinion, most programmers can more or less immediately understand the notion of a subset type at an intuitive level.
A subset type is just a type combined with a predicate on that type that specifies which values of the type we want. For
example, we may have something like { n:Nat | n /= 0 } meaning the type of naturals not equal to |0|. We may use this for
the type of the denominator for the division function. Consuming a value of a subset type is easy, a natural not equal to |0| is still
just a natural, and we can treat it as such. The difficult part is producing a value of a subset type. To do this, we
must, of course, produce a value of the underlying type — Nat in our example — but then we must further
convince the type checker that the predicate holds (e.g. that the value does not equal |0|). Most languages provide no mechanism
to prove potentially arbitrary facts about code, and this is why they do not support subset types. Dependently typed
languages do provide such mechanisms and thus either have or can encode subset types. Outside of dependently typed languages
the typical solution is to use an abstract data type and use a runtime check when values of that abstract data type are created.
The dual of subset types are quotient types. My impression is that this construction is the most difficult basic construction
for people to understand. Further, programmers aren’t much better off, because they have little to which to connect the idea.
Before I give a definition, I want to provide the example with which most people are familiar: modular (or clock) arithmetic.
A typical way this is first presented is as a system where the numbers “wrap-around”. For example, in arithmetic mod |3|, we
count |0|, |1|, |2|, and then wrap back around to |0|. Programmers are well aware that it’s not necessary to guarantee that an input
to addition, subtraction, or multiplication mod |3| is either |0|, |1|, or |2|. Instead, the operation can be done and the mod function
can be applied at the end. This will give the same result as applying the mod function to each argument at the beginning.
For example, |4+7 = 11| and |11 \bmod 3 = 2|, and |4 \bmod 3 = 1| and |7 \bmod 3 = 1| and |1+1 = 2 = 11 \bmod 3|.
For mathematicians, the type of integers mod |n| is represented by the quotient type |\mathbb{Z}/n\mathbb{Z}|. The idea is that the values of |\mathbb{Z}/n\mathbb{Z}| are integers except that we agree that any two integers |a| and |b| are treated as equal if |a - b = kn| for some integer |k|. For |\mathbb{Z}/3\mathbb{Z}|, |\dots -6 = -3 = 0 = 3 = 6 = \dots| and |\dots = -5 = -2 = 1 = 4 = 7 = \dots| and |\dots = -4 = -1 = 2 = 5 = 8 = \dots|.
To start to formalize this, we need the notion of an equivalence relation. An equivalence relation is a binary relation |\sim| which is reflexive (|x \sim x| for all |x|), symmetric (if |x \sim y| then |y \sim x|), and transitive (if |x \sim y| and |y \sim z| then |x \sim z|). We can check that “|a \sim b| if and only if there exists an integer |k| such that |a-b = kn|” defines an equivalence relation on the integers for any given |n|. For reflexivity, we have |a - a = 0n|. For symmetry, we have if |a - b = kn| then |b - a = -kn|. Finally, for transitivity, we have if |a - b = k_1 n| and |b - c = k_2 n| then |a - c = (k_1 + k_2)n| which we get by adding the preceding two equations.
Any relation can be extended to an equivalence relation. This is called the reflexive-, symmetric-, transitive-closure of the relation. For an arbitrary binary relation |R| we can define the equivalence relation |({\sim_R})| via “|a \sim_R b| if and only if |a = b| or |R(a, b)| or |b \sim_R a| or |a \sim_R c| and |c \sim_R b| for some |c|”. To be precise, |{\sim_R}| is the smallest relation satisfying those constraints. In Datalog syntax, this looks like:
eq_r(A, A).
eq_r(A, B) :- r(A, B).
eq_r(A, B) :- eq_r(B, A).
eq_r(A, B) :- eq_r(A, C), eq_r(C, B).If |T| is a type and |({\sim})| is an equivalence relation, we use |T/{\sim}| as the notation for the quotient type, which we read as “|T| quotiented by the equivalence relation |{\sim}|”. We call |T| the underlying type of the quotient type. We then say |a = b| at type |T/{\sim}| if and only if |a \sim b|. Dual to subset types, to produce a value of a quotient type is easy. Any value of the underlying type is a value of the quotient type. (In type theory, this produces the perhaps surprising result that |\mathbb Z| is a subtype of |\mathbb Z/n\mathbb Z|.) As expected, consuming a value of a quotient type is more complicated. To explain this, we need to explain what a function |f : T/{\sim} \to X| is for some type |X|. A function |f : T/{\sim} \to X| is a function |g : T \to X| which satisfies |g(a) = g(b)| for all |a| and |b| such that |a \sim b|. We call |f| (or |g|, they are often conflated) well-defined if |g| satisfies this condition. In other words, any well-defined function that consumes a quotient type isn’t allowed to produce an output that distinguishes between equivalent inputs. A better way to understand this is that quotient types allow us to change what the notion of equality is for a type. From this perspective, a function being well-defined just means that it is a function. Taking equal inputs to equal outputs is one of the defining characteristics of a function.
Sometimes we can finesse needing to check the side condition. Any function |h : T \to B| gives rise to an equivalence relation on |T| via |a \sim b| if and only if |h(a) = h(b)|. In this case, any function |g : B \to X| gives rise to a function |f : T/{\sim} \to X| via |f = g \circ h|. In particular, when |B = T| we are guaranteed to have a suitable |g| for any function |f : T/{\sim} \to X|. In this case, we can implement quotient types in a manner quite similar subset types, namely we make an abstract type and we normalize with the |h| function as we either produce or consume values of the abstract type. A common example of this is rational numbers. We can reduce a rational number to lowest terms either when it’s produced or when the numerator or denominator get accessed, so that we don’t accidentally write functions which distinguish between |1/2| and |2/4|. For modular arithmetic, the mod by |n| function is a suitable |h|.
In set theory such an |h| function can always be made by mapping the elements of |T| to the equivalence classes that contain them, i.e. |a| gets mapped to |\{b \mid a \sim b\}| which is called the equivalence class of |a|. In fact, in set theory, |T/{\sim}| is usually defined to be the set of equivalence classes of |({\sim})|. So, for the example of |\mathbb Z/3\mathbb Z|, in set theory, it is a set of exactly three elements: the elements are |\{ 3n+k \mid n \in \mathbb Z\}| for |k = 0, 1, 2|. Equivalence classes are also called partitions and are said to partition the underlying set. Elements of these equivalence classes are called representatives of the equivalence class. Often a notation like |[a]| is used for the equivalence class of |a|.
Here is a quick run-through of some significant applications of quotient types. I’ll give the underlying type and the equivalence relation and what the quotient type produces. I’ll leave it as an exercise to verify that the equivalence relations really are equivalence relations, i.e. reflexive, symmetric, and transitive. I’ll start with more basic examples. You should work through them to be sure you understand how they work.
Integers can be presented as pairs of naturals |(n, m)| with the idea being that the pair represents “|n - m|”. Of course, |1 - 2| should be the same as |2 - 3|. This is expressed as |(n_1, m_1) \sim (n_2, m_2)| if and only if |n_1 + m_2 = n_2 + m_1|. Note how this definition only relies on operations on natural numbers. You can explore how to define addition, subtraction, multiplication, and other operations on this representation in a well-defined manner.
Rationals can be presented very similarly to integers, only with multiplication instead of addition. We also have pairs |(n, d)|, usually written |n/d|, in this case of an integer |n| and a non-zero natural |d|. The equivalence relation is |(n_1, d_1) \sim (n_2, d_2)| if and only if |n_1 d_2 = n_2 d_1|.
We can extend the integers mod |n| to the continuous case. Consider the real numbers with the equivalence relation |r \sim s| if and only if |r - s = k| for some integer |k|. You could call this the reals mod |1|. Topologically, this is a circle. If you walk along it far enough, you end up back at a point equivalent to where you started. Occasionally this is written as |\mathbb R/\mathbb Z|.
Doing the previous example in 2D gives a torus. Specifically, we have pairs of real numbers and the equivalence relation |(x_1, y_1) \sim (x_2, y_2)| if and only if |x_1 - x_2 = k| and |y_1 - y_2 = l| for some integers |k| and |l|. Quite a bit of topology relies on similar constructions as will be expanded upon on the section on gluing.
Here’s an example that’s a bit closer to programming. Consider the following equivalence relation on arbitrary pairs of the same type: |(a_1, b_1) \sim (a_2, b_2)| if and only if |a_1 = a_2| and |b_1 = b_2| or |a_1 = b_2| and |b_1 = a_2|. This just says that a pair is equivalent to either itself, or a swapped version of itself. It’s interesting to consider what a well-defined function is on this type.1
Returning to topology and doing a bit more involved construction, we arrive at gluing or pushouts. In topology, we often want to take two topological
spaces and glue them together in some specified way. For example, we may want to take two discs and glue their boundaries together. This gives a sphere.
We can combine two spaces into one with the disjoint sum (or coproduct, i.e. Haskell’s Either type.) This produces a space that contains both
the input spaces, but they don’t interact in any way. You can visualize them as sitting next to each other but not touching. We now want to say that
certain pairs of points, one from each of the spaces, are really the same point. That is, we want to quotient by an equivalence relation that would
identify those points. We need some mechanism to specify which points we want to identify. One way to accomplish this is to have a pair of
functions, |f : C \to A| and |g : C \to B|, where |A| and |B| are the spaces we want to glue together. We can then define a relation |R| on the disjoint sum
via |R(a, b)| if and only if there’s a |c : C| such that |a = \mathtt{inl}(f(c))| and |b = \mathtt{inr}(g(c))|. This is not an equivalence relation, but we can extend it to one.
The quotient we get is then the gluing of |A| and |B| specified by |C| (or really by |f| and |g|). For our example of two discs, |f| and |g| are the same
function, namely the inclusion of the boundary of the disc into the disc. We can also glue a space to itself. Just drop the disjoint sum part. Indeed,
the circle and torus are examples.
We write |\mathbb R[X]| for the type of polynomials with one indeterminate |X| with real coefficients. For two indeterminates, we write |\mathbb R[X, Y]|. Values of these types are just polynomials such as |X^2 + 1| or |X^2 + Y^2|. We can consider quotienting these types by equivalence relations generated from identifications like |X^2 + 1 \sim 0| or |X^2 - Y \sim 0|, but we want more than just the reflexive-, symmetric-, transitive-closure. We want this equivalence relation to also respect the operations we have on polynomials, in particular, addition and multiplication. More precisely, we want if |a \sim b| and |c \sim d| then |ac \sim bd| and similarly for addition. An equivalence relation that respects all operations is called a congruence. The standard notation for the quotient of |\mathbb R[X, Y]| by a congruence generated by both of the previous identifications is |\mathbb R[X, Y]/(X^2 + 1, X^2 - Y)|. Now if |X^2 + 1 = 0| in |\mathbb R[X, Y]/(X^2 + 1, X^2 - Y)|, then for any polynomial |P(X, Y)|, we have |P(X, Y)(X^2 + 1) = 0| because |0| times anything is |0|. Similarly, for any polynomial |Q(X, Y)|, |Q(X, Y)(X^2 - Y) = 0|. Of course, |0 + 0 = 0|, so it must be the case that |P(X, Y)(X^2 + 1) + Q(X, Y)(X^2 - Y) = 0| for all polynomials |P| and |Q|. In fact, we can show that all elements in the equivalence class of |0| are of this form. You’ve now motivated the concrete definition of a ring ideal and given it’s significance. An ideal is an equivalence class of |0| with respect to some congruence. Let’s work out what |\mathbb R[X, Y]/(X^2 + 1, X^2 - Y)| looks like concretely. First, since |X^2 - Y = 0|, we have |Y = X^2| and so we see that values of |\mathbb R[X, Y]/(X^2 + 1, X^2 - Y)| will be polynomials in only one indeterminate because we can replace all |Y|s with |X^2|s. Since |X^2 = -1|, we can see that all those polynomials will be linear (i.e. of degree 1) because we can just keep replacing |X^2|s with |-1|s, i.e. |X^{n+2} = X^n X^2 = -X^n|. The end result is that an arbitrary polynomial in |\mathbb R[X, Y]/(X^2 + 1, X^2 - Y)| looks like |a + bX| for real numbers |a| and |b| and we have |X^2 = -1|. In other words, |\mathbb R[X, Y]/(X^2 + 1, X^2 - Y)| is isomorphic to the complex numbers, |\mathbb C|.
As a reasonably simple exercise, given a polynomial |P(X) : \mathbb R[X]|, what does it get mapped to when embedded into |\mathbb R[X]/(X - 3)|, i.e. what is |[P(X)] : \mathbb R[X]/(X - 3)|?2
Moving much closer to programming, we have a rather broad and important example that a mathematician might describe as free algebras modulo an equational
theory. This example covers several of the preceding examples. In programmer-speak, a free algebra is just a type of abstract syntax trees for some language.
We’ll call a specific abstract syntax tree a term. An equational theory is just a collection of pairs of terms with the idea being that we’d like these
terms to be considered equal. To be a bit more precise, we will actually allow terms to contain (meta)variables. An example equation for an expression
language might be Add(|x|,|x|) = Mul(2,|x|). We call a term with no variables a ground term. We say a ground term matches another
term if there is a consistent substitution for the variables that makes the latter term syntactically equal to the ground term. For example, Add(3, 3) matches
Add(|x|,|x|) via the substitution |x \mapsto|3. Now, the equations of our equational theory gives rise to a relation on ground terms |R(t_1, t_2)| if and only if there
exists an equation |l = r| such that |t_1| matches |l| and |t_2| matches |r|. This relation can be extended to an equivalence relation on ground terms, and
we can then quotient by that equivalence relation.
Let’s consider a worked example. We can consider the theory of monoids. We have two operations (types of AST nodes): Mul(|x|,|y|) and 1. We
have the following three equations: Mul(1,|x|) =|x|, Mul(|x|, 1) =|x|, and Mul(Mul(|x|,|y|),|z|) = Mul(|x|, Mul(|y|,|z|)).
We additionally have a bunch of constants subject to no equations. In this case, it turns out we can define a normalization function, what I called |h| far above,
and that the quotient type is isomorphic to lists of constants. Now, we can extend this theory to the theory of groups by adding a new operation, Inv(|x|),
and new equations: Inv(Inv(|x|)) =|x|, Inv(Mul(|x|,|y|)) = Mul(Inv(|y|), Inv(|x|)), and Mul(Inv(|x|),|x|) = 1. If we ignore the last
of these equations, you can show that we can normalize to a form that is isomorphic to a list of a disjoint sum of the constants, i.e. [Either Const Const]
in Haskell if Const were the type of the constant terms. Quotienting this type by the equivalence relation extended with that final equality corresponds
to adding the rule that a Left c cancels out Right c in the list whenever they are adjacent.
This overall example is a fairly profound one. Almost all of abstract algebra can be viewed as an instance of this or a closely related variation. When you hear about things defined in terms of “generators and relators”, it is an example of this sort. Indeed, those “relators” are used to define a relation that will be extended to an equivalence relation. Being defined in this way is arguably what it means for something to be “algebraic”.
The Introduction to Type Theory section of the NuPRL book provides a more comprehensive and somewhat more formal presentation of these and related concepts. While the quotient type view of quotients is conceptually different from the standard set theoretic presentation, it is much more amenable to computation as the |\mathbb Z/n\mathbb Z| example begins to illustrate.