Mercurial > dylan

annotate categorical/morphisms.org @ 2:b4de894a1e2e

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
initial import
author Robert McIntyre <rlm@mit.edu>
date Fri, 28 Oct 2011 00:03:05 -0700
parents
children
rev   line source
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.