#+TITLE: Categorical Programs

 #+AUTHOR: Dylan Holmes

 

 #+STYLE: <link rel="stylesheet" type="text/css" href="../css/aurellem.css" />

 

 #+BEGIN_HTML

 <h1>{{{title}}}</h1>

 #+END_HTML

 

 * The Category of Types

 Every computer language with data types (such as Integers,

 Floats, or

 Strings) corresponds with a certain category; the objects of the category are the data types

 of the language, and there is one arrow between data types $A$ and $B$

 for every function in the language whose argument has type $A$ and whose return value

 has type $B$. 

 

 #+begin_src clojure :results silent

 (ns categorical.morphisms)

 #+end_src

 

 ** Building new data types out of existing ones

 

 We will now discuss two processes which combine existing

 data types to yield composite data types. These higher-order processes will be 

 /functorial/, which means that they will recombine  not only the objects of

 our category (the data types), but the arrows as well (functions with

 typed input and output).

 

 The =product= functor combines two data types, $A$ and $B$, producing

 a new type, denoted $A\times B$. Conceptually, values with the data type $A\times

 B$ have two components, the first of which is a value of type $A$, the

 second of which is a value of type $B$. Concretely, the data type $A\times B$

 can be implemented as pairs of values, the first of which is

 of type $A$ and the second of which is of type $B$. With this

 implementation in mind, you can see that the type $A$ and type $B$

 constituents of type $A\times B$ value can be recovered; the so-called

 projection functors =first= and =second= recover them. A third

 functor, the =diagonal= functor, completes our toolkit; given

 value $a$ of type $A$, it produces the value $(a,a)$ of type $A\times A$.

 

 #+begin_src clojure :results silent

 (defn product[a b] (list a b))

 (def projections (list first second))

 (defn diagonal[a] (product a a))

 #+end_src

  

 The =coproduct= functor combines two data types, $A$ and $B$,

 producing a new type, denoted $A+B$. Conceptually, you construct the

 $A+B$ datatype by creating labelled versions of the data types $A$ and

 $B$ \mdash{} we'll call them black-$A$ and white-$B$ \mdash{} and

 then creating a data type $A+B$ which contains all the black-$A$

 values and all the white-$B$ values. Concretely, you can implement the

 $A+B$ data type using label-value pairs: the first value in the pair

 is either the label `black' or the label `white'; the second

 value must have type $A$ if the label is black, or type $B$ if the

 label is white. 

 

 Now, the =product= functor came with projection functors =first=

 and =second= that take $A\times B$ values and return (respectively) $A$ values and

 $B$ values. The =coproduct= functor, conversely, comes with two

 injection functors =make-black= and =make-white= that perform the

 opposite function: they take (respectively) $A$ values and $B$ values,

 promoting them to the $A+B$ datatype by making the $A$'s into

 black-$A$'s and the $B$'s into white-$B$'s. 

 

 #the =coproduct= functor comes with two injection functors =make-black=

 #and =make-white=  that take (respectively) $A$ values and $B$ values,

 #promoting them to the $A+B$ datatype by making them into black-$A$'s

 #or white-$B$'s.

 

 

 #The =coproduct= functor combines two data types, $A$ and $B$,

 #producing a new type, denoted $A+B$. Conceptually, values with the

 #data type $A+B$ can be either values with type $A$ that are designated /of the first

 #kind/, or values with type $B$ that are designated /of the second

 #kind/. Concretely, the data type $A+B$ can be implemented using pairs

 #of values in conjunction with a labelling convention; the first value

 #in the pair is of either type $A$ or $B$, and the second value is a label

 #indicating whether it is of the first or second kind. Our labelling

 #scheme uses the keywords =:black= and =:white= for this purpose.