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