Categorical Programs
Table of Contents
1 The Category of Types
Every computer language with data types (such as Integers, Floats, or Strings) corresponds with a certain category; the objects of the category are the data types of the language, and there is one arrow between data types \(A\) and \(B\) for every function in the language whose argument has type \(A\) and whose return value has type \(B\).
(ns categorical.morphisms)
1.1 Building new data types out of existing ones
We will now discuss two processes which combine existing data types to yield composite data types. These higher-order processes will be functorial, which means that they will recombine not only the objects of our category (the data types), but the arrows as well (functions with typed input and output).
The product
functor combines two data types, \(A\) and \(B\), producing
a new type, denoted \(A\times B\). Conceptually, values with the data type \(A\times
B\) have two components, the first of which is a value of type \(A\), the
second of which is a value of type \(B\). Concretely, the data type \(A\times B\)
can be implemented as pairs of values, the first of which is
of type \(A\) and the second of which is of type \(B\). With this
implementation in mind, you can see that the type \(A\) and type \(B\)
constituents of type \(A\times B\) value can be recovered; the so-called
projection functors first
and second
recover them. A third
functor, the diagonal
functor, completes our toolkit; given
value \(a\) of type \(A\), it produces the value \((a,a)\) of type \(A\times A\).
(defn product[a b] (list a b)) (def projections (list first second)) (defn diagonal[a] (product a a))
The coproduct
functor combines two data types, \(A\) and \(B\),
producing a new type, denoted \(A+B\). Conceptually, you construct the
\(A+B\) datatype by creating labelled versions of the data types \(A\) and
\(B\) — we'll call them black-\(A\) and white-\(B\) — and
then creating a data type \(A+B\) which contains all the black-\(A\)
values and all the white-\(B\) values. Concretely, you can implement the
\(A+B\) data type using label-value pairs: the first value in the pair
is either the label `black' or the label `white'; the second
value must have type \(A\) if the label is black, or type \(B\) if the
label is white.
Now, the product
functor came with projection functors first
and second
that take \(A\times B\) values and return (respectively) \(A\) values and
\(B\) values. The coproduct
functor, conversely, comes with two
injection functors make-black
and make-white
that perform the
opposite function: they take (respectively) \(A\) values and \(B\) values,
promoting them to the \(A+B\) datatype by making the \(A\)'s into
black-\(A\)'s and the \(B\)'s into white-\(B\)'s.