Permalink
Browse files

Refactored chapter one to move application domain model discussion to…

… chapter 5
  • Loading branch information...
1 parent db86b16 commit 7f3036d28d258316845358ea9b7cf9a347177b40 Meredith Gregory committed Mar 14, 2010
View
4 src/main/book/content/bibliography/monadic.aux
@@ -1,6 +1,6 @@
\relax
\@setckpt{bibliography/monadic}{
-\setcounter{page}{92}
+\setcounter{page}{94}
\setcounter{equation}{0}
\setcounter{enumi}{0}
\setcounter{enumii}{0}
@@ -19,7 +19,7 @@
\setcounter{table}{0}
\setcounter{parentequation}{0}
\setcounter{Item}{0}
-\setcounter{Hfootnote}{12}
+\setcounter{Hfootnote}{13}
\setcounter{lstnumber}{1}
\setcounter{theorem}{0}
\setcounter{section@level}{2}
View
32 src/main/book/content/chapters/eight/ch.aux
@@ -1,22 +1,22 @@
\relax
-\@writefile{toc}{\contentsline {chapter}{\numberline {8}Domain model, storage and state}{77}{chapter.8}}
+\@writefile{toc}{\contentsline {chapter}{\numberline {8}Domain model, storage and state}{79}{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}{77}{section.8.1}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {8.1.1}Functional and relational models}{77}{subsection.8.1.1}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {8.1.2}Functional and XML models}{77}{subsection.8.1.2}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {8.1.3}ORM}{77}{subsection.8.1.3}}
-\@writefile{toc}{\contentsline {section}{\numberline {8.2}Storage and language-integrated query}{77}{section.8.2}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {8.2.1}LINQ and \lstinline [language=Scala]!for!-comprehensions}{77}{subsection.8.2.1}}
-\@writefile{toc}{\contentsline {subsubsection}{Open source implementations}{77}{section*.44}}
-\@writefile{toc}{\contentsline {paragraph}{ScalaQuery}{77}{section*.45}}
-\@writefile{toc}{\contentsline {paragraph}{Squeryl}{77}{section*.46}}
-\@writefile{lof}{\contentsline {figure}{\numberline {8.1}{\ignorespaces Chapter map }}{78}{figure.8.1}}
-\@writefile{toc}{\contentsline {section}{\numberline {8.3}Continuations revisited}{78}{section.8.3}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {8.3.1}Stored state}{78}{subsection.8.3.1}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {8.3.2}Transactions}{78}{subsection.8.3.2}}
+\@writefile{toc}{\contentsline {section}{\numberline {8.1}Mapping our domain model to storage}{79}{section.8.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {8.1.1}Functional and relational models}{79}{subsection.8.1.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {8.1.2}Functional and XML models}{79}{subsection.8.1.2}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {8.1.3}ORM}{79}{subsection.8.1.3}}
+\@writefile{toc}{\contentsline {section}{\numberline {8.2}Storage and language-integrated query}{79}{section.8.2}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {8.2.1}LINQ and \lstinline [language=Scala]!for!-comprehensions}{79}{subsection.8.2.1}}
+\@writefile{toc}{\contentsline {subsubsection}{Open source implementations}{79}{section*.53}}
+\@writefile{toc}{\contentsline {paragraph}{ScalaQuery}{79}{section*.54}}
+\@writefile{toc}{\contentsline {paragraph}{Squeryl}{79}{section*.55}}
+\@writefile{lof}{\contentsline {figure}{\numberline {8.1}{\ignorespaces Chapter map }}{80}{figure.8.1}}
+\@writefile{toc}{\contentsline {section}{\numberline {8.3}Continuations revisited}{80}{section.8.3}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {8.3.1}Stored state}{80}{subsection.8.3.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {8.3.2}Transactions}{80}{subsection.8.3.2}}
\@setckpt{chapters/eight/ch}{
-\setcounter{page}{79}
+\setcounter{page}{81}
\setcounter{equation}{0}
\setcounter{enumi}{0}
\setcounter{enumii}{0}
@@ -35,7 +35,7 @@
\setcounter{table}{0}
\setcounter{parentequation}{0}
\setcounter{Item}{0}
-\setcounter{Hfootnote}{9}
+\setcounter{Hfootnote}{10}
\setcounter{lstnumber}{1}
\setcounter{theorem}{0}
\setcounter{section@level}{2}
View
34 src/main/book/content/chapters/five/abstract-syntax.tex
@@ -1,3 +1,35 @@
\section{Our abstract syntax}
-TBD
+\paragraph{Abstract syntax}
+%For our example we'll need a toy language.
+Fittingly for a book about \texttt{Scala} we'll use the
+$\lambda$-calculus as our toy language. \footnote{A word to the wise:
+ even if you are an old hand at programming language semantics, even
+ if you know the $\lambda$-calculus like the back of your hand, you
+ are likely to be surprised by some of the things you see in the next
+ few sections. Just to make sure that everyone gets a chance to look
+ at the formalism as if it were brand new, a few recent theoretical
+ developments have been thrown in. So, watch out!} The core
+\textit{abstract} syntax of the lambda calculus is given by the
+following \textit{EBNF} grammar.
+
+\begin{mathpar}
+ \inferrule* [lab=expression] {} {{M,N} ::=}
+ \and
+ \inferrule* [lab=mention] {} {x}
+ \and
+ \inferrule* [lab=abstraction] {} {\;| \; \lambda x . M}
+ \and
+ \inferrule* [lab=application] {} {\;| \; M N}
+\end{mathpar}
+
+Informally, this is really a language of pure variable management. For
+example, if the expression $M$ mentions $x$, then $\lambda x. M$ turns
+$x$ into a variable in $M$ and provides a means to substitute values
+into $M$, via application. Thus, $(\lambda x.M)N$ will result in a new
+term, sometimes written $M[N/x]$, in which every occurrence of $x$ has
+been replaced by an occurrence of $N$. Thus, $(\lambda x.x)M$ yields
+$M$, illustrating the implementation in the $\lambda$-calculus of the
+identity function. It turns out to be quite remarkable what you can do
+with pure variable management.
+
View
747 src/main/book/content/chapters/five/application-domain-model.tex
@@ -1,3 +1,748 @@
\section{Our application domain model}
-TBD
+\subsubsection{Our toy language}
+
+\paragraph{A simple-minded representation}
+At a syntactic level this has a direct representation as the following
+\texttt{Scala} code.
+
+\break
+\begin{lstlisting}[language=Scala,mathescape=true]
+ trait Expressions {
+ type Nominal
+ // $M,N ::=$
+ abstract class Expression
+
+ // $x$
+ case class Mention( reference : Nominal )
+ extends Expression
+
+ // $\lambda \; x_1,...,x_n.M$
+ case class Abstraction(
+ formals : List[Nominal],
+ body : Expression
+ ) extends Expression
+
+ // $M N_1 ... N_n$
+ case class Application(
+ operation : Expression,
+ actuals : List[Expression]
+ ) extends Expression
+ }
+\end{lstlisting}
+
+In this representation each \emph{syntactic category}, EXPRESSION, MENTION,
+ABSTRACTION and APPLICATION, is represented by a
+\lstinline[language=Scala]!trait! or \lstinline[language=Scala]!case class!.
+EXPRESSION's are \lstinline[language=Scala]!trait!'s because they
+are pure placeholders. The other categories elaborate the syntactic
+form, and the elaboration is matched by the
+\lstinline[language=Scala]!case class! structure. Thus, for example,
+an ABSTRACTION is modeled by an instance of the
+\lstinline[language=Scala]!case class! called
+\lstinline[language=Scala]!Abstraction! having members
+\lstinline[language=Scala]!formal! for the formal parameter of the
+abstraction, and \lstinline[language=Scala]!body! for the
+$\lambda$-term under the abstraction that might make use of the
+parameter. Similarly, an APPLICATION is modeled by an instance of the
+\lstinline[language=Scala]!case class! of the same name having members
+\lstinline[language=Scala]!operation! for the expression that will be applied
+to the actual parameter called (not surprisingly)
+\lstinline[language=Scala]!actual!.
+
+\paragraph{Currying}
+The attentive reader will have noticed that there's a difference
+between the abstract syntax and our \texttt{Scala} model. The abstract
+syntax only supports a single formal parameter under
+$\lambda$-abstraction, while the \texttt{Scala} model declares the
+\lstinline[language=Scala,mathescape=true]!formals! to be of type
+\lstinline[language=Scala,mathescape=true]!List[Nominal]!. The model
+anticipates the encoding $\lambda \; x \; y . M \stackrel{def}{=}
+\lambda \; x. \lambda \; y . M$. Given that abstractions are
+first-class values, in the sense that they can be returned as values
+and passed as parameters, this is a fairly intuitive encoding. It has
+some pleasant knock-on effects. For example, when there is an arity
+shortfall, i.e. the number of actual parameters is less than the
+number of formal parameters, then it is both natural and useful simply
+to return an abstraction. Thus, $(\lambda x y. f x y)u$ can be
+evaluated to return $(\lambda y. f u y)$. This is an extremely
+convenient mechanism to support partial evaluation.
+
+\paragraph{Type parametrization and quotation}
+One key aspect of this representation is that we acknowledge that the
+abstract syntax is strangely silent on what the \emph{terminals}
+are. It doesn't actually say what $x$'s are. Often implementations of
+the $\lambda$-calculus will make some choice, such as
+\lstinline[language=Scala]!String!s or
+\lstinline[language=Scala]!Integers! or some other
+representation. With \texttt{Scala}'s type parametrization we can
+defer this choice. In fact, to foreshadow some of what's to come, we
+illustrate that we never actually have to go outside of the basic
+grammar definition to come up with a supply of identifiers.
+
+In the code above we have deferred the choice of identifier. In the
+code below we provide several different kinds of identifiers (the term
+of art in this context is ``name''), but defer the notion of an
+expression by the same trick used to defer the choice of identifiers.
+
+\begin{lstlisting}[language=Scala]
+ trait Nominals {
+ type Term
+ abstract class Name
+ case class Transcription( expression : Term )
+ extends Name
+ case class StringLiteral( str : String )
+ extends Name
+ case class DeBruijn( outerIndex : Int, innerIndex : Int )
+ extends Name
+ case class URLLiteral( url : java.net.URL )
+ extends Name
+ }
+\end{lstlisting}
+
+Now we wire the two types together.
+
+\begin{lstlisting}[language=Scala]
+ trait ReflectiveGenerators
+ extends Expressions with Nominals {
+ type Nominal = Name
+ type Term = Expression
+ }
+\end{lstlisting}
+
+This allows us to use \emph{quoted} terms as variables in
+$lambda$-terms! The idea is very rich as it begs the question of
+whether such variables can be \emph{unquoted} and what that means for
+evaluation. Thus, \texttt{Scala}'s type system is already leading
+to some pretty interesting places! In fact, this is an instance of a
+much deeper design principle lurking here, called two-level type
+decomposition, that is enabled by type-level parametricity. We'll talk
+more about this in upcoming chapters, but just want to put it on the
+backlog.
+
+\paragraph{Some syntactic sugar}
+To this core let us add some syntactic sugar.
+
+\begin{mathpar}
+ \inferrule* [lab=previous] {} {{M,N} ::= ...}
+ \and
+ \inferrule* [lab=let] {} {\;| \; let \; x = M \; in \; N}
+ \and
+ \inferrule* [lab=seq] {} {\;| \; M;N}
+\end{mathpar}
+
+This is sugar because we can reduce $let \; x \; = \; M \; in \; N$ to
+$(\lambda x. N) M$ and $ M; N$ to $let \; x \; = \; M \; in \; N$ with
+$x$ not occurring in $N$.
+
+\paragraph{Digression: complexity management principle} In terms of
+our implementation, the existence of this reduction means that we can
+choose to have explicit representation of these syntactic categories
+or not. This choice is one of a those design situations that's of
+significant interest if our concern is complexity management. [Note:
+brief discussion of the relevance of super combinators.]
+
+\paragraph{Concrete syntax}
+Now let's wrap this up in concrete syntax.
+
+\begin{mathpar}
+ \inferrule* [lab=expression] {} {{M,N} ::=}
+ \and
+ \inferrule* [lab=mention] {} {x}
+ \and
+ \inferrule* [lab=abstraction] {} {\;| \; \texttt{(} x_1 \texttt{,} ... \texttt{,} x_k \texttt{)} \; \texttt{=>} \; M}
+ \and
+ \inferrule* [lab=application] {} {\;| \; M\texttt{(} N_1 \texttt{,} ... \texttt{,} N_k \texttt{)}}
+ \and
+ \inferrule* [lab=let] {} {\;| \; \texttt{val} \; x \; \texttt{=} \; M \texttt{;} N}
+ \and
+ \inferrule* [lab=seq] {} {\;| \; M \texttt{;} N }
+ \and
+ \inferrule* [lab=group] {} {\;| \; \texttt{ \{ } M \texttt{ \} } }
+\end{mathpar}
+
+It doesn't take much squinting to see that this looks a lot like a
+subset of \texttt{Scala}, and that's because -- of course! --
+functional languages like \texttt{Scala} all share a common core that
+is essentially the $\lambda$-calculus. Once you familiarize yourself
+with the $\lambda$-calculus as a kind of design pattern you'll see it
+poking out everywhere: in \texttt{Clojure} and \texttt{OCaml} and
+\texttt{F\#} and \texttt{Scala}. In fact, as we'll see later, just
+about any DSL you design that needs a notion of variables could do
+worse than simply to crib from this existing and well understood
+design pattern.
+
+If you've been following along so far, however, you will spot that
+something is actually wrong with this grammar. We still don't have an
+actual terminal! \emph{Concrete} syntax is what ``users'' type, so as
+soon as we get to concrete syntax we can no longer defer our choices
+about identifiers. Let's leave open the door for both ordinary
+identifiers -- such as we see in \texttt{Scala} -- and our funny
+quoted terms. This means we need to add the following productions to
+our grammar.
+
+\begin{mathpar}
+ \inferrule* [lab=identifier] {} {{x,y} ::=}
+ \and
+ \inferrule* [lab=string-id] {} {\;| \; String}
+ \and
+ \inferrule* [lab=quotation] {} {\;| \; \texttt{@} \texttt{<} M \texttt{>}}
+\end{mathpar}
+
+(The reason we use the \texttt{@} for quotation -- as will become
+clear later -- is that when we have both quote and dequote, the former
+functions a lot like asking for a \emph{pointer} to a term while the
+latter is a lot like dereferencing the pointer.)
+
+\paragraph{Translating concrete syntax to abstract syntax}
+The translation from the concrete syntax to the abstract syntax is
+compactly expressed as follows. Even if the form of the translation is
+unfamiliar, it should still leave you with the impression that some
+core of \texttt{Scala} is really the $\lambda$-calculus.
+
+% \begin{mathpar}
+% \inferrule* {} {\meaningof{\lstinline[language=Scala,mathescape=true]!x!} = x}
+% \and
+% \inferrule* {} {\meaningof{\lstinline[language=Scala,mathescape=true]!(x) $\Rightarrow$! expr } = \lambda \; x . \meaningof{expr} }
+% \inferrule* {} {\meaningof{\lstinline[language=Scala,mathescape=true]!val x!} = let \; x = \meaningof{expr_1} in \meaningof{expr_2} }
+% \end{mathpar}
+
+\begin{lstlisting}[language=Scala,mathescape=true,frame=single,caption={translating concrete to abstract syntax},captionpos=b]
+ $\ldb$ x $\rdb$ $=$ $x$
+ $\ldb$ (x) => expr $\rdb$ $=$ $\lambda \; x . \ldb$ expr $\rdb$
+ $\ldb$ expr( expr$_1$, ..., expr$_n$ ) $\rdb$
+ $=$ $\ldb$ expr $\rdb$ $\ldb$ expr$_1$ $\rdb$ ... $\ldb$ expr$_n$ $\rdb$
+ $\ldb$ val x = expr$_1$ ; expr$_2$ $\rdb$ $=$ $let$ $\ldb$ x $\rdb$ $=$ $\ldb$ expr$_1$ $\rdb$ $in$ $\ldb$ expr$_2$ $\rdb$
+ $\ldb$ expr$_1$ ; expr$_2$ $\rdb$ $=$ $\ldb$ expr$_1$ $\rdb$ $;$ $\ldb$ expr$_2$ $\rdb$
+ $\ldb$ { expr } $\rdb$ $=$ ( $\ldb$ expr $\rdb$ )
+\end{lstlisting}
+
+Further, the value of the explicit representation of sugar in terms of
+structuring the translation should be clear. Of course, in a book
+entitled \emph{Pro Scala} the best way to unpack this presentation
+is in terms of a \texttt{Scala} implementation.
+
+\begin{lstlisting}[language=Scala,mathescape=true]
+ trait Compiler extends Expressions with Nominals {
+ // Abstract away interning variables
+ type Internist =
+ {def intern( varExpr : Absyn.VariableExpr ) : Nominal}
+ def internist() : Internist
+
+ def intern( varExpr : Absyn.VariableExpr )
+ : Nominal = { internist().intern( varExpr ) }
+ def compileExpr( numericExpr : Absyn.Numeric )
+ : Expression = {
+ new IntegerExpression(
+ numericExpr.integer_.asInstanceOf[Int]
+ )
+ }
+
+ // $\ldb$ x $\rdb$ $=$ $x$
+ def compileExpr( mentionExpr : Absyn.Mention )
+ : Expression = {
+ new Mention( intern( mentionExpr.variableexpr_ ) )
+ }
+ // $\ldb$ (x) => expr $\rdb$ $=$ $\lambda \; x . \ldb$ expr $\rdb$
+ def compileExpr( abstractionExpr : Absyn.Abstraction )
+ : Expression = {
+ val fmls : List[Nominal] =
+ abstractionExpr.listvariableexpr_.map(
+ { ( vExpr : Absyn.VariableExpr ) => intern( vExpr ) }
+ ).toList
+ new Abstraction( fmls, compile( abstractionExpr.expression_ ) )
+ }
+ // $\ldb$ expr( expr$_1$, ..., expr$_n$ ) $\rdb$
+ // $=$ $\ldb$ expr $\rdb$ $\ldb$ expr$_1$ $\rdb$ ... $\ldb$ expr$n$ $\rdb$
+ def compileExpr( applicationExpr : Absyn.Application )
+ : Expression = {
+ new Application(
+ compile( applicationExpr.expression_1 ),
+ List( compile( applicationExpr.expression_2 ) )
+ )
+ }
+
+ // $\ldb$ - $\rdb$ $:$ Mini-Scala => $\lambda$-calculus
+ def compile( expr : Absyn.Expression )
+ : Expression = {
+ expr match {
+ case value : Absyn.Value => {
+ value.valueexpr_ match {
+ case numericExpr : Absyn.Numeric =>
+ compileExpr( numericExpr )
+ }
+ }
+ case numericExpr : Absyn.Numeric => {
+ compileExpr( numericExpr )
+ }
+ case mentionExpr : Absyn.Mention => {
+ compileExpr( mentionExpr )
+ }
+ case abstractionExpr : Absyn.Abstraction => {
+ compileExpr( abstractionExpr )
+ }
+ case applicationExpr : Absyn.Application => {
+ compileExpr( applicationExpr )
+ }
+ }
+ }
+
+ def parse( str : String ) : Absyn.Expression = {
+ (new parser(
+ new Yylex( new StringReader( str ) )
+ ) ).pExpression()
+ }
+
+ def compile( str : String ) : Expression = {
+ try {
+ compile( parse( str ) )
+ }
+ catch {
+ case e => { // log error
+ throw e
+ }
+ }
+ }
+ }
+\end{lstlisting}
+
+The first thing to notice about this translation is how faithfully it
+follows the equational specification. This aspect of functional
+programming in general and \texttt{Scala} in particular is one of the
+things that sets it apart. In a development culture where AGILE
+methodologies rightfully demand a justification thread running from
+feature to line of code, a means of tracing specification to
+implementation is of practical importance. Of course, rarely do
+today's SCRUM meetings result in equational specifications; however,
+they might result in diagrammatic specification which, as we will see
+in subsequent sections, can be given equational interpretations that
+then guide functional implementation. Of equal importance: it cannot
+have escaped notice how much more compact the notations we have used
+for specification actually are. In a context where brevity and
+complexity management are paramount, tools -- such as these
+specification techniques -- that help us gain a higher vantage point
+ought to carry some weight. This is another aim of this book, to
+provide at least some exposure to these higher-level techniques. One
+of the central points to be made is that if she's not already using
+them, the \emph{pro} \texttt{Scala} programmer is primed and ready to
+take advantage of them.
+
+\paragraph{Structural equivalence and Relations or What makes abstract syntax abstract}
+
+Apart from the fact that concrete syntax forces commitment to explicit
+representation of terminals, you might be wondering if there are any
+other differences between concrete and abstract syntax. It turns out
+there are. One of the key properties of abstract syntax is that it
+encodes a notion of equality of terms that is not generally
+represented in concrete syntax.
+
+It's easier to illustrate the idea in terms of our example. We know
+that programs that differ only by a change of bound variable are
+essentially the same. Concretely, the program
+\lstinline[language=Scala]!( x ) => x + 5! is essentially the same as
+the program \lstinline[language=Scala]!( y ) => y + 5!. By
+``essentially the same'' we mean that in every evaluation context
+where we might put the former if we substitute the latter we will get
+the same answer.
+
+However, this sort of equivalence doesn't have to be all intertwined
+with evaluation to be expressed. A little forethought shows we can
+achieve some separation of concerns by separating out certain kinds of
+\emph{structural} equivalences. Abstract syntax is where we express
+structural equivalence (often written using $\equiv$, for example $M \equiv N$).
+In terms of our example we can actually calculate when two
+$\lambda$-terms differ only by a change of \emph{bound} variable,
+where by bound variable we just mean a variable mention in a term also
+using the variable as formal parameter of an abstraction.
+
+Since we'll need that notion to express this structural equivalence,
+let's write some code to clarify the idea, but because it will be more
+convenient, let's calculate the variables not occurring bound,
+i.e. the \emph{free} variables of a $\lambda$-term.
+
+\begin{lstlisting}[language=Scala]
+ def freeVariables( term : Expression ) : Set[Nominal] = {
+ term match {
+ case Mention( reference ) => Set( reference )
+ case Abstraction( formals, body ) =>
+ freeVariables( body ) &~ formals.toSet
+ case Application( operation, actuals ) =>
+ ( freeVariables( operation ) /: actuals )(
+ { ( acc, elem ) => acc ++ freeVariables( elem ) }
+ )
+ }
+ }
+\end{lstlisting}
+
+In addition to this idea we'll need to represent exchanging bound
+variables. A traditional way to approach this is in terms of
+substituting a term (including variables) for a variable. A crucial
+point is that we need to avoid unwanted variable capture. For example,
+suppose we need to substitute $y$ for $x$ in a term of the form
+$\lambda y.(x y)$. Doing so blindly will result in a term of the form
+$\lambda y.(y y)$; but, now the first $y$ is bound by the abstraction
+-- probably not what we want. To avoid this -- using structural
+equivalence! -- we can move the bound variable ``out of the
+way''. That is, we can first change the term to an equivalent one, say
+$\lambda u.(x u)$. Now, we can make the substitution, resulting in
+$\lambda u.(y u)$. This is what's called capture-avoiding
+substitution. Central to this trick is the ability to come up with a
+fresh variable, one that doesn't occur in a term. Obviously, any
+implementation of this trick is going to depend implicitly on the
+internal structure of names. Until we have such a structure in hand we
+have to defer the implementation, but we mark it with a placeholder.
+
+\begin{lstlisting}[language=Scala]
+ def fresh( terms : List[Expression] ) : Nominal
+\end{lstlisting}
+
+Now we can write in \texttt{Scala} our definition of substitution.
+
+\break
+\begin{lstlisting}[language=Scala]
+ def substitute(
+ term : Expression,
+ actuals : List[Expression], formals : List[Nominal]
+ ) : Expression = {
+ term match {
+ case Mention( ref ) => {
+ formals.indexOf( ref ) match {
+ case -1 => term
+ case i => actuals( i )
+ }
+ }
+ case Abstraction( fmls, body ) => {
+ val fmlsN = fmls.map(
+ {
+ ( fml ) => {
+ formals.indexOf( fml ) match {
+ case -1 => fml
+ case i => fresh( List( body ) )
+ }
+ }
+ }
+ )
+ val bodyN =
+ substitute(
+ body,
+ fmlsN.map( _ => Mention( _ ) ),
+ fmlsN
+ )
+ Abstraction(
+ fmlsN,
+ substitute( bodyN, actuals, formals )
+ )
+ }
+ case Application( op, actls ) => {
+ Application(
+ substitute( op, actuals, formals ),
+ actls.map( _ => substitute( _, actuals, formals ) )
+ )
+ }
+ }
+ }
+\end{lstlisting}
+
+With this code in hand we have what we need to express the structural
+equivalence of terms.
+
+\begin{lstlisting}[language=Scala]
+ def `=a=`(
+ term1 : Expression, term2 : Expression
+ ) : Boolean = {
+ ( term1, term2 ) match {
+ case (
+ Mention( ref1 ),
+ Mention( ref2 )
+ ) => {
+ ref1 == ref2
+ }
+ case (
+ Abstraction( fmls1, body1 ), Abstraction( fmls2, body2 )
+ ) => {
+ if ( fmls1.length == fmls2.length ) {
+ val freshFmls =
+ fmls1.map(
+ { ( fml ) => Mention( fresh( List( body1, body2 ) ) ) }
+ )
+ `=a=`(
+ substitute( body1, freshFmls, fmls1 ),
+ substitute( body2, freshFmls, fmls2 )
+ )
+ }
+ else false
+ }
+ case (
+ Application( op1, actls1 ),
+ Application( op2, actls2 )
+ ) => {
+ ( `=a=`( op1, op2 ) /: actls1.zip actls2 )(
+ { ( acc, actlPair ) =>
+ acc && `=a=`( actlPair._1, actlPair._2 )
+ }
+ )
+ }
+ }
+ }
+\end{lstlisting}
+
+This is actually some significant piece of machinery just to be able
+to calculate what we mean when we write $M[N/x]$ and $M \equiv N$.
+People have wondered if this sort of machinery could be reasonably
+factored so that it could be mixed into a variety of variable-binding
+capabilities. It turns out that this is possible and is at the root of
+a whole family of language design proposals that began with Jamie
+Gabbay's \texttt{FreshML}.
+
+Beyond this separation of concerns the introduction of abstract syntax
+affords another kind of functionality. While we will look at this in
+much more detail in subsequent chapters, and especially the final
+chapter of the book, it is worthwhile setting up the discussion at the
+outset. A computationally effective notion of structural equivalence
+enables programmatic investigation of structure. In the context of our
+story, users not only write programs, but store them and expect to
+retrieve them later for further editing. In such a system it is easy
+to imagine they might want to search for structurally equivalent
+programs. In looking for patterns in their own code they might want to
+abstract it is easy to imagine them searching for programs
+structurally equivalent to one they've found themselves writing for
+the umpteenth time. Further, structural equivalence is one of the
+pillars of a system that supports automated refactoring.
+
+\paragraph{Digression: the internal structure of the type of variables}
+At this point the attentive reader may be bothered by something going
+on in the calculation of \lstinline[language=Scala]!freeVariables!. To
+actually perform the \lstinline[language=Scala]!remove! or the
+\lstinline[language=Scala]!union! we have to have equality defined on
+variables. Now, this works fine for
+\lstinline[language=Scala]!String!s, but what about
+\lstinline[language=Scala]!Quotations!?
+
+The question reveals something quite startling about the types\footnote{Note that here we mean the type of the entity in the model that represents variables -- not a typing for variables in the language we're modeling.} of
+variables. Clearly, the type has to include a definition of
+equality. Now, if we want to have an inexhaustible supply of
+variables, then the definition of equality of variables must make use
+of the ``internal'' structure of the variables. For example, checking
+equality of \lstinline[language=Scala]!String!s means checking the
+equality of the respective sequences of characters. There are a finite
+set of characters out of which all \lstinline[language=Scala]!String!s
+are built and so eventually the calculation of equality grounds
+out. The same would be true if we used
+\lstinline[language=Scala]!Integer!s as ``variables''. If our type of
+variables didn't have some evident internal structure (like a
+\lstinline[language=Scala]!String! has characters or an
+\lstinline[language=Scala]!Integer! has arithmetic structure) and yet
+it was to provide an endless supply of variables, then the equality
+check could only be an \emph{infinite} table -- which wouldn't fit
+inside a computer. So, the type of variables must also support some
+internal structure, i.e. it must be a container type!
+
+Fortunately, our \lstinline[language=Scala]!Quotation!s are
+containers, by definition. However, they face another challenge: are
+the \lstinline[language=Scala]!Quotation!s of two structurally
+equivalent terms equal as variables? If they are then there is a
+mutual recursion! Equivalence of terms depends on equality of
+\lstinline[language=Scala]!Quotation!s which depends on equivalence of
+terms. It turns out that we have cleverly arranged things so that this
+recursion will bottom out. The key property of the structure of the
+abstract syntax that makes this work is that there is an alternation:
+quotation, term constructor, quotation, ... . Each recursive call will
+lower the number of quotes, until we reach 0.
+
+\paragraph{Evaluation -- aka operational semantics}
+
+The computational engine of the $\lambda$-calculus is an operation
+called $\beta$-reduction. It's a very simple operation in
+principle. Whenever an \emph{abstraction} occurs in the
+\emph{operation} position of an \emph{application} the application as
+a whole reduces to the \emph{body} of the abstraction in which every
+occurrence of the formal parameter(s) of the abstraction has been
+replaced with the actual parameter(s) of the application. As an
+example, in the application $(\lambda u.(u u))(\lambda x.x)$, $\lambda
+u.(u u)$ is in operation position. Replacing in the body of the
+abstraction each occurrence of the formal parameter, $u$, with the
+actual parameter, $\lambda x.x$, of the application reduces the
+application to $(\lambda x.x)(\lambda x.x)$ which when we repeat the
+action of $\beta$-reduction reduces in turn to $\lambda x.x$.
+
+In symbols we write beta reduction like this
+
+\begin{mathpar}
+ \inferrule* [lab=$\beta$-reduction] {} {(\lambda x.M)N \to M[N/x]}
+\end{mathpar}
+
+In terms of our concrete syntax this means that we can expect
+expressions of the form
+\lstinline[language=Scala,mathescape=true]!((x$_1$,...,x$_n$) =>e)e$_1$ ... e$_n$! to evaluate to \lstinline[language=Scala,mathescape=true]!e[e$_1$/x$_1$ ... e$_n$/x$_n$]!.
+
+It is perhaps this last expression that brings home a point: we need
+to manage variable bindings, called environments in this discussion. The
+lambda calculus is silent on \emph{how} this is done. There are a
+variety of strategies for implementing environments.
+
+\paragraph{Ordinary maps}
+
+\paragraph{DeBruijn notation}
+
+\subsubsection{The \texttt{Scala} implementation}
+
+Here's the code
+
+\begin{lstlisting}[language=Scala]
+ trait Values {
+ type Environment
+ type Expression
+ abstract class Value
+ case class Closure(
+ fn : List[Value] => Value
+ ) extends Value
+ case class Quantity( quantity : Int )
+ extends Value
+ }
+
+ trait Reduction extends Expressions with Values {
+ type Dereferencer = {def apply( m : Mention ) : Value }
+ type Expansionist =
+ {def extend(
+ fmls : List[Mention],
+ actls : List[Value]
+ ) : Dereferencer}
+ type Environment <: (Dereferencer with Expansionist)
+ type Applicator = Expression => List[Value] => Value
+
+ val initialApplicator : Applicator =
+ { ( xpr : Expression ) => {
+ ( actls : List[Value] ) => {
+ xpr match {
+ case IntegerExpression( i ) => Quantity( i )
+ case _ => throw new Exception( "why are we here?" )
+ }
+ }
+ }
+ }
+
+ def reduce(
+ applicator : Applicator,
+ environment : Environment
+ ) : Expression => Value = {
+ case IntegerExpression( i ) => Quantity( i )
+ case Mention( v ) => environment( Mention( v ) )
+ case Abstraction( fmls, body ) =>
+ Closure(
+ { ( actuals : List[Value] ) => {
+ val keys : List[Mention] =
+ fmls.map( { ( fml : Nominal ) => Mention( fml ) });
+ reduce(
+ applicator,
+ environment.extend(
+ keys,
+ actuals ).asInstanceOf[Environment]
+ )( body )
+ }
+ }
+ )
+ case Application(
+ operator : Expression,
+ actuals : List[Expression]
+ ) => {
+ reduce( applicator, environment )( operator ) match {
+ case Closure( fn ) => {
+ fn.apply(
+ (actuals
+ map
+ {( actual : Expression) =>
+ (reduce( applicator, environment ))( actual )})
+ )
+ }
+ case _ =>
+ throw new Exception( "attempt to apply non function" )
+ }
+ }
+ case _ => throw new Exception( "not implemented, yet" )
+ }
+}
+\end{lstlisting}
+
+\subsubsection{What goes into a language definition}
+
+Before moving to the next chapter it is important to digest what we've
+done here. Since we've called out DSL-based design as a methodology
+worthy of attention, what does our little foray into defining a
+language tell us about language definition? It turns out that this is
+really part of folk lore in the programming language semantics
+community. At this point in time one of the commonly accepted
+presentations of a language definition has three components:
+
+\begin{itemize}
+ \item syntax -- usually given in terms of some variant of BNF
+ \item structural equivalence -- usually given in terms of a set of relations
+ \item operational semantics -- usually given as a set of conditional
+ rewrite rules, such as might be expressed in SOS format.
+\end{itemize}
+
+That's exactly what we see here. Our toy language can be completely
+characterized by the following aforementioned half-page specification.
+
+\paragraph{Syntax}
+
+\begin{mathpar}
+ \inferrule* [lab=expression] {} {{M,N} ::=}
+ \and
+ \inferrule* [lab=mention] {} {x}
+ \and
+ \inferrule* [lab=abstraction] {} {\;| \; \lambda x . M}
+ \and
+ \inferrule* [lab=application] {} {\;| \; M N}
+\end{mathpar}
+
+\paragraph{Structural equivalence}
+
+\begin{mathpar}
+ \inferrule*[left=$\alpha$-equivalence] { y \notin \mathcal{FN}( M ) } { \lambda x . M = \lambda y. M[y/x] }
+\end{mathpar}
+
+where
+
+\begin{mathpar}
+ \inferrule* {} {\mathcal{FN}( x ) = x} \and
+ \inferrule* {} {\mathcal{FN}( \lambda x . M ) = \mathcal{FN}( M ) \backslash \{ x \} } \and
+ \inferrule* {} {\mathcal{FN}( M N ) = \mathcal{FN}( M ) \cup \mathcal{FN}( N ) }
+\end{mathpar}
+
+and we write $M[y/x]$ to mean substitute a $y$ for every occurrence of $x$ in $M$.
+
+\paragraph{Operational semantics}
+
+\begin{mathpar}
+ \inferrule*[left=$\beta$-reduction] {} {( \lambda x. M )N \to M[N/y] } \and
+ \inferrule*[left=struct] { M \equiv M', M' \to N', N' \equiv N} {M \to N}
+\end{mathpar}
+
+\paragraph{Discussion}
+This specification leaves open some questions regarding order or
+evaluation. In this sense it's a kind of proto-specification. For
+example, to get a left-most evaluation order you could add the rule
+
+\begin{mathpar}
+ \inferrule*[left=leftmost] { M \to M'} {M N \to M' N}
+\end{mathpar}
+
+The \texttt{Scala} code we wrote in the preceding sections is
+essentially an elaboration of this specification. While this notation
+is clearly more compact, it is not hard to recognize that the code
+follows this structure very closely.
+
+\section{The project model}
+
+Recalling chapter one, the aim is not just to implement the
+$\lambda$-calculus, but to implement an editor and project management
+capability. One of the key points of this book is that DSL-based
+design really does work. So, the basic methods for specifying and
+implementing the toy language \emph{also} apply to specifying and
+implementing these features of our application as well.
+
+\subsection{Abstract syntax}
+
+\subsection{Concrete syntax -- and presentation layer}
+
+\subsection{Domain model}
View
47 src/main/book/content/chapters/five/ch.aux
@@ -1,23 +1,48 @@
\relax
-\@writefile{toc}{\contentsline {chapter}{\numberline {5}The domain model as abstract syntax}{63}{chapter.5}}
+\@writefile{toc}{\contentsline {chapter}{\numberline {5}The domain model as abstract syntax}{49}{chapter.5}}
\@writefile{lof}{\addvspace {10\p@ }}
\@writefile{lot}{\addvspace {10\p@ }}
-\@writefile{toc}{\contentsline {section}{\numberline {5.1}Our abstract syntax}{63}{section.5.1}}
-\@writefile{toc}{\contentsline {section}{\numberline {5.2}Our application domain model}{63}{section.5.2}}
-\@writefile{toc}{\contentsline {section}{\numberline {5.3}A transform pipeline}{63}{section.5.3}}
-\@writefile{lof}{\contentsline {figure}{\numberline {5.1}{\ignorespaces Chapter map }}{64}{figure.5.1}}
+\@writefile{toc}{\contentsline {section}{\numberline {5.1}Our abstract syntax}{49}{section.5.1}}
+\@writefile{toc}{\contentsline {paragraph}{Abstract syntax}{49}{section*.29}}
+\@writefile{lof}{\contentsline {figure}{\numberline {5.1}{\ignorespaces Chapter map }}{50}{figure.5.1}}
+\@writefile{toc}{\contentsline {section}{\numberline {5.2}Our application domain model}{50}{section.5.2}}
+\@writefile{toc}{\contentsline {subsubsection}{Our toy language}{50}{section*.30}}
+\@writefile{toc}{\contentsline {paragraph}{A simple-minded representation}{50}{section*.31}}
+\@writefile{toc}{\contentsline {paragraph}{Currying}{51}{section*.32}}
+\@writefile{toc}{\contentsline {paragraph}{Type parametrization and quotation}{52}{section*.33}}
+\@writefile{toc}{\contentsline {paragraph}{Some syntactic sugar}{53}{section*.34}}
+\@writefile{toc}{\contentsline {paragraph}{Digression: complexity management principle}{53}{section*.35}}
+\@writefile{toc}{\contentsline {paragraph}{Concrete syntax}{53}{section*.36}}
+\@writefile{toc}{\contentsline {paragraph}{Translating concrete syntax to abstract syntax}{54}{section*.37}}
+\@writefile{lol}{\contentsline {lstlisting}{\numberline {5.1}translating concrete to abstract syntax}{54}{lstlisting.5.1}}
+\@writefile{toc}{\contentsline {paragraph}{Structural equivalence and Relations or What makes abstract syntax abstract}{57}{section*.38}}
+\@writefile{toc}{\contentsline {paragraph}{Digression: the internal structure of the type of variables}{61}{section*.39}}
+\@writefile{toc}{\contentsline {paragraph}{Evaluation -- aka operational semantics}{62}{section*.40}}
+\@writefile{toc}{\contentsline {paragraph}{Ordinary maps}{62}{section*.41}}
+\@writefile{toc}{\contentsline {paragraph}{DeBruijn notation}{62}{section*.42}}
+\@writefile{toc}{\contentsline {subsubsection}{The \texttt {Scala} implementation}{62}{section*.43}}
+\@writefile{toc}{\contentsline {subsubsection}{What goes into a language definition}{64}{section*.44}}
+\@writefile{toc}{\contentsline {paragraph}{Syntax}{65}{section*.45}}
+\@writefile{toc}{\contentsline {paragraph}{Structural equivalence}{65}{section*.46}}
+\@writefile{toc}{\contentsline {paragraph}{Operational semantics}{65}{section*.47}}
+\@writefile{toc}{\contentsline {paragraph}{Discussion}{65}{section*.48}}
+\@writefile{toc}{\contentsline {section}{\numberline {5.3}The project model}{66}{section.5.3}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {5.3.1}Abstract syntax}{66}{subsection.5.3.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {5.3.2}Concrete syntax -- and presentation layer}{66}{subsection.5.3.2}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {5.3.3}Domain model}{66}{subsection.5.3.3}}
+\@writefile{toc}{\contentsline {section}{\numberline {5.4}A transform pipeline}{66}{section.5.4}}
\@setckpt{chapters/five/ch}{
-\setcounter{page}{65}
+\setcounter{page}{67}
\setcounter{equation}{0}
\setcounter{enumi}{0}
\setcounter{enumii}{0}
\setcounter{enumiii}{0}
\setcounter{enumiv}{0}
-\setcounter{footnote}{0}
+\setcounter{footnote}{2}
\setcounter{mpfootnote}{0}
\setcounter{part}{0}
\setcounter{chapter}{5}
-\setcounter{section}{3}
+\setcounter{section}{4}
\setcounter{subsection}{0}
\setcounter{subsubsection}{0}
\setcounter{paragraph}{0}
@@ -26,9 +51,9 @@
\setcounter{table}{0}
\setcounter{parentequation}{0}
\setcounter{Item}{0}
-\setcounter{Hfootnote}{9}
-\setcounter{lstnumber}{49}
+\setcounter{Hfootnote}{10}
+\setcounter{lstnumber}{73}
\setcounter{theorem}{0}
\setcounter{section@level}{1}
-\setcounter{lstlisting}{0}
+\setcounter{lstlisting}{1}
}
View
20 src/main/book/content/chapters/four/ch.aux
@@ -1,16 +1,16 @@
\relax
-\@writefile{toc}{\contentsline {chapter}{\numberline {4}Parsing requests, monadically}{59}{chapter.4}}
+\@writefile{toc}{\contentsline {chapter}{\numberline {4}Parsing requests, monadically}{45}{chapter.4}}
\@writefile{lof}{\addvspace {10\p@ }}
\@writefile{lot}{\addvspace {10\p@ }}
-\@writefile{toc}{\contentsline {section}{\numberline {4.1}Obligatory parsing monad}{59}{section.4.1}}
-\@writefile{toc}{\contentsline {section}{\numberline {4.2}Your parser combinators are showing}{59}{section.4.2}}
-\@writefile{toc}{\contentsline {section}{\numberline {4.3}EBNF and why higher levels of abstraction are better}{59}{section.4.3}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {4.3.1}Different platforms, different parsers}{59}{subsection.4.3.1}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {4.3.2}Different performance constraints, different parsers}{59}{subsection.4.3.2}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {4.3.3}Maintainability}{59}{subsection.4.3.3}}
-\@writefile{lof}{\contentsline {figure}{\numberline {4.1}{\ignorespaces Chapter map }}{60}{figure.4.1}}
+\@writefile{toc}{\contentsline {section}{\numberline {4.1}Obligatory parsing monad}{45}{section.4.1}}
+\@writefile{toc}{\contentsline {section}{\numberline {4.2}Your parser combinators are showing}{45}{section.4.2}}
+\@writefile{toc}{\contentsline {section}{\numberline {4.3}EBNF and why higher levels of abstraction are better}{45}{section.4.3}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {4.3.1}Different platforms, different parsers}{45}{subsection.4.3.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {4.3.2}Different performance constraints, different parsers}{45}{subsection.4.3.2}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {4.3.3}Maintainability}{45}{subsection.4.3.3}}
+\@writefile{lof}{\contentsline {figure}{\numberline {4.1}{\ignorespaces Chapter map }}{46}{figure.4.1}}
\@setckpt{chapters/four/ch}{
-\setcounter{page}{62}
+\setcounter{page}{48}
\setcounter{equation}{0}
\setcounter{enumi}{0}
\setcounter{enumii}{0}
@@ -29,7 +29,7 @@
\setcounter{table}{0}
\setcounter{parentequation}{0}
\setcounter{Item}{0}
-\setcounter{Hfootnote}{9}
+\setcounter{Hfootnote}{8}
\setcounter{lstnumber}{49}
\setcounter{theorem}{0}
\setcounter{section@level}{2}
View
16 src/main/book/content/chapters/nine/ch.aux
@@ -1,14 +1,14 @@
\relax
-\@writefile{toc}{\contentsline {chapter}{\numberline {9}Putting it all together}{79}{chapter.9}}
+\@writefile{toc}{\contentsline {chapter}{\numberline {9}Putting it all together}{81}{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}{79}{section.9.1}}
-\@writefile{toc}{\contentsline {section}{\numberline {9.2}Deploying our application}{79}{section.9.2}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {9.2.1}Why we are not deploying on GAE}{79}{subsection.9.2.1}}
-\@writefile{toc}{\contentsline {section}{\numberline {9.3}From one web application to web framework}{79}{section.9.3}}
-\@writefile{lof}{\contentsline {figure}{\numberline {9.1}{\ignorespaces Chapter map }}{80}{figure.9.1}}
+\@writefile{toc}{\contentsline {section}{\numberline {9.1}Our web application end-to-end}{81}{section.9.1}}
+\@writefile{toc}{\contentsline {section}{\numberline {9.2}Deploying our application}{81}{section.9.2}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {9.2.1}Why we are not deploying on GAE}{81}{subsection.9.2.1}}
+\@writefile{toc}{\contentsline {section}{\numberline {9.3}From one web application to web framework}{81}{section.9.3}}
+\@writefile{lof}{\contentsline {figure}{\numberline {9.1}{\ignorespaces Chapter map }}{82}{figure.9.1}}
\@setckpt{chapters/nine/ch}{
-\setcounter{page}{81}
+\setcounter{page}{83}
\setcounter{equation}{0}
\setcounter{enumi}{0}
\setcounter{enumii}{0}
@@ -27,7 +27,7 @@
\setcounter{table}{0}
\setcounter{parentequation}{0}
\setcounter{Item}{0}
-\setcounter{Hfootnote}{9}
+\setcounter{Hfootnote}{10}
\setcounter{lstnumber}{1}
\setcounter{theorem}{0}
\setcounter{section@level}{1}
View
34 src/main/book/content/chapters/one/ch.aux
@@ -17,32 +17,20 @@
\@writefile{lof}{\contentsline {figure}{\numberline {1.3}{\ignorespaces Example evaluation result page }}{16}{figure.1.3}}
\@writefile{toc}{\contentsline {subsubsection}{Our toy language}{17}{section*.7}}
\@writefile{toc}{\contentsline {paragraph}{Abstract syntax}{17}{section*.8}}
-\@writefile{toc}{\contentsline {paragraph}{A simple-minded representation}{17}{section*.9}}
-\@writefile{toc}{\contentsline {paragraph}{Currying}{18}{section*.10}}
-\@writefile{toc}{\contentsline {paragraph}{Type parametrization and quotation}{19}{section*.11}}
-\@writefile{toc}{\contentsline {paragraph}{Some syntactic sugar}{20}{section*.12}}
-\@writefile{toc}{\contentsline {paragraph}{Digression: complexity management principle}{20}{section*.13}}
-\@writefile{toc}{\contentsline {paragraph}{Concrete syntax}{20}{section*.14}}
-\@writefile{toc}{\contentsline {paragraph}{Translating concrete syntax to abstract syntax}{21}{section*.15}}
-\@writefile{lol}{\contentsline {lstlisting}{\numberline {1.1}translating concrete to abstract syntax}{21}{lstlisting.1.1}}
-\@writefile{toc}{\contentsline {paragraph}{Structural equivalence and Relations or What makes abstract syntax abstract}{23}{section*.16}}
-\@writefile{toc}{\contentsline {paragraph}{Digression: the internal structure of the type of variables}{28}{section*.17}}
-\@writefile{toc}{\contentsline {paragraph}{Evaluation -- aka operational semantics}{28}{section*.18}}
-\@writefile{toc}{\contentsline {subsubsection}{What goes into a language definition}{30}{section*.19}}
-\@writefile{toc}{\contentsline {paragraph}{Syntax}{31}{section*.20}}
-\@writefile{toc}{\contentsline {paragraph}{Structural equivalence}{31}{section*.21}}
-\@writefile{toc}{\contentsline {paragraph}{Operational semantics}{31}{section*.22}}
-\@writefile{toc}{\contentsline {paragraph}{Discussion}{31}{section*.23}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {1.3.2}Chapter map}{32}{subsection.1.3.2}}
-\@writefile{lof}{\contentsline {figure}{\numberline {1.4}{\ignorespaces Chapter map }}{33}{figure.1.4}}
+\@writefile{toc}{\contentsline {paragraph}{Concrete syntax}{17}{section*.9}}
+\@writefile{toc}{\contentsline {subsubsection}{Code editor}{18}{section*.10}}
+\@writefile{toc}{\contentsline {subsubsection}{Project editor}{18}{section*.11}}
+\@writefile{toc}{\contentsline {subsubsection}{Advanced features}{18}{section*.12}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {1.3.2}Chapter map}{18}{subsection.1.3.2}}
+\@writefile{lof}{\contentsline {figure}{\numberline {1.4}{\ignorespaces Chapter map }}{19}{figure.1.4}}
\@setckpt{chapters/one/ch}{
-\setcounter{page}{34}
+\setcounter{page}{20}
\setcounter{equation}{0}
\setcounter{enumi}{0}
\setcounter{enumii}{0}
\setcounter{enumiii}{0}
\setcounter{enumiv}{0}
-\setcounter{footnote}{6}
+\setcounter{footnote}{5}
\setcounter{mpfootnote}{0}
\setcounter{part}{0}
\setcounter{chapter}{1}
@@ -55,9 +43,9 @@
\setcounter{table}{0}
\setcounter{parentequation}{0}
\setcounter{Item}{0}
-\setcounter{Hfootnote}{6}
-\setcounter{lstnumber}{73}
+\setcounter{Hfootnote}{5}
+\setcounter{lstnumber}{1}
\setcounter{theorem}{0}
\setcounter{section@level}{2}
-\setcounter{lstlisting}{1}
+\setcounter{lstlisting}{0}
}
View
635 src/main/book/content/chapters/one/how-are-we-going-to-get-there.tex
@@ -95,148 +95,8 @@ \subsubsection{Our toy language}
identity function. It turns out to be quite remarkable what you can do
with pure variable management.
-\paragraph{A simple-minded representation}
-At a syntactic level this has a direct representation as the following
-\texttt{Scala} code.
-
-\break
-\begin{lstlisting}[language=Scala,mathescape=true]
- trait Expressions {
- type Nominal
- // $M,N ::=$
- abstract class Expression
-
- // $x$
- case class Mention( reference : Nominal )
- extends Expression
-
- // $\lambda \; x_1,...,x_n.M$
- case class Abstraction(
- formals : List[Nominal],
- body : Expression
- ) extends Expression
-
- // $M N_1 ... N_n$
- case class Application(
- operation : Expression,
- actuals : List[Expression]
- ) extends Expression
- }
-\end{lstlisting}
-
-In this representation each \emph{syntactic category}, EXPRESSION, MENTION,
-ABSTRACTION and APPLICATION, is represented by a
-\lstinline[language=Scala]!trait! or \lstinline[language=Scala]!case class!.
-EXPRESSION's are \lstinline[language=Scala]!trait!'s because they
-are pure placeholders. The other categories elaborate the syntactic
-form, and the elaboration is matched by the
-\lstinline[language=Scala]!case class! structure. Thus, for example,
-an ABSTRACTION is modeled by an instance of the
-\lstinline[language=Scala]!case class! called
-\lstinline[language=Scala]!Abstraction! having members
-\lstinline[language=Scala]!formal! for the formal parameter of the
-abstraction, and \lstinline[language=Scala]!body! for the
-$\lambda$-term under the abstraction that might make use of the
-parameter. Similarly, an APPLICATION is modeled by an instance of the
-\lstinline[language=Scala]!case class! of the same name having members
-\lstinline[language=Scala]!operation! for the expression that will be applied
-to the actual parameter called (not surprisingly)
-\lstinline[language=Scala]!actual!.
-
-\paragraph{Currying}
-The attentive reader will have noticed that there's a difference
-between the abstract syntax and our \texttt{Scala} model. The abstract
-syntax only supports a single formal parameter under
-$\lambda$-abstraction, while the \texttt{Scala} model declares the
-\lstinline[language=Scala,mathescape=true]!formals! to be of type
-\lstinline[language=Scala,mathescape=true]!List[Nominal]!. The model
-anticipates the encoding $\lambda \; x \; y . M \stackrel{def}{=}
-\lambda \; x. \lambda \; y . M$. Given that abstractions are
-first-class values, in the sense that they can be returned as values
-and passed as parameters, this is a fairly intuitive encoding. It has
-some pleasant knock-on effects. For example, when there is an arity
-shortfall, i.e. the number of actual parameters is less than the
-number of formal parameters, then it is both natural and useful simply
-to return an abstraction. Thus, $(\lambda x y. f x y)u$ can be
-evaluated to return $(\lambda y. f u y)$. This is an extremely
-convenient mechanism to support partial evaluation.
-
-\paragraph{Type parametrization and quotation}
-One key aspect of this representation is that we acknowledge that the
-abstract syntax is strangely silent on what the \emph{terminals}
-are. It doesn't actually say what $x$'s are. Often implementations of
-the $\lambda$-calculus will make some choice, such as
-\lstinline[language=Scala]!String!s or
-\lstinline[language=Scala]!Integers! or some other
-representation. With \texttt{Scala}'s type parametrization we can
-defer this choice. In fact, to foreshadow some of what's to come, we
-illustrate that we never actually have to go outside of the basic
-grammar definition to come up with a supply of identifiers.
-
-In the code above we have deferred the choice of identifier. In the
-code below we provide several different kinds of identifiers (the term
-of art in this context is ``name''), but defer the notion of an
-expression by the same trick used to defer the choice of identifiers.
-
-\begin{lstlisting}[language=Scala]
- trait Nominals {
- type Term
- abstract class Name
- case class Transcription( expression : Term )
- extends Name
- case class StringLiteral( str : String )
- extends Name
- case class DeBruijn( outerIndex : Int, innerIndex : Int )
- extends Name
- case class URLLiteral( url : java.net.URL )
- extends Name
- }
-\end{lstlisting}
-
-Now we wire the two types together.
-
-\begin{lstlisting}[language=Scala]
- trait ReflectiveGenerators
- extends Expressions with Nominals {
- type Nominal = Name
- type Term = Expression
- }
-\end{lstlisting}
-
-This allows us to use \emph{quoted} terms as variables in
-$lambda$-terms! The idea is very rich as it begs the question of
-whether such variables can be \emph{unquoted} and what that means for
-evaluation. Thus, \texttt{Scala}'s type system is already leading
-to some pretty interesting places! In fact, this is an instance of a
-much deeper design principle lurking here, called two-level type
-decomposition, that is enabled by type-level parametricity. We'll talk
-more about this in upcoming chapters, but just want to put it on the
-backlog.
-
-\paragraph{Some syntactic sugar}
-To this core let us add some syntactic sugar.
-
-\begin{mathpar}
- \inferrule* [lab=previous] {} {{M,N} ::= ...}
- \and
- \inferrule* [lab=let] {} {\;| \; let \; x = M \; in \; N}
- \and
- \inferrule* [lab=seq] {} {\;| \; M;N}
-\end{mathpar}
-
-This is sugar because we can reduce $let \; x \; = \; M \; in \; N$ to
-$(\lambda x. N) M$ and $ M; N$ to $let \; x \; = \; M \; in \; N$ with
-$x$ not occurring in $N$.
-
-\paragraph{Digression: complexity management principle} In terms of
-our implementation, the existence of this reduction means that we can
-choose to have explicit representation of these syntactic categories
-or not. This choice is one of a those design situations that's of
-significant interest if our concern is complexity management. [Note:
-brief discussion of the relevance of super combinators.]
-
\paragraph{Concrete syntax}
-Now let's wrap this up in concrete syntax.
+We'll wrap this up in concrete syntax.
\begin{mathpar}
\inferrule* [lab=expression] {} {{M,N} ::=}
@@ -265,498 +125,11 @@ \subsubsection{Our toy language}
worse than simply to crib from this existing and well understood
design pattern.
-If you've been following along so far, however, you will spot that
-something is actually wrong with this grammar. We still don't have an
-actual terminal! \emph{Concrete} syntax is what ``users'' type, so as
-soon as we get to concrete syntax we can no longer defer our choices
-about identifiers. Let's leave open the door for both ordinary
-identifiers -- such as we see in \texttt{Scala} -- and our funny
-quoted terms. This means we need to add the following productions to
-our grammar.
-
-\begin{mathpar}
- \inferrule* [lab=identifier] {} {{x,y} ::=}
- \and
- \inferrule* [lab=string-id] {} {\;| \; String}
- \and
- \inferrule* [lab=quotation] {} {\;| \; \texttt{@} \texttt{<} M \texttt{>}}
-\end{mathpar}
-
-(The reason we use the \texttt{@} for quotation -- as will become
-clear later -- is that when we have both quote and dequote, the former
-functions a lot like asking for a \emph{pointer} to a term while the
-latter is a lot like dereferencing the pointer.)
-
-\paragraph{Translating concrete syntax to abstract syntax}
-The translation from the concrete syntax to the abstract syntax is
-compactly expressed as follows. Even if the form of the translation is
-unfamiliar, it should still leave you with the impression that some
-core of \texttt{Scala} is really the $\lambda$-calculus.
-
-% \begin{mathpar}
-% \inferrule* {} {\meaningof{\lstinline[language=Scala,mathescape=true]!x!} = x}
-% \and
-% \inferrule* {} {\meaningof{\lstinline[language=Scala,mathescape=true]!(x) $\Rightarrow$! expr } = \lambda \; x . \meaningof{expr} }
-% \inferrule* {} {\meaningof{\lstinline[language=Scala,mathescape=true]!val x!} = let \; x = \meaningof{expr_1} in \meaningof{expr_2} }
-% \end{mathpar}
-
-\begin{lstlisting}[language=Scala,mathescape=true,frame=single,caption={translating concrete to abstract syntax},captionpos=b]
- $\ldb$ x $\rdb$ $=$ $x$
- $\ldb$ (x) => expr $\rdb$ $=$ $\lambda \; x . \ldb$ expr $\rdb$
- $\ldb$ expr( expr$_1$, ..., expr$_n$ ) $\rdb$
- $=$ $\ldb$ expr $\rdb$ $\ldb$ expr$_1$ $\rdb$ ... $\ldb$ expr$_n$ $\rdb$
- $\ldb$ val x = expr$_1$ ; expr$_2$ $\rdb$ $=$ $let$ $\ldb$ x $\rdb$ $=$ $\ldb$ expr$_1$ $\rdb$ $in$ $\ldb$ expr$_2$ $\rdb$
- $\ldb$ expr$_1$ ; expr$_2$ $\rdb$ $=$ $\ldb$ expr$_1$ $\rdb$ $;$ $\ldb$ expr$_2$ $\rdb$
- $\ldb$ { expr } $\rdb$ $=$ ( $\ldb$ expr $\rdb$ )
-\end{lstlisting}
-
-Further, the value of the explicit representation of sugar in terms of
-structuring the translation should be clear. Of course, in a book
-entitled \emph{Pro Scala} the best way to unpack this presentation
-is in terms of a \texttt{Scala} implementation.
-
-\begin{lstlisting}[language=Scala,mathescape=true]
- trait Compiler extends Expressions with Nominals {
- // Abstract away interning variables
- type Internist =
- {def intern( varExpr : Absyn.VariableExpr ) : Nominal}
- def internist() : Internist
-
- def intern( varExpr : Absyn.VariableExpr )
- : Nominal = { internist().intern( varExpr ) }
- def compileExpr( numericExpr : Absyn.Numeric )
- : Expression = {
- new IntegerExpression(
- numericExpr.integer_.asInstanceOf[Int]
- )
- }
-
- // $\ldb$ x $\rdb$ $=$ $x$
- def compileExpr( mentionExpr : Absyn.Mention )
- : Expression = {
- new Mention( intern( mentionExpr.variableexpr_ ) )
- }
- // $\ldb$ (x) => expr $\rdb$ $=$ $\lambda \; x . \ldb$ expr $\rdb$
- def compileExpr( abstractionExpr : Absyn.Abstraction )
- : Expression = {
- val fmls : List[Nominal] =
- abstractionExpr.listvariableexpr_.map(
- { ( vExpr : Absyn.VariableExpr ) => intern( vExpr ) }
- ).toList
- new Abstraction( fmls, compile( abstractionExpr.expression_ ) )
- }
- // $\ldb$ expr( expr$_1$, ..., expr$_n$ ) $\rdb$
- // $=$ $\ldb$ expr $\rdb$ $\ldb$ expr$_1$ $\rdb$ ... $\ldb$ expr$n$ $\rdb$
- def compileExpr( applicationExpr : Absyn.Application )
- : Expression = {
- new Application(
- compile( applicationExpr.expression_1 ),
- List( compile( applicationExpr.expression_2 ) )
- )
- }
-
- // $\ldb$ - $\rdb$ $:$ Mini-Scala => $\lambda$-calculus
- def compile( expr : Absyn.Expression )
- : Expression = {
- expr match {
- case value : Absyn.Value => {
- value.valueexpr_ match {
- case numericExpr : Absyn.Numeric =>
- compileExpr( numericExpr )
- }
- }
- case numericExpr : Absyn.Numeric => {
- compileExpr( numericExpr )
- }
- case mentionExpr : Absyn.Mention => {
- compileExpr( mentionExpr )
- }
- case abstractionExpr : Absyn.Abstraction => {
- compileExpr( abstractionExpr )
- }
- case applicationExpr : Absyn.Application => {
- compileExpr( applicationExpr )
- }
- }
- }
-
- def parse( str : String ) : Absyn.Expression = {
- (new parser(
- new Yylex( new StringReader( str ) )
- ) ).pExpression()
- }
-
- def compile( str : String ) : Expression = {
- try {
- compile( parse( str ) )
- }
- catch {
- case e => { // log error
- throw e
- }
- }
- }
- }
-\end{lstlisting}
-
-The first thing to notice about this translation is how faithfully it
-follows the equational specification.
-
-\paragraph{Structural equivalence and Relations or What makes abstract syntax abstract}
-
-Apart from the fact that concrete syntax forces commitment to explicit
-representation of terminals, you might be wondering if there are any
-other differences between concrete and abstract syntax. It turns out
-there are. One of the key properties of abstract syntax is that it
-encodes a notion of equality of terms that is not generally
-represented in concrete syntax.
-
-It's easier to illustrate the idea in terms of our example. We know
-that programs that differ only by a change of bound variable are
-essentially the same. Concretely, the program
-\lstinline[language=Scala]!( x ) => x + 5! is essentially the same as
-the program \lstinline[language=Scala]!( y ) => y + 5!. By
-``essentially the same'' we mean that in every evaluation context
-where we might put the former if we substitute the latter we will get
-the same answer.
-
-However, this sort of equivalence doesn't have to be all intertwined
-with evaluation to be expressed. A little forethought shows we can
-achieve some separation of concerns by separating out certain kinds of
-\emph{structural} equivalences. Abstract syntax is where we express
-structural equivalence (often written using $\equiv$, for example $M \equiv N$).
-In terms of our example we can actually calculate when two
-$\lambda$-terms differ only by a change of \emph{bound} variable,
-where by bound variable we just mean a variable mention in a term also
-using the variable as formal parameter of an abstraction.
-
-Since we'll need that notion to express this structural equivalence,
-let's write some code to clarify the idea, but because it will be more
-convenient, let's calculate the variables not occurring bound,
-i.e. the \emph{free} variables of a $\lambda$-term.
-
-\begin{lstlisting}[language=Scala]
- def freeVariables( term : Expression ) : Set[Nominal] = {
- term match {
- case Mention( reference ) => Set( reference )
- case Abstraction( formals, body ) =>
- freeVariables( body ) &~ formals.toSet
- case Application( operation, actuals ) =>
- ( freeVariables( operation ) /: actuals )(
- { ( acc, elem ) => acc ++ freeVariables( elem ) }
- )
- }
- }
-\end{lstlisting}
-
-In addition to this idea we'll need to represent exchanging bound
-variables. A traditional way to approach this is in terms of
-substituting a term (including variables) for a variable. A crucial
-point is that we need to avoid unwanted variable capture. For example,
-suppose we need to substitute $y$ for $x$ in a term of the form
-$\lambda y.(x y)$. Doing so blindly will result in a term of the form
-$\lambda y.(y y)$; but, now the first $y$ is bound by the abstraction
--- probably not what we want. To avoid this -- using structural
-equivalence! -- we can move the bound variable ``out of the
-way''. That is, we can first change the term to an equivalent one, say
-$\lambda u.(x u)$. Now, we can make the substitution, resulting in
-$\lambda u.(y u)$. This is what's called capture-avoiding
-substitution. Central to this trick is the ability to come up with a
-fresh variable, one that doesn't occur in a term. Obviously, any
-implementation of this trick is going to depend implicitly on the
-internal structure of names. Until we have such a structure in hand we
-have to defer the implementation, but we mark it with a placeholder.
-
-\begin{lstlisting}[language=Scala]
- def fresh( terms : List[Expression] ) : Nominal
-\end{lstlisting}
+\subsubsection{Code editor}
-Now we can write in \texttt{Scala} our definition of substitution.
-
-\break
-\begin{lstlisting}[language=Scala]
- def substitute(
- term : Expression,
- actuals : List[Expression], formals : List[Nominal]
- ) : Expression = {
- term match {
- case Mention( ref ) => {
- formals.indexOf( ref ) match {
- case -1 => term
- case i => actuals( i )
- }
- }
- case Abstraction( fmls, body ) => {
- val fmlsN = fmls.map(
- {
- ( fml ) => {
- formals.indexOf( fml ) match {
- case -1 => fml
- case i => fresh( List( body ) )
- }
- }
- }
- )
- val bodyN =
- substitute(
- body,
- fmlsN.map( _ => Mention( _ ) ),
- fmlsN
- )
- Abstraction(
- fmlsN,
- substitute( bodyN, actuals, formals )
- )
- }
- case Application( op, actls ) => {
- Application(
- substitute( op, actuals, formals ),
- actls.map( _ => substitute( _, actuals, formals ) )
- )
- }
- }
- }
-\end{lstlisting}
-
-With this code in hand we have what we need to express the structural
-equivalence of terms.
-
-\begin{lstlisting}[language=Scala]
- def `=a=`(
- term1 : Expression, term2 : Expression
- ) : Boolean = {
- ( term1, term2 ) match {
- case (
- Mention( ref1 ),
- Mention( ref2 )
- ) => {
- ref1 == ref2
- }
- case (
- Abstraction( fmls1, body1 ), Abstraction( fmls2, body2 )
- ) => {
- if ( fmls1.length == fmls2.length ) {
- val freshFmls =
- fmls1.map(
- { ( fml ) => Mention( fresh( List( body1, body2 ) ) ) }
- )
- `=a=`(
- substitute( body1, freshFmls, fmls1 ),
- substitute( body2, freshFmls, fmls2 )
- )
- }
- else false
- }
- case (
- Application( op1, actls1 ),
- Application( op2, actls2 )
- ) => {
- ( `=a=`( op1, op2 ) /: actls1.zip actls2 )(
- { ( acc, actlPair ) =>
- acc && `=a=`( actlPair._1, actlPair._2 )
- }
- )
- }
- }
- }
-\end{lstlisting}
-
-This is actually some significant piece of machinery just to be able
-to calculate what we mean when we write $M[N/x]$ and $M \equiv N$.
-People have wondered if this sort of machinery could be reasonably
-factored so that it could be mixed into a variety of variable-binding
-capabilities. It turns out that this is possible and is at the root of
-a whole family of language design proposals that began with Jamie
-Gabbay's \texttt{FreshML}.
-
-\paragraph{Digression: the internal structure of the type of variables}
-If you've been paying attention, you will note that there's something
-very funny going on in the calculation of
-\lstinline[language=Scala]!freeVariables!. To actually perform the
-\lstinline[language=Scala]!remove! or the
-\lstinline[language=Scala]!union! we have to have equality defined on
-variables. Now, this works fine for
-\lstinline[language=Scala]!String!s, but what about
-\lstinline[language=Scala]!Quotations!?
-
-The question reveals something quite startling about the types\footnote{Note that here we mean the type of the entity in the model that represents variables -- not a typing for variables in the language we're modeling.} of
-variables. Clearly, the type has to include a definition of
-equality. Now, if we want to have an inexhaustible supply of
-variables, then the definition of equality of variables must make use
-of the ``internal'' structure of the variables. For example, checking
-equality of \lstinline[language=Scala]!String!s means checking the
-equality of the respective sequences of characters. There are a finite
-set of characters out of which all \lstinline[language=Scala]!String!s
-are built and so eventually the calculation of equality grounds
-out. The same would be true if we used
-\lstinline[language=Scala]!Integer!s as ``variables''. If our type of
-variables didn't have some evident internal structure (like a
-\lstinline[language=Scala]!String! has characters or an
-\lstinline[language=Scala]!Integer! has arithmetic structure) and yet
-it was to provide an endless supply of variables, then the equality
-check could only be an \emph{infinite} table -- which wouldn't fit
-inside a computer. So, the type of variables must also support some
-internal structure, i.e. it must be a container type!
-
-Fortunately, our \lstinline[language=Scala]!Quotation!s are
-containers, by definition. However, they face another challenge: are
-the \lstinline[language=Scala]!Quotation!s of two structurally
-equivalent terms equal as variables? If they are then there is a
-mutual recursion! Equivalence of terms depends on equality of
-\lstinline[language=Scala]!Quotation!s which depends on equivalence of
-terms. It turns out that we have cleverly arranged things so that this
-recursion will bottom out. The key property of the structure of the
-abstract syntax that makes this work is that there is an alternation:
-quotation, term constructor, quotation, ... . Each recursive call will
-lower the number of quotes, until we reach 0.
-
-\paragraph{Evaluation -- aka operational semantics}
-
-Here's the code
-
-\begin{lstlisting}[language=Scala]
- trait Values {
- type Environment
- type Expression
- abstract class Value
- case class Closure(
- fn : List[Value] => Value
- ) extends Value
- case class Quantity( quantity : Int )
- extends Value
- }
-
- trait Reduction extends Expressions with Values {
- type Dereferencer = {def apply( m : Mention ) : Value }
- type Expansionist =
- {def extend(
- fmls : List[Mention],
- actls : List[Value]
- ) : Dereferencer}
- type Environment <: (Dereferencer with Expansionist)
- type Applicator = Expression => List[Value] => Value
-
- val initialApplicator : Applicator =
- { ( xpr : Expression ) => {
- ( actls : List[Value] ) => {
- xpr match {
- case IntegerExpression( i ) => Quantity( i )
- case _ => throw new Exception( "why are we here?" )
- }
- }
- }
- }
-
- def reduce(
- applicator : Applicator,
- environment : Environment
- ) : Expression => Value = {
- case IntegerExpression( i ) => Quantity( i )
- case Mention( v ) => environment( Mention( v ) )
- case Abstraction( fmls, body ) =>
- Closure(
- { ( actuals : List[Value] ) => {
- val keys : List[Mention] =
- fmls.map( { ( fml : Nominal ) => Mention( fml ) });
- reduce(
- applicator,
- environment.extend(
- keys,
- actuals ).asInstanceOf[Environment]
- )( body )
- }
- }
- )
- case Application(
- operator : Expression,
- actuals : List[Expression]
- ) => {
- reduce( applicator, environment )( operator ) match {
- case Closure( fn ) => {
- fn.apply(
- (actuals
- map
- {( actual : Expression) =>
- (reduce( applicator, environment ))( actual )})
- )
- }
- case _ =>
- throw new Exception( "attempt to apply non function" )
- }
- }
- case _ => throw new Exception( "not implemented, yet" )
- }
-}
-\end{lstlisting}
-
-\subsubsection{What goes into a language definition}
-
-Before moving to the next chapter it is important to digest what we've
-done here. Since we've called out DSL-based design as a methodology
-worthy of attention, what does our little foray into defining a
-language tell us about language definition? It turns out that this is
-really part of folk lore in the programming language semantics
-community. At this point in time one of the commonly accepted
-presentations of a language definition has three components:
-
-\begin{itemize}
- \item syntax -- usually given in terms of some variant of BNF
- \item structural equivalence -- usually given in terms of a set of relations
- \item operational semantics -- usually given as a set of conditional
- rewrite rules, such as might be expressed in SOS format.
-\end{itemize}
-
-That's exactly what we see here. Our toy language can be completely
-characterized by the following aforementioned half-page specification.
-
-\paragraph{Syntax}
-
-\begin{mathpar}
- \inferrule* [lab=expression] {} {{M,N} ::=}
- \and
- \inferrule* [lab=mention] {} {x}
- \and
- \inferrule* [lab=abstraction] {} {\;| \; \lambda x . M}
- \and
- \inferrule* [lab=application] {} {\;| \; M N}
-\end{mathpar}
-
-\paragraph{Structural equivalence}
-
-\begin{mathpar}
- \inferrule*[left=$\alpha$-equivalence] { y \notin \mathcal{FN}( M ) } { \lambda x . M = \lambda y. M[y/x] }
-\end{mathpar}
-
-where
-
-\begin{mathpar}
- \inferrule* {} {\mathcal{FN}( x ) = x} \and
- \inferrule* {} {\mathcal{FN}( \lambda x . M ) = \mathcal{FN}( M ) \backslash \{ x \} } \and
- \inferrule* {} {\mathcal{FN}( M N ) = \mathcal{FN}( M ) \cup \mathcal{FN}( N ) }
-\end{mathpar}
-
-and we write $M[y/x]$ to mean substitute a $y$ for every occurrence of $x$ in $M$.
-
-\paragraph{Operational semantics}
-
-\begin{mathpar}
- \inferrule*[left=$\beta$-reduction] {} {( \lambda x. M )N \to M[N/y] } \and
- \inferrule*[left=struct] { M \equiv M', M' \to N', N' \equiv N} {M \to N}
-\end{mathpar}
-
-\paragraph{Discussion}
-This specification leaves open some questions regarding order or
-evaluation. In this sense it's a kind of proto-specification. For
-example, to get a left-most evaluation order you could add the rule
-
-\begin{mathpar}
- \inferrule*[left=leftmost] { M \to M'} {M N \to M' N}
-\end{mathpar}
+\subsubsection{Project editor}
-The \texttt{Scala} code we wrote in the preceding sections is
-essentially an elaboration of this specification. While this notation
-is clearly more compact, it is not hard to recognize that the code
-follows this structure very closely.
+\subsubsection{Advanced features}
\subsection{Chapter map}
View
52 src/main/book/content/chapters/seven/ch.aux
@@ -1,32 +1,32 @@
\relax
-\@writefile{toc}{\contentsline {chapter}{\numberline {7}A review of collections as monads}{73}{chapter.7}}
+\@writefile{toc}{\contentsline {chapter}{\numberline {7}A review of collections as monads}{75}{chapter.7}}
\@writefile{lof}{\addvspace {10\p@ }}
\@writefile{lot}{\addvspace {10\p@ }}
-\@writefile{lof}{\contentsline {figure}{\numberline {7.1}{\ignorespaces Chapter map }}{74}{figure.7.1}}
-\@writefile{toc}{\contentsline {section}{\numberline {7.1}Sets, Lists and Languages}{75}{section.7.1}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {7.1.1}Witnessing Sets and Lists monadicity}{75}{subsection.7.1.1}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {7.1.2}Languages and Sets of Words}{75}{subsection.7.1.2}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {7.1.3}Of lenses and bananas}{75}{subsection.7.1.3}}
-\@writefile{toc}{\contentsline {section}{\numberline {7.2}Containers and syntax}{75}{section.7.2}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {7.2.1}The algebra of Sets}{75}{subsection.7.2.1}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {7.2.2}The algebra of Lists}{75}{subsection.7.2.2}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {7.2.3}The algebra of Sets of Words}{75}{subsection.7.2.3}}
-\@writefile{toc}{\contentsline {section}{\numberline {7.3}Algebras}{75}{section.7.3}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {7.3.1}Kleisli}{75}{subsection.7.3.1}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {7.3.2}Eilenberg-Moore}{75}{subsection.7.3.2}}
-\@writefile{toc}{\contentsline {section}{\numberline {7.4}Monad as container}{75}{section.7.4}}
-\@writefile{toc}{\contentsline {section}{\numberline {7.5}Monads and take-out}{76}{section.7.5}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {7.5.1}Option as container}{76}{subsection.7.5.1}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {7.5.2}I/O monad for contrast}{76}{subsection.7.5.2}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {7.5.3}Matching gazintas and gazoutas}{76}{subsection.7.5.3}}
-\@writefile{toc}{\contentsline {subsubsection}{Intuitionistic discipline}{76}{section*.42}}
-\@writefile{toc}{\contentsline {subsubsection}{Linear discipline}{76}{section*.43}}
-\@writefile{toc}{\contentsline {section}{\numberline {7.6}Co-monad and take-out}{76}{section.7.6}}
-\@writefile{toc}{\contentsline {section}{\numberline {7.7}Hopf structure}{76}{section.7.7}}
-\@writefile{toc}{\contentsline {section}{\numberline {7.8}Container and control}{76}{section.7.8}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {7.8.1}Delimited continuations reconsidered}{76}{subsection.7.8.1}}
+\@writefile{lof}{\contentsline {figure}{\numberline {7.1}{\ignorespaces Chapter map }}{76}{figure.7.1}}
+\@writefile{toc}{\contentsline {section}{\numberline {7.1}Sets, Lists and Languages}{77}{section.7.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {7.1.1}Witnessing Sets and Lists monadicity}{77}{subsection.7.1.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {7.1.2}Languages and Sets of Words}{77}{subsection.7.1.2}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {7.1.3}Of lenses and bananas}{77}{subsection.7.1.3}}
+\@writefile{toc}{\contentsline {section}{\numberline {7.2}Containers and syntax}{77}{section.7.2}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {7.2.1}The algebra of Sets}{77}{subsection.7.2.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {7.2.2}The algebra of Lists}{77}{subsection.7.2.2}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {7.2.3}The algebra of Sets of Words}{77}{subsection.7.2.3}}
+\@writefile{toc}{\contentsline {section}{\numberline {7.3}Algebras}{77}{section.7.3}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {7.3.1}Kleisli}{77}{subsection.7.3.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {7.3.2}Eilenberg-Moore}{77}{subsection.7.3.2}}
+\@writefile{toc}{\contentsline {section}{\numberline {7.4}Monad as container}{77}{section.7.4}}
+\@writefile{toc}{\contentsline {section}{\numberline {7.5}Monads and take-out}{78}{section.7.5}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {7.5.1}Option as container}{78}{subsection.7.5.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {7.5.2}I/O monad for contrast}{78}{subsection.7.5.2}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {7.5.3}Matching gazintas and gazoutas}{78}{subsection.7.5.3}}
+\@writefile{toc}{\contentsline {subsubsection}{Intuitionistic discipline}{78}{section*.51}}
+\@writefile{toc}{\contentsline {subsubsection}{Linear discipline}{78}{section*.52}}
+\@writefile{toc}{\contentsline {section}{\numberline {7.6}Co-monad and take-out}{78}{section.7.6}}
+\@writefile{toc}{\contentsline {section}{\numberline {7.7}Hopf structure}{78}{section.7.7}}
+\@writefile{toc}{\contentsline {section}{\numberline {7.8}Container and control}{78}{section.7.8}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {7.8.1}Delimited continuations reconsidered}{78}{subsection.7.8.1}}
\@setckpt{chapters/seven/ch}{
-\setcounter{page}{77}
+\setcounter{page}{79}
\setcounter{equation}{0}
\setcounter{enumi}{0}
\setcounter{enumii}{0}
@@ -45,7 +45,7 @@
\setcounter{table}{0}
\setcounter{parentequation}{0}
\setcounter{Item}{0}
-\setcounter{Hfootnote}{9}
+\setcounter{Hfootnote}{10}
\setcounter{lstnumber}{133}
\setcounter{theorem}{0}
\setcounter{section@level}{2}
View
43 src/main/book/content/chapters/six/ch.aux
@@ -1,25 +1,28 @@
\relax
-\@writefile{toc}{\contentsline {chapter}{\numberline {6}Zippers and contexts and URI's, oh my!}{65}{chapter.6}}
+\@writefile{toc}{\contentsline {chapter}{\numberline {6}Zippers and contexts and URI's, oh my!}{67}{chapter.6}}
\@writefile{lof}{\addvspace {10\p@ }}
\@writefile{lot}{\addvspace {10\p@ }}
-\@writefile{toc}{\contentsline {section}{\numberline {6.1}Zippers are not just for Bruno anymore}{65}{section.6.1}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {6.1.1}The history of the zipper}{65}{subsection.6.1.1}}
-\@writefile{toc}{\contentsline {subsubsection}{Huet's zipper}{65}{section*.40}}
-\@writefile{toc}{\contentsline {subsubsection}{Zippers generically}{65}{section*.41}}
-\@writefile{lof}{\contentsline {figure}{\numberline {6.1}{\ignorespaces Chapter map }}{66}{figure.6.1}}
-\@writefile{toc}{\contentsline {section}{\numberline {6.2}Zipper and one-holed contexts}{66}{section.6.2}}
-\@writefile{toc}{\contentsline {section}{\numberline {6.3}Differentiation and contexts}{66}{section.6.3}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {6.3.1}Regular types}{66}{subsection.6.3.1}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {6.3.2}Container types}{66}{subsection.6.3.2}}
-\@writefile{toc}{\contentsline {section}{\numberline {6.4}Generic zipper -- differentiating navigation}{66}{section.6.4}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {6.4.1}Delimited continuations}{66}{subsection.6.4.1}}
-\@writefile{toc}{\contentsline {section}{\numberline {6.5}Species of Structure}{66}{section.6.5}}
-\@writefile{toc}{\contentsline {section}{\numberline {6.6}Constructing contexts and zippers from data types}{66}{section.6.6}}
-\@writefile{toc}{\contentsline {section}{\numberline {6.7}Mapping URIs to zipper-based paths and back}{71}{section.6.7}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {6.7.1}Path and context}{71}{subsection.6.7.1}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {6.7.2}Homomorphisms and obfuscation}{71}{subsection.6.7.2}}
+\@writefile{toc}{\contentsline {section}{\numberline {6.1}Zippers are not just for Bruno anymore}{67}{section.6.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {6.1.1}The history of the zipper}{67}{subsection.6.1.1}}
+\@writefile{toc}{\contentsline {subsubsection}{Huet's zipper}{67}{section*.49}}
+\@writefile{toc}{\contentsline {subsubsection}{Zippers generically}{67}{section*.50}}
+\@writefile{lof}{\contentsline {figure}{\numberline {6.1}{\ignorespaces Chapter map }}{68}{figure.6.1}}
+\@writefile{toc}{\contentsline {section}{\numberline {6.2}Zipper and one-holed contexts}{68}{section.6.2}}
+\@writefile{toc}{\contentsline {section}{\numberline {6.3}Differentiation and contexts}{68}{section.6.3}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {6.3.1}Regular types}{68}{subsection.6.3.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {6.3.2}Container types}{68}{subsection.6.3.2}}
+\@writefile{toc}{\contentsline {section}{\numberline {6.4}Generic zipper -- differentiating navigation}{68}{section.6.4}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {6.4.1}Delimited continuations}{68}{subsection.6.4.1}}
+\@writefile{toc}{\contentsline {section}{\numberline {6.5}Species of Structure}{68}{section.6.5}}
+\@writefile{toc}{\contentsline {section}{\numberline {6.6}Constructing contexts and zippers from data types}{68}{section.6.6}}
+\@writefile{toc}{\contentsline {section}{\numberline {6.7}Mapping URIs to zipper-based paths and back}{73}{section.6.7}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {6.7.1}Path and context}{73}{subsection.6.7.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {6.7.2}Homomorphisms and obfuscation}{73}{subsection.6.7.2}}
+\@writefile{toc}{\contentsline {section}{\numberline {6.8}Applying zippers to our project}{73}{section.6.8}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {6.8.1}Navigating and editing terms}{73}{subsection.6.8.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {6.8.2}Navigating and editing projects}{73}{subsection.6.8.2}}
\@setckpt{chapters/six/ch}{
-\setcounter{page}{72}
+\setcounter{page}{74}
\setcounter{equation}{0}
\setcounter{enumi}{0}
\setcounter{enumii}{0}
@@ -29,7 +32,7 @@
\setcounter{mpfootnote}{0}
\setcounter{part}{0}
\setcounter{chapter}{6}
-\setcounter{section}{7}
+\setcounter{section}{8}
\setcounter{subsection}{2}
\setcounter{subsubsection}{0}
\setcounter{paragraph}{0}
@@ -38,7 +41,7 @@
\setcounter{table}{0}
\setcounter{parentequation}{0}
\setcounter{Item}{0}
-\setcounter{Hfootnote}{9}
+\setcounter{Hfootnote}{10}
\setcounter{lstnumber}{133}
\setcounter{theorem}{0}
\setcounter{section@level}{2}
View
8 src/main/book/content/chapters/six/mapping-uris-zipper-based-paths.tex
@@ -2,4 +2,10 @@ \section{Mapping URIs to zipper-based paths and back}
\subsection{Path and context}
-\subsection{Homomorphisms and obfuscation}
+\subsection{Homomorphisms and obfuscation}
+
+\section{Applying zippers to our project}
+
+\subsection{Navigating and editing terms}
+
+\subsection{Navigating and editing projects}
View
52 src/main/book/content/chapters/ten/ch.aux
@@ -1,32 +1,32 @@
\relax
-\@writefile{toc}{\contentsline {chapter}{\numberline {10}The semantic web}{81}{chapter.10}}
+\@writefile{toc}{\contentsline {chapter}{\numberline {10}The semantic web}{83}{chapter.10}}
\@writefile{lof}{\addvspace {10\p@ }}
\@writefile{lot}{\addvspace {10\p@ }}
-\@writefile{toc}{\contentsline {section}{\numberline {10.1}Referential transparency}{81}{section.10.1}}
-\@writefile{lof}{\contentsline {figure}{\numberline {10.1}{\ignorespaces Chapter map }}{82}{figure.10.1}}
-\@writefile{toc}{\contentsline {paragraph}{A little motivation}{82}{section*.47}}
-\@writefile{toc}{\contentsline {section}{\numberline {10.2}Composing monads}{83}{section.10.2}}
-\@writefile{toc}{\contentsline {subsubsection}{Preliminary}{84}{section*.48}}
-\@writefile{toc}{\contentsline {section}{\numberline {10.3}Semantic application queries}{85}{section.10.3}}
-\@writefile{toc}{\contentsline {subsubsection}{An alternative presentation}{85}{section*.49}}
-\@writefile{toc}{\contentsline {paragraph}{Logic: the set monad as an algebra}{86}{section*.50}}
-\@writefile{toc}{\contentsline {paragraph}{Primes: an application}{87}{section*.51}}
-\@writefile{toc}{\contentsline {paragraph}{Summary}{87}{section*.52}}
-\@writefile{toc}{\contentsline {subsubsection}{Patterns}{88}{section*.53}}
-\@writefile{toc}{\contentsline {subsubsection}{A first mini-query language}{88}{section*.54}}
-\@writefile{toc}{\contentsline {subsubsection}{Iterating the design pattern}{88}{section*.55}}
-\@writefile{toc}{\contentsline {paragraph}{A spatial-behavioral-style logic for $\lambda $-calculus}{89}{section*.56}}
-\@writefile{toc}{\contentsline {paragraph}{Examples}{89}{section*.57}}
-\@writefile{toc}{\contentsline {subsubsection}{Logical semantics}{90}{section*.58}}
-\@writefile{toc}{\contentsline {subsubsection}{Other collection monads, other logics}{90}{section*.59}}
-\@writefile{toc}{\contentsline {paragraph}{Stateful collections}{90}{section*.60}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {10.3.1}Other logical operations}{91}{subsection.10.3.1}}
-\@writefile{toc}{\contentsline {section}{\numberline {10.4}Searching for programs}{91}{section.10.4}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {10.4.1}A new foundation for search}{91}{subsection.10.4.1}}
-\@writefile{toc}{\contentsline {subsubsection}{Monad composition via distributive laws}{91}{section*.61}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {10.4.2}Examples}{91}{subsection.10.4.2}}
+\@writefile{toc}{\contentsline {section}{\numberline {10.1}Referential transparency}{83}{section.10.1}}
+\@writefile{lof}{\contentsline {figure}{\numberline {10.1}{\ignorespaces Chapter map }}{84}{figure.10.1}}
+\@writefile{toc}{\contentsline {paragraph}{A little motivation}{84}{section*.56}}
+\@writefile{toc}{\contentsline {section}{\numberline {10.2}Composing monads}{85}{section.10.2}}
+\@writefile{toc}{\contentsline {subsubsection}{Preliminary}{86}{section*.57}}
+\@writefile{toc}{\contentsline {section}{\numberline {10.3}Semantic application queries}{87}{section.10.3}}
+\@writefile{toc}{\contentsline {subsubsection}{An alternative presentation}{87}{section*.58}}
+\@writefile{toc}{\contentsline {paragraph}{Logic: the set monad as an algebra}{88}{section*.59}}
+\@writefile{toc}{\contentsline {paragraph}{Primes: an application}{89}{section*.60}}
+\@writefile{toc}{\contentsline {paragraph}{Summary}{89}{section*.61}}
+\@writefile{toc}{\contentsline {subsubsection}{Patterns}{90}{section*.62}}
+\@writefile{toc}{\contentsline {subsubsection}{A first mini-query language}{90}{section*.63}}
+\@writefile{toc}{\contentsline {subsubsection}{Iterating the design pattern}{90}{section*.64}}
+\@writefile{toc}{\contentsline {paragraph}{A spatial-behavioral-style logic for $\lambda $-calculus}{91}{section*.65}}
+\@writefile{toc}{\contentsline {paragraph}{Examples}{91}{section*.66}}
+\@writefile{toc}{\contentsline {subsubsection}{Logical semantics}{92}{section*.67}}
+\@writefile{toc}{\contentsline {subsubsection}{Other collection monads, other logics}{92}{section*.68}}
+\@writefile{toc}{\contentsline {paragraph}{Stateful collections}{92}{section*.69}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {10.3.1}Other logical operations}{93}{subsection.10.3.1}}
+\@writefile{toc}{\contentsline {section}{\numberline {10.4}Searching for programs}{93}{section.10.4}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {10.4.1}A new foundation for search}{93}{subsection.10.4.1}}
+\@writefile{toc}{\contentsline {subsubsection}{Monad composition via distributive laws}{93}{section*.70}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {10.4.2}Examples}{93}{subsection.10.4.2}}
\@setckpt{chapters/ten/ch}{
-\setcounter{page}{92}
+\setcounter{page}{94}
\setcounter{equation}{0}
\setcounter{enumi}{0}
\setcounter{enumii}{0}
@@ -45,7 +45,7 @@
\setcounter{table}{0}
\setcounter{parentequation}{0}
\setcounter{Item}{0}
-\setcounter{Hfootnote}{12}
+\setcounter{Hfootnote}{13}
\setcounter{lstnumber}{1}
\setcounter{theorem}{0}
\setcounter{section@level}{2}
View
18 src/main/book/content/chapters/three/ch.aux
@@ -1,15 +1,15 @@
\relax
-\@writefile{toc}{\contentsline {chapter}{\numberline {3}An IO-monad for http streams}{51}{chapter.3}}
+\@writefile{toc}{\contentsline {chapter}{\numberline {3}An IO-monad for http streams}{37}{chapter.3}}
\@writefile{lof}{\addvspace {10\p@ }}
\@writefile{lot}{\addvspace {10\p@ }}
-\@writefile{toc}{\contentsline {section}{\numberline {3.1}Code first, questions later}{51}{section.3.1}}
-\@writefile{lof}{\contentsline {figure}{\numberline {3.1}{\ignorespaces Chapter map }}{52}{figure.3.1}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {3.1.1}An HTTP-request processor}{58}{subsection.3.1.1}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {3.1.2}What we did}{58}{subsection.3.1.2}}
-\@writefile{toc}{\contentsline {section}{\numberline {3.2}Synchrony, asynchrony and buffering}{58}{section.3.2}}
-\@writefile{toc}{\contentsline {section}{\numberline {3.3}State, statelessness and continuations}{58}{section.3.3}}
+\@writefile{toc}{\contentsline {section}{\numberline {3.1}Code first, questions later}{37}{section.3.1}}
+\@writefile{lof}{\contentsline {figure}{\numberline {3.1}{\ignorespaces Chapter map }}{38}{figure.3.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {3.1.1}An HTTP-request processor}{44}{subsection.3.1.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {3.1.2}What we did}{44}{subsection.3.1.2}}
+\@writefile{toc}{\contentsline {section}{\numberline {3.2}Synchrony, asynchrony and buffering}{44}{section.3.2}}
+\@writefile{toc}{\contentsline {section}{\numberline {3.3}State, statelessness and continuations}{44}{section.3.3}}
\@setckpt{chapters/three/ch}{
-\setcounter{page}{59}
+\setcounter{page}{45}
\setcounter{equation}{0}
\setcounter{enumi}{0}
\setcounter{enumii}{0}
@@ -28,7 +28,7 @@
\setcounter{table}{0}
\setcounter{parentequation}{0}
\setcounter{Item}{0}
-\setcounter{Hfootnote}{9}
+\setcounter{Hfootnote}{8}
\setcounter{lstnumber}{264}
\setcounter{theorem}{0}
\setcounter{section@level}{1}
View
56 src/main/book/content/chapters/two/ch.aux
@@ -1,33 +1,35 @@
\relax
-\@writefile{toc}{\contentsline {chapter}{\numberline {2}Toolbox}{35}{chapter.2}}
+\@writefile{toc}{\contentsline {chapter}{\numberline {2}Toolbox}{21}{chapter.2}}
\@writefile{lof}{\addvspace {10\p@ }}
\@writefile{lot}{\addvspace {10\p@ }}
-\@writefile{toc}{\contentsline {section}{\numberline {2.1}Introduction to notation and terminology}{35}{section.2.1}}
-\@writefile{toc}{\contentsline {section}{\numberline {2.2}Introduction to core design patterns}{35}{section.2.2}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {2.2.1}A little history}{35}{subsection.2.2.1}}
-\@writefile{toc}{\contentsline {paragraph}{Haskell's monad API}{36}{section*.24}}
-\@writefile{lol}{\contentsline {lstlisting}{\numberline {2.1}monad typeclass}{36}{lstlisting.2.1}}
-\@writefile{toc}{\contentsline {paragraph}{Do-notation}{36}{section*.25}}
-\@writefile{lol}{\contentsline {lstlisting}{\numberline {2.2}do-notation de-sugaring}{37}{lstlisting.2.2}}
-\@writefile{toc}{\contentsline {paragraph}{for-comprehensions}{37}{section*.26}}
-\@writefile{lol}{\contentsline {lstlisting}{\numberline {2.3}for-comprehension de-sugaring}{39}{lstlisting.2.3}}
-\@writefile{toc}{\contentsline {section}{\numberline {2.3}Variations in presentation}{40}{section.2.3}}
-\@writefile{toc}{\contentsline {subsection}{\numberline {2.3.1}A little more history}{40}{subsection.2.3.1}}
-\@writefile{toc}{\contentsline {subsubsection}{Intuition: Monad as container}{40}{section*.27}}
-\@writefile{toc}{\contentsline {paragraph}{Shape of the container}{40}{section*.28}}
-\@writefile{toc}{\contentsline {paragraph}{Putting things into the container}{40}{section*.29}}
-\@writefile{toc}{\contentsline {paragraph}{Flattening nested containers}{40}{section*.30}}
-\@writefile{toc}{\contentsline {subsubsection}{Preserving connection to existing structure: Monad as generalization of monoid}{41}{section*.31}}
-\@writefile{toc}{\contentsline {paragraph}{Associativity as flattening}{43}{section*.32}}
-\@writefile{toc}{\contentsline {paragraph}{Bracing for \texttt {XML}}{43}{section*.33}}
-\@writefile{toc}{\contentsline {paragraph}{The connection with set-comprehensions}{44}{section*.34}}
-\@writefile{toc}{\contentsline {paragraph}{Syntax and containers}{45}{section*.35}}
-\@writefile{toc}{\contentsline {subsubsection}{Decomposition of monad requirements}{45}{section*.36}}
-\@writefile{toc}{\contentsline {subsubsection}{A categorical way to look at monads}{46}{section*.37}}
-\@writefile{toc}{\contentsline {paragraph}{Quick digression about design by diagram-chasing}{47}{section*.38}}
-\@writefile{toc}{\contentsline {paragraph}{Monads are triples}{48}{section*.39}}
+\@writefile{toc}{\contentsline {section}{\numberline {2.1}Introduction to notation and terminology}{21}{section.2.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {2.1.1}Scala}{21}{subsection.2.1.1}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {2.1.2}Maths}{21}{subsection.2.1.2}}
+\@writefile{toc}{\contentsline {section}{\numberline {2.2}Introduction to core design patterns}{21}{section.2.2}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {2.2.1}A little history}{21}{subsection.2.2.1}}
+\@writefile{toc}{\contentsline {paragraph}{Haskell's monad API}{22}{section*.13}}
+\@writefile{lol}{\contentsline {lstlisting}{\numberline {2.1}monad typeclass}{22}{lstlisting.2.1}}
+\@writefile{toc}{\contentsline {paragraph}{Do-notation}{22}{section*.14}}
+\@writefile{lol}{\contentsline {lstlisting}{\numberline {2.2}do-notation de-sugaring}{23}{lstlisting.2.2}}
+\@writefile{toc}{\contentsline {paragraph}{for-comprehensions}{23}{section*.15}}
+\@writefile{lol}{\contentsline {lstlisting}{\numberline {2.3}for-comprehension de-sugaring}{25}{lstlisting.2.3}}
+\@writefile{toc}{\contentsline {section}{\numberline {2.3}Variations in presentation}{26}{section.2.3}}
+\@writefile{toc}{\contentsline {subsection}{\numberline {2.3.1}A little more history}{26}{subsection.2.3.1}}
+\@writefile{toc}{\contentsline {subsubsection}{Intuition: Monad as container}{26}{section*.16}}
+\@writefile{toc}{\contentsline {paragraph}{Shape of the container}{26}{section*.17}}
+\@writefile{toc}{\contentsline {paragraph}{Putting things into the container}{26}{section*.18}}
+\@writefile{toc}{\contentsline {paragraph}{Flattening nested containers}{26}{section*.19}}
+\@writefile{toc}{\contentsline {subsubsection}{Preserving connection to existing structure: Monad as generalization of monoid}{27}{section*.20}}
+\@writefile{toc}{\contentsline {paragraph}{Associativity as flattening}{29}{section*.21}}
+\@writefile{toc}{\contentsline {paragraph}{Bracing for \texttt {XML}}{29}{section*.22}}
+\@writefile{toc}{\contentsline {paragraph}{The connection with set-comprehensions}{30}{section*.23}}
+\@writefile{toc}{\contentsline {paragraph}{Syntax and containers}{31}{section*.24}}
+\@writefile{toc}{\contentsline {subsubsection}{Decomposition of monad requirements}{31}{section*.25}}
+\@writefile{toc}{\contentsline {subsubsection}{A categorical way to look at monads}{32}{section*.26}}
+\@writefile{toc}{\contentsline {paragraph}{Quick digression about design by diagram-chasing}{33}{section*.27}}
+\@writefile{toc}{\contentsline {paragraph}{Monads are triples}{34}{section*.28}}
\@setckpt{chapters/two/ch}{
-\setcounter{page}{51}
+\setcounter{page}{37}
\setcounter{equation}{0}
\setcounter{enumi}{0}
\setcounter{enumii}{0}
@@ -46,7 +48,7 @@
\setcounter{table}{0}
\setcounter{parentequation}{0}
\setcounter{Item}{0}
-\setcounter{Hfootnote}{9}
+\setcounter{Hfootnote}{8}
\setcounter{lstnumber}{1}
\setcounter{theorem}{0}
\setcounter{section@level}{4}
View
4 src/main/book/content/chapters/two/notation-and-terminology.tex
@@ -4,3 +4,7 @@ \section{Introduction to notation and terminology}
provide a more complete set of references for basic Scala notation, to
be somewhat self-contained in this section we review the notation and
terminology we will need for this book.
+
+\subsection{Scala}
+
+\subsection{Maths}
View
18 src/main/book/content/monadic.lof
@@ -2,21 +2,21 @@
\contentsline {figure}{\numberline {1.1}{\ignorespaces Example sign up page }}{14}{figure.1.1}
\contentsline {figure}{\numberline {1.2}{\ignorespaces Example REPL page }}{15}{figure.1.2}
\contentsline {figure}{\numberline {1.3}{\ignorespaces Example evaluation result page }}{16}{figure.1.3}
-\contentsline {figure}{\numberline {1.4}{\ignorespaces Chapter map }}{33}{figure.1.4}
+\contentsline {figure}{\numberline {1.4}{\ignorespaces Chapter map }}{19}{figure.1.4}
\addvspace {10\p@ }
\addvspace {10\p@ }
-\contentsline {figure}{\numberline {3.1}{\ignorespaces Chapter map }}{52}{figure.3.1}
+\contentsline {figure}{\numberline {3.1}{\ignorespaces Chapter map }}{38}{figure.3.1}
\addvspace {10\p@ }
-\contentsline {figure}{\numberline {4.1}{\ignorespaces Chapter map }}{60}{figure.4.1}
+\contentsline {figure}{\numberline {4.1}{\ignorespaces Chapter map }}{46}{figure.4.1}
\addvspace {10\p@ }
-\contentsline {figure}{\numberline {5.1}{\ignorespaces Chapter map }}{64}{figure.5.1}
+\contentsline {figure}{\numberline {5.1}{\ignorespaces Chapter map }}{50}{figure.5.1}
\addvspace {10\p@ }
-\contentsline {figure}{\numberline {6.1}{\ignorespaces Chapter map }}{66}{figure.6.1}
+\contentsline {figure}{\numberline {6.1}{\ignorespaces Chapter map }}{68}{figure.6.1}
\addvspace {10\p@ }
-\contentsline {figure}{\numberline {7.1}{\ignorespaces Chapter map }}{74}{figure.7.1}
+\contentsline {figure}{\numberline {7.1}{\ignorespaces Chapter map }}{76}{figure.7.1}
\addvspace {10\p@ }
-\contentsline {figure}{\numberline {8.1}{\ignorespaces Chapter map }}{78}{figure.8.1}
+\contentsline {figure}{\numberline {8.1}{\ignorespaces Chapter map }}{80}{figure.8.1}
\addvspace {10\p@ }
-\contentsline {figure}{\numberline {9.1}{\ignorespaces Chapter map }}{80}{figure.9.1}
+\contentsline {figure}{\numberline {9.1}{\ignorespaces Chapter map }}{82}{figure.9.1}
\addvspace {10\p@ }
-\contentsline {figure}{\numberline {10.1}{\ignorespaces Chapter map }}{82}{figure.10.1}
+\contentsline {figure}{\numberline {10.1}{\ignorespaces Chapter map }}{84}{figure.10.1}
View
339 src/main/book/content/monadic.log
@@ -1,4 +1,4 @@
-This is pdfeTeX, Version 3.141592-1.21a-2.2 (Web2C 7.5.4) (format=pdflatex 2008.11.17) 13 MAR 2010 05:27
+This is pdfeTeX, Version 3.141592-1.21a-2.2 (Web2C 7.5.4) (format=pdflatex 2008.11.17) 14 MAR 2010 00:58
entering extended mode
**monadic.tex
(./monadic.tex
@@ -440,18 +440,15 @@ Package hyperref Warning: No destination for bookmark of \addcontentsline,
s been already used, duplicate ignored
<to be read again>
\penalty
-l.54 ... IO-monad for http streams}{51}{chapter.3}
+l.31 ...little more history}{26}{subsection.2.3.1}
[1
-] [2]
-Underfull \vbox (badness 1394) has occurred while \output is active []
-
- [3])
+] [2] [3])
\tf@toc=\write6
\openout6 = `monadic.toc'.
-
-[4] (./monadic.lof)
+ [4]
+(./monadic.lof)
\tf@lof=\write7
\openout7 = `monadic.lof'.
@@ -537,7 +534,7 @@ LaTeX Font Info: Font shape `OMS/cmr/m/n' in size <12> not available
) (./chapters/one/where-are-we-going.tex [9] [10] [11] [12])
(./chapters/one/how-are-we-going-to-get-there.tex
</Users/lgm/work/src/projex/biosimilarity/trace/src/main/book/content/figures/R
-LambdaSignupPageScreenShot.pdf, id=633, 1353.055pt x 881.2925pt>
+LambdaSignupPageScreenShot.pdf, id=678, 1353.055pt x 881.2925pt>
File: /Users/lgm/work/src/projex/biosimilarity/trace/src/main/book/content/figu
res/RLambdaSignupPageScreenShot.pdf Graphic file (type pdf)
@@ -550,7 +547,7 @@ Overfull \hbox (46.785pt too wide) in paragraph at lines 26--27
[13] [14 </Users/lgm/work/src/projex/biosimilarity/trace/src/main/book/content/
figures/RLambdaSignupPageScreenShot.pdf>]
</Users/lgm/work/src/projex/biosimilarity/trace/src/main/book/content/figures/R
-LambdaREPLPageScreenShot.pdf, id=651, 1353.055pt x 881.2925pt>
+LambdaREPLPageScreenShot.pdf, id=696, 1353.055pt x 881.2925pt>
File: /Users/lgm/work/src/projex/biosimilarity/trace/src/main/book/content/figu
res/RLambdaREPLPageScreenShot.pdf Graphic file (type pdf)
@@ -562,7 +559,7 @@ Overfull \hbox (46.785pt too wide) in paragraph at lines 51--52
</Users/lgm/work/src/projex/biosimilarity/trace/src/main/book/content/figures/R
-LambdaSampleEvaluationResultPage.pdf, id=652, 1353.055pt x 881.2925pt>
+LambdaSampleEvaluationResultPage.pdf, id=697, 1353.055pt x 881.2925pt>
File: /Users/lgm/work/src/projex/biosimilarity/trace/src/main/book/content/figu
res/RLambdaSampleEvaluationResultPage.pdf Graphic file (type pdf)
@@ -578,139 +575,67 @@ Underfull \vbox (badness 10000) has occurred while \output is active []
[15 </Users/lgm/work/src/projex/biosimilarity/trace/src/main/book/content/figu
res/RLambdaREPLPageScreenShot.pdf>] [16 </Users/lgm/work/src/projex/biosimilari
ty/trace/src/main/book/content/figures/RLambdaSampleEvaluationResultPage.pdf>]
-Underfull \vbox (badness 10000) has occurred while \output is active []
-
- [17]
-[18]
-Overfull \hbox (3.25792pt too wide) in paragraph at lines 189--190
-[][][][][][][][][][][][][][][][][][][][][][][][][]
- []
-
-[19]
-LaTeX Font Info: Try loading font information for OMS+cmtt on input line 254
+LaTeX Font Info: Try loading font information for OMS+cmtt on input line 114
.
-LaTeX Font Info: No file OMScmtt.fd. on input line 254.
+LaTeX Font Info: No file OMScmtt.fd. on input line 114.
LaTeX Font Warning: Font shape `OMS/cmtt/m/n' undefined
(Font) using `OMS/cmsy/m/n' instead
-(Font) for symbol `textbraceleft' on input line 254.
-
-[20]
-Package hyperref Info: bookmark level for unknown lstlisting defaults to 0 on i
-nput line 303.
-LaTeX Font Info: Try loading font information for OML+cmr on input line 305.
-
- (/opt/local/share/texmf-dist/tex/latex/base/omlcmr.fd
-File: omlcmr.fd 1999/05/25 v2.5h Standard LaTeX font definitions
-)
-LaTeX Font Info: Font shape `OML/cmr/bx/n' in size <12> not available
-(Font) Font shape `OML/cmm/b/it' tried instead on input line 305.
- [21]
-Overfull \hbox (59.65782pt too wide) in paragraph at lines 346--347
-[][][][][][][][][][][][][][][][][][][][][][]
- []
-
+(Font) for symbol `textbraceleft' on input line 114.
-Underfull \vbox (badness 10000) has occurred while \output is active []
-
- [22]
-[23]
-Overfull \hbox (3.25792pt too wide) in paragraph at lines 439--440
-[][][][][][][][][][][][][][][][][][][][][][][][][][][]
- []
-
-[24]
-Underfull \vbox (badness 10000) has occurred while \output is active []
-
- [25]
-Overfull \hbox (3.25792pt too wide) in paragraph at lines 514--515
-[][][][][][][][][][][][][][][][][][][][][][][][][][][][]
- []
-
-
-Underfull \vbox (badness 10000) has occurred while \output is active []
-
- [26]
-Overfull \hbox (24.40788pt too wide) in paragraph at lines 536--537
-[][][][][][][][][][][][][][][][][][][][][][][]
- []
-
-
-Overfull \hbox (59.65782pt too wide) in paragraph at lines 541--542
-[][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][]
- []
-
-[27] [28]
-Overfull \hbox (10.3079pt too wide) in paragraph at lines 644--645
-[][][][][][][][][][][][][][][][][][][][][][][][][][][][][][]
- []
-
-
-Overfull \hbox (17.3579pt too wide) in paragraph at lines 660--661
-[][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][][]
- []
-
-
-Underfull \vbox (badness 10000) has occurred while \output is active []
-
- [29]
-Overfull \hbox (3.25792pt too wide) in paragraph at lines 674--675
-[][][][][][][][][][][][][][][][][][][][][]
- []
-
-
-Overfull \hbox (24.40788pt too wide) in paragraph at lines 680--681
-[][][][][][][][][][][][][][][][][][]
- []
-
-
-Overfull \hbox (45.55785pt too wide) in paragraph at lines 684--685
-[][][][][][][][][][][][][][][][][][][][][][][][]
- []
-
-[30] [31]
+[17]
</Users/lgm/work/src/projex/biosimilarity/trace/src/main/book/content/figures/M
-onadicDesignPatternsChapterMap2.pdf, id=1076, 748.7975pt x 582.175pt>
+onadicDesignPatternsChapterMap2.pdf, id=743, 748.7975pt x 582.175pt>
File: /Users/lgm/work/src/projex/biosimilarity/trace/src/main/book/content/figu
res/MonadicDesignPatternsChapterMap2.pdf Graphic file (type pdf)
<use /Users/lgm/work/src/projex/biosimilarity/trace/src/main/book/content/figur
es/MonadicDesignPatternsChapterMap2.pdf>
-Overfull \hbox (59.92126pt too wide) in paragraph at lines 785--786
+Overfull \hbox (59.92126pt too wide) in paragraph at lines 158--159
[]
[]
-) [32] [33 </Users/lgm/work/src/projex/biosimilarity/trace/src/main/book/conten
+) [18] [19 </Users/lgm/work/src/projex/biosimilarity/trace/src/main/book/conten
t/figures/MonadicDesignPatternsChapterMap2.pdf>])
\openout2 = `chapters/two/ch.aux'.
(./chapters/two/ch.tex
-[34
+[20
]
Chapter 2.
(./chapters/two/toolbox.tex) (./chapters/two/notation-and-terminology.tex)
-(./chapters/two/core-design-patterns.tex [35]
+(./chapters/two/core-design-patterns.tex [21]
+LaTeX Font Info: Try loading font information for OML+cmr on input line 26.
+
+(/opt/local/share/texmf-dist/tex/latex/base/omlcmr.fd
+File: omlcmr.fd 1999/05/25 v2.5h Standard LaTeX font definitions
+)
LaTeX Font Info: Font shape `OML/cmr/m/n' in size <12> not available
(Font) Font shape `OML/cmm/m/it' tried instead on input line 26.
- [36] [37]
+Package hyperref Info: bookmark level for unknown lstlisting defaults to 0 on i
+nput line 36.
+ [22] [23]
+LaTeX Font Info: Font shape `OML/cmr/bx/n' in size <12> not available
+(Font) Font shape `OML/cmm/b/it' tried instead on input line 118.
+
Underfull \vbox (badness 10000) has occurred while \output is active []
- [38])
-(./chapters/two/variation-in-presentation.tex [39] [40] [41] [42]
+ [24])
+(./chapters/two/variation-in-presentation.tex [25] [