|
rlm@2
|
1 #+TITLE: Categorical Programs
|
|
rlm@2
|
2 #+AUTHOR: Dylan Holmes
|
|
rlm@2
|
3
|
|
rlm@2
|
4 #+STYLE: <link rel="stylesheet" type="text/css" href="../css/aurellem.css" />
|
|
rlm@2
|
5
|
|
rlm@2
|
6 #+BEGIN_HTML
|
|
rlm@2
|
7 <h1>{{{title}}}</h1>
|
|
rlm@2
|
8 #+END_HTML
|
|
rlm@2
|
9
|
|
rlm@2
|
10 * The Category of Types
|
|
rlm@2
|
11 Every computer language with data types (such as Integers,
|
|
rlm@2
|
12 Floats, or
|
|
rlm@2
|
13 Strings) corresponds with a certain category; the objects of the category are the data types
|
|
rlm@2
|
14 of the language, and there is one arrow between data types $A$ and $B$
|
|
rlm@2
|
15 for every function in the language whose argument has type $A$ and whose return value
|
|
rlm@2
|
16 has type $B$.
|
|
rlm@2
|
17
|
|
rlm@2
|
18 #+begin_src clojure :results silent
|
|
rlm@2
|
19 (ns categorical.morphisms)
|
|
rlm@2
|
20 #+end_src
|
|
rlm@2
|
21
|
|
rlm@2
|
22 ** Building new data types out of existing ones
|
|
rlm@2
|
23
|
|
rlm@2
|
24 We will now discuss two processes which combine existing
|
|
rlm@2
|
25 data types to yield composite data types. These higher-order processes will be
|
|
rlm@2
|
26 /functorial/, which means that they will recombine not only the objects of
|
|
rlm@2
|
27 our category (the data types), but the arrows as well (functions with
|
|
rlm@2
|
28 typed input and output).
|
|
rlm@2
|
29
|
|
rlm@2
|
30 The =product= functor combines two data types, $A$ and $B$, producing
|
|
rlm@2
|
31 a new type, denoted $A\times B$. Conceptually, values with the data type $A\times
|
|
rlm@2
|
32 B$ have two components, the first of which is a value of type $A$, the
|
|
rlm@2
|
33 second of which is a value of type $B$. Concretely, the data type $A\times B$
|
|
rlm@2
|
34 can be implemented as pairs of values, the first of which is
|
|
rlm@2
|
35 of type $A$ and the second of which is of type $B$. With this
|
|
rlm@2
|
36 implementation in mind, you can see that the type $A$ and type $B$
|
|
rlm@2
|
37 constituents of type $A\times B$ value can be recovered; the so-called
|
|
rlm@2
|
38 projection functors =first= and =second= recover them. A third
|
|
rlm@2
|
39 functor, the =diagonal= functor, completes our toolkit; given
|
|
rlm@2
|
40 value $a$ of type $A$, it produces the value $(a,a)$ of type $A\times A$.
|
|
rlm@2
|
41
|
|
rlm@2
|
42 #+begin_src clojure :results silent
|
|
rlm@2
|
43 (defn product[a b] (list a b))
|
|
rlm@2
|
44 (def projections (list first second))
|
|
rlm@2
|
45 (defn diagonal[a] (product a a))
|
|
rlm@2
|
46 #+end_src
|
|
rlm@2
|
47
|
|
rlm@2
|
48 The =coproduct= functor combines two data types, $A$ and $B$,
|
|
rlm@2
|
49 producing a new type, denoted $A+B$. Conceptually, you construct the
|
|
rlm@2
|
50 $A+B$ datatype by creating labelled versions of the data types $A$ and
|
|
rlm@2
|
51 $B$ \mdash{} we'll call them black-$A$ and white-$B$ \mdash{} and
|
|
rlm@2
|
52 then creating a data type $A+B$ which contains all the black-$A$
|
|
rlm@2
|
53 values and all the white-$B$ values. Concretely, you can implement the
|
|
rlm@2
|
54 $A+B$ data type using label-value pairs: the first value in the pair
|
|
rlm@2
|
55 is either the label `black' or the label `white'; the second
|
|
rlm@2
|
56 value must have type $A$ if the label is black, or type $B$ if the
|
|
rlm@2
|
57 label is white.
|
|
rlm@2
|
58
|
|
rlm@2
|
59 Now, the =product= functor came with projection functors =first=
|
|
rlm@2
|
60 and =second= that take $A\times B$ values and return (respectively) $A$ values and
|
|
rlm@2
|
61 $B$ values. The =coproduct= functor, conversely, comes with two
|
|
rlm@2
|
62 injection functors =make-black= and =make-white= that perform the
|
|
rlm@2
|
63 opposite function: they take (respectively) $A$ values and $B$ values,
|
|
rlm@2
|
64 promoting them to the $A+B$ datatype by making the $A$'s into
|
|
rlm@2
|
65 black-$A$'s and the $B$'s into white-$B$'s.
|
|
rlm@2
|
66
|
|
rlm@2
|
67 #the =coproduct= functor comes with two injection functors =make-black=
|
|
rlm@2
|
68 #and =make-white= that take (respectively) $A$ values and $B$ values,
|
|
rlm@2
|
69 #promoting them to the $A+B$ datatype by making them into black-$A$'s
|
|
rlm@2
|
70 #or white-$B$'s.
|
|
rlm@2
|
71
|
|
rlm@2
|
72
|
|
rlm@2
|
73 #The =coproduct= functor combines two data types, $A$ and $B$,
|
|
rlm@2
|
74 #producing a new type, denoted $A+B$. Conceptually, values with the
|
|
rlm@2
|
75 #data type $A+B$ can be either values with type $A$ that are designated /of the first
|
|
rlm@2
|
76 #kind/, or values with type $B$ that are designated /of the second
|
|
rlm@2
|
77 #kind/. Concretely, the data type $A+B$ can be implemented using pairs
|
|
rlm@2
|
78 #of values in conjunction with a labelling convention; the first value
|
|
rlm@2
|
79 #in the pair is of either type $A$ or $B$, and the second value is a label
|
|
rlm@2
|
80 #indicating whether it is of the first or second kind. Our labelling
|
|
rlm@2
|
81 #scheme uses the keywords =:black= and =:white= for this purpose.
|
