1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/categorical/morphisms.org	Fri Oct 28 00:03:05 2011 -0700
     1.3 @@ -0,0 +1,81 @@
     1.4 +#+TITLE: Categorical Programs
     1.5 +#+AUTHOR: Dylan Holmes
     1.6 +
     1.7 +#+STYLE: <link rel="stylesheet" type="text/css" href="../css/aurellem.css" />
     1.8 +
     1.9 +#+BEGIN_HTML
    1.10 +<h1>{{{title}}}</h1>
    1.11 +#+END_HTML
    1.12 +
    1.13 +* The Category of Types
    1.14 +Every computer language with data types (such as Integers,
    1.15 +Floats, or
    1.16 +Strings) corresponds with a certain category; the objects of the category are the data types
    1.17 +of the language, and there is one arrow between data types $A$ and $B$
    1.18 +for every function in the language whose argument has type $A$ and whose return value
    1.19 +has type $B$. 
    1.20 +
    1.21 +#+begin_src clojure :results silent
    1.22 +(ns categorical.morphisms)
    1.23 +#+end_src
    1.24 +
    1.25 +** Building new data types out of existing ones
    1.26 +
    1.27 +We will now discuss two processes which combine existing
    1.28 +data types to yield composite data types. These higher-order processes will be 
    1.29 +/functorial/, which means that they will recombine  not only the objects of
    1.30 +our category (the data types), but the arrows as well (functions with
    1.31 +typed input and output).
    1.32 +
    1.33 +The =product= functor combines two data types, $A$ and $B$, producing
    1.34 +a new type, denoted $A\times B$. Conceptually, values with the data type $A\times
    1.35 +B$ have two components, the first of which is a value of type $A$, the
    1.36 +second of which is a value of type $B$. Concretely, the data type $A\times B$
    1.37 +can be implemented as pairs of values, the first of which is
    1.38 +of type $A$ and the second of which is of type $B$. With this
    1.39 +implementation in mind, you can see that the type $A$ and type $B$
    1.40 +constituents of type $A\times B$ value can be recovered; the so-called
    1.41 +projection functors =first= and =second= recover them. A third
    1.42 +functor, the =diagonal= functor, completes our toolkit; given
    1.43 +value $a$ of type $A$, it produces the value $(a,a)$ of type $A\times A$.
    1.44 +
    1.45 +#+begin_src clojure :results silent
    1.46 +(defn product[a b] (list a b))
    1.47 +(def projections (list first second))
    1.48 +(defn diagonal[a] (product a a))
    1.49 +#+end_src
    1.50 + 
    1.51 +The =coproduct= functor combines two data types, $A$ and $B$,
    1.52 +producing a new type, denoted $A+B$. Conceptually, you construct the
    1.53 +$A+B$ datatype by creating labelled versions of the data types $A$ and
    1.54 +$B$ \mdash{} we'll call them black-$A$ and white-$B$ \mdash{} and
    1.55 +then creating a data type $A+B$ which contains all the black-$A$
    1.56 +values and all the white-$B$ values. Concretely, you can implement the
    1.57 +$A+B$ data type using label-value pairs: the first value in the pair
    1.58 +is either the label `black' or the label `white'; the second
    1.59 +value must have type $A$ if the label is black, or type $B$ if the
    1.60 +label is white. 
    1.61 +
    1.62 +Now, the =product= functor came with projection functors =first=
    1.63 +and =second= that take $A\times B$ values and return (respectively) $A$ values and
    1.64 +$B$ values. The =coproduct= functor, conversely, comes with two
    1.65 +injection functors =make-black= and =make-white= that perform the
    1.66 +opposite function: they take (respectively) $A$ values and $B$ values,
    1.67 +promoting them to the $A+B$ datatype by making the $A$'s into
    1.68 +black-$A$'s and the $B$'s into white-$B$'s. 
    1.69 +
    1.70 +#the =coproduct= functor comes with two injection functors =make-black=
    1.71 +#and =make-white=  that take (respectively) $A$ values and $B$ values,
    1.72 +#promoting them to the $A+B$ datatype by making them into black-$A$'s
    1.73 +#or white-$B$'s.
    1.74 +
    1.75 +
    1.76 +#The =coproduct= functor combines two data types, $A$ and $B$,
    1.77 +#producing a new type, denoted $A+B$. Conceptually, values with the
    1.78 +#data type $A+B$ can be either values with type $A$ that are designated /of the first
    1.79 +#kind/, or values with type $B$ that are designated /of the second
    1.80 +#kind/. Concretely, the data type $A+B$ can be implemented using pairs
    1.81 +#of values in conjunction with a labelling convention; the first value
    1.82 +#in the pair is of either type $A$ or $B$, and the second value is a label
    1.83 +#indicating whether it is of the first or second kind. Our labelling
    1.84 +#scheme uses the keywords =:black= and =:white= for this purpose.