Added discussion of takeout-based analysis of monads

leithaus · Jun 25, 2010 · 8498f32 · 8498f32
1 parent 62ca88f
commit 8498f32
Show file tree

Hide file tree

Showing 10 changed files with 328 additions and 136 deletions.
diff --git a/src/main/book/content/bibliography/monadic.aux b/src/main/book/content/bibliography/monadic.aux
@@ -1,6 +1,6 @@
 \relax 
 \@setckpt{bibliography/monadic}{
-\setcounter{page}{123}
+\setcounter{page}{125}
 \setcounter{equation}{0}
 \setcounter{enumi}{0}
 \setcounter{enumii}{0}

diff --git a/src/main/book/content/chapters/eight/ch.aux b/src/main/book/content/chapters/eight/ch.aux
@@ -1,22 +1,22 @@
 \relax 
-\@writefile{toc}{\contentsline {chapter}{\numberline {8}Domain model, storage and state}{107}{chapter.8}}
+\@writefile{toc}{\contentsline {chapter}{\numberline {8}Domain model, storage and state}{109}{chapter.8}}
 \@writefile{lof}{\addvspace {10\p@ }}
 \@writefile{lot}{\addvspace {10\p@ }}
-\@writefile{toc}{\contentsline {section}{\numberline {8.1}Mapping our domain model to storage}{107}{section.8.1}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {8.1.1}Functional and relational models}{107}{subsection.8.1.1}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {8.1.2}Functional and XML models}{107}{subsection.8.1.2}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {8.1.3}ORM}{107}{subsection.8.1.3}}
-\@writefile{toc}{\contentsline {section}{\numberline {8.2}Storage and language-integrated query}{107}{section.8.2}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {8.2.1}LINQ and \lstinline [language=Scala]!for!-comprehensions}{107}{subsection.8.2.1}}
-\@writefile{toc}{\contentsline {subsubsection}{Open source implementations}{107}{section*.62}}
-\@writefile{toc}{\contentsline {paragraph}{ScalaQuery}{107}{section*.63}}
-\@writefile{toc}{\contentsline {paragraph}{Squeryl}{107}{section*.64}}
-\@writefile{lof}{\contentsline {figure}{\numberline {8.1}{\ignorespaces  Chapter map }}{108}{figure.8.1}}
-\@writefile{toc}{\contentsline {section}{\numberline {8.3}Continuations revisited}{108}{section.8.3}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {8.3.1}Stored state}{108}{subsection.8.3.1}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {8.3.2}Transactions}{108}{subsection.8.3.2}}
+\@writefile{toc}{\contentsline {section}{\numberline {8.1}Mapping our domain model to storage}{109}{section.8.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {8.1.1}Functional and relational models}{109}{subsection.8.1.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {8.1.2}Functional and XML models}{109}{subsection.8.1.2}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {8.1.3}ORM}{109}{subsection.8.1.3}}
+\@writefile{toc}{\contentsline {section}{\numberline {8.2}Storage and language-integrated query}{109}{section.8.2}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {8.2.1}LINQ and \lstinline [language=Scala]!for!-comprehensions}{109}{subsection.8.2.1}}
+\@writefile{toc}{\contentsline {subsubsection}{Open source implementations}{109}{section*.62}}
+\@writefile{toc}{\contentsline {paragraph}{ScalaQuery}{109}{section*.63}}
+\@writefile{toc}{\contentsline {paragraph}{Squeryl}{109}{section*.64}}
+\@writefile{lof}{\contentsline {figure}{\numberline {8.1}{\ignorespaces  Chapter map }}{110}{figure.8.1}}
+\@writefile{toc}{\contentsline {section}{\numberline {8.3}Continuations revisited}{110}{section.8.3}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {8.3.1}Stored state}{110}{subsection.8.3.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {8.3.2}Transactions}{110}{subsection.8.3.2}}
 \@setckpt{chapters/eight/ch}{
-\setcounter{page}{109}
+\setcounter{page}{111}
 \setcounter{equation}{0}
 \setcounter{enumi}{0}
 \setcounter{enumii}{0}

diff --git a/src/main/book/content/chapters/nine/ch.aux b/src/main/book/content/chapters/nine/ch.aux
@@ -1,14 +1,14 @@
 \relax 
-\@writefile{toc}{\contentsline {chapter}{\numberline {9}Putting it all together}{109}{chapter.9}}
+\@writefile{toc}{\contentsline {chapter}{\numberline {9}Putting it all together}{111}{chapter.9}}
 \@writefile{lof}{\addvspace {10\p@ }}
 \@writefile{lot}{\addvspace {10\p@ }}
-\@writefile{toc}{\contentsline {section}{\numberline {9.1}Our web application end-to-end}{109}{section.9.1}}
-\@writefile{toc}{\contentsline {section}{\numberline {9.2}Deploying our application}{109}{section.9.2}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {9.2.1}Why we are not deploying on GAE}{109}{subsection.9.2.1}}
-\@writefile{toc}{\contentsline {section}{\numberline {9.3}From one web application to web framework}{109}{section.9.3}}
-\@writefile{lof}{\contentsline {figure}{\numberline {9.1}{\ignorespaces  Chapter map }}{110}{figure.9.1}}
+\@writefile{toc}{\contentsline {section}{\numberline {9.1}Our web application end-to-end}{111}{section.9.1}}
+\@writefile{toc}{\contentsline {section}{\numberline {9.2}Deploying our application}{111}{section.9.2}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {9.2.1}Why we are not deploying on GAE}{111}{subsection.9.2.1}}
+\@writefile{toc}{\contentsline {section}{\numberline {9.3}From one web application to web framework}{111}{section.9.3}}
+\@writefile{lof}{\contentsline {figure}{\numberline {9.1}{\ignorespaces  Chapter map }}{112}{figure.9.1}}
 \@setckpt{chapters/nine/ch}{
-\setcounter{page}{111}
+\setcounter{page}{113}
 \setcounter{equation}{0}
 \setcounter{enumi}{0}
 \setcounter{enumii}{0}

diff --git a/src/main/book/content/chapters/seven/ch.aux b/src/main/book/content/chapters/seven/ch.aux
@@ -18,17 +18,17 @@
 \@writefile{toc}{\contentsline {subsection}{\numberline {7.3.2}Eilenberg-Moore}{105}{subsection.7.3.2}}
 \@writefile{toc}{\contentsline {section}{\numberline {7.4}Monad as container}{105}{section.7.4}}
 \@writefile{toc}{\contentsline {section}{\numberline {7.5}Monads and take-out}{105}{section.7.5}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {7.5.1}Option as container}{106}{subsection.7.5.1}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {7.5.2}I/O monad for contrast}{106}{subsection.7.5.2}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {7.5.3}Matching gazintas and gazoutas}{106}{subsection.7.5.3}}
-\@writefile{toc}{\contentsline {subsubsection}{Intuitionistic discipline}{106}{section*.60}}
-\@writefile{toc}{\contentsline {subsubsection}{Linear discipline}{106}{section*.61}}
-\@writefile{toc}{\contentsline {section}{\numberline {7.6}Co-monad and take-out}{106}{section.7.6}}
-\@writefile{toc}{\contentsline {section}{\numberline {7.7}Hopf structure}{106}{section.7.7}}
-\@writefile{toc}{\contentsline {section}{\numberline {7.8}Container and control}{106}{section.7.8}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {7.8.1}Delimited continuations reconsidered}{106}{subsection.7.8.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {7.5.1}Option as container}{107}{subsection.7.5.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {7.5.2}I/O monad for contrast}{108}{subsection.7.5.2}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {7.5.3}Matching gazintas and gazoutas}{108}{subsection.7.5.3}}
+\@writefile{toc}{\contentsline {subsubsection}{Intuitionistic discipline}{108}{section*.60}}
+\@writefile{toc}{\contentsline {subsubsection}{Linear discipline}{108}{section*.61}}
+\@writefile{toc}{\contentsline {section}{\numberline {7.6}Co-monad and take-out}{108}{section.7.6}}
+\@writefile{toc}{\contentsline {section}{\numberline {7.7}Hopf structure}{108}{section.7.7}}
+\@writefile{toc}{\contentsline {section}{\numberline {7.8}Container and control}{108}{section.7.8}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {7.8.1}Delimited continuations reconsidered}{108}{subsection.7.8.1}}
 \@setckpt{chapters/seven/ch}{
-\setcounter{page}{107}
+\setcounter{page}{109}
 \setcounter{equation}{0}
 \setcounter{enumi}{0}
 \setcounter{enumii}{0}

diff --git a/src/main/book/content/chapters/seven/monad-and-comonad.tex b/src/main/book/content/chapters/seven/monad-and-comonad.tex
@@ -1,7 +1,119 @@
 \section{Monads and take-out}
 
+In the previous sections we've explored the idea of collections as
+monads. Likewise, we've suggested that that you can turn this
+interpretation around in the sense that you can use the notion of
+container to bootstrap an understanding of the notion of monad. In
+this section we expand this approach. More specifically, we begin with
+the notion of container as a first approximation of the notion of
+monad and then notice (some rather subtle) differences between the two
+ideas which allows us to refine our understanding of monad, and -- as
+it turns out -- our understanding of container.
+
+As we've observed before, intuitively a monad is like a ``box'' into
+which we can put things. One of the most important things we can put
+into ``boxes'' like this is other ``boxes''. The monad laws govern the
+nesting of boxes and as nesting is one of the core concepts underlying
+a notion of composition, we see that monads capture some fundamental
+aspects of the notion of composition. Monads provide a minimalist
+characterization of composition. As software engineers we must pay
+attention to this a proposal of this kind -- minimalist, yet evidently
+rich -- because composition is really one of the few tools we have to
+manage complexity. There are several ways, however, that the notion of
+composition codified by the theory of monads seems to break with our
+intuitive sense of what a physical container is.
+
+There's a favorite childhood tale that illustrates one of the vital
+differences. 
+
+\begin{quotation}
+  When Eeyore saw the pot, he became quite excited.
+  “Why!” he said. “I believe my Balloon will just go into that Pot!”
+  “Oh, no, Eeyore,” said Pooh. “Balloons are much too big to go into Pots. What you do with a balloon is, you hold the balloon -”
+  “Not mine,” said Eeyore proudly. “Look, Piglet!”
+  And as Piglet looked sorrowfully round, Eeyore picked the balloon up with his teeth, and placed it carefully in the pot; picked it out and put it on the ground; and then picked it up again and put it carefully back.
+  “So it does!” said Pooh. “It goes in!”
+  “So it does!” said Piglet. “And it comes out!”
+  “Doesn’t it?” said Eeyore. “It goes in and out like anything.”
+\end{quotation}
+
+Gloomy Eeyore takes a surprising delight in the configuration that
+allows him to put things into his very useful pot and then take them
+out again. In this sense Eeyore's honey pot was strictly richer, as an
+idea, than a monad because a monad, by itself, \emph{does not support
+  an operation to take things out of the box}. Things go in, but they
+don't go out. In this sense a monad -- without any additional gadetry
+-- is more like a piggybank than Eeyore's honey pot. This question of
+``takeout'' turns out to have some currency as it helps us classify
+and characterize a number of situations in the design of data
+structures and control flow -- common to computer scientists and
+professional programmers alike.
+
 \subsection{Option as container}
 
+To see this idea at work, recall the oft used example of the
+\lstinline[language=Scala,mathescape=true]!Option! monad. When viewed
+in terms of the question of ``takeout'' we see several things at
+once. First of all, if we are in the role of Eeyore and put something
+-- say the \lstinline[language=Scala,mathescape=true]!String!
+\lstinline[language=Scala,mathescape=true]!"ballon"! -- into our very
+useful pot, say an \lstinline[language=Scala,mathescape=true]!Option!,
+in \lstinline[language=Scala,mathescape=true]!val pigletsGift = Some( "balloon" )!, then we know that we can take it out:
+\lstinline[language=Scala,mathescape=true]!pigletsGift match { case Some( s ) => s }!. On the other hand, if we play in the role of Christopher Robin, and Eeyore hands us a very useful pot, i.e. something typed like \lstinline[language=Scala,mathescape=true]!pigletsGift : Option[String]!, then we cannot know whether there is something in the pot to take out or not \emph{without looking into the pot}: \lstinline[language=Scala,mathescape=true]!pigletsGift match { case Some( s ) => s case None => "no balloon" }!.
+
+Notice that nearly all the common containers,
+\lstinline[language=Scala,mathescape=true]!Set!,
+\lstinline[language=Scala,mathescape=true]!List!, etc, have this
+property. If we are in the role of constructing the container, we know
+whether or not the container enjoys any contents; but, if we are in
+the role of recipient, we cannot know if the container enjoys contents
+without looking inside.
+
+Now, this all may seem like plain common sense until we start to put
+it in context. As we will see in the next section, lots of monads very
+rightly do not support any sort of takeout whatsoever. This
+differentiates these situations of structure and control from the
+sorts we find with the commonly encountered containers. These
+situations and the dividing line between them turn out to be
+intimately connected with the notion of transaction! 
+
+On the flip side, there are very specialized containers and control
+disciplines in which every act of insertion is matched by an act of
+removal. Lest this seem strange, just think about the \emph{syntactic}
+structure of containers like
+\lstinline[language=Scala,mathescape=true]!List!s. For a
+\lstinline[language=Scala,mathescape=true]!List! to be well formed
+every left paren, \lstinline[language=Scala,mathescape=true]!(!, must
+eventually be matched by a right paren,
+\lstinline[language=Scala,mathescape=true]!)!. This property of
+matching pairs is really a deep, but common design pattern. When we
+think about the design of messaging systems, one of the properties we
+would like to ensure is that every request is eventually answered by a
+response. Protocols like \texttt{HTTP} are very draconian in the way
+they guarantee this property. It's not possible to ``nest''
+\texttt{HTTP} request/response pairs. This design choice forces a kind
+of ``statelessness'' on the protocol that doesn't have to be. It also
+gives rise to all kinds of work arounds to introduce sessions that
+give the modern programmer, as well as the modern user, all kinds of
+headaches. After all, why should Grandma ever have to be worried about
+``cleaning cookies out of the cache'' -- whatever that is! -- when all
+she wants to do is use the browser to book tickets to the movies for
+her grandkids?
+
+Intriguingly, the interplay between these very practical concerns and
+very deep mathematical patterns doesn't stop there. It turns out that
+this takeout-based classification scheme
+
+\begin{itemize}
+  \item contents go in, but don't come out
+  \item asymmetric roles of container provider and container recipient
+  \item matched pair discipline
+\end{itemize}
+
+is closely related to a famous historical development in logic! As
+we'll see below, the latter two categories have to do with
+\emph{intuitionistic} and \emph{linear} logics.
+
 \subsection{I/O monad for contrast}
 
 \subsection{Matching gazintas and gazoutas}

diff --git a/src/main/book/content/chapters/ten/ch.aux b/src/main/book/content/chapters/ten/ch.aux
@@ -1,33 +1,33 @@
 \relax 
-\@writefile{toc}{\contentsline {chapter}{\numberline {10}The semantic web}{111}{chapter.10}}
+\@writefile{toc}{\contentsline {chapter}{\numberline {10}The semantic web}{113}{chapter.10}}
 \@writefile{lof}{\addvspace {10\p@ }}
 \@writefile{lot}{\addvspace {10\p@ }}
-\@writefile{toc}{\contentsline {section}{\numberline {10.1}Referential transparency}{111}{section.10.1}}
-\@writefile{lof}{\contentsline {figure}{\numberline {10.1}{\ignorespaces  Chapter map }}{112}{figure.10.1}}
-\@writefile{toc}{\contentsline {paragraph}{A little motivation}{112}{section*.65}}
-\@writefile{toc}{\contentsline {section}{\numberline {10.2}Composing monads}{113}{section.10.2}}
-\@writefile{toc}{\contentsline {subsubsection}{Preliminary}{114}{section*.66}}
-\@writefile{toc}{\contentsline {section}{\numberline {10.3}Semantic application queries}{115}{section.10.3}}
-\@writefile{toc}{\contentsline {subsubsection}{An alternative presentation}{115}{section*.67}}
-\@writefile{toc}{\contentsline {paragraph}{Logic: the set monad as an algebra}{116}{section*.68}}
-\@writefile{toc}{\contentsline {paragraph}{Primes: an application}{117}{section*.69}}
-\@writefile{toc}{\contentsline {paragraph}{Summary}{117}{section*.70}}
-\@writefile{toc}{\contentsline {subsubsection}{Patterns}{118}{section*.71}}
-\@writefile{toc}{\contentsline {subsubsection}{A first mini-query language}{118}{section*.72}}
-\@writefile{toc}{\contentsline {subsubsection}{Iterating the design pattern}{118}{section*.73}}
-\@writefile{toc}{\contentsline {paragraph}{A spatial-behavioral-style logic for $\lambda $-calculus}{119}{section*.74}}
-\@writefile{toc}{\contentsline {paragraph}{Examples}{119}{section*.75}}
-\@writefile{toc}{\contentsline {subsubsection}{Logical semantics}{120}{section*.76}}
-\@writefile{toc}{\contentsline {subsubsection}{Other collection monads, other logics}{120}{section*.77}}
-\@writefile{toc}{\contentsline {paragraph}{Stateful collections}{120}{section*.78}}
-\@writefile{lof}{\contentsline {figure}{\numberline {10.2}{\ignorespaces  Comprehensions and distributive maps }}{121}{figure.10.2}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {10.3.1}Other logical operations}{122}{subsection.10.3.1}}
-\@writefile{toc}{\contentsline {section}{\numberline {10.4}Searching for programs}{122}{section.10.4}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {10.4.1}A new foundation for search}{122}{subsection.10.4.1}}
-\@writefile{toc}{\contentsline {subsubsection}{Monad composition via distributive laws}{122}{section*.79}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {10.4.2}Examples}{122}{subsection.10.4.2}}
+\@writefile{toc}{\contentsline {section}{\numberline {10.1}Referential transparency}{113}{section.10.1}}
+\@writefile{lof}{\contentsline {figure}{\numberline {10.1}{\ignorespaces  Chapter map }}{114}{figure.10.1}}
+\@writefile{toc}{\contentsline {paragraph}{A little motivation}{114}{section*.65}}
+\@writefile{toc}{\contentsline {section}{\numberline {10.2}Composing monads}{115}{section.10.2}}
+\@writefile{toc}{\contentsline {subsubsection}{Preliminary}{116}{section*.66}}
+\@writefile{toc}{\contentsline {section}{\numberline {10.3}Semantic application queries}{117}{section.10.3}}
+\@writefile{toc}{\contentsline {subsubsection}{An alternative presentation}{117}{section*.67}}
+\@writefile{toc}{\contentsline {paragraph}{Logic: the set monad as an algebra}{118}{section*.68}}
+\@writefile{toc}{\contentsline {paragraph}{Primes: an application}{119}{section*.69}}
+\@writefile{toc}{\contentsline {paragraph}{Summary}{119}{section*.70}}
+\@writefile{toc}{\contentsline {subsubsection}{Patterns}{120}{section*.71}}
+\@writefile{toc}{\contentsline {subsubsection}{A first mini-query language}{120}{section*.72}}
+\@writefile{toc}{\contentsline {subsubsection}{Iterating the design pattern}{120}{section*.73}}
+\@writefile{toc}{\contentsline {paragraph}{A spatial-behavioral-style logic for $\lambda $-calculus}{121}{section*.74}}
+\@writefile{toc}{\contentsline {paragraph}{Examples}{121}{section*.75}}
+\@writefile{toc}{\contentsline {subsubsection}{Logical semantics}{122}{section*.76}}
+\@writefile{toc}{\contentsline {subsubsection}{Other collection monads, other logics}{122}{section*.77}}
+\@writefile{toc}{\contentsline {paragraph}{Stateful collections}{122}{section*.78}}
+\@writefile{lof}{\contentsline {figure}{\numberline {10.2}{\ignorespaces  Comprehensions and distributive maps }}{123}{figure.10.2}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {10.3.1}Other logical operations}{124}{subsection.10.3.1}}
+\@writefile{toc}{\contentsline {section}{\numberline {10.4}Searching for programs}{124}{section.10.4}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {10.4.1}A new foundation for search}{124}{subsection.10.4.1}}
+\@writefile{toc}{\contentsline {subsubsection}{Monad composition via distributive laws}{124}{section*.79}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {10.4.2}Examples}{124}{subsection.10.4.2}}
 \@setckpt{chapters/ten/ch}{
-\setcounter{page}{123}
+\setcounter{page}{125}
 \setcounter{equation}{0}
 \setcounter{enumi}{0}
 \setcounter{enumii}{0}