comparison doc/manual.tex @ 1400:c57414e39321

Updating documentation in preparation for a release
author Adam Chlipala <adam@chlipala.net>
date Sun, 16 Jan 2011 12:06:38 -0500
parents ede95ecb4000
children 860c245a7c4d
comparison
equal deleted inserted replaced
1399:898dc978c39d 1400:c57414e39321
74 To begin an interactive session with the Ur compiler modules, run \texttt{make smlnj}, and then, from within an \texttt{sml} session, run \texttt{CM.make "src/urweb.cm";}. The \texttt{Compiler} module is the main entry point. 74 To begin an interactive session with the Ur compiler modules, run \texttt{make smlnj}, and then, from within an \texttt{sml} session, run \texttt{CM.make "src/urweb.cm";}. The \texttt{Compiler} module is the main entry point.
75 75
76 To run an SQL-backed application with a backend besides SQLite, you will probably want to install one of these servers. 76 To run an SQL-backed application with a backend besides SQLite, you will probably want to install one of these servers.
77 77
78 \begin{verbatim} 78 \begin{verbatim}
79 apt-get install postgresql-8.3 mysql-server-5.0 79 apt-get install postgresql-8.4 mysql-server-5.1
80 \end{verbatim} 80 \end{verbatim}
81 81
82 To use the Emacs mode, you must have a modern Emacs installed. We assume that you already know how to do this, if you're in the business of looking for an Emacs mode. The demo generation facility of the compiler will also call out to Emacs to syntax-highlight code, and that process depends on the \texttt{htmlize} module, which can be installed in Debian testing via: 82 To use the Emacs mode, you must have a modern Emacs installed. We assume that you already know how to do this, if you're in the business of looking for an Emacs mode. The demo generation facility of the compiler will also call out to Emacs to syntax-highlight code, and that process depends on the \texttt{htmlize} module, which can be installed in Debian testing via:
83 83
84 \begin{verbatim} 84 \begin{verbatim}
133 For each entry \texttt{M} in the module list, the file \texttt{M.urs} is included in the project if it exists, and the file \texttt{M.ur} must exist and is always included. 133 For each entry \texttt{M} in the module list, the file \texttt{M.urs} is included in the project if it exists, and the file \texttt{M.ur} must exist and is always included.
134 134
135 Here is the complete list of directive forms. ``FFI'' stands for ``foreign function interface,'' Ur's facility for interaction between Ur programs and C and JavaScript libraries. 135 Here is the complete list of directive forms. ``FFI'' stands for ``foreign function interface,'' Ur's facility for interaction between Ur programs and C and JavaScript libraries.
136 \begin{itemize} 136 \begin{itemize}
137 \item \texttt{[allow|deny] [url|mime] PATTERN} registers a rule governing which URLs or MIME types are allowed in this application. The first such rule to match a URL or MIME type determines the verdict. If \texttt{PATTERN} ends in \texttt{*}, it is interpreted as a prefix rule. Otherwise, a string must match it exactly. 137 \item \texttt{[allow|deny] [url|mime] PATTERN} registers a rule governing which URLs or MIME types are allowed in this application. The first such rule to match a URL or MIME type determines the verdict. If \texttt{PATTERN} ends in \texttt{*}, it is interpreted as a prefix rule. Otherwise, a string must match it exactly.
138 \item \texttt{alwaysInline PATH} requests that every call to the referenced function be inlined. Section \ref{structure} explains how functions are assigned path strings.
138 \item \texttt{benignEffectful Module.ident} registers an FFI function or transaction as having side effects. The optimizer avoids removing, moving, or duplicating calls to such functions. Every effectful FFI function must be registered, or the optimizer may make invalid transformations. This version of the \texttt{effectful} directive registers that this function has only session-local side effects. 139 \item \texttt{benignEffectful Module.ident} registers an FFI function or transaction as having side effects. The optimizer avoids removing, moving, or duplicating calls to such functions. Every effectful FFI function must be registered, or the optimizer may make invalid transformations. This version of the \texttt{effectful} directive registers that this function has only session-local side effects.
139 \item \texttt{clientOnly Module.ident} registers an FFI function or transaction that may only be run in client browsers. 140 \item \texttt{clientOnly Module.ident} registers an FFI function or transaction that may only be run in client browsers.
140 \item \texttt{clientToServer Module.ident} adds FFI type \texttt{Module.ident} to the list of types that are OK to marshal from clients to servers. Values like XML trees and SQL queries are hard to marshal without introducing expensive validity checks, so it's easier to ensure that the server never trusts clients to send such values. The file \texttt{include/urweb.h} shows examples of the C support functions that are required of any type that may be marshalled. These include \texttt{attrify}, \texttt{urlify}, and \texttt{unurlify} functions. 141 \item \texttt{clientToServer Module.ident} adds FFI type \texttt{Module.ident} to the list of types that are OK to marshal from clients to servers. Values like XML trees and SQL queries are hard to marshal without introducing expensive validity checks, so it's easier to ensure that the server never trusts clients to send such values. The file \texttt{include/urweb.h} shows examples of the C support functions that are required of any type that may be marshalled. These include \texttt{attrify}, \texttt{urlify}, and \texttt{unurlify} functions.
141 \item \texttt{database DBSTRING} sets the string to pass to libpq to open a database connection. 142 \item \texttt{database DBSTRING} sets the string to pass to libpq to open a database connection.
142 \item \texttt{debug} saves some intermediate C files, which is mostly useful to help in debugging the compiler itself. 143 \item \texttt{debug} saves some intermediate C files, which is mostly useful to help in debugging the compiler itself.
1334 The Ur compiler treats $\mt{folder}$ like a constructor class, using built-in rules to infer $\mt{folder}$s for records with known structure. The order in which field names are mentioned in source code is used as a hint about the permutation that the programmer would like. 1335 The Ur compiler treats $\mt{folder}$ like a constructor class, using built-in rules to infer $\mt{folder}$s for records with known structure. The order in which field names are mentioned in source code is used as a hint about the permutation that the programmer would like.
1335 1336
1336 1337
1337 \section{The Ur/Web Standard Library} 1338 \section{The Ur/Web Standard Library}
1338 1339
1340 Some operations are only allowed in server-side code or only in client-side code. The type system does not enforce such restrictions, but the compiler enforces them in the process of whole-program compilation. In the discussion below, we note when a set of operations has a location restriction.
1341
1339 \subsection{Monads} 1342 \subsection{Monads}
1340 1343
1341 The Ur Basis defines the monad constructor class from Haskell. 1344 The Ur Basis defines the monad constructor class from Haskell.
1342 1345
1343 $$\begin{array}{l} 1346 $$\begin{array}{l}
1364 \mt{val} \; \mt{debug} : \mt{string} \to \mt{transaction} \; \mt{unit} 1367 \mt{val} \; \mt{debug} : \mt{string} \to \mt{transaction} \; \mt{unit}
1365 \end{array}$$ 1368 \end{array}$$
1366 1369
1367 \subsection{HTTP} 1370 \subsection{HTTP}
1368 1371
1369 There are transactions for reading an HTTP header by name and for getting and setting strongly-typed cookies. Cookies may only be created by the $\mt{cookie}$ declaration form, ensuring that they be named consistently based on module structure. 1372 There are transactions for reading an HTTP header by name and for getting and setting strongly-typed cookies. Cookies may only be created by the $\mt{cookie}$ declaration form, ensuring that they be named consistently based on module structure. For now, cookie operations are server-side only.
1370 $$\begin{array}{l} 1373 $$\begin{array}{l}
1371 \mt{val} \; \mt{requestHeader} : \mt{string} \to \mt{transaction} \; (\mt{option} \; \mt{string}) \\
1372 \\
1373 \mt{con} \; \mt{http\_cookie} :: \mt{Type} \to \mt{Type} \\ 1374 \mt{con} \; \mt{http\_cookie} :: \mt{Type} \to \mt{Type} \\
1374 \mt{val} \; \mt{getCookie} : \mt{t} ::: \mt{Type} \to \mt{http\_cookie} \; \mt{t} \to \mt{transaction} \; (\mt{option} \; \mt{t}) \\ 1375 \mt{val} \; \mt{getCookie} : \mt{t} ::: \mt{Type} \to \mt{http\_cookie} \; \mt{t} \to \mt{transaction} \; (\mt{option} \; \mt{t}) \\
1375 \mt{val} \; \mt{setCookie} : \mt{t} ::: \mt{Type} \to \mt{http\_cookie} \; \mt{t} \to \{\mt{Value} : \mt{t}, \mt{Expires} : \mt{option} \; \mt{time}, \mt{Secure} : \mt{bool}\} \to \mt{transaction} \; \mt{unit} \\ 1376 \mt{val} \; \mt{setCookie} : \mt{t} ::: \mt{Type} \to \mt{http\_cookie} \; \mt{t} \to \{\mt{Value} : \mt{t}, \mt{Expires} : \mt{option} \; \mt{time}, \mt{Secure} : \mt{bool}\} \to \mt{transaction} \; \mt{unit} \\
1376 \mt{val} \; \mt{clearCookie} : \mt{t} ::: \mt{Type} \to \mt{http\_cookie} \; \mt{t} \to \mt{transaction} \; \mt{unit} 1377 \mt{val} \; \mt{clearCookie} : \mt{t} ::: \mt{Type} \to \mt{http\_cookie} \; \mt{t} \to \mt{transaction} \; \mt{unit}
1377 \end{array}$$ 1378 \end{array}$$
1382 \mt{val} \; \mt{bless} : \mt{string} \to \mt{url} \\ 1383 \mt{val} \; \mt{bless} : \mt{string} \to \mt{url} \\
1383 \mt{val} \; \mt{checkUrl} : \mt{string} \to \mt{option} \; \mt{url} 1384 \mt{val} \; \mt{checkUrl} : \mt{string} \to \mt{option} \; \mt{url}
1384 \end{array}$$ 1385 \end{array}$$
1385 $\mt{bless}$ raises a runtime error if the string passed to it fails the URL policy. 1386 $\mt{bless}$ raises a runtime error if the string passed to it fails the URL policy.
1386 1387
1387 It is possible to grab the current page's URL or to build a URL for an arbitrary transaction that would also be an acceptable value of a \texttt{link} attribute of the \texttt{a} tag. 1388 It is possible to grab the current page's URL or to build a URL for an arbitrary transaction that would also be an acceptable value of a \texttt{link} attribute of the \texttt{a} tag. These are server-side operations.
1388 $$\begin{array}{l} 1389 $$\begin{array}{l}
1389 \mt{val} \; \mt{currentUrl} : \mt{transaction} \; \mt{url} \\ 1390 \mt{val} \; \mt{currentUrl} : \mt{transaction} \; \mt{url} \\
1390 \mt{val} \; \mt{url} : \mt{transaction} \; \mt{page} \to \mt{url} 1391 \mt{val} \; \mt{url} : \mt{transaction} \; \mt{page} \to \mt{url}
1391 \end{array}$$ 1392 \end{array}$$
1392 1393
1393 Page generation may be interrupted at any time with a request to redirect to a particular URL instead. 1394 Page generation may be interrupted at any time with a request to redirect to a particular URL instead.
1394 $$\begin{array}{l} 1395 $$\begin{array}{l}
1395 \mt{val} \; \mt{redirect} : \mt{t} ::: \mt{Type} \to \mt{url} \to \mt{transaction} \; \mt{t} 1396 \mt{val} \; \mt{redirect} : \mt{t} ::: \mt{Type} \to \mt{url} \to \mt{transaction} \; \mt{t}
1396 \end{array}$$ 1397 \end{array}$$
1397 1398
1398 It's possible for pages to return files of arbitrary MIME types. A file can be input from the user using this data type, along with the $\mt{upload}$ form tag. 1399 It's possible for pages to return files of arbitrary MIME types. A file can be input from the user using this data type, along with the $\mt{upload}$ form tag. These functions and those described in the following paragraph are server-side.
1399 $$\begin{array}{l} 1400 $$\begin{array}{l}
1400 \mt{type} \; \mt{file} \\ 1401 \mt{type} \; \mt{file} \\
1401 \mt{val} \; \mt{fileName} : \mt{file} \to \mt{option} \; \mt{string} \\ 1402 \mt{val} \; \mt{fileName} : \mt{file} \to \mt{option} \; \mt{string} \\
1402 \mt{val} \; \mt{fileMimeType} : \mt{file} \to \mt{string} \\ 1403 \mt{val} \; \mt{fileMimeType} : \mt{file} \to \mt{string} \\
1403 \mt{val} \; \mt{fileData} : \mt{file} \to \mt{blob} 1404 \mt{val} \; \mt{fileData} : \mt{file} \to \mt{blob}
1410 \mt{val} \; \mt{checkMime} : \mt{string} \to \mt{option} \; \mt{mimeType} \\ 1411 \mt{val} \; \mt{checkMime} : \mt{string} \to \mt{option} \; \mt{mimeType} \\
1411 \mt{val} \; \mt{returnBlob} : \mt{t} ::: \mt{Type} \to \mt{blob} \to \mt{mimeType} \to \mt{transaction} \; \mt{t} 1412 \mt{val} \; \mt{returnBlob} : \mt{t} ::: \mt{Type} \to \mt{blob} \to \mt{mimeType} \to \mt{transaction} \; \mt{t}
1412 \end{array}$$ 1413 \end{array}$$
1413 1414
1414 \subsection{SQL} 1415 \subsection{SQL}
1416
1417 Everything about SQL database access is restricted to server-side code.
1415 1418
1416 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. 1419 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.
1417 $$\begin{array}{l} 1420 $$\begin{array}{l}
1418 \mt{con} \; \mt{sql\_table} :: \{\mt{Type}\} \to \{\{\mt{Unit}\}\} \to \mt{Type} 1421 \mt{con} \; \mt{sql\_table} :: \{\mt{Type}\} \to \{\{\mt{Unit}\}\} \to \mt{Type}
1419 \end{array}$$ 1422 \end{array}$$
1519 Section \ref{tables} shows the expanded syntax of the $\mt{table}$ declaration and signature item that includes constraints. There is no other way to use constraints with SQL in Ur/Web. 1522 Section \ref{tables} shows the expanded syntax of the $\mt{table}$ declaration and signature item that includes constraints. There is no other way to use constraints with SQL in Ur/Web.
1520 1523
1521 1524
1522 \subsubsection{Queries} 1525 \subsubsection{Queries}
1523 1526
1524 A final query is constructed via the $\mt{sql\_query}$ function. Constructor arguments respectively specify the free table variables (which will only be available in subqueries), 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. 1527 A final query is constructed via the $\mt{sql\_query}$ function. Constructor arguments respectively specify the unrestricted free table variables (which will only be available in subqueries), the free table variables that may only be mentioned within arguments to aggregate functions, 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.
1525 $$\begin{array}{l} 1528 $$\begin{array}{l}
1526 \mt{con} \; \mt{sql\_query} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \\ 1529 \mt{con} \; \mt{sql\_query} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \\
1527 \mt{val} \; \mt{sql\_query} : \mt{free} ::: \{\{\mt{Type}\}\} \\ 1530 \mt{val} \; \mt{sql\_query} : \mt{free} ::: \{\{\mt{Type}\}\} \\
1531 \hspace{.1in} \to \mt{afree} ::: \{\{\mt{Type}\}\} \\
1528 \hspace{.1in} \to \mt{tables} ::: \{\{\mt{Type}\}\} \\ 1532 \hspace{.1in} \to \mt{tables} ::: \{\{\mt{Type}\}\} \\
1529 \hspace{.1in} \to \mt{selectedFields} ::: \{\{\mt{Type}\}\} \\ 1533 \hspace{.1in} \to \mt{selectedFields} ::: \{\{\mt{Type}\}\} \\
1530 \hspace{.1in} \to \mt{selectedExps} ::: \{\mt{Type}\} \\ 1534 \hspace{.1in} \to \mt{selectedExps} ::: \{\mt{Type}\} \\
1531 \hspace{.1in} \to [\mt{free} \sim \mt{tables}] \\ 1535 \hspace{.1in} \to [\mt{free} \sim \mt{tables}] \\
1532 \hspace{.1in} \Rightarrow \{\mt{Rows} : \mt{sql\_query1} \; \mt{free} \; \mt{tables} \; \mt{selectedFields} \; \mt{selectedExps}, \\ 1536 \hspace{.1in} \Rightarrow \{\mt{Rows} : \mt{sql\_query1} \; \mt{free} \; \mt{afree} \; \mt{tables} \; \mt{selectedFields} \; \mt{selectedExps}, \\
1533 \hspace{.2in} \mt{OrderBy} : \mt{sql\_order\_by} \; (\mt{free} \rc \mt{tables}) \; \mt{selectedExps}, \\ 1537 \hspace{.2in} \mt{OrderBy} : \mt{sql\_order\_by} \; (\mt{free} \rc \mt{tables}) \; \mt{selectedExps}, \\
1534 \hspace{.2in} \mt{Limit} : \mt{sql\_limit}, \\ 1538 \hspace{.2in} \mt{Limit} : \mt{sql\_limit}, \\
1535 \hspace{.2in} \mt{Offset} : \mt{sql\_offset}\} \\ 1539 \hspace{.2in} \mt{Offset} : \mt{sql\_offset}\} \\
1536 \hspace{.1in} \to \mt{sql\_query} \; \mt{free} \; \mt{selectedFields} \; \mt{selectedExps} 1540 \hspace{.1in} \to \mt{sql\_query} \; \mt{free} \; \mt{afree} \; \mt{selectedFields} \; \mt{selectedExps}
1537 \end{array}$$ 1541 \end{array}$$
1538 1542
1539 Queries are used by folding over their results inside transactions. 1543 Queries are used by folding over their results inside transactions.
1540 $$\begin{array}{l} 1544 $$\begin{array}{l}
1541 \mt{val} \; \mt{query} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to [\mt{tables} \sim \mt{exps}] \Rightarrow \mt{state} ::: \mt{Type} \to \mt{sql\_query} \; [] \; \mt{tables} \; \mt{exps} \\ 1545 \mt{val} \; \mt{query} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to [\mt{tables} \sim \mt{exps}] \Rightarrow \mt{state} ::: \mt{Type} \to \mt{sql\_query} \; [] \; [] \; \mt{tables} \; \mt{exps} \\
1542 \hspace{.1in} \to (\$(\mt{exps} \rc \mt{map} \; (\lambda \mt{fields} :: \{\mt{Type}\} \Rightarrow \$\mt{fields}) \; \mt{tables}) \\ 1546 \hspace{.1in} \to (\$(\mt{exps} \rc \mt{map} \; (\lambda \mt{fields} :: \{\mt{Type}\} \Rightarrow \$\mt{fields}) \; \mt{tables}) \\
1543 \hspace{.2in} \to \mt{state} \to \mt{transaction} \; \mt{state}) \\ 1547 \hspace{.2in} \to \mt{state} \to \mt{transaction} \; \mt{state}) \\
1544 \hspace{.1in} \to \mt{state} \to \mt{transaction} \; \mt{state} 1548 \hspace{.1in} \to \mt{state} \to \mt{transaction} \; \mt{state}
1545 \end{array}$$ 1549 \end{array}$$
1546 1550
1547 Most of the complexity of the query encoding is in the type $\mt{sql\_query1}$, which includes simple queries and derived queries based on relational operators. Constructor arguments respectively specify the free table veriables, the tables we select from, the subset of fields that we keep from each table for the result rows, and the extra expressions that we select. 1551 Most of the complexity of the query encoding is in the type $\mt{sql\_query1}$, which includes simple queries and derived queries based on relational operators. Constructor arguments respectively specify the unrestricted free table veriables, the aggregate-only free table variables, the tables we select from, the subset of fields that we keep from each table for the result rows, and the extra expressions that we select.
1548 $$\begin{array}{l} 1552 $$\begin{array}{l}
1549 \mt{con} \; \mt{sql\_query1} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \\ 1553 \mt{con} \; \mt{sql\_query1} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \\
1550 \\ 1554 \\
1551 \mt{type} \; \mt{sql\_relop} \\ 1555 \mt{type} \; \mt{sql\_relop} \\
1552 \mt{val} \; \mt{sql\_union} : \mt{sql\_relop} \\ 1556 \mt{val} \; \mt{sql\_union} : \mt{sql\_relop} \\
1553 \mt{val} \; \mt{sql\_intersect} : \mt{sql\_relop} \\ 1557 \mt{val} \; \mt{sql\_intersect} : \mt{sql\_relop} \\
1554 \mt{val} \; \mt{sql\_except} : \mt{sql\_relop} \\ 1558 \mt{val} \; \mt{sql\_except} : \mt{sql\_relop} \\
1555 \mt{val} \; \mt{sql\_relop} : \mt{tables1} ::: \{\{\mt{Type}\}\} \\ 1559 \mt{val} \; \mt{sql\_relop} : \mt{free} ::: \{\{\mt{Type}\}\} \\
1560 \hspace{.1in} \to \mt{afree} ::: \{\{\mt{Type}\}\} \\
1561 \hspace{.1in} \to \mt{tables1} ::: \{\{\mt{Type}\}\} \\
1556 \hspace{.1in} \to \mt{tables2} ::: \{\{\mt{Type}\}\} \\ 1562 \hspace{.1in} \to \mt{tables2} ::: \{\{\mt{Type}\}\} \\
1557 \hspace{.1in} \to \mt{selectedFields} ::: \{\{\mt{Type}\}\} \\ 1563 \hspace{.1in} \to \mt{selectedFields} ::: \{\{\mt{Type}\}\} \\
1558 \hspace{.1in} \to \mt{selectedExps} ::: \{\mt{Type}\} \\ 1564 \hspace{.1in} \to \mt{selectedExps} ::: \{\mt{Type}\} \\
1559 \hspace{.1in} \to \mt{sql\_relop} \\ 1565 \hspace{.1in} \to \mt{sql\_relop} \\
1560 \hspace{.1in} \to \mt{sql\_query1} \; \mt{tables1} \; \mt{selectedFields} \; \mt{selectedExps} \\ 1566 \hspace{.1in} \to \mt{sql\_query1} \; \mt{free} \; \mt{afree} \; \mt{tables1} \; \mt{selectedFields} \; \mt{selectedExps} \\
1561 \hspace{.1in} \to \mt{sql\_query1} \; \mt{tables2} \; \mt{selectedFields} \; \mt{selectedExps} \\ 1567 \hspace{.1in} \to \mt{sql\_query1} \; \mt{free} \; \mt{afree} \; \mt{tables2} \; \mt{selectedFields} \; \mt{selectedExps} \\
1562 \hspace{.1in} \to \mt{sql\_query1} \; \mt{selectedFields} \; \mt{selectedFields} \; \mt{selectedExps} 1568 \hspace{.1in} \to \mt{sql\_query1} \; \mt{free} \; \mt{afree} \; \mt{selectedFields} \; \mt{selectedFields} \; \mt{selectedExps}
1563 \end{array}$$ 1569 \end{array}$$
1564 1570
1565 $$\begin{array}{l} 1571 $$\begin{array}{l}
1566 \mt{val} \; \mt{sql\_query1} : \mt{free} ::: \{\{\mt{Type}\}\} \\ 1572 \mt{val} \; \mt{sql\_query1} : \mt{free} ::: \{\{\mt{Type}\}\} \\
1573 \hspace{.1in} \to \mt{afree} ::: \{\{\mt{Type}\}\} \\
1567 \hspace{.1in} \to \mt{tables} ::: \{\{\mt{Type}\}\} \\ 1574 \hspace{.1in} \to \mt{tables} ::: \{\{\mt{Type}\}\} \\
1568 \hspace{.1in} \to \mt{grouped} ::: \{\{\mt{Type}\}\} \\ 1575 \hspace{.1in} \to \mt{grouped} ::: \{\{\mt{Type}\}\} \\
1569 \hspace{.1in} \to \mt{selectedFields} ::: \{\{\mt{Type}\}\} \\ 1576 \hspace{.1in} \to \mt{selectedFields} ::: \{\{\mt{Type}\}\} \\
1570 \hspace{.1in} \to \mt{selectedExps} ::: \{\mt{Type}\} \\ 1577 \hspace{.1in} \to \mt{selectedExps} ::: \{\mt{Type}\} \\
1571 \hspace{.1in} \to \mt{empties} :: \{\mt{Unit}\} \\ 1578 \hspace{.1in} \to \mt{empties} :: \{\mt{Unit}\} \\
1572 \hspace{.1in} \to [\mt{free} \sim \mt{tables}] \\ 1579 \hspace{.1in} \to [\mt{free} \sim \mt{tables}] \\
1573 \hspace{.1in} \Rightarrow [\mt{free} \sim \mt{grouped}] \\ 1580 \hspace{.1in} \Rightarrow [\mt{free} \sim \mt{grouped}] \\
1581 \hspace{.1in} \Rightarrow [\mt{afree} \sim \mt{tables}] \\
1574 \hspace{.1in} \Rightarrow [\mt{empties} \sim \mt{selectedFields}] \\ 1582 \hspace{.1in} \Rightarrow [\mt{empties} \sim \mt{selectedFields}] \\
1575 \hspace{.1in} \Rightarrow \{\mt{Distinct} : \mt{bool}, \\ 1583 \hspace{.1in} \Rightarrow \{\mt{Distinct} : \mt{bool}, \\
1576 \hspace{.2in} \mt{From} : \mt{sql\_from\_items} \; \mt{free} \; \mt{tables}, \\ 1584 \hspace{.2in} \mt{From} : \mt{sql\_from\_items} \; \mt{free} \; \mt{tables}, \\
1577 \hspace{.2in} \mt{Where} : \mt{sql\_exp} \; (\mt{free} \rc \mt{tables}) \; [] \; [] \; \mt{bool}, \\ 1585 \hspace{.2in} \mt{Where} : \mt{sql\_exp} \; (\mt{free} \rc \mt{tables}) \; \mt{afree} \; [] \; \mt{bool}, \\
1578 \hspace{.2in} \mt{GroupBy} : \mt{sql\_subset} \; \mt{tables} \; \mt{grouped}, \\ 1586 \hspace{.2in} \mt{GroupBy} : \mt{sql\_subset} \; \mt{tables} \; \mt{grouped}, \\
1579 \hspace{.2in} \mt{Having} : \mt{sql\_exp} \; (\mt{free} \rc \mt{grouped}) \; \mt{tables} \; [] \; \mt{bool}, \\ 1587 \hspace{.2in} \mt{Having} : \mt{sql\_exp} \; (\mt{free} \rc \mt{grouped}) \; (\mt{afree} \rc \mt{tables}) \; [] \; \mt{bool}, \\
1580 \hspace{.2in} \mt{SelectFields} : \mt{sql\_subset} \; \mt{grouped} \; (\mt{map} \; (\lambda \_ \Rightarrow []) \; \mt{empties} \rc \mt{selectedFields}), \\ 1588 \hspace{.2in} \mt{SelectFields} : \mt{sql\_subset} \; \mt{grouped} \; (\mt{map} \; (\lambda \_ \Rightarrow []) \; \mt{empties} \rc \mt{selectedFields}), \\
1581 \hspace{.2in} \mt {SelectExps} : \$(\mt{map} \; (\mt{sql\_exp} \; (\mt{free} \rc \mt{grouped}) \; \mt{tables} \; []) \; \mt{selectedExps}) \} \\ 1589 \hspace{.2in} \mt {SelectExps} : \$(\mt{map} \; (\mt{sql\_exp} \; (\mt{free} \rc \mt{grouped}) \; (\mt{afree} \rc \mt{tables}) \; []) \; \mt{selectedExps}) \} \\
1582 \hspace{.1in} \to \mt{sql\_query1} \; \mt{free} \; \mt{tables} \; \mt{selectedFields} \; \mt{selectedExps} 1590 \hspace{.1in} \to \mt{sql\_query1} \; \mt{free} \; \mt{afree} \; \mt{tables} \; \mt{selectedFields} \; \mt{selectedExps}
1583 \end{array}$$ 1591 \end{array}$$
1584 1592
1585 To encode projection of subsets of fields in $\mt{SELECT}$ clauses, and to encode $\mt{GROUP} \; \mt{BY}$ clauses, we rely on a type family $\mt{sql\_subset}$, capturing what it means for one record of table fields to be a subset of another. The main constructor $\mt{sql\_subset}$ ``proves subset facts'' by requiring a split of a record into kept and dropped parts. The extra constructor $\mt{sql\_subset\_all}$ is a convenience for keeping all fields of a record. 1593 To encode projection of subsets of fields in $\mt{SELECT}$ clauses, and to encode $\mt{GROUP} \; \mt{BY}$ clauses, we rely on a type family $\mt{sql\_subset}$, capturing what it means for one record of table fields to be a subset of another. The main constructor $\mt{sql\_subset}$ ``proves subset facts'' by requiring a split of a record into kept and dropped parts. The extra constructor $\mt{sql\_subset\_all}$ is a convenience for keeping all fields of a record.
1586 $$\begin{array}{l} 1594 $$\begin{array}{l}
1587 \mt{con} \; \mt{sql\_subset} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \mt{Type} \\ 1595 \mt{con} \; \mt{sql\_subset} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \mt{Type} \\
1692 \end{array}$$ 1700 \end{array}$$
1693 1701
1694 $$\begin{array}{l} 1702 $$\begin{array}{l}
1695 \mt{val} \; \mt{sql\_count\_col} : \mt{t} ::: \mt{Type} \to \mt{sql\_aggregate} \; (\mt{option} \; \mt{t}) \; \mt{int} 1703 \mt{val} \; \mt{sql\_count\_col} : \mt{t} ::: \mt{Type} \to \mt{sql\_aggregate} \; (\mt{option} \; \mt{t}) \; \mt{int}
1696 \end{array}$$ 1704 \end{array}$$
1705
1706 Most aggregate functions are typed using a two-parameter constructor class $\mt{nullify}$ which maps $\mt{option}$ types to themselves and adds $\mt{option}$ to others. That is, this constructor class represents the process of making an SQL type ``nullable.''
1697 1707
1698 $$\begin{array}{l} 1708 $$\begin{array}{l}
1699 \mt{class} \; \mt{sql\_summable} \\ 1709 \mt{class} \; \mt{sql\_summable} \\
1700 \mt{val} \; \mt{sql\_summable\_int} : \mt{sql\_summable} \; \mt{int} \\ 1710 \mt{val} \; \mt{sql\_summable\_int} : \mt{sql\_summable} \; \mt{int} \\
1701 \mt{val} \; \mt{sql\_summable\_float} : \mt{sql\_summable} \; \mt{float} \\ 1711 \mt{val} \; \mt{sql\_summable\_float} : \mt{sql\_summable} \; \mt{float} \\
1702 \mt{val} \; \mt{sql\_avg} : \mt{t} ::: \mt{Type} \to \mt{sql\_summable} \; \mt{t} \to \mt{sql\_aggregate} \; \mt{t} \; \mt{t} \\ 1712 \mt{val} \; \mt{sql\_avg} : \mt{t} ::: \mt{Type} \to \mt{nt} ::: \mt{Type} \to \mt{sql\_summable} \; \mt{t} \to \mt{nullify} \; \mt{t} \; \mt{nt} \to \mt{sql\_aggregate} \; \mt{t} \; \mt{nt} \\
1703 \mt{val} \; \mt{sql\_sum} : \mt{t} ::: \mt{Type} \to \mt{sql\_summable} \mt{t} \to \mt{sql\_aggregate} \; \mt{t} \; \mt{t} 1713 \mt{val} \; \mt{sql\_sum} : \mt{t} ::: \mt{Type} \to \mt{nt} ::: \mt{Type} \to \mt{sql\_summable} \; \mt{t} \to \mt{nullify} \; \mt{t} \; \mt{nt} \to \mt{sql\_aggregate} \; \mt{t} \; \mt{nt}
1704 \end{array}$$ 1714 \end{array}$$
1705 1715
1706 $$\begin{array}{l} 1716 $$\begin{array}{l}
1707 \mt{class} \; \mt{sql\_maxable} \\ 1717 \mt{class} \; \mt{sql\_maxable} \\
1708 \mt{val} \; \mt{sql\_maxable\_int} : \mt{sql\_maxable} \; \mt{int} \\ 1718 \mt{val} \; \mt{sql\_maxable\_int} : \mt{sql\_maxable} \; \mt{int} \\
1709 \mt{val} \; \mt{sql\_maxable\_float} : \mt{sql\_maxable} \; \mt{float} \\ 1719 \mt{val} \; \mt{sql\_maxable\_float} : \mt{sql\_maxable} \; \mt{float} \\
1710 \mt{val} \; \mt{sql\_maxable\_string} : \mt{sql\_maxable} \; \mt{string} \\ 1720 \mt{val} \; \mt{sql\_maxable\_string} : \mt{sql\_maxable} \; \mt{string} \\
1711 \mt{val} \; \mt{sql\_maxable\_time} : \mt{sql\_maxable} \; \mt{time} \\ 1721 \mt{val} \; \mt{sql\_maxable\_time} : \mt{sql\_maxable} \; \mt{time} \\
1712 \mt{val} \; \mt{sql\_max} : \mt{t} ::: \mt{Type} \to \mt{sql\_maxable} \; \mt{t} \to \mt{sql\_aggregate} \; \mt{t} \; \mt{t} \\ 1722 \mt{val} \; \mt{sql\_max} : \mt{t} ::: \mt{Type} \to \mt{nt} ::: \mt{Type} \to \mt{sql\_maxable} \; \mt{t} \to \mt{nullify} \; \mt{t} \; \mt{nt} \to \mt{sql\_aggregate} \; \mt{t} \; \mt{nt} \\
1713 \mt{val} \; \mt{sql\_min} : \mt{t} ::: \mt{Type} \to \mt{sql\_maxable} \; \mt{t} \to \mt{sql\_aggregate} \; \mt{t} \; \mt{t} 1723 \mt{val} \; \mt{sql\_min} : \mt{t} ::: \mt{Type} \to \mt{nt} ::: \mt{Type} \to \mt{sql\_maxable} \; \mt{t} \to \mt{nullify} \; \mt{t} \; \mt{nt} \to \mt{sql\_aggregate} \; \mt{t} \; \mt{nt}
1714 \end{array}$$ 1724 \end{array}$$
1715 1725
1716 Any SQL query that returns single columns may be turned into a subquery expression. 1726 Any SQL query that returns single columns may be turned into a subquery expression.
1717 1727
1718 $$\begin{array}{l} 1728 $$\begin{array}{l}
1719 \mt{val} \; \mt{sql\_subquery} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{nm} ::: \mt{Name} \to \mt{t} ::: \mt{Type} \\ 1729 \mt{val} \; \mt{sql\_subquery} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{nm} ::: \mt{Name} \to \mt{t} ::: \mt{Type} \\
1720 \hspace{.1in} \to \mt{sql\_query} \; \mt{tables} \; [] \; [\mt{nm} = \mt{t}] \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} 1730 \hspace{.1in} \to \mt{sql\_query} \; \mt{tables} \; \mt{agg} \; [\mt{nm} = \mt{t}] \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t}
1721 \end{array}$$ 1731 \end{array}$$
1722 1732
1723 \texttt{FROM} clauses are specified using a type family, whose arguments are the free table variables and the table variables bound by this clause. 1733 \texttt{FROM} clauses are specified using a type family, whose arguments are the free table variables and the table variables bound by this clause.
1724 $$\begin{array}{l} 1734 $$\begin{array}{l}
1725 \mt{con} \; \mt{sql\_from\_items} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \mt{Type} \\ 1735 \mt{con} \; \mt{sql\_from\_items} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \mt{Type} \\
1880 1890
1881 Ur/Web supports running code on web browsers, via automatic compilation to JavaScript. 1891 Ur/Web supports running code on web browsers, via automatic compilation to JavaScript.
1882 1892
1883 \subsubsection{The Basics} 1893 \subsubsection{The Basics}
1884 1894
1895 All of the functions in this subsection are client-side only.
1896
1885 Clients can open alert and confirm dialog boxes, in the usual annoying JavaScript way. 1897 Clients can open alert and confirm dialog boxes, in the usual annoying JavaScript way.
1886 $$\begin{array}{l} 1898 $$\begin{array}{l}
1887 \mt{val} \; \mt{alert} : \mt{string} \to \mt{transaction} \; \mt{unit} \\ 1899 \mt{val} \; \mt{alert} : \mt{string} \to \mt{transaction} \; \mt{unit} \\
1888 \mt{val} \; \mt{confirm} : \mt{string} \to \mt{transaction} \; \mt{bool} 1900 \mt{val} \; \mt{confirm} : \mt{string} \to \mt{transaction} \; \mt{bool}
1889 \end{array}$$ 1901 \end{array}$$
1916 \mt{val} \; \mt{source} : \mt{t} ::: \mt{Type} \to \mt{t} \to \mt{transaction} \; (\mt{source} \; \mt{t}) \\ 1928 \mt{val} \; \mt{source} : \mt{t} ::: \mt{Type} \to \mt{t} \to \mt{transaction} \; (\mt{source} \; \mt{t}) \\
1917 \mt{val} \; \mt{set} : \mt{t} ::: \mt{Type} \to \mt{source} \; \mt{t} \to \mt{t} \to \mt{transaction} \; \mt{unit} \\ 1929 \mt{val} \; \mt{set} : \mt{t} ::: \mt{Type} \to \mt{source} \; \mt{t} \to \mt{t} \to \mt{transaction} \; \mt{unit} \\
1918 \mt{val} \; \mt{get} : \mt{t} ::: \mt{Type} \to \mt{source} \; \mt{t} \to \mt{transaction} \; \mt{t} 1930 \mt{val} \; \mt{get} : \mt{t} ::: \mt{Type} \to \mt{source} \; \mt{t} \to \mt{transaction} \; \mt{t}
1919 \end{array}$$ 1931 \end{array}$$
1920 1932
1921 Pure functions over sources are represented in a monad of \emph{signals}. 1933 Only source creation and setting are supported server-side, as a convenience to help in setting up a page, where you may wish to allocate many sources that will be referenced through the page. All server-side storage of values inside sources uses string serializations of values, while client-side storage uses normal JavaScript values.
1934
1935 Pure functions over arbitrary numbers of sources are represented in a monad of \emph{signals}, which may only be used in client-side code.
1922 1936
1923 $$\begin{array}{l} 1937 $$\begin{array}{l}
1924 \mt{con} \; \mt{signal} :: \mt{Type} \to \mt{Type} \\ 1938 \mt{con} \; \mt{signal} :: \mt{Type} \to \mt{Type} \\
1925 \mt{val} \; \mt{signal\_monad} : \mt{monad} \; \mt{signal} \\ 1939 \mt{val} \; \mt{signal\_monad} : \mt{monad} \; \mt{signal} \\
1926 \mt{val} \; \mt{signal} : \mt{t} ::: \mt{Type} \to \mt{source} \; \mt{t} \to \mt{signal} \; \mt{t} 1940 \mt{val} \; \mt{signal} : \mt{t} ::: \mt{Type} \to \mt{source} \; \mt{t} \to \mt{signal} \; \mt{t}