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.

Date: 2011-07-01 12:28:39 CDT

Author: Dylan Holmes

Org version 7.5 with Emacs version 23

Validate XHTML 1.0