Ur/Web: doc/manual.tex comparison

comparison doc/manual.tex @ 784:990f80c1cec1

Revising manual through end of Section 6

author	Adam Chlipala <adamc@hcoop.net>
date	Tue, 05 May 2009 11:59:50 -0400
parents	ec0a0dd0ca12
children	fe63a08cbb91

comparison

equal deleted inserted replaced

-:ec0a0dd0ca12
+:990f80c1cec1
 \end{verbatim}
 \section{Ur Syntax}
-In this section, we describe the syntax of Ur, deferring to a later section discussion of most of the syntax specific to SQL and XML.  The sole exceptions are the declaration forms for tables, sequences, and cookies.
+In this section, we describe the syntax of Ur, deferring to a later section discussion of most of the syntax specific to SQL and XML.  The sole exceptions are the declaration forms for relations, cookies, and styles.
 \subsection{Lexical Conventions}
 We give the Ur language definition in \LaTeX $\;$ math mode, since that is prettier than monospaced ASCII.  The corresponding ASCII syntax can be read off directly.  Here is the key for mapping math symbols to ASCII character sequences.
 &&& \mt{signature} \; X = S & \textrm{signature definition} \\
 &&& \mt{open} \; M & \textrm{module inclusion} \\
 &&& \mt{constraint} \; c \sim c & \textrm{record disjointness constraint} \\
 &&& \mt{open} \; \mt{constraints} \; M & \textrm{inclusion of just the constraints from a module} \\
 &&& \mt{table} \; x : c & \textrm{SQL table} \\
+&&& \mt{view} \; x : c & \textrm{SQL view} \\
 &&& \mt{sequence} \; x & \textrm{SQL sequence} \\
 &&& \mt{cookie} \; x : \tau & \textrm{HTTP cookie} \\
+&&& \mt{style} \; x : \tau & \textrm{CSS class} \\
 &&& \mt{class} \; x :: \kappa = c & \textrm{concrete constructor class} \\
 \\
 \textrm{Modules} & M &::=& \mt{struct} \; d^* \; \mt{end} & \textrm{constant} \\
 &&& X & \textrm{variable} \\
 &&& M.X & \textrm{projection} \\
 &&& \mt{functor}(X : S) : S = M & \textrm{functor abstraction} \\
 \end{array}$$
 There are two kinds of Ur files.  A file named $M\texttt{.ur}$ is an \emph{implementation file}, and it should contain a sequence of declarations $d^*$.  A file named $M\texttt{.urs}$ is an \emph{interface file}; it must always have a matching $M\texttt{.ur}$ and should contain a sequence of signature items $s^*$.  When both files are present, the overall effect is the same as a monolithic declaration $\mt{structure} \; M : \mt{sig} \; s^* \; \mt{end} = \mt{struct} \; d^* \; \mt{end}$.  When no interface file is included, the overall effect is similar, with a signature for module $M$ being inferred rather than just checked against an interface.
+We omit some extra possibilities in $\mt{table}$ syntax, deferring them to Section \ref{tables}.
 \subsection{Shorthands}
 There are a variety of derived syntactic forms that elaborate into the core syntax from the last subsection.  We will present the additional forms roughly following the order in which we presented the constructs that they elaborate into.
 In many contexts where record fields are expected, like in a projection $e.c$, a constant field may be written as simply $X$, rather than $\#X$.
 The syntax $\mt{if} \; e \; \mt{then} \; e_1 \; \mt{else} \; e_2$ expands to $\mt{case} \; e \; \mt{of} \; \mt{Basis}.\mt{True} \Rightarrow e_1 \mid \mt{Basis}.\mt{False} \Rightarrow e_2$.
 There are infix operator syntaxes for a number of functions defined in the $\mt{Basis}$ module.  There is $=$ for $\mt{eq}$, $\neq$ for $\mt{neq}$, $-$ for $\mt{neg}$ (as a prefix operator) and $\mt{minus}$, $+$ for $\mt{plus}$, $\times$ for $\mt{times}$, $/$ for $\mt{div}$, $\%$ for $\mt{mod}$, $<$ for $\mt{lt}$, $\leq$ for $\mt{le}$, $>$ for $\mt{gt}$, and $\geq$ for $\mt{ge}$.
-A signature item $\mt{table} \; x : c$ is shorthand for $\mt{val} \; x : \mt{Basis}.\mt{sql\_table} \; c$.  $\mt{sequence} \; x$ is short for $\mt{val} \; x : \mt{Basis}.\mt{sql\_sequence}$, and $\mt{cookie} \; x : \tau$ is shorthand for $\mt{val} \; x : \mt{Basis}.\mt{http\_cookie} \; \tau$.
+A signature item $\mt{table} \; x : c$ is shorthand for $\mt{val} \; x : \mt{Basis}.\mt{sql\_table} \; c \; []$.  $\mt{view} \; x : c$ is shorthand for $\mt{val} \; x : \mt{Basis}.\mt{sql\_view} \; c$, $\mt{sequence} \; x$ is short for $\mt{val} \; x : \mt{Basis}.\mt{sql\_sequence}$.  $\mt{cookie} \; x : \tau$ is shorthand for $\mt{val} \; x : \mt{Basis}.\mt{http\_cookie} \; \tau$, and $\mt{style} \; x$ is shorthand for $\mt{val} \; x : \mt{Basis}.\mt{css\_class}$.
 \section{Static Semantics}
 In this section, we give a declarative presentation of Ur's typing rules and related judgments.  Inference is the subject of the next section; here, we assume that an oracle has filled in all wildcards with concrete values.
 }
 \quad \infer{\Gamma \vdash \mt{open} \; \mt{constraints} \; M \leadsto \Gamma, \mathcal O_c(M, \overline{s})}{
 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
 }$$
-$$\infer{\Gamma \vdash \mt{table} \; x : c \leadsto \Gamma, x : \mt{Basis}.\mt{sql\_table} \; c}{
+$$\infer{\Gamma \vdash \mt{table} \; x : c \leadsto \Gamma, x : \mt{Basis}.\mt{sql\_table} \; c \; []}{
 \Gamma \vdash c :: \{\mt{Type}\}
 }
-\quad \infer{\Gamma \vdash \mt{sequence} \; x \leadsto \Gamma, x : \mt{Basis}.\mt{sql\_sequence}}{}$$
+\quad \infer{\Gamma \vdash \mt{view} \; x : c \leadsto \Gamma, x : \mt{Basis}.\mt{sql\_view} \; c}{
+\Gamma \vdash c :: \{\mt{Type}\}
+}$$
+$$\infer{\Gamma \vdash \mt{sequence} \; x \leadsto \Gamma, x : \mt{Basis}.\mt{sql\_sequence}}{}$$
 $$\infer{\Gamma \vdash \mt{cookie} \; x : \tau \leadsto \Gamma, x : \mt{Basis}.\mt{http\_cookie} \; \tau}{
 \Gamma \vdash \tau :: \mt{Type}
-}$$
+}
+\quad \infer{\Gamma \vdash \mt{style} \; x \leadsto \Gamma, x : \mt{Basis}.\mt{css\_class}}{}$$
-$$\infer{\Gamma \vdash \mt{class} \; x :: \kappa = c \leadsto \Gamma, x :: \kappa \to \mt{Type} = c}{
-\Gamma \vdash c :: \kappa \to \mt{Type}
+$$\infer{\Gamma \vdash \mt{class} \; x :: \kappa = c \leadsto \Gamma, x :: \kappa = c}{
+\Gamma \vdash c :: \kappa
 }$$
 $$\infer{\overline{y}; x; \Gamma \vdash \cdot \leadsto \Gamma}{}
 \quad \infer{\overline{y}; x; \Gamma \vdash X \mid \overline{dc} \leadsto \Gamma', X : \overline{y ::: \mt{Type}} \to x \; \overline{y}}{
 \overline{y}; x; \Gamma \vdash \overline{dc} \leadsto \Gamma'
 $$\infer{\Gamma \vdash \mt{constraint} \; c_1 \sim c_2 \leadsto \Gamma, c_1 \sim c_2}{
 \Gamma \vdash c_1 :: \{\kappa\}
 & \Gamma \vdash c_2 :: \{\kappa\}
 }$$
-$$\infer{\Gamma \vdash \mt{class} \; x :: \kappa = c \leadsto \Gamma, x :: \kappa \to \mt{Type} = c}{
+$$\infer{\Gamma \vdash \mt{class} \; x :: \kappa = c \leadsto \Gamma, x :: \kappa = c}{
-\Gamma \vdash c :: \kappa \to \mt{Type}
+\Gamma \vdash c :: \kappa
 }
-\quad \infer{\Gamma \vdash \mt{class} \; x :: \kappa \leadsto \Gamma, x :: \kappa \to \mt{Type}}{}$$
+\quad \infer{\Gamma \vdash \mt{class} \; x :: \kappa \leadsto \Gamma, x :: \kappa}{}$$
 \subsection{Signature Compatibility}
 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.
 $$\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})
 }$$
-$$\infer{\Gamma \vdash \mt{class} \; x :: \kappa \leq \mt{con} \; x :: \kappa \to \mt{Type}}{}
+$$\infer{\Gamma \vdash \mt{class} \; x :: \kappa \leq \mt{con} \; x :: \kappa}{}
-\quad \infer{\Gamma \vdash \mt{class} \; x :: \kappa = c \leq \mt{con} \; x :: \kappa \to \mt{Type}}{}$$
+\quad \infer{\Gamma \vdash \mt{class} \; x :: \kappa = c \leq \mt{con} \; x :: \kappa}{}$$
 $$\infer{\Gamma \vdash \mt{con} \; x :: \kappa = c_1 \leq \mt{con} \; x :: \mt{\kappa} = c_2}{
 \Gamma \vdash c_1 \equiv c_2
 }
-\quad \infer{\Gamma \vdash \mt{class} \; x :: \kappa = c_1 \leq \mt{con} \; x :: \kappa \to \mt{Type} = c_2}{
+\quad \infer{\Gamma \vdash \mt{class} \; x :: \kappa = c_1 \leq \mt{con} \; x :: \kappa = c_2}{
 \Gamma \vdash c_1 \equiv c_2
 }$$
 $$\infer{\Gamma \vdash \mt{datatype} \; x \; \overline{y} = \overline{dc} \leq \mt{datatype} \; x \; \overline{y} = \overline{dc'}}{
 \Gamma, \overline{y :: \mt{Type}} \vdash \overline{dc} \leq \overline{dc'}
 \mt{sigOf}(\mt{signature} \; X = S) &=& \mt{signature} \; X = S \\
 \mt{sigOf}(\mt{open} \; M) &=& \mt{include} \; S \textrm{ (where $\Gamma \vdash M : S$)} \\
 \mt{sigOf}(\mt{constraint} \; c_1 \sim c_2) &=& \mt{constraint} \; c_1 \sim c_2 \\
 \mt{sigOf}(\mt{open} \; \mt{constraints} \; M) &=& \cdot \\
 \mt{sigOf}(\mt{table} \; x : c) &=& \mt{table} \; x : c \\
+\mt{sigOf}(\mt{view} \; x : c) &=& \mt{view} \; x : c \\
 \mt{sigOf}(\mt{sequence} \; x) &=& \mt{sequence} \; x \\
 \mt{sigOf}(\mt{cookie} \; x : \tau) &=& \mt{cookie} \; x : \tau \\
+\mt{sigOf}(\mt{style} \; x) &=& \mt{style} \; x \\
 \mt{sigOf}(\mt{class} \; x :: \kappa = c) &=& \mt{class} \; x :: \kappa = c \\
 \end{eqnarray*}
 \begin{eqnarray*}
 \mt{selfify}(M, \cdot) &=& \cdot \\
 \mt{selfify}(M, s \; \overline{s'}) &=& \mt{selfify}(M, s) \; \mt{selfify}(M, \overline{s'}) \\
 The type inference engine tries to take advantage of the algebraic rules governing type-level records, as shown in Section \ref{definitional}.  When two constructors of record kind are unified, they are reduced to normal forms, with like terms crossed off from each normal form until, hopefully, nothing remains.  This cannot be complete, with the inclusion of unification variables.  The type-checker can help you understand what goes wrong when the process fails, as it outputs the unmatched remainders of the two normal forms.
 \subsection{\label{typeclasses}Constructor Classes}
-Ur includes a constructor class facility inspired by Haskell's.  The current version is very rudimentary, only supporting instances for particular constructors built up from abstract constructors and datatypes and type-level application.
+Ur includes a constructor class facility inspired by Haskell's.  The current version is experimental, with very general Prolog-like facilities that can lead to compile-time non-termination.
-Constructor classes are integrated with the module system.  A constructor class of kind $\kappa$ is just a constructor of kind $\kappa \to \mt{Type}$.  By marking such a constructor $c$ as a constructor class, the programmer instructs the type inference engine to, in each scope, record all values of types $c \; c'$ as \emph{instances}.  Any function argument whose type is of such a form is treated as implicit, to be determined by examining the current instance database.
+Constructor classes are integrated with the module system.  A constructor class of kind $\kappa$ is just a constructor of kind $\kappa$.  By marking such a constructor $c$ as a constructor class, the programmer instructs the type inference engine to, in each scope, record all values of types $c \; c_1 \; \ldots \; c_n$ as \emph{instances}.  Any function argument whose type is of such a form is treated as implicit, to be determined by examining the current instance database.
 The ``dictionary encoding'' often used in Haskell implementations is made explicit in Ur.  Constructor class instances are just properly-typed values, and they can also be considered as ``proofs'' of membership in the class.  In some cases, it is useful to pass these proofs around explicitly.  An underscore written where a proof is expected will also be inferred, if possible, from the current instance database.
 Just as for constructors, constructors classes may be exported from modules, and they may be exported as concrete or abstract.  Concrete constructor classes have their ``real'' definitions exposed, so that client code may add new instances freely.  Abstract constructor classes are useful as ``predicates'' that can be used to enforce invariants, as we will see in some definitions of SQL syntax in the Ur/Web standard library.
 The fundamental unit of interest in the embedding of SQL is tables, described by a type family and creatable only via the $\mt{table}$ declaration form.
 $$\begin{array}{l}
 \mt{con} \; \mt{sql\_table} :: \{\mt{Type}\} \to \mt{Type}
 \end{array}$$
+\subsubsection{\label{tables}Tables}
 \subsubsection{Queries}
 A final query is constructed via the $\mt{sql\_query}$ function.  Constructor arguments respectively specify the table fields we select (as records mapping tables to the subsets of their fields that we choose) and the (always named) extra expressions that we select.
 $$\begin{array}{l}

Mercurial > urweb

comparison doc/manual.tex @ 784:990f80c1cec1