rlm@2: #+TITLE: Categorical Programs rlm@2: #+AUTHOR: Dylan Holmes rlm@2: rlm@2: #+STYLE: rlm@2: rlm@2: #+BEGIN_HTML rlm@2:

{{{title}}}

rlm@2: #+END_HTML rlm@2: rlm@2: * 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: #+begin_src clojure :results silent rlm@2: (ns categorical.morphisms) rlm@2: #+end_src rlm@2: rlm@2: ** 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: 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: rlm@2: #+begin_src clojure :results silent 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: #+end_src 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$ \mdash{} we'll call them black-$A$ and white-$B$ \mdash{} 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: rlm@2: #the =coproduct= functor comes with two injection functors =make-black= rlm@2: #and =make-white= that take (respectively) $A$ values and $B$ values, rlm@2: #promoting them to the $A+B$ datatype by making them into black-$A$'s rlm@2: #or white-$B$'s. 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, values with the rlm@2: #data type $A+B$ can be either values with type $A$ that are designated /of the first rlm@2: #kind/, or values with type $B$ that are designated /of the second rlm@2: #kind/. Concretely, the data type $A+B$ can be implemented using pairs rlm@2: #of values in conjunction with a labelling convention; the first value rlm@2: #in the pair is of either type $A$ or $B$, and the second value is a label rlm@2: #indicating whether it is of the first or second kind. Our labelling rlm@2: #scheme uses the keywords =:black= and =:white= for this purpose.