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