Merge pull request #8 from yfyf/arr_practically

[WIP] Add arrows intro

report/chapters/arrows-practice.tex

@@ -0,0 +1,145 @@
+\section{Arrows in Haskell}
+
+If all that computer programs do would be to operate on a fixed number of inputs
+to produce output at most one time (that is, to never halt or terminate with
+the result), pure language semantics would be sufficient. But real programs do
+much more than that. They are interactive, that is, they query the environment
+for input during runtime, and depend on this additional input for their runtime
+behavior. They cause effects in their environment by leveraging built-in
+capabilities of the machine they run on. They may run indefinitely, all the
+while periodically producing output.
+
+All of these types of computation are impossible to achieve with a pure
+language, so any general purpose programming language needs to have notions of
+computation to capture all of the above, and more.
+
+In Haskell, the most obvious type of a computation with input of type \verb|a|
+and output of type \verb|b| is the pure function type \verb|a -> b|, which is
+built from types \verb|a| and \verb|b| by the \verb|(->)| type constructor. It
+seems to make sense to adopt this notion of a computation being from something
+to something\footnote{We could always make it from or to some uninteresting
+fixed thing if we don't care about parameters or output.}, so we will generally
+expect any type of computation to be a two-parametric type.
+
+One of the powerful features of Haskell is the possibility of treating functions
+as values, empowering programmers to build up complex functionality from simple
+functions by assembling them using \emph{function combinators}. It seems
+sensible, though not necessary, to expect equivalent compositionality for other
+types of computation. The most basic kind of combinator for functions is
+composition, and we will require an analogue. Our common expectations for types
+of computations can be expressed in Haskell using a \emph{type class}.
+
+\begin{code}
+  class Computation a where
+      (>>>) :: a b c -> a c d -> a b d
+\end{code}
+
+This in essence states that any type \verb|a| can be made a computation by
+giving an implementation of the ``composition'' function, \verb|(>>>)|,
+combining two computations \verb|a b c| and \verb|a c d| to a computation
+\verb|a b d|.
+
+Under these preconditions it seems clear that any pure function should always
+fulfill the requirements for any kind of computation, so we require additionally
+an embedding of pure functions into computation types, arriving at type class
+
+\begin{code}
+  class Computation a where
+      pure   :: (b -> c) -> a b c
+      (>>>)  :: a b c -> a c d -> a b d\textrm{.}
+\end{code}
+
+It should become clear from the act of choosing common requirements for
+computations that this is not the only possible interface. And in fact,
+historically, it was not the first approach implemented in Haskell. As sketched
+in the introduction, the related but similar notion of monads was adopted from
+category theory with requirements described by something akin to
+
+\begin{code}
+  class Monad m where
+      return :: a -> m a
+      fmap   :: (a -> b) -> m a -> m b
+      (>>=)  :: m a -> (a -> m b) -> m b\textrm{,}
+\end{code}
+
+with \verb|return| describing how to turn values of type \verb|a| into
+computations of type \verb|m a|, \verb|fmap| explaining how \verb|m| is an
+endofunctor on the category of types, and \verb|(>>=)| a combinator for monads
+and Kleisli arrows. With this model of computation, it is possible to model
+computations with a specific return type, but without regard to specifically
+\emph{structured} input of the computation.
+
+While this is convenient in many cases, the method of producing computations of
+type \verb|m b| from values of type \verb|a| by means of function application
+dooms the combinator \verb|(>>=)| to execute computation \verb|m a| before being
+able to actually construct a computation \verb|m b|. This sequencing means that
+it is impossible for the \verb|(>>=)| combinator to analyse commonalities in
+the input structure. Unfortunately, this property of the monad structure entails
+that certain optimisations are out of bounds.
+
+This is disappointing, as it limits the practicability of the monad as a general
+interface to computation. By the time this detriment became clear, illustrated
+in the work on LL(1) parsers by Swierstra and Duponcheel (\cite{swierstra}), the
+benefits of such a general interface had become clear however. This incited John
+Hughes's proposal of a notion of computation along the lines of above's
+\verb|Computation|, which he called \emph{arrows}\footnote{Why this name? The
+authors could not find an explanation in the literature, but as each kind of
+\emph{arrow} in Hughes's sense describes the arrows---that is, morphisms---in
+some category of data types, this seems like a likely reason.}.
+
+The \verb|Arrow| typeclass proposed in~\cite{hughes-monad2arr} contains one
+additional request atop \linebreak\verb|Computation|, as this is actually
+\emph{too} general. We can observe that its applicability is seriously
+diminished by the fact it gives no general way of combining the \emph{results}
+of computations. A concise way of enabling this kind of operation is the
+addition of the function \verb|first|:
+
+\begin{code}
+  class Arrow a where
+      arr   :: (b -> c) -> a b c
+      (>>>) :: a b c -> a c d -> a b d
+      first :: a b c -> a (b, d) (c, d)
+\end{code}
+
+This interface allows the definition of a kind of non-commutative product with
+signature,
+
+\begin{code}
+  (***) :: Arrow a => a b c -> a b' c' -> a (b, b') (c, c')\textrm{.}
+\end{code}
+
+In addition to the constraints expressed by the type class, the semantics of the
+functions are subject to a set of laws, the \emph{arrow laws}, which need to be
+verified by the author of each instance's implementation.
+
+\begin{code}[numbers=left]
+                (a >>> b) >>> c == a >>> (b >>> c)
+                    arr (g . f) == arr f >>> arr g
+                   arr id >>> a == a
+                              a == a >>> arr id
+            first a >>> arr fst == arr fst >>> a
+     first a >>> arr (id *** f) == arr (id *** f) >>> first a
+  first (first a) >>> arr assoc == arr assoc >>> first a
+                  first (arr f) == arr (f *** id)
+                first (a >>> b) == first a >>> first b
+\end{code}
+
+The function \verb|assoc| translates tuples \verb|((a,b),c)| to
+\verb|(a,(b,c))|, and the functions \verb|fst| and \verb|snd| produce the first
+and second position of a tuple, respectively.
+
+The obvious instance of \verb|Arrow| is the pure function type \verb|(->)|. With
+\verb|(.)| being the composition function for pure functions, functions of the
+adequate types can be given by
+
+\begin{code}
+  instance Arrow (->) where
+      arr f     = f
+      (>>>) f g = (.) g f
+      first f   = \symbol{92}(x, y) -> (f x, y)\textrm{,}
+\end{code}
+
+where the right-hand expression in the definition of \verb|first| is an
+anonymous function defined on pairs \verb|(x, y)|.
+
+% TODO Example of an actual NON-pure computation?

report/literature.bib

@@ -35,7 +35,7 @@ @article{backus
   publisher = {ACM},
   address = {New York, NY, USA},
   keywords = {algebra of programs, applicative computing systems, applicative state transition systems, combining forms, functional forms, functional programming, metacomposition, models of computing systems, program correctness, program termination, program transformation, programming languages, von Neumann computers, von Neumann languages},
-} 
+}
 @article{cat-semantics-arr,
   author = {Jacobs, Bart and Heunen, Chris and Hasuo, Ichiro},
   title = {Categorical semantics for arrows},
@@ -106,6 +106,14 @@ @article{paterson
  publisher = {ACM},
  address = {New York, NY, USA},
 }
+@INPROCEEDINGS{swierstra,
+  author = {S. Doaitse Swierstra and Luc Duponcheel},
+  title = {Deterministic, Error-Correcting Combinator Parsers},
+  booktitle = {ADVANCED FUNCTIONAL PROGRAMMING},
+  year = {1996},
+  pages = {184--207},
+  publisher = {Springer-Verlag}
+}
 @INPROCEEDINGS{freyd-is-kleisli,
     author = {Bart Jacobs and Ichiro Hasuo},
     title = {Freyd is Kleisli, for arrows},

report/report.tex

@@ -26,7 +26,7 @@
 
 \newtheorem{definition}{Definition}
 
-\DefineVerbatimEnvironment{code}{Verbatim}{fontsize=\small}
+\DefineVerbatimEnvironment{code}{Verbatim}{fontsize=\small,commandchars=\\\{\},codes={\catcode`$=3\catcode`_=8}}
 
 \hypersetup{
     colorlinks,
@@ -58,9 +58,10 @@
 
 \input{chapters/context}
 \chapter{Modelling Computation in Theory and Practice}
+    \input{chapters/arrows-practice}
     \input{chapters/freyd-cats}
-\chapter{Categorical semantics of arrows (?)}
     \input{chapters/cat-arrows-hist}
+\chapter{Categorical semantics of arrows (?)}
 
 \nocite{mustard}
 \printbibliography