Ur/Web: doc/manual.tex comparison

comparison doc/manual.tex @ 558:390cba747188

Proofreading pass

author	Adam Chlipala <adamc@hcoop.net>
date	Tue, 09 Dec 2008 14:06:51 -0500
parents	0d3db8d6a586
children	5d494183ca89

comparison

equal deleted inserted replaced

-:0d3db8d6a586
+:390cba747188
 To compile project \texttt{P.urp}, simply run
 \begin{verbatim}
 urweb P
 \end{verbatim}
+The output executable is a standalone web server.  Run it with the command-line argument \texttt{-h} to see which options it takes.  If the project file lists a database, the web server will attempt to connect to that database on startup.
 To time how long the different compiler phases run, without generating an executable, run
 \begin{verbatim}
 urweb -timing P
 \end{verbatim}
 \end{array}$$
 Ur supports several different notions of functions that take types as arguments.  These arguments can be either implicit, causing them to be inferred at use sites; or explicit, forcing them to be specified manually at use sites.  There is a common explicitness annotation convention applied at the definitions of and in the types of such functions.
 $$\begin{array}{rrcll}
 \textrm{Explicitness} & ? &::=& :: & \textrm{explicit} \\
-&&& \; ::: & \textrm{implicit}
+&&& ::: & \textrm{implicit}
 \end{array}$$
 \emph{Constructors} are the main class of compile-time-only data.  They include proper types and are classified by kinds.
 $$\begin{array}{rrcll}
 \textrm{Constructors} & c, \tau &::=& (c) :: \kappa & \textrm{kind annotation} \\
 \\
 &&& [(c = c)^*] & \textrm{known-length type-level record} \\
 &&& c \rc c & \textrm{type-level record concatenation} \\
 &&& \mt{fold} & \textrm{type-level record fold} \\
 \\
-&&& (c^+) & \textrm{type-level tuple} \\
+&&& (c,^+) & \textrm{type-level tuple} \\
 &&& c.n & \textrm{type-level tuple projection ($n \in \mathbb N^+$)} \\
 \\
 &&& \lambda [c \sim c] \Rightarrow c & \textrm{guarded constructor} \\
 \\
 &&& \_ :: \kappa & \textrm{wildcard} \\
 \subsection{Record Disjointness}
 We will use a keyword $\mt{map}$ as a shorthand, such that, for $f$ of kind $\kappa \to \kappa'$, $\mt{map} \; f$ stands for $\mt{fold} \; (\lambda (x_1 :: \mt{Name}) (x_2 :: \kappa) (x_3 :: \{\kappa'\}) \Rightarrow [x_1 = f \; x_2] \rc x_3) \; []$.
 $$\infer{\Gamma \vdash c_1 \sim c_2}{
-\Gamma \vdash c_1 \hookrightarrow c'_1
+\Gamma \vdash c_1 \hookrightarrow C_1
-& \Gamma \vdash c_2 \hookrightarrow c'_2
+& \Gamma \vdash c_2 \hookrightarrow C_2
-& \forall c''_1 \in c'_1, c''_2 \in c'_2: \Gamma \vdash c''_1 \sim c''_2
+& \forall c'_1 \in C_1, c'_2 \in C_2: \Gamma \vdash c'_1 \sim c'_2
 }
 \quad \infer{\Gamma \vdash X \sim X'}{
 X \neq X'
 }$$
 $$\infer{\Gamma \vdash c_1 \sim c_2}{
 c'_1 \sim c'_2 \in \Gamma
-& \Gamma \vdash c'_1 \hookrightarrow c''_1
+& \Gamma \vdash c'_1 \hookrightarrow C_1
-& \Gamma \vdash c'_2 \hookrightarrow c''_2
+& \Gamma \vdash c'_2 \hookrightarrow C_2
-& c_1 \in c''_1
+& c_1 \in C_1
-& c_2 \in c''_2
+& c_2 \in C_2
 }$$
 $$\infer{\Gamma \vdash c \hookrightarrow \{c\}}{}
 \quad \infer{\Gamma \vdash [\overline{c = c'}] \hookrightarrow \{\overline{c}\}}{}
 \quad \infer{\Gamma \vdash c_1 \rc c_2 \hookrightarrow C_1 \cup C_2}{
 We use an auxiliary judgment $\overline{y}; x; \Gamma \vdash \overline{dc} \leadsto \Gamma'$, expressing the enrichment of $\Gamma$ with the types of the datatype constructors $\overline{dc}$, when they are known to belong to datatype $x$ with type parameters $\overline{y}$.
 This is the first judgment where we deal with type classes, for the $\mt{class}$ declaration form.  We will omit their special handling in this formal specification.  Section \ref{typeclasses} gives an informal description of how type classes influence type inference.
-We presuppose the existence of a function $\mathcal O$, where $\mathcal(M, \overline{s})$ implements the $\mt{open}$ declaration by producing a context with the appropriate entry for each available component of module $M$ with signature items $\overline{s}$.  Where possible, $\mathcal O$ uses ``transparent'' entries (e.g., an abstract type $M.x$ is mapped to $x :: \mt{Type} = M.x$), so that the relationship with $M$ is maintained.  A related function $\mathcal O_c$ builds a context containing the disjointness constraints found in $S$.
+We presuppose the existence of a function $\mathcal O$, where $\mathcal O(M, \overline{s})$ implements the $\mt{open}$ declaration by producing a context with the appropriate entry for each available component of module $M$ with signature items $\overline{s}$.  Where possible, $\mathcal O$ uses ``transparent'' entries (e.g., an abstract type $M.x$ is mapped to $x :: \mt{Type} = M.x$), so that the relationship with $M$ is maintained.  A related function $\mathcal O_c$ builds a context containing the disjointness constraints found in $\overline s$.
 We write $\kappa_1^n \to \kappa$ as a shorthand, where $\kappa_1^0 \to \kappa = \kappa$ and $\kappa_1^{n+1} \to \kappa_2 = \kappa_1 \to (\kappa_1^n \to \kappa_2)$.  We write $\mt{len}(\overline{y})$ for the length of vector $\overline{y}$ of variables.
 $$\infer{\Gamma \vdash \cdot \leadsto \Gamma}{}
 \quad \infer{\Gamma \vdash d, \overline{d} \leadsto \Gamma''}{
 \Gamma \vdash d \leadsto \Gamma'
 & \textrm{$e_i$ starts with an expression $\lambda$, optionally preceded by constructor and disjointness $\lambda$s}
 }$$
 $$\infer{\Gamma \vdash \mt{structure} \; X : S = M \leadsto \Gamma, X : S}{
 \Gamma \vdash M : S
-& \textrm{ ($M$ not a $\mt{struct} \; \ldots \; \mt{end}$)}
+& \textrm{ $M$ not a constant or application}
 }
-\quad \infer{\Gamma \vdash \mt{structure} \; X : S = \mt{struct} \; \overline{d} \; \mt{end} \leadsto \Gamma, X : \mt{selfify}(X, \overline{s})}{
+\quad \infer{\Gamma \vdash \mt{structure} \; X : S = M \leadsto \Gamma, X : \mt{selfify}(X, \overline{s})}{
-\Gamma \vdash \mt{struct} \; \overline{d} \; \mt{end} : \mt{sig} \; \overline{s} \; \mt{end}
+\Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
 }$$
 $$\infer{\Gamma \vdash \mt{signature} \; X = S \leadsto \Gamma, X = S}{
 \Gamma \vdash S
 }$$
 }
 \quad \infer{\Gamma \vdash \mt{class} \; x \leadsto \Gamma, x :: \mt{Type} \to \mt{Type}}{}$$
 \subsection{Signature Compatibility}
-To simplify the judgments in this section, we assume that all signatures are alpha-varied as necessary to avoid including mmultiple bindings for the same identifier.  This is in addition to the usual alpha-variation of locally-bound variables.
+To simplify the judgments in this section, we assume that all signatures are alpha-varied as necessary to avoid including multiple bindings for the same identifier.  This is in addition to the usual alpha-variation of locally-bound variables.
 We rely on a judgment $\Gamma \vdash \overline{s} \leq s'$, which expresses the occurrence in signature items $\overline{s}$ of an item compatible with $s'$.  We also use a judgment $\Gamma \vdash \overline{dc} \leq \overline{dc}$, which expresses compatibility of datatype definitions.
 $$\infer{\Gamma \vdash S \equiv S}{}
 \quad \infer{\Gamma \vdash S_1 \equiv S_2}{
 & \Gamma, X : S'_1 \vdash S_2 \leq S'_2
 }$$
 $$\infer{\Gamma \vdash \mt{con} \; x :: \kappa \leq \mt{con} \; x :: \kappa}{}
 \quad \infer{\Gamma \vdash \mt{con} \; x :: \kappa = c \leq \mt{con} \; x :: \kappa}{}
-\quad \infer{\Gamma \vdash \mt{datatype} \; x \; \overline{y} = \overline{dc} \leq \mt{con} \; x :: \mt{Type}}{}$$
+\quad \infer{\Gamma \vdash \mt{datatype} \; x \; \overline{y} = \overline{dc} \leq \mt{con} \; x :: \mt{Type}^{\mt{len}(\overline y)} \to \mt{Type}}{}$$
 $$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leq \mt{con} \; x :: \mt{Type}^{\mt{len}(y)} \to \mt{Type}}{
 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
 & \mt{proj}(M, \overline{s}, \mt{datatype} \; z) = (\overline{y}, \overline{dc})
 }$$
 \mt{sigOf}(\mt{table} \; x : c) &=& \mt{table} \; x : c \\
 \mt{sigOf}(\mt{sequence} \; x) &=& \mt{sequence} \; x \\
 \mt{sigOf}(\mt{cookie} \; x : \tau) &=& \mt{cookie} \; x : \tau \\
 \mt{sigOf}(\mt{class} \; x = c) &=& \mt{class} \; x = c \\
 \end{eqnarray*}
 \begin{eqnarray*}
 \mt{selfify}(M, \cdot) &=& \cdot \\
-\mt{selfify}(M, s \; \overline{s'}) &=& \mt{selfify}(M, \sigma, s) \; \mt{selfify}(M, \overline{s'}) \\
+\mt{selfify}(M, s \; \overline{s'}) &=& \mt{selfify}(M, s) \; \mt{selfify}(M, \overline{s'}) \\
 \\
 \mt{selfify}(M, \mt{con} \; x :: \kappa) &=& \mt{con} \; x :: \kappa = M.x \\
 \mt{selfify}(M, \mt{con} \; x :: \kappa = c) &=& \mt{con} \; x :: \kappa = c \\
 \mt{selfify}(M, \mt{datatype} \; x \; \overline{y} = \overline{dc}) &=& \mt{datatype} \; x \; \overline{y} = \mt{datatype} \; M.x \\
 \mt{selfify}(M, \mt{datatype} \; x = \mt{datatype} \; M'.z) &=& \mt{datatype} \; x = \mt{datatype} \; M'.z \\
 \mt{proj}(M, \mt{datatype} \; x \; \overline{y} = \overline{dc} \; \overline{s}, \mt{val} \; X) &=& \overline{y ::: \mt{Type}} \to M.x \; \overline y \textrm{ (where $X \in \overline{dc}$)} \\
 \mt{proj}(M, \mt{datatype} \; x \; \overline{y} = \overline{dc} \; \overline{s}, \mt{val} \; X) &=& \overline{y ::: \mt{Type}} \to \tau \to M.x \; \overline y \textrm{ (where $X \; \mt{of} \; \tau \in \overline{dc}$)} \\
 \mt{proj}(M, \mt{datatype} \; x = \mt{datatype} \; M'.z, \mt{val} \; X) &=& \overline{y ::: \mt{Type}} \to M.x \; \overline y \textrm{ (where $\Gamma \vdash M' : \mt{sig} \; \overline{s'} \; \mt{end}$} \\
 && \textrm{and $\mt{proj}(M', \overline{s'}, \mt{datatype} \; z = (\overline{y}, \overline{dc})$ and $X \in \overline{dc}$)} \\
 \mt{proj}(M, \mt{datatype} \; x = \mt{datatype} \; M'.z, \mt{val} \; X) &=& \overline{y ::: \mt{Type}} \to \tau \to M.x \; \overline y \textrm{ (where $\Gamma \vdash M' : \mt{sig} \; \overline{s'} \; \mt{end}$} \\
-&& \textrm{and $\mt{proj}(M', \overline{s'}, \mt{datatype} \; z = (\overline{y}, \overline{dc})$ and $X : \tau \in \overline{dc}$)} \\
+&& \textrm{and $\mt{proj}(M', \overline{s'}, \mt{datatype} \; z = (\overline{y}, \overline{dc})$ and $X \; \mt{of} \; \tau \in \overline{dc}$)} \\
 \\
 \mt{proj}(M, \mt{structure} \; X : S \; \overline{s}, \mt{structure} \; X) &=& S \\
 \\
 \mt{proj}(M, \mt{signature} \; X = S \; \overline{s}, \mt{signature} \; X) &=& S \\
 \\
 $$\begin{array}{rrcll}
 \textrm{Projections} & P &::=& \ast & \textrm{all columns} \\
 &&& p,^+ & \textrm{particular columns} \\
 \textrm{Pre-projections} & p &::=& t.f & \textrm{one column from a table} \\
-&&& t.\{\{c\}\} & \textrm{a record of colums from a table (of kind $\{\mt{Type}\}$)} \\
+&&& t.\{\{c\}\} & \textrm{a record of columns from a table (of kind $\{\mt{Type}\}$)} \\
 \textrm{Table names} & t &::=& x & \textrm{constant table name (automatically capitalized)} \\
 &&& X & \textrm{constant table name} \\
 &&& \{\{c\}\} & \textrm{computed table name (of kind $\mt{Name}$)} \\
 \textrm{Column names} & f &::=& X & \textrm{constant column name} \\
 &&& \{c\} & \textrm{computed column name (of kind $\mt{Name}$)} \\
 When the standalone web server receives a request for a known page, it calls the function for that page, ``running'' the resulting transaction to produce the page to return to the client.  Pages link to other pages with the \texttt{link} attribute of the \texttt{a} HTML tag.  A link has type $\mt{transaction} \; \mt{page}$, and the semantics of a link are that this transaction should be run to compute the result page, when the link is followed.  Link targets are assigned URL names in the same way as top-level entry points.
 HTML forms are handled in a similar way.  The $\mt{action}$ attribute of a $\mt{submit}$ form tag takes a value of type $\$\mt{use} \to \mt{transaction} \; \mt{page}$, where $\mt{use}$ is a kind-$\{\mt{Type}\}$ record of the form fields used by this action handler.  Action handlers are assigned URL patterns in the same way as above.
-For both links and actions, direct arguments and local variables mentioned implicitly via closures are automatically included in serialized form in URLs, in the order in which they appeared in the source code.
+For both links and actions, direct arguments and local variables mentioned implicitly via closures are automatically included in serialized form in URLs, in the order in which they appear in the source code.
 \section{Compiler Phases}
 The Ur/Web compiler is unconventional in that it relies on a kind of \emph{heuristic compilation}.  Not all valid programs will compile successfully.  Informally, programs fail to compile when they are ``too higher order.''  Compiler phases do their best to eliminate different kinds of higher order-ness, but some programs just won't compile.  This is a trade-off for producing very efficient executables.  Compiled Ur/Web programs use native C representations and require no garbage collection.
 This phase specializes polymorphic functions to the specific arguments passed to them in the program.  If the program contains real polymorphic recursion, Unpoly will be insufficient to avoid later error messages about too much polymorphism.
 \subsection{Specialize}
-Replace uses of parametrized datatypes with versions specialized to specific parameters.  As for Unpoly, this phase will not be effective enough in the presence of polymorphic recursion or other fancy uses of impredicative polymorphism.
+Replace uses of parameterized datatypes with versions specialized to specific parameters.  As for Unpoly, this phase will not be effective enough in the presence of polymorphic recursion or other fancy uses of impredicative polymorphism.
 \subsection{Shake}
-Here the compiler repeats the earlier shake phase.
+Here the compiler repeats the earlier Shake phase.
 \subsection{Monoize}
 Programs are translated to a new intermediate language without polymorphism or non-$\mt{Type}$ constructors.  Error messages may pop up here if earlier phases failed to remove such features.

Mercurial > urweb

comparison doc/manual.tex @ 558:390cba747188