Ur/Web: doc/manual.tex annotate

annotate doc/manual.tex @ 1166:e1df4c63e336

New release

author	Adam Chlipala <adamc@hcoop.net>
date	Sat, 13 Feb 2010 10:13:50 -0500
parents	8679ba87cf3c
children	52c6ac6a59f1

rev	line source
adamc@524	1 \documentclass{article}
adamc@554	2 \usepackage{fullpage,amsmath,amssymb,proof,url}
adamc@524	3
adamc@524	4 \newcommand{\cd}[1]{\texttt{#1}}
adamc@524	5 \newcommand{\mt}[1]{\mathsf{#1}}
adamc@524	6
adamc@524	7 \newcommand{\rc}{+ \hspace{-.075in} + \;}
adamc@527	8 \newcommand{\rcut}{\; \texttt{--} \;}
adamc@527	9 \newcommand{\rcutM}{\; \texttt{---} \;}
adamc@524	10
adamc@524	11 \begin{document}
adamc@524	12
adamc@524	13 \title{The Ur/Web Manual}
adamc@524	14 \author{Adam Chlipala}
adamc@524	15
adamc@524	16 \maketitle
adamc@524	17
adamc@540	18 \tableofcontents
adamc@540	19
adamc@554	20
adamc@554	21 \section{Introduction}
adamc@554	22
adamc@1160	23 \emph{Ur} is a programming language designed to introduce richer type system features into functional programming in the tradition of ML and Haskell. Ur is functional, pure, statically-typed, and strict. Ur supports a powerful kind of \emph{metaprogramming} based on \emph{type-level computation with type-level records}.
adamc@554	24
adamc@554	25 \emph{Ur/Web} is Ur plus a special standard library and associated rules for parsing and optimization. Ur/Web supports construction of dynamic web applications backed by SQL databases. The signature of the standard library is such that well-typed Ur/Web programs ``don't go wrong'' in a very broad sense. Not only do they not crash during particular page generations, but they also may not:
adamc@554	26
adamc@554	27 \begin{itemize}
adamc@554	28 \item Suffer from any kinds of code-injection attacks
adamc@554	29 \item Return invalid HTML
adamc@554	30 \item Contain dead intra-application links
adamc@554	31 \item Have mismatches between HTML forms and the fields expected by their handlers
adamc@652	32 \item Include client-side code that makes incorrect assumptions about the ``AJAX''-style services that the remote web server provides
adamc@554	33 \item Attempt invalid SQL queries
adamc@652	34 \item Use improper marshaling or unmarshaling in communication with SQL databases or between browsers and web servers
adamc@554	35 \end{itemize}
adamc@554	36
adamc@554	37 This type safety is just the foundation of the Ur/Web methodology. It is also possible to use metaprogramming to build significant application pieces by analysis of type structure. For instance, the demo includes an ML-style functor for building an admin interface for an arbitrary SQL table. The type system guarantees that the admin interface sub-application that comes out will always be free of the above-listed bugs, no matter which well-typed table description is given as input.
adamc@554	38
adamc@652	39 The Ur/Web compiler also produces very efficient object code that does not use garbage collection. These compiled programs will often be even more efficient than what most programmers would bother to write in C. The compiler also generates JavaScript versions of client-side code, with no need to write those parts of applications in a different language.
adamc@554	40
adamc@554	41 \medskip
adamc@554	42
adamc@554	43 The official web site for Ur is:
adamc@554	44 \begin{center}
adamc@554	45 \url{http://www.impredicative.com/ur/}
adamc@554	46 \end{center}
adamc@554	47
adamc@555	48
adamc@555	49 \section{Installation}
adamc@555	50
adamc@555	51 If you are lucky, then the following standard command sequence will suffice for installation, in a directory to which you have unpacked the latest distribution tarball.
adamc@555	52
adamc@555	53 \begin{verbatim}
adamc@555	54 ./configure
adamc@555	55 make
adamc@555	56 sudo make install
adamc@555	57 \end{verbatim}
adamc@555	58
adamc@896	59 Some other packages must be installed for the above to work. At a minimum, you need a standard UNIX shell, with standard UNIX tools like sed and GCC in your execution path; MLton, the whole-program optimizing compiler for Standard ML; and the mhash C library. As of this writing, in the ``testing'' version of Debian Linux, this command will install the more uncommon of these dependencies:
adamc@896	60 \begin{verbatim}
adamc@896	61 apt-get install mlton libmhash-dev
adamc@896	62 \end{verbatim}
adamc@555	63
adamc@896	64 To build programs that access SQL databases, you also need one of these client libraries for supported backends.
adamc@555	65 \begin{verbatim}
adamc@896	66 apt-get install libpq-dev libmysqlclient15-dev libsqlite3-dev
adamc@555	67 \end{verbatim}
adamc@555	68
adamc@555	69 It is also possible to access the modules of the Ur/Web compiler interactively, within Standard ML of New Jersey. To install the prerequisites in Debian testing:
adamc@555	70 \begin{verbatim}
adamc@555	71 apt-get install smlnj libsmlnj-smlnj ml-yacc ml-lpt
adamc@555	72 \end{verbatim}
adamc@555	73
adamc@555	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.
adamc@555	75
adamc@896	76 To run an SQL-backed application with a backend besides SQLite, you will probably want to install one of these servers.
adamc@555	77
adamc@555	78 \begin{verbatim}
adamc@896	79 apt-get install postgresql-8.3 mysql-server-5.0
adamc@555	80 \end{verbatim}
adamc@555	81
adamc@555	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:
adamc@555	83
adamc@555	84 \begin{verbatim}
adamc@555	85 apt-get install emacs-goodies-el
adamc@555	86 \end{verbatim}
adamc@555	87
adamc@555	88 Even with the right packages installed, configuration and building might fail to work. After you run \texttt{./configure}, you will see the values of some named environment variables printed. You may need to adjust these values to get proper installation for your system. To change a value, store your preferred alternative in the corresponding UNIX environment variable, before running \texttt{./configure}. For instance, here is how to change the list of extra arguments that the Ur/Web compiler will pass to GCC on every invocation.
adamc@555	89
adamc@555	90 \begin{verbatim}
adamc@555	91 GCCARGS=-fnested-functions ./configure
adamc@555	92 \end{verbatim}
adamc@555	93
adamc@1137	94 Some Mac OS X users have reported needing to use this particular GCCARGS value.
adamc@1137	95
adamc@1161	96 Since the author is still getting a handle on the GNU Autotools that provide the build system, you may need to do some further work to get started, especially in environments with significant differences from Linux (where most testing is done). One OS X user reported needing to run \texttt{./configure} with \texttt{CFLAGS=-I/opt/local/include}, since this directory wound up holding a header file associated with a \texttt{libmhash} package installed via DarwinPorts. Further, to get libpq to link, another user reported setting \texttt{GCCARGS="-I/opt/local/include -L/opt/local/lib/postgresql84"}, after creating a symbolic link with \texttt{ln -s /opt/local/include/postgresql84 /opt/local/include/postgresql}.
adamc@555	97
adamc@555	98 The Emacs mode can be set to autoload by adding the following to your \texttt{.emacs} file.
adamc@555	99
adamc@555	100 \begin{verbatim}
adamc@555	101 (add-to-list 'load-path "/usr/local/share/emacs/site-lisp/urweb-mode")
adamc@555	102 (load "urweb-mode-startup")
adamc@555	103 \end{verbatim}
adamc@555	104
adamc@555	105 Change the path in the first line if you chose a different Emacs installation path during configuration.
adamc@555	106
adamc@555	107
adamc@556	108 \section{Command-Line Compiler}
adamc@556	109
adamc@556	110 \subsection{Project Files}
adamc@556	111
adamc@556	112 The basic inputs to the \texttt{urweb} compiler are project files, which have the extension \texttt{.urp}. Here is a sample \texttt{.urp} file.
adamc@556	113
adamc@556	114 \begin{verbatim}
adamc@556	115 database dbname=test
adamc@556	116 sql crud1.sql
adamc@556	117
adamc@556	118 crud
adamc@556	119 crud1
adamc@556	120 \end{verbatim}
adamc@556	121
adamc@556	122 The \texttt{database} line gives the database information string to pass to libpq. In this case, the string only says to connect to a local database named \texttt{test}.
adamc@556	123
adamc@556	124 The \texttt{sql} line asks for an SQL source file to be generated, giving the commands to run to create the tables and sequences that this application expects to find. After building this \texttt{.urp} file, the following commands could be used to initialize the database, assuming that the current UNIX user exists as a Postgres user with database creation privileges:
adamc@556	125
adamc@556	126 \begin{verbatim}
adamc@556	127 createdb test
adamc@556	128 psql -f crud1.sql test
adamc@556	129 \end{verbatim}
adamc@556	130
adamc@1151	131 A blank line separates the named directives from a list of modules to include in the project.
adamc@556	132
adamc@556	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.
adamc@556	134
adamc@783	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.
adamc@783	136 \begin{itemize}
adamc@783	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.
adamc@783	138 \item \texttt{clientOnly Module.ident} registers an FFI function or transaction that may only be run in client browsers.
adamc@783	139 \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.
adamc@783	140 \item \texttt{database DBSTRING} sets the string to pass to libpq to open a database connection.
adamc@783	141 \item \texttt{debug} saves some intermediate C files, which is mostly useful to help in debugging the compiler itself.
adamc@783	142 \item \texttt{effectful 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.
adamc@783	143 \item \texttt{exe FILENAME} sets the filename to which to write the output executable. The default for file \texttt{P.urp} is \texttt{P.exe}.
adamc@783	144 \item \texttt{ffi FILENAME} reads the file \texttt{FILENAME.urs} to determine the interface to a new FFI module. The name of the module is calculated from \texttt{FILENAME} in the same way as for normal source files. See the files \texttt{include/urweb.h} and \texttt{src/c/urweb.c} for examples of C headers and implementations for FFI modules. In general, every type or value \texttt{Module.ident} becomes \texttt{uw\_Module\_ident} in C.
adamc@1099	145 \item \texttt{include FILENAME} adds \texttt{FILENAME} to the list of files to be \texttt{\#include}d in C sources. This is most useful for interfacing with new FFI modules.
adamc@783	146 \item \texttt{jsFunc Module.ident=name} gives the JavaScript name of an FFI value.
adamc@1089	147 \item \texttt{library FILENAME} parses \texttt{FILENAME.urp} and merges its contents with the rest of the current file's contents. If \texttt{FILENAME.urp} doesn't exist, the compiler also tries \texttt{FILENAME/lib.urp}.
adamc@783	148 \item \texttt{link FILENAME} adds \texttt{FILENAME} to the list of files to be passed to the GCC linker at the end of compilation. This is most useful for importing extra libraries needed by new FFI modules.
adamc@852	149 \item \texttt{path NAME=VALUE} creates a mapping from \texttt{NAME} to \texttt{VALUE}. This mapping may be used at the beginnings of filesystem paths given to various other configuration directives. A path like \texttt{\$NAME/rest} is expanded to \texttt{VALUE/rest}. There is an initial mapping from the empty name (for paths like \texttt{\$/list}) to the directory where the Ur/Web standard library is installed. If you accept the default \texttt{configure} options, this directory is \texttt{/usr/local/lib/urweb/ur}.
adamc@783	150 \item \texttt{prefix PREFIX} sets the prefix included before every URI within the generated application. The default is \texttt{/}.
adamc@783	151 \item \texttt{profile} generates an executable that may be used with gprof.
adamc@783	152 \item \texttt{rewrite KIND FROM TO} gives a rule for rewriting canonical module paths. For instance, the canonical path of a page may be \texttt{Mod1.Mod2.mypage}, while you would rather the page were accessed via a URL containing only \texttt{page}. The directive \texttt{rewrite url Mod1/Mod2/mypage page} would accomplish that. The possible values of \texttt{KIND} determine which kinds of objects are affected. The kind \texttt{all} matches any object, and \texttt{url} matches page URLs. The kinds \texttt{table}, \texttt{sequence}, and \texttt{view} match those sorts of SQL entities, and \texttt{relation} matches any of those three. \texttt{cookie} matches HTTP cookies, and \texttt{style} matches CSS class names. If \texttt{FROM} ends in \texttt{/*}, it is interpreted as a prefix matching rule, and rewriting occurs by replacing only the appropriate prefix of a path with \texttt{TO}. While the actual external names of relations and styles have parts separated by underscores instead of slashes, all rewrite rules must be written in terms of slashes.
adamc@783	153 \item \texttt{script URL} adds \texttt{URL} to the list of extra JavaScript files to be included at the beginning of any page that uses JavaScript. This is most useful for importing JavaScript versions of functions found in new FFI modules.
adamc@783	154 \item \texttt{serverOnly Module.ident} registers an FFI function or transaction that may only be run on the server.
adamc@1164	155 \item \texttt{sigfile PATH} sets a path where your application should look for a key to use in cryptographic signing. This is used to prevent cross-site request forgery attacks for any form handler that both reads a cookie and creates side effects. If the referenced file doesn't exist, an application will create it and read its saved data on future invocations. You can also initialize the file manually with any contents at least 16 bytes long; the first 16 bytes will be treated as the key.
adamc@783	156 \item \texttt{sql FILENAME} sets where to write an SQL file with the commands to create the expected database schema. The default is not to create such a file.
adamc@783	157 \item \texttt{timeout N} sets to \texttt{N} seconds the amount of time that the generated server will wait after the last contact from a client before determining that that client has exited the application. Clients that remain active will take the timeout setting into account in determining how often to ping the server, so it only makes sense to set a high timeout to cope with browser and network delays and failures. Higher timeouts can lead to more unnecessary client information taking up memory on the server. The timeout goes unused by any page that doesn't involve the \texttt{recv} function, since the server only needs to store per-client information for clients that receive asynchronous messages.
adamc@783	158 \end{itemize}
adamc@701	159
adamc@701	160
adamc@557	161 \subsection{Building an Application}
adamc@557	162
adamc@557	163 To compile project \texttt{P.urp}, simply run
adamc@557	164 \begin{verbatim}
adamc@557	165 urweb P
adamc@557	166 \end{verbatim}
adamc@558	167 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.
adamc@557	168
adamc@557	169 To time how long the different compiler phases run, without generating an executable, run
adamc@557	170 \begin{verbatim}
adamc@557	171 urweb -timing P
adamc@557	172 \end{verbatim}
adamc@557	173
adamc@1086	174 To stop the compilation process after type-checking, run
adamc@1086	175 \begin{verbatim}
adamc@1086	176 urweb -tc P
adamc@1086	177 \end{verbatim}
adamc@1086	178
adamc@896	179 Some other command-line parameters are accepted:
adamc@896	180 \begin{itemize}
adamc@896	181 \item \texttt{-db <DBSTRING>}: Set database connection information, using the format expected by Postgres's \texttt{PQconnectdb()}, which is \texttt{name1=value1 ... nameN=valueN}. The same format is also parsed and used to discover connection parameters for MySQL and SQLite. The only significant settings for MySQL are \texttt{host}, \texttt{hostaddr}, \texttt{port}, \texttt{dbname}, \texttt{user}, and \texttt{password}. The only significant setting for SQLite is \texttt{dbname}, which is interpreted as the filesystem path to the database. Additionally, when using SQLite, a database string may be just a file path.
adamc@896	182
adamc@896	183 \item \texttt{-dbms [postgres\|mysql\|sqlite]}: Sets the database backend to use.
adamc@896	184 \begin{itemize}
adamc@896	185 \item \texttt{postgres}: This is PostgreSQL, the default. Among the supported engines, Postgres best matches the design philosophy behind Ur, with a focus on consistent views of data, even in the face of much concurrency. Different database engines have different quirks of SQL syntax. Ur/Web tends to use Postgres idioms where there are choices to be made, though the compiler translates SQL as needed to support other backends.
adamc@896	186
adamc@896	187 A command sequence like this can initialize a Postgres database, using a file \texttt{app.sql} generated by the compiler:
adamc@896	188 \begin{verbatim}
adamc@896	189 createdb app
adamc@896	190 psql -f app.sql app
adamc@896	191 \end{verbatim}
adamc@896	192
adamc@896	193 \item \texttt{mysql}: This is MySQL, another popular relational database engine that uses persistent server processes. Ur/Web needs transactions to function properly. Many installations of MySQL use non-transactional storage engines by default. Ur/Web generates table definitions that try to use MySQL's InnoDB engine, which supports transactions. You can edit the first line of a generated \texttt{.sql} file to change this behavior, but it really is true that Ur/Web applications will exhibit bizarre behavior if you choose an engine that ignores transaction commands.
adamc@896	194
adamc@896	195 A command sequence like this can initialize a MySQL database:
adamc@896	196 \begin{verbatim}
adamc@896	197 echo "CREATE DATABASE app" \| mysql
adamc@896	198 mysql -D app <app.sql
adamc@896	199 \end{verbatim}
adamc@896	200
adamc@896	201 \item \texttt{sqlite}: This is SQLite, a simple filesystem-based transactional database engine. With this backend, Ur/Web applications can run without any additional server processes. The other engines are generally preferred for large-workload performance and full admin feature sets, while SQLite is popular for its low resource footprint and ease of set-up.
adamc@896	202
adamc@896	203 A command like this can initialize an SQLite database:
adamc@896	204 \begin{verbatim}
adamc@896	205 sqlite3 path/to/database/file <app.sql
adamc@896	206 \end{verbatim}
adamc@896	207 \end{itemize}
adamc@896	208
adamc@896	209 \item \texttt{-output FILENAME}: Set where the application executable is written.
adamc@896	210
adamc@1127	211 \item \texttt{-path NAME VALUE}: Set the value of path variable \texttt{\$NAME} to \texttt{VALUE}, for use in \texttt{.urp} files.
adamc@1127	212
adamc@896	213 \item \texttt{-protocol [http\|cgi\|fastcgi]}: Set the protocol that the generated application speaks.
adamc@896	214 \begin{itemize}
adamc@896	215 \item \texttt{http}: This is the default. It is for building standalone web servers that can be accessed by web browsers directly.
adamc@896	216
adamc@896	217 \item \texttt{cgi}: This is the classic protocol that web servers use to generate dynamic content by spawning new processes. While Ur/Web programs may in general use message-passing with the \texttt{send} and \texttt{recv} functions, that functionality is not yet supported in CGI, since CGI needs a fresh process for each request, and message-passing needs to use persistent sockets to deliver messages.
adamc@896	218
adamc@896	219 Since Ur/Web treats paths in an unusual way, a configuration line like this one can be used to configure an application that was built with URL prefix \texttt{/Hello}:
adamc@896	220 \begin{verbatim}
adamc@896	221 ScriptAlias /Hello /path/to/hello.exe
adamc@896	222 \end{verbatim}
adamc@896	223
adamc@1163	224 A different method can be used for, e.g., a shared host, where you can only configure Apache via \texttt{.htaccess} files. Drop the generated executable into your web space and mark it as CGI somehow. For instance, if the script ends in \texttt{.exe}, you might put this in \texttt{.htaccess} in the directory containing the script:
adamc@1163	225 \begin{verbatim}
adamc@1163	226 Options +ExecCGI
adamc@1163	227 AddHandler cgi-script .exe
adamc@1163	228 \end{verbatim}
adamc@1163	229
adamc@1163	230 Additionally, make sure that Ur/Web knows the proper URI prefix for your script. For instance, if the script is accessed via \texttt{http://somewhere/dir/script.exe}, then include this line in your \texttt{.urp} file:
adamc@1163	231 \begin{verbatim}
adamc@1163	232 prefix /dir/script.exe/
adamc@1163	233 \end{verbatim}
adamc@1163	234
adamc@1163	235 To access the \texttt{foo} function in the \texttt{Bar} module, you would then hit \texttt{http://somewhere/dir/script.exe/Bar/foo}.
adamc@1163	236
adamc@1164	237 If your application contains form handlers that read cookies before causing side effects, then you will need to use the \texttt{sigfile} \texttt{.urp} directive, too.
adamc@1164	238
adamc@896	239 \item \texttt{fastcgi}: This is a newer protocol inspired by CGI, wherein web servers can start and reuse persistent external processes to generate dynamic content. Ur/Web doesn't implement the whole protocol, but Ur/Web's support has been tested to work with the \texttt{mod\_fastcgi}s of Apache and lighttpd.
adamc@896	240
adamc@896	241 To configure a FastCGI program with Apache, one could combine the above \texttt{ScriptAlias} line with a line like this:
adamc@896	242 \begin{verbatim}
adamc@896	243 FastCgiServer /path/to/hello.exe -idle-timeout 99999
adamc@896	244 \end{verbatim}
adamc@896	245 The idle timeout is only important for applications that use message-passing. Client connections may go long periods without receiving messages, and Apache tries to be helpful and garbage collect them in such cases. To prevent that behavior, we specify how long a connection must be idle to be collected.
adamc@896	246
adamc@896	247 Here is some lighttpd configuration for the same application.
adamc@896	248 \begin{verbatim}
adamc@896	249 fastcgi.server = (
adamc@896	250 "/Hello/" =>
adamc@896	251 (( "bin-path" => "/path/to/hello.exe",
adamc@896	252 "socket" => "/tmp/hello",
adamc@896	253 "check-local" => "disable",
adamc@896	254 "docroot" => "/",
adamc@896	255 "max-procs" => "1"
adamc@896	256 ))
adamc@896	257 )
adamc@896	258 \end{verbatim}
adamc@896	259 The least obvious requirement is setting \texttt{max-procs} to 1, so that lighttpd doesn't try to multiplex requests across multiple external processes. This is required for message-passing applications, where a single database of client connections is maintained within a multi-threaded server process. Multiple processes may, however, be used safely with applications that don't use message-passing.
adamc@896	260
adamc@896	261 A FastCGI process reads the environment variable \texttt{URWEB\_NUM\_THREADS} to determine how many threads to spawn for handling client requests. The default is 1.
adamc@896	262 \end{itemize}
adamc@896	263
adamc@1127	264 \item \texttt{-root Name PATH}: Trigger an alternate module convention for all source files found in directory \texttt{PATH} or any of its subdirectories. Any file \texttt{PATH/foo.ur} defines a module \texttt{Name.Foo} instead of the usual \texttt{Foo}. Any file \texttt{PATH/subdir/foo.ur} defines a module \texttt{Name.Subdir.Foo}, and so on for arbitrary nesting of subdirectories.
adamc@1127	265
adamc@1164	266 \item \texttt{-sigfile PATH}: Same as the \texttt{sigfile} directive in \texttt{.urp} files
adamc@1164	267
adamc@896	268 \item \texttt{-sql FILENAME}: Set where a database set-up SQL script is written.
adamc@1095	269
adamc@1095	270 \item \texttt{-static}: Link the runtime system statically. The default is to link against dynamic libraries.
adamc@896	271 \end{itemize}
adamc@896	272
adamc@556	273
adamc@529	274 \section{Ur Syntax}
adamc@529	275
adamc@784	276 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.
adamc@524	277
adamc@524	278 \subsection{Lexical Conventions}
adamc@524	279
adamc@524	280 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.
adamc@524	281
adamc@524	282 \begin{center}
adamc@524	283 \begin{tabular}{rl}
adamc@524	284 \textbf{\LaTeX} & \textbf{ASCII} \\
adamc@524	285 $\to$ & \cd{->} \\
adamc@652	286 $\longrightarrow$ & \cd{-->} \\
adamc@524	287 $\times$ & \cd{*} \\
adamc@524	288 $\lambda$ & \cd{fn} \\
adamc@524	289 $\Rightarrow$ & \cd{=>} \\
adamc@652	290 $\Longrightarrow$ & \cd{==>} \\
adamc@529	291 $\neq$ & \cd{<>} \\
adamc@529	292 $\leq$ & \cd{<=} \\
adamc@529	293 $\geq$ & \cd{>=} \\
adamc@524	294 \\
adamc@524	295 $x$ & Normal textual identifier, not beginning with an uppercase letter \\
adamc@525	296 $X$ & Normal textual identifier, beginning with an uppercase letter \\
adamc@524	297 \end{tabular}
adamc@524	298 \end{center}
adamc@524	299
adamc@525	300 We often write syntax like $e^$ to indicate zero or more copies of $e$, $e^+$ to indicate one or more copies, and $e,^$ and $e,^+$ to indicate multiple copies separated by commas. Another separator may be used in place of a comma. The $e$ term may be surrounded by parentheses to indicate grouping; those parentheses should not be included in the actual ASCII.
adamc@524	301
adamc@873	302 We write $\ell$ for literals of the primitive types, for the most part following C conventions. There are $\mt{int}$, $\mt{float}$, $\mt{char}$, and $\mt{string}$ literals. Character literals follow the SML convention instead of the C convention, written like \texttt{\#"a"} instead of \texttt{'a'}.
adamc@526	303
adamc@527	304 This version of the manual doesn't include operator precedences; see \texttt{src/urweb.grm} for that.
adamc@527	305
adamc@552	306 \subsection{\label{core}Core Syntax}
adamc@524	307
adamc@524	308 \emph{Kinds} classify types and other compile-time-only entities. Each kind in the grammar is listed with a description of the sort of data it classifies.
adamc@524	309 $$\begin{array}{rrcll}
adamc@524	310 \textrm{Kinds} & \kappa &::=& \mt{Type} & \textrm{proper types} \\
adamc@525	311 &&& \mt{Unit} & \textrm{the trivial constructor} \\
adamc@525	312 &&& \mt{Name} & \textrm{field names} \\
adamc@525	313 &&& \kappa \to \kappa & \textrm{type-level functions} \\
adamc@525	314 &&& \{\kappa\} & \textrm{type-level records} \\
adamc@525	315 &&& (\kappa\times^+) & \textrm{type-level tuples} \\
adamc@652	316 &&& X & \textrm{variable} \\
adamc@652	317 &&& X \longrightarrow k & \textrm{kind-polymorphic type-level function} \\
adamc@529	318 &&& \_\_ & \textrm{wildcard} \\
adamc@525	319 &&& (\kappa) & \textrm{explicit precedence} \\
adamc@524	320 \end{array}$$
adamc@524	321
adamc@524	322 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.
adamc@524	323 $$\begin{array}{rrcll}
adamc@524	324 \textrm{Explicitness} & ? &::=& :: & \textrm{explicit} \\
adamc@558	325 &&& ::: & \textrm{implicit}
adamc@524	326 \end{array}$$
adamc@524	327
adamc@524	328 \emph{Constructors} are the main class of compile-time-only data. They include proper types and are classified by kinds.
adamc@524	329 $$\begin{array}{rrcll}
adamc@524	330 \textrm{Constructors} & c, \tau &::=& (c) :: \kappa & \textrm{kind annotation} \\
adamc@530	331 &&& \hat{x} & \textrm{constructor variable} \\
adamc@524	332 \\
adamc@525	333 &&& \tau \to \tau & \textrm{function type} \\
adamc@525	334 &&& x \; ? \; \kappa \to \tau & \textrm{polymorphic function type} \\
adamc@652	335 &&& X \longrightarrow \tau & \textrm{kind-polymorphic function type} \\
adamc@525	336 &&& \$ c & \textrm{record type} \\
adamc@524	337 \\
adamc@525	338 &&& c \; c & \textrm{type-level function application} \\
adamc@530	339 &&& \lambda x \; :: \; \kappa \Rightarrow c & \textrm{type-level function abstraction} \\
adamc@524	340 \\
adamc@652	341 &&& X \Longrightarrow c & \textrm{type-level kind-polymorphic function abstraction} \\
adamc@655	342 &&& c [\kappa] & \textrm{type-level kind-polymorphic function application} \\
adamc@652	343 \\
adamc@525	344 &&& () & \textrm{type-level unit} \\
adamc@525	345 &&& \#X & \textrm{field name} \\
adamc@524	346 \\
adamc@525	347 &&& [(c = c)^*] & \textrm{known-length type-level record} \\
adamc@525	348 &&& c \rc c & \textrm{type-level record concatenation} \\
adamc@652	349 &&& \mt{map} & \textrm{type-level record map} \\
adamc@524	350 \\
adamc@558	351 &&& (c,^+) & \textrm{type-level tuple} \\
adamc@525	352 &&& c.n & \textrm{type-level tuple projection ($n \in \mathbb N^+$)} \\
adamc@524	353 \\
adamc@652	354 &&& [c \sim c] \Rightarrow \tau & \textrm{guarded type} \\
adamc@524	355 \\
adamc@529	356 &&& \_ :: \kappa & \textrm{wildcard} \\
adamc@525	357 &&& (c) & \textrm{explicit precedence} \\
adamc@530	358 \\
adamc@530	359 \textrm{Qualified uncapitalized variables} & \hat{x} &::=& x & \textrm{not from a module} \\
adamc@530	360 &&& M.x & \textrm{projection from a module} \\
adamc@525	361 \end{array}$$
adamc@525	362
adamc@655	363 We include both abstraction and application for kind polymorphism, but applications are only inferred internally; they may not be written explicitly in source programs.
adamc@655	364
adamc@525	365 Modules of the module system are described by \emph{signatures}.
adamc@525	366 $$\begin{array}{rrcll}
adamc@525	367 \textrm{Signatures} & S &::=& \mt{sig} \; s^* \; \mt{end} & \textrm{constant} \\
adamc@525	368 &&& X & \textrm{variable} \\
adamc@525	369 &&& \mt{functor}(X : S) : S & \textrm{functor} \\
adamc@529	370 &&& S \; \mt{where} \; \mt{con} \; x = c & \textrm{concretizing an abstract constructor} \\
adamc@525	371 &&& M.X & \textrm{projection from a module} \\
adamc@525	372 \\
adamc@525	373 \textrm{Signature items} & s &::=& \mt{con} \; x :: \kappa & \textrm{abstract constructor} \\
adamc@525	374 &&& \mt{con} \; x :: \kappa = c & \textrm{concrete constructor} \\
adamc@528	375 &&& \mt{datatype} \; x \; x^* = dc\mid^+ & \textrm{algebraic datatype definition} \\
adamc@529	376 &&& \mt{datatype} \; x = \mt{datatype} \; M.x & \textrm{algebraic datatype import} \\
adamc@525	377 &&& \mt{val} \; x : \tau & \textrm{value} \\
adamc@525	378 &&& \mt{structure} \; X : S & \textrm{sub-module} \\
adamc@525	379 &&& \mt{signature} \; X = S & \textrm{sub-signature} \\
adamc@525	380 &&& \mt{include} \; S & \textrm{signature inclusion} \\
adamc@525	381 &&& \mt{constraint} \; c \sim c & \textrm{record disjointness constraint} \\
adamc@654	382 &&& \mt{class} \; x :: \kappa & \textrm{abstract constructor class} \\
adamc@654	383 &&& \mt{class} \; x :: \kappa = c & \textrm{concrete constructor class} \\
adamc@525	384 \\
adamc@525	385 \textrm{Datatype constructors} & dc &::=& X & \textrm{nullary constructor} \\
adamc@525	386 &&& X \; \mt{of} \; \tau & \textrm{unary constructor} \\
adamc@524	387 \end{array}$$
adamc@524	388
adamc@526	389 \emph{Patterns} are used to describe structural conditions on expressions, such that expressions may be tested against patterns, generating assignments to pattern variables if successful.
adamc@526	390 $$\begin{array}{rrcll}
adamc@526	391 \textrm{Patterns} & p &::=& \_ & \textrm{wildcard} \\
adamc@526	392 &&& x & \textrm{variable} \\
adamc@526	393 &&& \ell & \textrm{constant} \\
adamc@526	394 &&& \hat{X} & \textrm{nullary constructor} \\
adamc@526	395 &&& \hat{X} \; p & \textrm{unary constructor} \\
adamc@526	396 &&& \{(x = p,)^*\} & \textrm{rigid record pattern} \\
adamc@526	397 &&& \{(x = p,)^+, \ldots\} & \textrm{flexible record pattern} \\
adamc@852	398 &&& p : \tau & \textrm{type annotation} \\
adamc@527	399 &&& (p) & \textrm{explicit precedence} \\
adamc@526	400 \\
adamc@529	401 \textrm{Qualified capitalized variables} & \hat{X} &::=& X & \textrm{not from a module} \\
adamc@526	402 &&& M.X & \textrm{projection from a module} \\
adamc@526	403 \end{array}$$
adamc@526	404
adamc@527	405 \emph{Expressions} are the main run-time entities, corresponding to both ``expressions'' and ``statements'' in mainstream imperative languages.
adamc@527	406 $$\begin{array}{rrcll}
adamc@527	407 \textrm{Expressions} & e &::=& e : \tau & \textrm{type annotation} \\
adamc@529	408 &&& \hat{x} & \textrm{variable} \\
adamc@529	409 &&& \hat{X} & \textrm{datatype constructor} \\
adamc@527	410 &&& \ell & \textrm{constant} \\
adamc@527	411 \\
adamc@527	412 &&& e \; e & \textrm{function application} \\
adamc@527	413 &&& \lambda x : \tau \Rightarrow e & \textrm{function abstraction} \\
adamc@527	414 &&& e [c] & \textrm{polymorphic function application} \\
adamc@852	415 &&& \lambda [x \; ? \; \kappa] \Rightarrow e & \textrm{polymorphic function abstraction} \\
adamc@655	416 &&& e [\kappa] & \textrm{kind-polymorphic function application} \\
adamc@652	417 &&& X \Longrightarrow e & \textrm{kind-polymorphic function abstraction} \\
adamc@527	418 \\
adamc@527	419 &&& \{(c = e,)^*\} & \textrm{known-length record} \\
adamc@527	420 &&& e.c & \textrm{record field projection} \\
adamc@527	421 &&& e \rc e & \textrm{record concatenation} \\
adamc@527	422 &&& e \rcut c & \textrm{removal of a single record field} \\
adamc@527	423 &&& e \rcutM c & \textrm{removal of multiple record fields} \\
adamc@527	424 \\
adamc@527	425 &&& \mt{let} \; ed^* \; \mt{in} \; e \; \mt{end} & \textrm{local definitions} \\
adamc@527	426 \\
adamc@527	427 &&& \mt{case} \; e \; \mt{of} \; (p \Rightarrow e\|)^+ & \textrm{pattern matching} \\
adamc@527	428 \\
adamc@654	429 &&& \lambda [c \sim c] \Rightarrow e & \textrm{guarded expression abstraction} \\
adamc@654	430 &&& e \; ! & \textrm{guarded expression application} \\
adamc@527	431 \\
adamc@527	432 &&& \_ & \textrm{wildcard} \\
adamc@527	433 &&& (e) & \textrm{explicit precedence} \\
adamc@527	434 \\
adamc@527	435 \textrm{Local declarations} & ed &::=& \cd{val} \; x : \tau = e & \textrm{non-recursive value} \\
adamc@527	436 &&& \cd{val} \; \cd{rec} \; (x : \tau = e \; \cd{and})^+ & \textrm{mutually-recursive values} \\
adamc@527	437 \end{array}$$
adamc@527	438
adamc@655	439 As with constructors, we include both abstraction and application for kind polymorphism, but applications are only inferred internally.
adamc@655	440
adamc@528	441 \emph{Declarations} primarily bring new symbols into context.
adamc@528	442 $$\begin{array}{rrcll}
adamc@528	443 \textrm{Declarations} & d &::=& \mt{con} \; x :: \kappa = c & \textrm{constructor synonym} \\
adamc@528	444 &&& \mt{datatype} \; x \; x^* = dc\mid^+ & \textrm{algebraic datatype definition} \\
adamc@529	445 &&& \mt{datatype} \; x = \mt{datatype} \; M.x & \textrm{algebraic datatype import} \\
adamc@528	446 &&& \mt{val} \; x : \tau = e & \textrm{value} \\
adamc@528	447 &&& \mt{val} \; \cd{rec} \; (x : \tau = e \; \mt{and})^+ & \textrm{mutually-recursive values} \\
adamc@528	448 &&& \mt{structure} \; X : S = M & \textrm{module definition} \\
adamc@528	449 &&& \mt{signature} \; X = S & \textrm{signature definition} \\
adamc@528	450 &&& \mt{open} \; M & \textrm{module inclusion} \\
adamc@528	451 &&& \mt{constraint} \; c \sim c & \textrm{record disjointness constraint} \\
adamc@528	452 &&& \mt{open} \; \mt{constraints} \; M & \textrm{inclusion of just the constraints from a module} \\
adamc@528	453 &&& \mt{table} \; x : c & \textrm{SQL table} \\
adamc@784	454 &&& \mt{view} \; x : c & \textrm{SQL view} \\
adamc@528	455 &&& \mt{sequence} \; x & \textrm{SQL sequence} \\
adamc@535	456 &&& \mt{cookie} \; x : \tau & \textrm{HTTP cookie} \\
adamc@784	457 &&& \mt{style} \; x : \tau & \textrm{CSS class} \\
adamc@654	458 &&& \mt{class} \; x :: \kappa = c & \textrm{concrete constructor class} \\
adamc@1085	459 &&& \mt{task} \; e = e & \textrm{recurring task} \\
adamc@528	460 \\
adamc@529	461 \textrm{Modules} & M &::=& \mt{struct} \; d^* \; \mt{end} & \textrm{constant} \\
adamc@529	462 &&& X & \textrm{variable} \\
adamc@529	463 &&& M.X & \textrm{projection} \\
adamc@529	464 &&& M(M) & \textrm{functor application} \\
adamc@529	465 &&& \mt{functor}(X : S) : S = M & \textrm{functor abstraction} \\
adamc@528	466 \end{array}$$
adamc@528	467
adamc@528	468 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.
adamc@527	469
adamc@784	470 We omit some extra possibilities in $\mt{table}$ syntax, deferring them to Section \ref{tables}.
adamc@784	471
adamc@529	472 \subsection{Shorthands}
adamc@529	473
adamc@529	474 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.
adamc@529	475
adamc@529	476 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$.
adamc@529	477
adamc@529	478 A record type may be written $\{(c = c,)^\}$, which elaborates to $\$[(c = c,)^]$.
adamc@529	479
adamc@533	480 The notation $[c_1, \ldots, c_n]$ is shorthand for $[c_1 = (), \ldots, c_n = ()]$.
adamc@533	481
adamc@529	482 A tuple type $(\tau_1, \ldots, \tau_n)$ expands to a record type $\{1 = \tau_1, \ldots, n = \tau_n\}$, with natural numbers as field names. A tuple pattern $(p_1, \ldots, p_n)$ expands to a rigid record pattern $\{1 = p_1, \ldots, n = p_n\}$. Positive natural numbers may be used in most places where field names would be allowed.
adamc@529	483
adamc@852	484 In general, several adjacent $\lambda$ forms may be combined into one, and kind and type annotations may be omitted, in which case they are implicitly included as wildcards. More formally, for constructor-level abstractions, we can define a new non-terminal $b ::= x \mid (x :: \kappa) \mid X$ and allow composite abstractions of the form $\lambda b^+ \Rightarrow c$, elaborating into the obvious sequence of one core $\lambda$ per element of $b^+$.
adamc@529	485
adamc@529	486 For any signature item or declaration that defines some entity to be equal to $A$ with classification annotation $B$ (e.g., $\mt{val} \; x : B = A$), $B$ and the preceding colon (or similar punctuation) may be omitted, in which case it is filled in as a wildcard.
adamc@529	487
adamc@529	488 A signature item or declaration $\mt{type} \; x$ or $\mt{type} \; x = \tau$ is elaborated into $\mt{con} \; x :: \mt{Type}$ or $\mt{con} \; x :: \mt{Type} = \tau$, respectively.
adamc@529	489
adamc@654	490 A signature item or declaration $\mt{class} \; x = \lambda y \Rightarrow c$ may be abbreviated $\mt{class} \; x \; y = c$.
adamc@529	491
adamc@1102	492 Handling of implicit and explicit constructor arguments may be tweaked with some prefixes to variable references. An expression $@x$ is a version of $x$ where all implicit constructor arguments have been made explicit. An expression $@@x$ achieves the same effect, additionally halting automatic resolution of type class instances and automatic proving of disjointness constraints. The default is that implicit arguments are inserted automatically after any reference to a non-local variable, or after any application of a non-local variable to one or more arguments. For such an expression, implicit wildcard arguments are added for the longest prefix of the expression's type consisting only of implicit polymorphism, type class instances, and disjointness obligations. The same syntax works for variables projected out of modules and for capitalized variables (datatype constructors).
adamc@529	493
adamc@852	494 At the expression level, an analogue is available of the composite $\lambda$ form for constructors. We define the language of binders as $b ::= p \mid [x] \mid [x \; ? \; \kappa] \mid X \mid [c \sim c]$. A lone variable $[x]$ stands for an implicit constructor variable of unspecified kind. The standard value-level function binder is recovered as the type-annotated pattern form $x : \tau$. It is a compile-time error to include a pattern $p$ that does not match every value of the appropriate type.
adamc@529	495
adamc@852	496 A local $\mt{val}$ declaration may bind a pattern instead of just a plain variable. As for function arguments, only irrefutable patterns are legal.
adamc@852	497
adamc@852	498 The keyword $\mt{fun}$ is a shorthand for $\mt{val} \; \mt{rec}$ that allows arguments to be specified before the equal sign in the definition of each mutually-recursive function, as in SML. Each curried argument must follow the grammar of the $b$ non-terminal introduced two paragraphs ago. A $\mt{fun}$ declaration is elaborated into a version that adds additional $\lambda$s to the fronts of the righthand sides, as appropriate.
adamc@529	499
adamc@529	500 A signature item $\mt{functor} \; X_1 \; (X_2 : S_1) : S_2$ is elaborated into $\mt{structure} \; X_1 : \mt{functor}(X_2 : S_1) : S_2$. A declaration $\mt{functor} \; X_1 \; (X_2 : S_1) : S_2 = M$ is elaborated into $\mt{structure} \; X_1 : \mt{functor}(X_2 : S_1) : S_2 = \mt{functor}(X_2 : S_1) : S_2 = M$.
adamc@529	501
adamc@852	502 An $\mt{open} \; \mt{constraints}$ declaration is implicitly inserted for the argument of every functor at the beginning of the functor body. For every declaration of the form $\mt{structure} \; X : S = \mt{struct} \ldots \mt{end}$, an $\mt{open} \; \mt{constraints} \; X$ declaration is implicitly inserted immediately afterward.
adamc@852	503
adamc@853	504 A declaration $\mt{table} \; x : \{(c = c,)^\}$ is elaborated into $\mt{table} \; x : [(c = c,)^]$.
adamc@529	505
adamc@529	506 The syntax $\mt{where} \; \mt{type}$ is an alternate form of $\mt{where} \; \mt{con}$.
adamc@529	507
adamc@529	508 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$.
adamc@529	509
adamc@529	510 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}$.
adamc@529	511
adamc@784	512 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}$.
adamc@529	513
adamc@530	514
adamc@530	515 \section{Static Semantics}
adamc@530	516
adamc@530	517 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.
adamc@530	518
adamc@530	519 Since there is significant mutual recursion among the judgments, we introduce them all before beginning to give rules. We use the same variety of contexts throughout this section, implicitly introducing new sorts of context entries as needed.
adamc@530	520 \begin{itemize}
adamc@655	521 \item $\Gamma \vdash \kappa$ expresses kind well-formedness.
adamc@530	522 \item $\Gamma \vdash c :: \kappa$ assigns a kind to a constructor in a context.
adamc@530	523 \item $\Gamma \vdash c \sim c$ proves the disjointness of two record constructors; that is, that they share no field names. We overload the judgment to apply to pairs of field names as well.
adamc@531	524 \item $\Gamma \vdash c \hookrightarrow C$ proves that record constructor $c$ decomposes into set $C$ of field names and record constructors.
adamc@530	525 \item $\Gamma \vdash c \equiv c$ proves the computational equivalence of two constructors. This is often called a \emph{definitional equality} in the world of type theory.
adamc@530	526 \item $\Gamma \vdash e : \tau$ is a standard typing judgment.
adamc@534	527 \item $\Gamma \vdash p \leadsto \Gamma; \tau$ combines typing of patterns with calculation of which new variables they bind.
adamc@537	528 \item $\Gamma \vdash d \leadsto \Gamma$ expresses how a declaration modifies a context. We overload this judgment to apply to sequences of declarations, as well as to signature items and sequences of signature items.
adamc@537	529 \item $\Gamma \vdash S \equiv S$ is the signature equivalence judgment.
adamc@536	530 \item $\Gamma \vdash S \leq S$ is the signature compatibility judgment. We write $\Gamma \vdash S$ as shorthand for $\Gamma \vdash S \leq S$.
adamc@530	531 \item $\Gamma \vdash M : S$ is the module signature checking judgment.
adamc@537	532 \item $\mt{proj}(M, \overline{s}, V)$ is a partial function for projecting a signature item from $\overline{s}$, given the module $M$ that we project from. $V$ may be $\mt{con} \; x$, $\mt{datatype} \; x$, $\mt{val} \; x$, $\mt{signature} \; X$, or $\mt{structure} \; X$. The parameter $M$ is needed because the projected signature item may refer to other items from $\overline{s}$.
adamc@539	533 \item $\mt{selfify}(M, \overline{s})$ adds information to signature items $\overline{s}$ to reflect the fact that we are concerned with the particular module $M$. This function is overloaded to work over individual signature items as well.
adamc@530	534 \end{itemize}
adamc@530	535
adamc@655	536
adamc@655	537 \subsection{Kind Well-Formedness}
adamc@655	538
adamc@655	539 $$\infer{\Gamma \vdash \mt{Type}}{}
adamc@655	540 \quad \infer{\Gamma \vdash \mt{Unit}}{}
adamc@655	541 \quad \infer{\Gamma \vdash \mt{Name}}{}
adamc@655	542 \quad \infer{\Gamma \vdash \kappa_1 \to \kappa_2}{
adamc@655	543 \Gamma \vdash \kappa_1
adamc@655	544 & \Gamma \vdash \kappa_2
adamc@655	545 }
adamc@655	546 \quad \infer{\Gamma \vdash \{\kappa\}}{
adamc@655	547 \Gamma \vdash \kappa
adamc@655	548 }
adamc@655	549 \quad \infer{\Gamma \vdash (\kappa_1 \times \ldots \times \kappa_n)}{
adamc@655	550 \forall i: \Gamma \vdash \kappa_i
adamc@655	551 }$$
adamc@655	552
adamc@655	553 $$\infer{\Gamma \vdash X}{
adamc@655	554 X \in \Gamma
adamc@655	555 }
adamc@655	556 \quad \infer{\Gamma \vdash X \longrightarrow \kappa}{
adamc@655	557 \Gamma, X \vdash \kappa
adamc@655	558 }$$
adamc@655	559
adamc@530	560 \subsection{Kinding}
adamc@530	561
adamc@655	562 We write $[X \mapsto \kappa_1]\kappa_2$ for capture-avoiding substitution of $\kappa_1$ for $X$ in $\kappa_2$.
adamc@655	563
adamc@530	564 $$\infer{\Gamma \vdash (c) :: \kappa :: \kappa}{
adamc@530	565 \Gamma \vdash c :: \kappa
adamc@530	566 }
adamc@530	567 \quad \infer{\Gamma \vdash x :: \kappa}{
adamc@530	568 x :: \kappa \in \Gamma
adamc@530	569 }
adamc@530	570 \quad \infer{\Gamma \vdash x :: \kappa}{
adamc@530	571 x :: \kappa = c \in \Gamma
adamc@530	572 }$$
adamc@530	573
adamc@530	574 $$\infer{\Gamma \vdash M.x :: \kappa}{
adamc@537	575 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537	576 & \mt{proj}(M, \overline{s}, \mt{con} \; x) = \kappa
adamc@530	577 }
adamc@530	578 \quad \infer{\Gamma \vdash M.x :: \kappa}{
adamc@537	579 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537	580 & \mt{proj}(M, \overline{s}, \mt{con} \; x) = (\kappa, c)
adamc@530	581 }$$
adamc@530	582
adamc@530	583 $$\infer{\Gamma \vdash \tau_1 \to \tau_2 :: \mt{Type}}{
adamc@530	584 \Gamma \vdash \tau_1 :: \mt{Type}
adamc@530	585 & \Gamma \vdash \tau_2 :: \mt{Type}
adamc@530	586 }
adamc@530	587 \quad \infer{\Gamma \vdash x \; ? \: \kappa \to \tau :: \mt{Type}}{
adamc@530	588 \Gamma, x :: \kappa \vdash \tau :: \mt{Type}
adamc@530	589 }
adamc@655	590 \quad \infer{\Gamma \vdash X \longrightarrow \tau :: \mt{Type}}{
adamc@655	591 \Gamma, X \vdash \tau :: \mt{Type}
adamc@655	592 }
adamc@530	593 \quad \infer{\Gamma \vdash \$c :: \mt{Type}}{
adamc@530	594 \Gamma \vdash c :: \{\mt{Type}\}
adamc@530	595 }$$
adamc@530	596
adamc@530	597 $$\infer{\Gamma \vdash c_1 \; c_2 :: \kappa_2}{
adamc@530	598 \Gamma \vdash c_1 :: \kappa_1 \to \kappa_2
adamc@530	599 & \Gamma \vdash c_2 :: \kappa_1
adamc@530	600 }
adamc@530	601 \quad \infer{\Gamma \vdash \lambda x \; :: \; \kappa_1 \Rightarrow c :: \kappa_1 \to \kappa_2}{
adamc@530	602 \Gamma, x :: \kappa_1 \vdash c :: \kappa_2
adamc@530	603 }$$
adamc@530	604
adamc@655	605 $$\infer{\Gamma \vdash c[\kappa'] :: [X \mapsto \kappa']\kappa}{
adamc@655	606 \Gamma \vdash c :: X \to \kappa
adamc@655	607 & \Gamma \vdash \kappa'
adamc@655	608 }
adamc@655	609 \quad \infer{\Gamma \vdash X \Longrightarrow c :: X \to \kappa}{
adamc@655	610 \Gamma, X \vdash c :: \kappa
adamc@655	611 }$$
adamc@655	612
adamc@530	613 $$\infer{\Gamma \vdash () :: \mt{Unit}}{}
adamc@530	614 \quad \infer{\Gamma \vdash \#X :: \mt{Name}}{}$$
adamc@530	615
adamc@530	616 $$\infer{\Gamma \vdash [\overline{c_i = c'_i}] :: \{\kappa\}}{
adamc@530	617 \forall i: \Gamma \vdash c_i : \mt{Name}
adamc@530	618 & \Gamma \vdash c'_i :: \kappa
adamc@530	619 & \forall i \neq j: \Gamma \vdash c_i \sim c_j
adamc@530	620 }
adamc@530	621 \quad \infer{\Gamma \vdash c_1 \rc c_2 :: \{\kappa\}}{
adamc@530	622 \Gamma \vdash c_1 :: \{\kappa\}
adamc@530	623 & \Gamma \vdash c_2 :: \{\kappa\}
adamc@530	624 & \Gamma \vdash c_1 \sim c_2
adamc@530	625 }$$
adamc@530	626
adamc@655	627 $$\infer{\Gamma \vdash \mt{map} :: (\kappa_1 \to \kappa_2) \to \{\kappa_1\} \to \{\kappa_2\}}{}$$
adamc@530	628
adamc@573	629 $$\infer{\Gamma \vdash (\overline c) :: (\kappa_1 \times \ldots \times \kappa_n)}{
adamc@573	630 \forall i: \Gamma \vdash c_i :: \kappa_i
adamc@530	631 }
adamc@573	632 \quad \infer{\Gamma \vdash c.i :: \kappa_i}{
adamc@573	633 \Gamma \vdash c :: (\kappa_1 \times \ldots \times \kappa_n)
adamc@530	634 }$$
adamc@530	635
adamc@655	636 $$\infer{\Gamma \vdash \lambda [c_1 \sim c_2] \Rightarrow \tau :: \mt{Type}}{
adamc@655	637 \Gamma \vdash c_1 :: \{\kappa\}
adamc@530	638 & \Gamma \vdash c_2 :: \{\kappa'\}
adamc@655	639 & \Gamma, c_1 \sim c_2 \vdash \tau :: \mt{Type}
adamc@530	640 }$$
adamc@530	641
adamc@531	642 \subsection{Record Disjointness}
adamc@531	643
adamc@531	644 $$\infer{\Gamma \vdash c_1 \sim c_2}{
adamc@558	645 \Gamma \vdash c_1 \hookrightarrow C_1
adamc@558	646 & \Gamma \vdash c_2 \hookrightarrow C_2
adamc@558	647 & \forall c'_1 \in C_1, c'_2 \in C_2: \Gamma \vdash c'_1 \sim c'_2
adamc@531	648 }
adamc@531	649 \quad \infer{\Gamma \vdash X \sim X'}{
adamc@531	650 X \neq X'
adamc@531	651 }$$
adamc@531	652
adamc@531	653 $$\infer{\Gamma \vdash c_1 \sim c_2}{
adamc@531	654 c'_1 \sim c'_2 \in \Gamma
adamc@558	655 & \Gamma \vdash c'_1 \hookrightarrow C_1
adamc@558	656 & \Gamma \vdash c'_2 \hookrightarrow C_2
adamc@558	657 & c_1 \in C_1
adamc@558	658 & c_2 \in C_2
adamc@531	659 }$$
adamc@531	660
adamc@531	661 $$\infer{\Gamma \vdash c \hookrightarrow \{c\}}{}
adamc@531	662 \quad \infer{\Gamma \vdash [\overline{c = c'}] \hookrightarrow \{\overline{c}\}}{}
adamc@531	663 \quad \infer{\Gamma \vdash c_1 \rc c_2 \hookrightarrow C_1 \cup C_2}{
adamc@531	664 \Gamma \vdash c_1 \hookrightarrow C_1
adamc@531	665 & \Gamma \vdash c_2 \hookrightarrow C_2
adamc@531	666 }
adamc@531	667 \quad \infer{\Gamma \vdash c \hookrightarrow C}{
adamc@531	668 \Gamma \vdash c \equiv c'
adamc@531	669 & \Gamma \vdash c' \hookrightarrow C
adamc@531	670 }
adamc@531	671 \quad \infer{\Gamma \vdash \mt{map} \; f \; c \hookrightarrow C}{
adamc@531	672 \Gamma \vdash c \hookrightarrow C
adamc@531	673 }$$
adamc@531	674
adamc@541	675 \subsection{\label{definitional}Definitional Equality}
adamc@532	676
adamc@655	677 We use $\mathcal C$ to stand for a one-hole context that, when filled, yields a constructor. The notation $\mathcal C[c]$ plugs $c$ into $\mathcal C$. We omit the standard definition of one-hole contexts. We write $[x \mapsto c_1]c_2$ for capture-avoiding substitution of $c_1$ for $x$ in $c_2$, with analogous notation for substituting a kind in a constructor.
adamc@532	678
adamc@532	679 $$\infer{\Gamma \vdash c \equiv c}{}
adamc@532	680 \quad \infer{\Gamma \vdash c_1 \equiv c_2}{
adamc@532	681 \Gamma \vdash c_2 \equiv c_1
adamc@532	682 }
adamc@532	683 \quad \infer{\Gamma \vdash c_1 \equiv c_3}{
adamc@532	684 \Gamma \vdash c_1 \equiv c_2
adamc@532	685 & \Gamma \vdash c_2 \equiv c_3
adamc@532	686 }
adamc@532	687 \quad \infer{\Gamma \vdash \mathcal C[c_1] \equiv \mathcal C[c_2]}{
adamc@532	688 \Gamma \vdash c_1 \equiv c_2
adamc@532	689 }$$
adamc@532	690
adamc@532	691 $$\infer{\Gamma \vdash x \equiv c}{
adamc@532	692 x :: \kappa = c \in \Gamma
adamc@532	693 }
adamc@532	694 \quad \infer{\Gamma \vdash M.x \equiv c}{
adamc@537	695 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537	696 & \mt{proj}(M, \overline{s}, \mt{con} \; x) = (\kappa, c)
adamc@532	697 }
adamc@532	698 \quad \infer{\Gamma \vdash (\overline c).i \equiv c_i}{}$$
adamc@532	699
adamc@532	700 $$\infer{\Gamma \vdash (\lambda x :: \kappa \Rightarrow c) \; c' \equiv [x \mapsto c'] c}{}
adamc@655	701 \quad \infer{\Gamma \vdash (X \Longrightarrow c) [\kappa] \equiv [X \mapsto \kappa] c}{}$$
adamc@655	702
adamc@655	703 $$\infer{\Gamma \vdash c_1 \rc c_2 \equiv c_2 \rc c_1}{}
adamc@532	704 \quad \infer{\Gamma \vdash c_1 \rc (c_2 \rc c_3) \equiv (c_1 \rc c_2) \rc c_3}{}$$
adamc@532	705
adamc@532	706 $$\infer{\Gamma \vdash [] \rc c \equiv c}{}
adamc@532	707 \quad \infer{\Gamma \vdash [\overline{c_1 = c'_1}] \rc [\overline{c_2 = c'_2}] \equiv [\overline{c_1 = c'_1}, \overline{c_2 = c'_2}]}{}$$
adamc@532	708
adamc@655	709 $$\infer{\Gamma \vdash \mt{map} \; f \; [] \equiv []}{}
adamc@655	710 \quad \infer{\Gamma \vdash \mt{map} \; f \; ([c_1 = c_2] \rc c) \equiv [c_1 = f \; c_2] \rc \mt{map} \; f \; c}{}$$
adamc@532	711
adamc@532	712 $$\infer{\Gamma \vdash \mt{map} \; (\lambda x \Rightarrow x) \; c \equiv c}{}
adamc@655	713 \quad \infer{\Gamma \vdash \mt{map} \; f \; (\mt{map} \; f' \; c)
adamc@655	714 \equiv \mt{map} \; (\lambda x \Rightarrow f \; (f' \; x)) \; c}{}$$
adamc@532	715
adamc@532	716 $$\infer{\Gamma \vdash \mt{map} \; f \; (c_1 \rc c_2) \equiv \mt{map} \; f \; c_1 \rc \mt{map} \; f \; c_2}{}$$
adamc@531	717
adamc@534	718 \subsection{Expression Typing}
adamc@533	719
adamc@873	720 We assume the existence of a function $T$ assigning types to literal constants. It maps integer constants to $\mt{Basis}.\mt{int}$, float constants to $\mt{Basis}.\mt{float}$, character constants to $\mt{Basis}.\mt{char}$, and string constants to $\mt{Basis}.\mt{string}$.
adamc@533	721
adamc@533	722 We also refer to a function $\mathcal I$, such that $\mathcal I(\tau)$ ``uses an oracle'' to instantiate all constructor function arguments at the beginning of $\tau$ that are marked implicit; i.e., replace $x_1 ::: \kappa_1 \to \ldots \to x_n ::: \kappa_n \to \tau$ with $[x_1 \mapsto c_1]\ldots[x_n \mapsto c_n]\tau$, where the $c_i$s are inferred and $\tau$ does not start like $x ::: \kappa \to \tau'$.
adamc@533	723
adamc@533	724 $$\infer{\Gamma \vdash e : \tau : \tau}{
adamc@533	725 \Gamma \vdash e : \tau
adamc@533	726 }
adamc@533	727 \quad \infer{\Gamma \vdash e : \tau}{
adamc@533	728 \Gamma \vdash e : \tau'
adamc@533	729 & \Gamma \vdash \tau' \equiv \tau
adamc@533	730 }
adamc@533	731 \quad \infer{\Gamma \vdash \ell : T(\ell)}{}$$
adamc@533	732
adamc@533	733 $$\infer{\Gamma \vdash x : \mathcal I(\tau)}{
adamc@533	734 x : \tau \in \Gamma
adamc@533	735 }
adamc@533	736 \quad \infer{\Gamma \vdash M.x : \mathcal I(\tau)}{
adamc@537	737 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537	738 & \mt{proj}(M, \overline{s}, \mt{val} \; x) = \tau
adamc@533	739 }
adamc@533	740 \quad \infer{\Gamma \vdash X : \mathcal I(\tau)}{
adamc@533	741 X : \tau \in \Gamma
adamc@533	742 }
adamc@533	743 \quad \infer{\Gamma \vdash M.X : \mathcal I(\tau)}{
adamc@537	744 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537	745 & \mt{proj}(M, \overline{s}, \mt{val} \; X) = \tau
adamc@533	746 }$$
adamc@533	747
adamc@533	748 $$\infer{\Gamma \vdash e_1 \; e_2 : \tau_2}{
adamc@533	749 \Gamma \vdash e_1 : \tau_1 \to \tau_2
adamc@533	750 & \Gamma \vdash e_2 : \tau_1
adamc@533	751 }
adamc@533	752 \quad \infer{\Gamma \vdash \lambda x : \tau_1 \Rightarrow e : \tau_1 \to \tau_2}{
adamc@533	753 \Gamma, x : \tau_1 \vdash e : \tau_2
adamc@533	754 }$$
adamc@533	755
adamc@533	756 $$\infer{\Gamma \vdash e [c] : [x \mapsto c]\tau}{
adamc@533	757 \Gamma \vdash e : x :: \kappa \to \tau
adamc@533	758 & \Gamma \vdash c :: \kappa
adamc@533	759 }
adamc@852	760 \quad \infer{\Gamma \vdash \lambda [x \; ? \; \kappa] \Rightarrow e : x \; ? \; \kappa \to \tau}{
adamc@533	761 \Gamma, x :: \kappa \vdash e : \tau
adamc@533	762 }$$
adamc@533	763
adamc@655	764 $$\infer{\Gamma \vdash e [\kappa] : [X \mapsto \kappa]\tau}{
adamc@655	765 \Gamma \vdash e : X \longrightarrow \tau
adamc@655	766 & \Gamma \vdash \kappa
adamc@655	767 }
adamc@655	768 \quad \infer{\Gamma \vdash X \Longrightarrow e : X \longrightarrow \tau}{
adamc@655	769 \Gamma, X \vdash e : \tau
adamc@655	770 }$$
adamc@655	771
adamc@533	772 $$\infer{\Gamma \vdash \{\overline{c = e}\} : \{\overline{c : \tau}\}}{
adamc@533	773 \forall i: \Gamma \vdash c_i :: \mt{Name}
adamc@533	774 & \Gamma \vdash e_i : \tau_i
adamc@533	775 & \forall i \neq j: \Gamma \vdash c_i \sim c_j
adamc@533	776 }
adamc@533	777 \quad \infer{\Gamma \vdash e.c : \tau}{
adamc@533	778 \Gamma \vdash e : \$([c = \tau] \rc c')
adamc@533	779 }
adamc@533	780 \quad \infer{\Gamma \vdash e_1 \rc e_2 : \$(c_1 \rc c_2)}{
adamc@533	781 \Gamma \vdash e_1 : \$c_1
adamc@533	782 & \Gamma \vdash e_2 : \$c_2
adamc@573	783 & \Gamma \vdash c_1 \sim c_2
adamc@533	784 }$$
adamc@533	785
adamc@533	786 $$\infer{\Gamma \vdash e \rcut c : \$c'}{
adamc@533	787 \Gamma \vdash e : \$([c = \tau] \rc c')
adamc@533	788 }
adamc@533	789 \quad \infer{\Gamma \vdash e \rcutM c : \$c'}{
adamc@533	790 \Gamma \vdash e : \$(c \rc c')
adamc@533	791 }$$
adamc@533	792
adamc@533	793 $$\infer{\Gamma \vdash \mt{let} \; \overline{ed} \; \mt{in} \; e \; \mt{end} : \tau}{
adamc@533	794 \Gamma \vdash \overline{ed} \leadsto \Gamma'
adamc@533	795 & \Gamma' \vdash e : \tau
adamc@533	796 }
adamc@533	797 \quad \infer{\Gamma \vdash \mt{case} \; e \; \mt{of} \; \overline{p \Rightarrow e} : \tau}{
adamc@533	798 \forall i: \Gamma \vdash p_i \leadsto \Gamma_i, \tau'
adamc@533	799 & \Gamma_i \vdash e_i : \tau
adamc@533	800 }$$
adamc@533	801
adamc@573	802 $$\infer{\Gamma \vdash \lambda [c_1 \sim c_2] \Rightarrow e : \lambda [c_1 \sim c_2] \Rightarrow \tau}{
adamc@533	803 \Gamma \vdash c_1 :: \{\kappa\}
adamc@655	804 & \Gamma \vdash c_2 :: \{\kappa'\}
adamc@533	805 & \Gamma, c_1 \sim c_2 \vdash e : \tau
adamc@662	806 }
adamc@662	807 \quad \infer{\Gamma \vdash e \; ! : \tau}{
adamc@662	808 \Gamma \vdash e : [c_1 \sim c_2] \Rightarrow \tau
adamc@662	809 & \Gamma \vdash c_1 \sim c_2
adamc@533	810 }$$
adamc@533	811
adamc@534	812 \subsection{Pattern Typing}
adamc@534	813
adamc@534	814 $$\infer{\Gamma \vdash \_ \leadsto \Gamma; \tau}{}
adamc@534	815 \quad \infer{\Gamma \vdash x \leadsto \Gamma, x : \tau; \tau}{}
adamc@534	816 \quad \infer{\Gamma \vdash \ell \leadsto \Gamma; T(\ell)}{}$$
adamc@534	817
adamc@534	818 $$\infer{\Gamma \vdash X \leadsto \Gamma; \overline{[x_i \mapsto \tau'_i]}\tau}{
adamc@534	819 X : \overline{x ::: \mt{Type}} \to \tau \in \Gamma
adamc@534	820 & \textrm{$\tau$ not a function type}
adamc@534	821 }
adamc@534	822 \quad \infer{\Gamma \vdash X \; p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau}{
adamc@534	823 X : \overline{x ::: \mt{Type}} \to \tau'' \to \tau \in \Gamma
adamc@534	824 & \Gamma \vdash p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau''
adamc@534	825 }$$
adamc@534	826
adamc@534	827 $$\infer{\Gamma \vdash M.X \leadsto \Gamma; \overline{[x_i \mapsto \tau'_i]}\tau}{
adamc@537	828 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537	829 & \mt{proj}(M, \overline{s}, \mt{val} \; X) = \overline{x ::: \mt{Type}} \to \tau
adamc@534	830 & \textrm{$\tau$ not a function type}
adamc@534	831 }$$
adamc@534	832
adamc@534	833 $$\infer{\Gamma \vdash M.X \; p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau}{
adamc@537	834 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537	835 & \mt{proj}(M, \overline{s}, \mt{val} \; X) = \overline{x ::: \mt{Type}} \to \tau'' \to \tau
adamc@534	836 & \Gamma \vdash p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau''
adamc@534	837 }$$
adamc@534	838
adamc@534	839 $$\infer{\Gamma \vdash \{\overline{x = p}\} \leadsto \Gamma_n; \{\overline{x = \tau}\}}{
adamc@534	840 \Gamma_0 = \Gamma
adamc@534	841 & \forall i: \Gamma_i \vdash p_i \leadsto \Gamma_{i+1}; \tau_i
adamc@534	842 }
adamc@534	843 \quad \infer{\Gamma \vdash \{\overline{x = p}, \ldots\} \leadsto \Gamma_n; \$([\overline{x = \tau}] \rc c)}{
adamc@534	844 \Gamma_0 = \Gamma
adamc@534	845 & \forall i: \Gamma_i \vdash p_i \leadsto \Gamma_{i+1}; \tau_i
adamc@534	846 }$$
adamc@534	847
adamc@852	848 $$\infer{\Gamma \vdash p : \tau \leadsto \Gamma'; \tau}{
adamc@852	849 \Gamma \vdash p \leadsto \Gamma'; \tau'
adamc@852	850 & \Gamma \vdash \tau' \equiv \tau
adamc@852	851 }$$
adamc@852	852
adamc@535	853 \subsection{Declaration Typing}
adamc@535	854
adamc@535	855 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}$.
adamc@535	856
adamc@655	857 This is the first judgment where we deal with constructor 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 constructor classes influence type inference.
adamc@535	858
adamc@558	859 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$.
adamc@537	860 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.
adamc@535	861
adamc@535	862 $$\infer{\Gamma \vdash \cdot \leadsto \Gamma}{}
adamc@535	863 \quad \infer{\Gamma \vdash d, \overline{d} \leadsto \Gamma''}{
adamc@535	864 \Gamma \vdash d \leadsto \Gamma'
adamc@535	865 & \Gamma' \vdash \overline{d} \leadsto \Gamma''
adamc@535	866 }$$
adamc@535	867
adamc@535	868 $$\infer{\Gamma \vdash \mt{con} \; x :: \kappa = c \leadsto \Gamma, x :: \kappa = c}{
adamc@535	869 \Gamma \vdash c :: \kappa
adamc@535	870 }
adamc@535	871 \quad \infer{\Gamma \vdash \mt{datatype} \; x \; \overline{y} = \overline{dc} \leadsto \Gamma'}{
adamc@535	872 \overline{y}; x; \Gamma, x :: \mt{Type}^{\mt{len}(\overline y)} \to \mt{Type} \vdash \overline{dc} \leadsto \Gamma'
adamc@535	873 }$$
adamc@535	874
adamc@535	875 $$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leadsto \Gamma'}{
adamc@537	876 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537	877 & \mt{proj}(M, \overline{s}, \mt{datatype} \; z) = (\overline{y}, \overline{dc})
adamc@535	878 & \overline{y}; x; \Gamma, x :: \mt{Type}^{\mt{len}(\overline y)} \to \mt{Type} = M.z \vdash \overline{dc} \leadsto \Gamma'
adamc@535	879 }$$
adamc@535	880
adamc@535	881 $$\infer{\Gamma \vdash \mt{val} \; x : \tau = e \leadsto \Gamma, x : \tau}{
adamc@535	882 \Gamma \vdash e : \tau
adamc@535	883 }$$
adamc@535	884
adamc@535	885 $$\infer{\Gamma \vdash \mt{val} \; \mt{rec} \; \overline{x : \tau = e} \leadsto \Gamma, \overline{x : \tau}}{
adamc@535	886 \forall i: \Gamma, \overline{x : \tau} \vdash e_i : \tau_i
adamc@535	887 & \textrm{$e_i$ starts with an expression $\lambda$, optionally preceded by constructor and disjointness $\lambda$s}
adamc@535	888 }$$
adamc@535	889
adamc@535	890 $$\infer{\Gamma \vdash \mt{structure} \; X : S = M \leadsto \Gamma, X : S}{
adamc@535	891 \Gamma \vdash M : S
adamc@558	892 & \textrm{ $M$ not a constant or application}
adamc@535	893 }
adamc@558	894 \quad \infer{\Gamma \vdash \mt{structure} \; X : S = M \leadsto \Gamma, X : \mt{selfify}(X, \overline{s})}{
adamc@558	895 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@539	896 }$$
adamc@539	897
adamc@539	898 $$\infer{\Gamma \vdash \mt{signature} \; X = S \leadsto \Gamma, X = S}{
adamc@535	899 \Gamma \vdash S
adamc@535	900 }$$
adamc@535	901
adamc@537	902 $$\infer{\Gamma \vdash \mt{open} \; M \leadsto \Gamma, \mathcal O(M, \overline{s})}{
adamc@537	903 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@535	904 }$$
adamc@535	905
adamc@535	906 $$\infer{\Gamma \vdash \mt{constraint} \; c_1 \sim c_2 \leadsto \Gamma}{
adamc@535	907 \Gamma \vdash c_1 :: \{\kappa\}
adamc@535	908 & \Gamma \vdash c_2 :: \{\kappa\}
adamc@535	909 & \Gamma \vdash c_1 \sim c_2
adamc@535	910 }
adamc@537	911 \quad \infer{\Gamma \vdash \mt{open} \; \mt{constraints} \; M \leadsto \Gamma, \mathcal O_c(M, \overline{s})}{
adamc@537	912 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@535	913 }$$
adamc@535	914
adamc@784	915 $$\infer{\Gamma \vdash \mt{table} \; x : c \leadsto \Gamma, x : \mt{Basis}.\mt{sql\_table} \; c \; []}{
adamc@535	916 \Gamma \vdash c :: \{\mt{Type}\}
adamc@535	917 }
adamc@784	918 \quad \infer{\Gamma \vdash \mt{view} \; x : c \leadsto \Gamma, x : \mt{Basis}.\mt{sql\_view} \; c}{
adamc@784	919 \Gamma \vdash c :: \{\mt{Type}\}
adamc@784	920 }$$
adamc@784	921
adamc@784	922 $$\infer{\Gamma \vdash \mt{sequence} \; x \leadsto \Gamma, x : \mt{Basis}.\mt{sql\_sequence}}{}$$
adamc@535	923
adamc@535	924 $$\infer{\Gamma \vdash \mt{cookie} \; x : \tau \leadsto \Gamma, x : \mt{Basis}.\mt{http\_cookie} \; \tau}{
adamc@535	925 \Gamma \vdash \tau :: \mt{Type}
adamc@784	926 }
adamc@784	927 \quad \infer{\Gamma \vdash \mt{style} \; x \leadsto \Gamma, x : \mt{Basis}.\mt{css\_class}}{}$$
adamc@535	928
adamc@1085	929 $$\infer{\Gamma \vdash \mt{task} \; e_1 = e_2 \leadsto \Gamma}{
adamc@1085	930 \Gamma \vdash e_1 :: \mt{Basis}.\mt{task\_kind}
adamc@1085	931 & \Gamma \vdash e_2 :: \mt{Basis}.\mt{transaction} \; \{\}
adamc@1085	932 }$$
adamc@1085	933
adamc@784	934 $$\infer{\Gamma \vdash \mt{class} \; x :: \kappa = c \leadsto \Gamma, x :: \kappa = c}{
adamc@784	935 \Gamma \vdash c :: \kappa
adamc@535	936 }$$
adamc@535	937
adamc@535	938 $$\infer{\overline{y}; x; \Gamma \vdash \cdot \leadsto \Gamma}{}
adamc@535	939 \quad \infer{\overline{y}; x; \Gamma \vdash X \mid \overline{dc} \leadsto \Gamma', X : \overline{y ::: \mt{Type}} \to x \; \overline{y}}{
adamc@535	940 \overline{y}; x; \Gamma \vdash \overline{dc} \leadsto \Gamma'
adamc@535	941 }
adamc@535	942 \quad \infer{\overline{y}; x; \Gamma \vdash X \; \mt{of} \; \tau \mid \overline{dc} \leadsto \Gamma', X : \overline{y ::: \mt{Type}} \to \tau \to x \; \overline{y}}{
adamc@535	943 \overline{y}; x; \Gamma \vdash \overline{dc} \leadsto \Gamma'
adamc@535	944 }$$
adamc@535	945
adamc@537	946 \subsection{Signature Item Typing}
adamc@537	947
adamc@537	948 We appeal to a signature item analogue of the $\mathcal O$ function from the last subsection.
adamc@537	949
adamc@537	950 $$\infer{\Gamma \vdash \cdot \leadsto \Gamma}{}
adamc@537	951 \quad \infer{\Gamma \vdash s, \overline{s} \leadsto \Gamma''}{
adamc@537	952 \Gamma \vdash s \leadsto \Gamma'
adamc@537	953 & \Gamma' \vdash \overline{s} \leadsto \Gamma''
adamc@537	954 }$$
adamc@537	955
adamc@537	956 $$\infer{\Gamma \vdash \mt{con} \; x :: \kappa \leadsto \Gamma, x :: \kappa}{}
adamc@537	957 \quad \infer{\Gamma \vdash \mt{con} \; x :: \kappa = c \leadsto \Gamma, x :: \kappa = c}{
adamc@537	958 \Gamma \vdash c :: \kappa
adamc@537	959 }
adamc@537	960 \quad \infer{\Gamma \vdash \mt{datatype} \; x \; \overline{y} = \overline{dc} \leadsto \Gamma'}{
adamc@537	961 \overline{y}; x; \Gamma, x :: \mt{Type}^{\mt{len}(\overline y)} \to \mt{Type} \vdash \overline{dc} \leadsto \Gamma'
adamc@537	962 }$$
adamc@537	963
adamc@537	964 $$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leadsto \Gamma'}{
adamc@537	965 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537	966 & \mt{proj}(M, \overline{s}, \mt{datatype} \; z) = (\overline{y}, \overline{dc})
adamc@537	967 & \overline{y}; x; \Gamma, x :: \mt{Type}^{\mt{len}(\overline y)} \to \mt{Type} = M.z \vdash \overline{dc} \leadsto \Gamma'
adamc@537	968 }$$
adamc@537	969
adamc@537	970 $$\infer{\Gamma \vdash \mt{val} \; x : \tau \leadsto \Gamma, x : \tau}{
adamc@537	971 \Gamma \vdash \tau :: \mt{Type}
adamc@537	972 }$$
adamc@537	973
adamc@537	974 $$\infer{\Gamma \vdash \mt{structure} \; X : S \leadsto \Gamma, X : S}{
adamc@537	975 \Gamma \vdash S
adamc@537	976 }
adamc@537	977 \quad \infer{\Gamma \vdash \mt{signature} \; X = S \leadsto \Gamma, X = S}{
adamc@537	978 \Gamma \vdash S
adamc@537	979 }$$
adamc@537	980
adamc@537	981 $$\infer{\Gamma \vdash \mt{include} \; S \leadsto \Gamma, \mathcal O(\overline{s})}{
adamc@537	982 \Gamma \vdash S
adamc@537	983 & \Gamma \vdash S \equiv \mt{sig} \; \overline{s} \; \mt{end}
adamc@537	984 }$$
adamc@537	985
adamc@537	986 $$\infer{\Gamma \vdash \mt{constraint} \; c_1 \sim c_2 \leadsto \Gamma, c_1 \sim c_2}{
adamc@537	987 \Gamma \vdash c_1 :: \{\kappa\}
adamc@537	988 & \Gamma \vdash c_2 :: \{\kappa\}
adamc@537	989 }$$
adamc@537	990
adamc@784	991 $$\infer{\Gamma \vdash \mt{class} \; x :: \kappa = c \leadsto \Gamma, x :: \kappa = c}{
adamc@784	992 \Gamma \vdash c :: \kappa
adamc@537	993 }
adamc@784	994 \quad \infer{\Gamma \vdash \mt{class} \; x :: \kappa \leadsto \Gamma, x :: \kappa}{}$$
adamc@537	995
adamc@536	996 \subsection{Signature Compatibility}
adamc@536	997
adamc@558	998 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.
adamc@537	999
adamc@537	1000 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.
adamc@537	1001
adamc@536	1002 $$\infer{\Gamma \vdash S \equiv S}{}
adamc@536	1003 \quad \infer{\Gamma \vdash S_1 \equiv S_2}{
adamc@536	1004 \Gamma \vdash S_2 \equiv S_1
adamc@536	1005 }
adamc@536	1006 \quad \infer{\Gamma \vdash X \equiv S}{
adamc@536	1007 X = S \in \Gamma
adamc@536	1008 }
adamc@536	1009 \quad \infer{\Gamma \vdash M.X \equiv S}{
adamc@537	1010 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537	1011 & \mt{proj}(M, \overline{s}, \mt{signature} \; X) = S
adamc@536	1012 }$$
adamc@536	1013
adamc@536	1014 $$\infer{\Gamma \vdash S \; \mt{where} \; \mt{con} \; x = c \equiv \mt{sig} \; \overline{s^1} \; \mt{con} \; x :: \kappa = c \; \overline{s_2} \; \mt{end}}{
adamc@536	1015 \Gamma \vdash S \equiv \mt{sig} \; \overline{s^1} \; \mt{con} \; x :: \kappa \; \overline{s_2} \; \mt{end}
adamc@536	1016 & \Gamma \vdash c :: \kappa
adamc@537	1017 }
adamc@537	1018 \quad \infer{\Gamma \vdash \mt{sig} \; \overline{s^1} \; \mt{include} \; S \; \overline{s^2} \; \mt{end} \equiv \mt{sig} \; \overline{s^1} \; \overline{s} \; \overline{s^2} \; \mt{end}}{
adamc@537	1019 \Gamma \vdash S \equiv \mt{sig} \; \overline{s} \; \mt{end}
adamc@536	1020 }$$
adamc@536	1021
adamc@536	1022 $$\infer{\Gamma \vdash S_1 \leq S_2}{
adamc@536	1023 \Gamma \vdash S_1 \equiv S_2
adamc@536	1024 }
adamc@536	1025 \quad \infer{\Gamma \vdash \mt{sig} \; \overline{s} \; \mt{end} \leq \mt{sig} \; \mt{end}}{}
adamc@537	1026 \quad \infer{\Gamma \vdash \mt{sig} \; \overline{s} \; \mt{end} \leq \mt{sig} \; s' \; \overline{s'} \; \mt{end}}{
adamc@537	1027 \Gamma \vdash \overline{s} \leq s'
adamc@537	1028 & \Gamma \vdash s' \leadsto \Gamma'
adamc@537	1029 & \Gamma' \vdash \mt{sig} \; \overline{s} \; \mt{end} \leq \mt{sig} \; \overline{s'} \; \mt{end}
adamc@537	1030 }$$
adamc@537	1031
adamc@537	1032 $$\infer{\Gamma \vdash s \; \overline{s} \leq s'}{
adamc@537	1033 \Gamma \vdash s \leq s'
adamc@537	1034 }
adamc@537	1035 \quad \infer{\Gamma \vdash s \; \overline{s} \leq s'}{
adamc@537	1036 \Gamma \vdash s \leadsto \Gamma'
adamc@537	1037 & \Gamma' \vdash \overline{s} \leq s'
adamc@536	1038 }$$
adamc@536	1039
adamc@536	1040 $$\infer{\Gamma \vdash \mt{functor} (X : S_1) : S_2 \leq \mt{functor} (X : S'_1) : S'_2}{
adamc@536	1041 \Gamma \vdash S'_1 \leq S_1
adamc@536	1042 & \Gamma, X : S'_1 \vdash S_2 \leq S'_2
adamc@536	1043 }$$
adamc@536	1044
adamc@537	1045 $$\infer{\Gamma \vdash \mt{con} \; x :: \kappa \leq \mt{con} \; x :: \kappa}{}
adamc@537	1046 \quad \infer{\Gamma \vdash \mt{con} \; x :: \kappa = c \leq \mt{con} \; x :: \kappa}{}
adamc@558	1047 \quad \infer{\Gamma \vdash \mt{datatype} \; x \; \overline{y} = \overline{dc} \leq \mt{con} \; x :: \mt{Type}^{\mt{len}(\overline y)} \to \mt{Type}}{}$$
adamc@537	1048
adamc@537	1049 $$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leq \mt{con} \; x :: \mt{Type}^{\mt{len}(y)} \to \mt{Type}}{
adamc@537	1050 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537	1051 & \mt{proj}(M, \overline{s}, \mt{datatype} \; z) = (\overline{y}, \overline{dc})
adamc@537	1052 }$$
adamc@537	1053
adamc@784	1054 $$\infer{\Gamma \vdash \mt{class} \; x :: \kappa \leq \mt{con} \; x :: \kappa}{}
adamc@784	1055 \quad \infer{\Gamma \vdash \mt{class} \; x :: \kappa = c \leq \mt{con} \; x :: \kappa}{}$$
adamc@537	1056
adamc@537	1057 $$\infer{\Gamma \vdash \mt{con} \; x :: \kappa = c_1 \leq \mt{con} \; x :: \mt{\kappa} = c_2}{
adamc@537	1058 \Gamma \vdash c_1 \equiv c_2
adamc@537	1059 }
adamc@784	1060 \quad \infer{\Gamma \vdash \mt{class} \; x :: \kappa = c_1 \leq \mt{con} \; x :: \kappa = c_2}{
adamc@537	1061 \Gamma \vdash c_1 \equiv c_2
adamc@537	1062 }$$
adamc@537	1063
adamc@537	1064 $$\infer{\Gamma \vdash \mt{datatype} \; x \; \overline{y} = \overline{dc} \leq \mt{datatype} \; x \; \overline{y} = \overline{dc'}}{
adamc@537	1065 \Gamma, \overline{y :: \mt{Type}} \vdash \overline{dc} \leq \overline{dc'}
adamc@537	1066 }$$
adamc@537	1067
adamc@537	1068 $$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leq \mt{datatype} \; x \; \overline{y} = \overline{dc'}}{
adamc@537	1069 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537	1070 & \mt{proj}(M, \overline{s}, \mt{datatype} \; z) = (\overline{y}, \overline{dc})
adamc@537	1071 & \Gamma, \overline{y :: \mt{Type}} \vdash \overline{dc} \leq \overline{dc'}
adamc@537	1072 }$$
adamc@537	1073
adamc@537	1074 $$\infer{\Gamma \vdash \cdot \leq \cdot}{}
adamc@537	1075 \quad \infer{\Gamma \vdash X; \overline{dc} \leq X; \overline{dc'}}{
adamc@537	1076 \Gamma \vdash \overline{dc} \leq \overline{dc'}
adamc@537	1077 }
adamc@537	1078 \quad \infer{\Gamma \vdash X \; \mt{of} \; \tau_1; \overline{dc} \leq X \; \mt{of} \; \tau_2; \overline{dc'}}{
adamc@537	1079 \Gamma \vdash \tau_1 \equiv \tau_2
adamc@537	1080 & \Gamma \vdash \overline{dc} \leq \overline{dc'}
adamc@537	1081 }$$
adamc@537	1082
adamc@537	1083 $$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leq \mt{datatype} \; x = \mt{datatype} \; M'.z'}{
adamc@537	1084 \Gamma \vdash M.z \equiv M'.z'
adamc@537	1085 }$$
adamc@537	1086
adamc@537	1087 $$\infer{\Gamma \vdash \mt{val} \; x : \tau_1 \leq \mt{val} \; x : \tau_2}{
adamc@537	1088 \Gamma \vdash \tau_1 \equiv \tau_2
adamc@537	1089 }
adamc@537	1090 \quad \infer{\Gamma \vdash \mt{structure} \; X : S_1 \leq \mt{structure} \; X : S_2}{
adamc@537	1091 \Gamma \vdash S_1 \leq S_2
adamc@537	1092 }
adamc@537	1093 \quad \infer{\Gamma \vdash \mt{signature} \; X = S_1 \leq \mt{signature} \; X = S_2}{
adamc@537	1094 \Gamma \vdash S_1 \leq S_2
adamc@537	1095 & \Gamma \vdash S_2 \leq S_1
adamc@537	1096 }$$
adamc@537	1097
adamc@537	1098 $$\infer{\Gamma \vdash \mt{constraint} \; c_1 \sim c_2 \leq \mt{constraint} \; c'_1 \sim c'_2}{
adamc@537	1099 \Gamma \vdash c_1 \equiv c'_1
adamc@537	1100 & \Gamma \vdash c_2 \equiv c'_2
adamc@537	1101 }$$
adamc@537	1102
adamc@655	1103 $$\infer{\Gamma \vdash \mt{class} \; x :: \kappa \leq \mt{class} \; x :: \kappa}{}
adamc@655	1104 \quad \infer{\Gamma \vdash \mt{class} \; x :: \kappa = c \leq \mt{class} \; x :: \kappa}{}
adamc@655	1105 \quad \infer{\Gamma \vdash \mt{class} \; x :: \kappa = c_1 \leq \mt{class} \; x :: \kappa = c_2}{
adamc@537	1106 \Gamma \vdash c_1 \equiv c_2
adamc@537	1107 }$$
adamc@537	1108
adamc@538	1109 \subsection{Module Typing}
adamc@538	1110
adamc@538	1111 We use a helper function $\mt{sigOf}$, which converts declarations and sequences of declarations into their principal signature items and sequences of signature items, respectively.
adamc@538	1112
adamc@538	1113 $$\infer{\Gamma \vdash M : S}{
adamc@538	1114 \Gamma \vdash M : S'
adamc@538	1115 & \Gamma \vdash S' \leq S
adamc@538	1116 }
adamc@538	1117 \quad \infer{\Gamma \vdash \mt{struct} \; \overline{d} \; \mt{end} : \mt{sig} \; \mt{sigOf}(\overline{d}) \; \mt{end}}{
adamc@538	1118 \Gamma \vdash \overline{d} \leadsto \Gamma'
adamc@538	1119 }
adamc@538	1120 \quad \infer{\Gamma \vdash X : S}{
adamc@538	1121 X : S \in \Gamma
adamc@538	1122 }$$
adamc@538	1123
adamc@538	1124 $$\infer{\Gamma \vdash M.X : S}{
adamc@538	1125 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@538	1126 & \mt{proj}(M, \overline{s}, \mt{structure} \; X) = S
adamc@538	1127 }$$
adamc@538	1128
adamc@538	1129 $$\infer{\Gamma \vdash M_1(M_2) : [X \mapsto M_2]S_2}{
adamc@538	1130 \Gamma \vdash M_1 : \mt{functor}(X : S_1) : S_2
adamc@538	1131 & \Gamma \vdash M_2 : S_1
adamc@538	1132 }
adamc@538	1133 \quad \infer{\Gamma \vdash \mt{functor} (X : S_1) : S_2 = M : \mt{functor} (X : S_1) : S_2}{
adamc@538	1134 \Gamma \vdash S_1
adamc@538	1135 & \Gamma, X : S_1 \vdash S_2
adamc@538	1136 & \Gamma, X : S_1 \vdash M : S_2
adamc@538	1137 }$$
adamc@538	1138
adamc@538	1139 \begin{eqnarray*}
adamc@538	1140 \mt{sigOf}(\cdot) &=& \cdot \\
adamc@538	1141 \mt{sigOf}(s \; \overline{s'}) &=& \mt{sigOf}(s) \; \mt{sigOf}(\overline{s'}) \\
adamc@538	1142 \\
adamc@538	1143 \mt{sigOf}(\mt{con} \; x :: \kappa = c) &=& \mt{con} \; x :: \kappa = c \\
adamc@538	1144 \mt{sigOf}(\mt{datatype} \; x \; \overline{y} = \overline{dc}) &=& \mt{datatype} \; x \; \overline{y} = \overline{dc} \\
adamc@538	1145 \mt{sigOf}(\mt{datatype} \; x = \mt{datatype} \; M.z) &=& \mt{datatype} \; x = \mt{datatype} \; M.z \\
adamc@538	1146 \mt{sigOf}(\mt{val} \; x : \tau = e) &=& \mt{val} \; x : \tau \\
adamc@538	1147 \mt{sigOf}(\mt{val} \; \mt{rec} \; \overline{x : \tau = e}) &=& \overline{\mt{val} \; x : \tau} \\
adamc@538	1148 \mt{sigOf}(\mt{structure} \; X : S = M) &=& \mt{structure} \; X : S \\
adamc@538	1149 \mt{sigOf}(\mt{signature} \; X = S) &=& \mt{signature} \; X = S \\
adamc@538	1150 \mt{sigOf}(\mt{open} \; M) &=& \mt{include} \; S \textrm{ (where $\Gamma \vdash M : S$)} \\
adamc@538	1151 \mt{sigOf}(\mt{constraint} \; c_1 \sim c_2) &=& \mt{constraint} \; c_1 \sim c_2 \\
adamc@538	1152 \mt{sigOf}(\mt{open} \; \mt{constraints} \; M) &=& \cdot \\
adamc@538	1153 \mt{sigOf}(\mt{table} \; x : c) &=& \mt{table} \; x : c \\
adamc@784	1154 \mt{sigOf}(\mt{view} \; x : c) &=& \mt{view} \; x : c \\
adamc@538	1155 \mt{sigOf}(\mt{sequence} \; x) &=& \mt{sequence} \; x \\
adamc@538	1156 \mt{sigOf}(\mt{cookie} \; x : \tau) &=& \mt{cookie} \; x : \tau \\
adamc@784	1157 \mt{sigOf}(\mt{style} \; x) &=& \mt{style} \; x \\
adamc@655	1158 \mt{sigOf}(\mt{class} \; x :: \kappa = c) &=& \mt{class} \; x :: \kappa = c \\
adamc@538	1159 \end{eqnarray*}
adamc@539	1160 \begin{eqnarray*}
adamc@539	1161 \mt{selfify}(M, \cdot) &=& \cdot \\
adamc@558	1162 \mt{selfify}(M, s \; \overline{s'}) &=& \mt{selfify}(M, s) \; \mt{selfify}(M, \overline{s'}) \\
adamc@539	1163 \\
adamc@539	1164 \mt{selfify}(M, \mt{con} \; x :: \kappa) &=& \mt{con} \; x :: \kappa = M.x \\
adamc@539	1165 \mt{selfify}(M, \mt{con} \; x :: \kappa = c) &=& \mt{con} \; x :: \kappa = c \\
adamc@539	1166 \mt{selfify}(M, \mt{datatype} \; x \; \overline{y} = \overline{dc}) &=& \mt{datatype} \; x \; \overline{y} = \mt{datatype} \; M.x \\
adamc@539	1167 \mt{selfify}(M, \mt{datatype} \; x = \mt{datatype} \; M'.z) &=& \mt{datatype} \; x = \mt{datatype} \; M'.z \\
adamc@539	1168 \mt{selfify}(M, \mt{val} \; x : \tau) &=& \mt{val} \; x : \tau \\
adamc@539	1169 \mt{selfify}(M, \mt{structure} \; X : S) &=& \mt{structure} \; X : \mt{selfify}(M.X, \overline{s}) \textrm{ (where $\Gamma \vdash S \equiv \mt{sig} \; \overline{s} \; \mt{end}$)} \\
adamc@539	1170 \mt{selfify}(M, \mt{signature} \; X = S) &=& \mt{signature} \; X = S \\
adamc@539	1171 \mt{selfify}(M, \mt{include} \; S) &=& \mt{include} \; S \\
adamc@539	1172 \mt{selfify}(M, \mt{constraint} \; c_1 \sim c_2) &=& \mt{constraint} \; c_1 \sim c_2 \\
adamc@655	1173 \mt{selfify}(M, \mt{class} \; x :: \kappa) &=& \mt{class} \; x :: \kappa = M.x \\
adamc@655	1174 \mt{selfify}(M, \mt{class} \; x :: \kappa = c) &=& \mt{class} \; x :: \kappa = c \\
adamc@539	1175 \end{eqnarray*}
adamc@539	1176
adamc@540	1177 \subsection{Module Projection}
adamc@540	1178
adamc@540	1179 \begin{eqnarray*}
adamc@540	1180 \mt{proj}(M, \mt{con} \; x :: \kappa \; \overline{s}, \mt{con} \; x) &=& \kappa \\
adamc@540	1181 \mt{proj}(M, \mt{con} \; x :: \kappa = c \; \overline{s}, \mt{con} \; x) &=& (\kappa, c) \\
adamc@540	1182 \mt{proj}(M, \mt{datatype} \; x \; \overline{y} = \overline{dc} \; \overline{s}, \mt{con} \; x) &=& \mt{Type}^{\mt{len}(\overline{y})} \to \mt{Type} \\
adamc@540	1183 \mt{proj}(M, \mt{datatype} \; x = \mt{datatype} \; M'.z \; \overline{s}, \mt{con} \; x) &=& (\mt{Type}^{\mt{len}(\overline{y})} \to \mt{Type}, M'.z) \textrm{ (where $\Gamma \vdash M' : \mt{sig} \; \overline{s'} \; \mt{end}$} \\
adamc@540	1184 && \textrm{and $\mt{proj}(M', \overline{s'}, \mt{datatype} \; z) = (\overline{y}, \overline{dc})$)} \\
adamc@655	1185 \mt{proj}(M, \mt{class} \; x :: \kappa \; \overline{s}, \mt{con} \; x) &=& \kappa \to \mt{Type} \\
adamc@655	1186 \mt{proj}(M, \mt{class} \; x :: \kappa = c \; \overline{s}, \mt{con} \; x) &=& (\kappa \to \mt{Type}, c) \\
adamc@540	1187 \\
adamc@540	1188 \mt{proj}(M, \mt{datatype} \; x \; \overline{y} = \overline{dc} \; \overline{s}, \mt{datatype} \; x) &=& (\overline{y}, \overline{dc}) \\
adamc@540	1189 \mt{proj}(M, \mt{datatype} \; x = \mt{datatype} \; M'.z \; \overline{s}, \mt{con} \; x) &=& \mt{proj}(M', \overline{s'}, \mt{datatype} \; z) \textrm{ (where $\Gamma \vdash M' : \mt{sig} \; \overline{s'} \; \mt{end}$)} \\
adamc@540	1190 \\
adamc@540	1191 \mt{proj}(M, \mt{val} \; x : \tau \; \overline{s}, \mt{val} \; x) &=& \tau \\
adamc@540	1192 \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}$)} \\
adamc@540	1193 \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}$)} \\
adamc@540	1194 \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}$} \\
adamc@540	1195 && \textrm{and $\mt{proj}(M', \overline{s'}, \mt{datatype} \; z = (\overline{y}, \overline{dc})$ and $X \in \overline{dc}$)} \\
adamc@540	1196 \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}$} \\
adamc@558	1197 && \textrm{and $\mt{proj}(M', \overline{s'}, \mt{datatype} \; z = (\overline{y}, \overline{dc})$ and $X \; \mt{of} \; \tau \in \overline{dc}$)} \\
adamc@540	1198 \\
adamc@540	1199 \mt{proj}(M, \mt{structure} \; X : S \; \overline{s}, \mt{structure} \; X) &=& S \\
adamc@540	1200 \\
adamc@540	1201 \mt{proj}(M, \mt{signature} \; X = S \; \overline{s}, \mt{signature} \; X) &=& S \\
adamc@540	1202 \\
adamc@540	1203 \mt{proj}(M, \mt{con} \; x :: \kappa \; \overline{s}, V) &=& [x \mapsto M.x]\mt{proj}(M, \overline{s}, V) \\
adamc@540	1204 \mt{proj}(M, \mt{con} \; x :: \kappa = c \; \overline{s}, V) &=& [x \mapsto M.x]\mt{proj}(M, \overline{s}, V) \\
adamc@540	1205 \mt{proj}(M, \mt{datatype} \; x \; \overline{y} = \overline{dc} \; \overline{s}, V) &=& [x \mapsto M.x]\mt{proj}(M, \overline{s}, V) \\
adamc@540	1206 \mt{proj}(M, \mt{datatype} \; x = \mt{datatype} \; M'.z \; \overline{s}, V) &=& [x \mapsto M.x]\mt{proj}(M, \overline{s}, V) \\
adamc@540	1207 \mt{proj}(M, \mt{val} \; x : \tau \; \overline{s}, V) &=& \mt{proj}(M, \overline{s}, V) \\
adamc@540	1208 \mt{proj}(M, \mt{structure} \; X : S \; \overline{s}, V) &=& [X \mapsto M.X]\mt{proj}(M, \overline{s}, V) \\
adamc@540	1209 \mt{proj}(M, \mt{signature} \; X = S \; \overline{s}, V) &=& [X \mapsto M.X]\mt{proj}(M, \overline{s}, V) \\
adamc@540	1210 \mt{proj}(M, \mt{include} \; S \; \overline{s}, V) &=& \mt{proj}(M, \overline{s'} \; \overline{s}, V) \textrm{ (where $\Gamma \vdash S \equiv \mt{sig} \; \overline{s'} \; \mt{end}$)} \\
adamc@540	1211 \mt{proj}(M, \mt{constraint} \; c_1 \sim c_2 \; \overline{s}, V) &=& \mt{proj}(M, \overline{s}, V) \\
adamc@655	1212 \mt{proj}(M, \mt{class} \; x :: \kappa \; \overline{s}, V) &=& [x \mapsto M.x]\mt{proj}(M, \overline{s}, V) \\
adamc@655	1213 \mt{proj}(M, \mt{class} \; x :: \kappa = c \; \overline{s}, V) &=& [x \mapsto M.x]\mt{proj}(M, \overline{s}, V) \\
adamc@540	1214 \end{eqnarray*}
adamc@540	1215
adamc@541	1216
adamc@541	1217 \section{Type Inference}
adamc@541	1218
adamc@541	1219 The Ur/Web compiler uses \emph{heuristic type inference}, with no claims of completeness with respect to the declarative specification of the last section. The rules in use seem to work well in practice. This section summarizes those rules, to help Ur programmers predict what will work and what won't.
adamc@541	1220
adamc@541	1221 \subsection{Basic Unification}
adamc@541	1222
adamc@560	1223 Type-checkers for languages based on the Hindley-Milner type discipline, like ML and Haskell, take advantage of \emph{principal typing} properties, making complete type inference relatively straightforward. Inference algorithms are traditionally implemented using type unification variables, at various points asserting equalities between types, in the process discovering the values of type variables. The Ur/Web compiler uses the same basic strategy, but the complexity of the type system rules out easy completeness.
adamc@541	1224
adamc@656	1225 Type-checking can require evaluating recursive functional programs, thanks to the type-level $\mt{map}$ operator. When a unification variable appears in such a type, the next step of computation can be undetermined. The value of that variable might be determined later, but this would be ``too late'' for the unification problems generated at the first occurrence. This is the essential source of incompleteness.
adamc@541	1226
adamc@541	1227 Nonetheless, the unification engine tends to do reasonably well. Unlike in ML, polymorphism is never inferred in definitions; it must be indicated explicitly by writing out constructor-level parameters. By writing these and other annotations, the programmer can generally get the type inference engine to do most of the type reconstruction work.
adamc@541	1228
adamc@541	1229 \subsection{Unifying Record Types}
adamc@541	1230
adamc@570	1231 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.
adamc@541	1232
adamc@656	1233 \subsection{\label{typeclasses}Constructor Classes}
adamc@541	1234
adamc@784	1235 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.
adamc@541	1236
adamc@784	1237 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.
adamc@541	1238
adamc@656	1239 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.
adamc@541	1240
adamc@656	1241 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.
adamc@541	1242
adamc@541	1243 \subsection{Reverse-Engineering Record Types}
adamc@541	1244
adamc@656	1245 It's useful to write Ur functions and functors that take record constructors as inputs, but these constructors can grow quite long, even though their values are often implied by other arguments. The compiler uses a simple heuristic to infer the values of unification variables that are mapped over, yielding known results. If the result is empty, we're done; if it's not empty, we replace a single unification variable with a new constructor formed from three new unification variables, as in $[\alpha = \beta] \rc \gamma$. This process can often be repeated to determine a unification variable fully.
adamc@541	1246
adamc@541	1247 \subsection{Implicit Arguments in Functor Applications}
adamc@541	1248
adamc@656	1249 Constructor, constraint, and constructor class witness members of structures may be omitted, when those structures are used in contexts where their assigned signatures imply how to fill in those missing members. This feature combines well with reverse-engineering to allow for uses of complicated meta-programming functors with little more code than would be necessary to invoke an untyped, ad-hoc code generator.
adamc@541	1250
adamc@541	1251
adamc@542	1252 \section{The Ur Standard Library}
adamc@542	1253
adamc@542	1254 The built-in parts of the Ur/Web standard library are described by the signature in \texttt{lib/basis.urs} in the distribution. A module $\mt{Basis}$ ascribing to that signature is available in the initial environment, and every program is implicitly prefixed by $\mt{open} \; \mt{Basis}$.
adamc@542	1255
adamc@542	1256 Additionally, other common functions that are definable within Ur are included in \texttt{lib/top.urs} and \texttt{lib/top.ur}. This $\mt{Top}$ module is also opened implicitly.
adamc@542	1257
adamc@542	1258 The idea behind Ur is to serve as the ideal host for embedded domain-specific languages. For now, however, the ``generic'' functionality is intermixed with Ur/Web-specific functionality, including in these two library modules. We hope that these generic library components have types that speak for themselves. The next section introduces the Ur/Web-specific elements. Here, we only give the type declarations from the beginning of $\mt{Basis}$.
adamc@542	1259 $$\begin{array}{l}
adamc@542	1260 \mt{type} \; \mt{int} \\
adamc@542	1261 \mt{type} \; \mt{float} \\
adamc@873	1262 \mt{type} \; \mt{char} \\
adamc@542	1263 \mt{type} \; \mt{string} \\
adamc@542	1264 \mt{type} \; \mt{time} \\
adamc@785	1265 \mt{type} \; \mt{blob} \\
adamc@542	1266 \\
adamc@542	1267 \mt{type} \; \mt{unit} = \{\} \\
adamc@542	1268 \\
adamc@542	1269 \mt{datatype} \; \mt{bool} = \mt{False} \mid \mt{True} \\
adamc@542	1270 \\
adamc@785	1271 \mt{datatype} \; \mt{option} \; \mt{t} = \mt{None} \mid \mt{Some} \; \mt{of} \; \mt{t} \\
adamc@785	1272 \\
adamc@785	1273 \mt{datatype} \; \mt{list} \; \mt{t} = \mt{Nil} \mid \mt{Cons} \; \mt{of} \; \mt{t} \times \mt{list} \; \mt{t}
adamc@542	1274 \end{array}$$
adamc@542	1275
adamc@1123	1276 The only unusual element of this list is the $\mt{blob}$ type, which stands for binary sequences. Simple blobs can be created from strings via $\mt{Basis.textBlob}$. Blobs will also be generated from HTTP file uploads.
adamc@785	1277
adamc@657	1278 Another important generic Ur element comes at the beginning of \texttt{top.urs}.
adamc@657	1279
adamc@657	1280 $$\begin{array}{l}
adamc@657	1281 \mt{con} \; \mt{folder} :: \mt{K} \longrightarrow \{\mt{K}\} \to \mt{Type} \\
adamc@657	1282 \\
adamc@657	1283 \mt{val} \; \mt{fold} : \mt{K} \longrightarrow \mt{tf} :: (\{\mt{K}\} \to \mt{Type}) \\
adamc@657	1284 \hspace{.1in} \to (\mt{nm} :: \mt{Name} \to \mt{v} :: \mt{K} \to \mt{r} :: \{\mt{K}\} \to [[\mt{nm}] \sim \mt{r}] \Rightarrow \\
adamc@657	1285 \hspace{.2in} \mt{tf} \; \mt{r} \to \mt{tf} \; ([\mt{nm} = \mt{v}] \rc \mt{r})) \\
adamc@657	1286 \hspace{.1in} \to \mt{tf} \; [] \\
adamc@657	1287 \hspace{.1in} \to \mt{r} :: \{\mt{K}\} \to \mt{folder} \; \mt{r} \to \mt{tf} \; \mt{r}
adamc@657	1288 \end{array}$$
adamc@657	1289
adamc@657	1290 For a type-level record $\mt{r}$, a $\mt{folder} \; \mt{r}$ encodes a permutation of $\mt{r}$'s elements. The $\mt{fold}$ function can be called on a $\mt{folder}$ to iterate over the elements of $\mt{r}$ in that order. $\mt{fold}$ is parameterized on a type-level function to be used to calculate the type of each intermediate result of folding. After processing a subset $\mt{r'}$ of $\mt{r}$'s entries, the type of the accumulator should be $\mt{tf} \; \mt{r'}$. The next two expression arguments to $\mt{fold}$ are the usual step function and initial accumulator, familiar from fold functions over lists. The final two arguments are the record to fold over and a $\mt{folder}$ for it.
adamc@657	1291
adamc@664	1292 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.
adamc@657	1293
adamc@542	1294
adamc@542	1295 \section{The Ur/Web Standard Library}
adamc@542	1296
adamc@658	1297 \subsection{Monads}
adamc@658	1298
adamc@658	1299 The Ur Basis defines the monad constructor class from Haskell.
adamc@658	1300
adamc@658	1301 $$\begin{array}{l}
adamc@658	1302 \mt{class} \; \mt{monad} :: \mt{Type} \to \mt{Type} \\
adamc@658	1303 \mt{val} \; \mt{return} : \mt{m} ::: (\mt{Type} \to \mt{Type}) \to \mt{t} ::: \mt{Type} \\
adamc@658	1304 \hspace{.1in} \to \mt{monad} \; \mt{m} \\
adamc@658	1305 \hspace{.1in} \to \mt{t} \to \mt{m} \; \mt{t} \\
adamc@658	1306 \mt{val} \; \mt{bind} : \mt{m} ::: (\mt{Type} \to \mt{Type}) \to \mt{t1} ::: \mt{Type} \to \mt{t2} ::: \mt{Type} \\
adamc@658	1307 \hspace{.1in} \to \mt{monad} \; \mt{m} \\
adamc@658	1308 \hspace{.1in} \to \mt{m} \; \mt{t1} \to (\mt{t1} \to \mt{m} \; \mt{t2}) \\
adamc@658	1309 \hspace{.1in} \to \mt{m} \; \mt{t2}
adamc@658	1310 \end{array}$$
adamc@658	1311
adamc@542	1312 \subsection{Transactions}
adamc@542	1313
adamc@542	1314 Ur is a pure language; we use Haskell's trick to support controlled side effects. The standard library defines a monad $\mt{transaction}$, meant to stand for actions that may be undone cleanly. By design, no other kinds of actions are supported.
adamc@542	1315 $$\begin{array}{l}
adamc@542	1316 \mt{con} \; \mt{transaction} :: \mt{Type} \to \mt{Type} \\
adamc@658	1317 \mt{val} \; \mt{transaction\_monad} : \mt{monad} \; \mt{transaction}
adamc@542	1318 \end{array}$$
adamc@542	1319
adamc@1123	1320 For debugging purposes, a transactional function is provided for outputting a string on the server process' \texttt{stderr}.
adamc@1123	1321 $$\begin{array}{l}
adamc@1123	1322 \mt{val} \; \mt{debug} : \mt{string} \to \mt{transaction} \; \mt{unit}
adamc@1123	1323 \end{array}$$
adamc@1123	1324
adamc@542	1325 \subsection{HTTP}
adamc@542	1326
adamc@542	1327 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.
adamc@542	1328 $$\begin{array}{l}
adamc@786	1329 \mt{val} \; \mt{requestHeader} : \mt{string} \to \mt{transaction} \; (\mt{option} \; \mt{string}) \\
adamc@786	1330 \\
adamc@786	1331 \mt{con} \; \mt{http\_cookie} :: \mt{Type} \to \mt{Type} \\
adamc@786	1332 \mt{val} \; \mt{getCookie} : \mt{t} ::: \mt{Type} \to \mt{http\_cookie} \; \mt{t} \to \mt{transaction} \; (\mt{option} \; \mt{t}) \\
adamc@1050	1333 \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} \\
adamc@1050	1334 \mt{val} \; \mt{clearCookie} : \mt{t} ::: \mt{Type} \to \mt{http\_cookie} \; \mt{t} \to \mt{transaction} \; \mt{unit}
adamc@786	1335 \end{array}$$
adamc@786	1336
adamc@786	1337 There are also an abstract $\mt{url}$ type and functions for converting to it, based on the policy defined by \texttt{[allow\|deny] url} directives in the project file.
adamc@786	1338 $$\begin{array}{l}
adamc@786	1339 \mt{type} \; \mt{url} \\
adamc@786	1340 \mt{val} \; \mt{bless} : \mt{string} \to \mt{url} \\
adamc@786	1341 \mt{val} \; \mt{checkUrl} : \mt{string} \to \mt{option} \; \mt{url}
adamc@786	1342 \end{array}$$
adamc@786	1343 $\mt{bless}$ raises a runtime error if the string passed to it fails the URL policy.
adamc@786	1344
adamc@1085	1345 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.
adamc@1085	1346 $$\begin{array}{l}
adamc@1085	1347 \mt{val} \; \mt{currentUrl} : \mt{transaction} \; \mt{url} \\
adamc@1085	1348 \mt{val} \; \mt{url} : \mt{transaction} \; \mt{page} \to \mt{url}
adamc@1085	1349 \end{array}$$
adamc@1085	1350
adamc@1085	1351 Page generation may be interrupted at any time with a request to redirect to a particular URL instead.
adamc@1085	1352 $$\begin{array}{l}
adamc@1085	1353 \mt{val} \; \mt{redirect} : \mt{t} ::: \mt{Type} \to \mt{url} \to \mt{transaction} \; \mt{t}
adamc@1085	1354 \end{array}$$
adamc@1085	1355
adamc@786	1356 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.
adamc@786	1357 $$\begin{array}{l}
adamc@786	1358 \mt{type} \; \mt{file} \\
adamc@786	1359 \mt{val} \; \mt{fileName} : \mt{file} \to \mt{option} \; \mt{string} \\
adamc@786	1360 \mt{val} \; \mt{fileMimeType} : \mt{file} \to \mt{string} \\
adamc@786	1361 \mt{val} \; \mt{fileData} : \mt{file} \to \mt{blob}
adamc@786	1362 \end{array}$$
adamc@786	1363
adamc@786	1364 A blob can be extracted from a file and returned as the page result. There are bless and check functions for MIME types analogous to those for URLs.
adamc@786	1365 $$\begin{array}{l}
adamc@786	1366 \mt{type} \; \mt{mimeType} \\
adamc@786	1367 \mt{val} \; \mt{blessMime} : \mt{string} \to \mt{mimeType} \\
adamc@786	1368 \mt{val} \; \mt{checkMime} : \mt{string} \to \mt{option} \; \mt{mimeType} \\
adamc@786	1369 \mt{val} \; \mt{returnBlob} : \mt{t} ::: \mt{Type} \to \mt{blob} \to \mt{mimeType} \to \mt{transaction} \; \mt{t}
adamc@542	1370 \end{array}$$
adamc@542	1371
adamc@543	1372 \subsection{SQL}
adamc@543	1373
adamc@543	1374 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.
adamc@543	1375 $$\begin{array}{l}
adamc@785	1376 \mt{con} \; \mt{sql\_table} :: \{\mt{Type}\} \to \{\{\mt{Unit}\}\} \to \mt{Type}
adamc@785	1377 \end{array}$$
adamc@785	1378 The first argument to this constructor gives the names and types of a table's columns, and the second argument gives the set of valid keys. Keys are the only subsets of the columns that may be referenced as foreign keys. Each key has a name.
adamc@785	1379
adamc@785	1380 We also have the simpler type family of SQL views, which have no keys.
adamc@785	1381 $$\begin{array}{l}
adamc@785	1382 \mt{con} \; \mt{sql\_view} :: \{\mt{Type}\} \to \mt{Type}
adamc@543	1383 \end{array}$$
adamc@543	1384
adamc@785	1385 A multi-parameter type class is used to allow tables and views to be used interchangeably, with a way of extracting the set of columns from each.
adamc@785	1386 $$\begin{array}{l}
adamc@785	1387 \mt{class} \; \mt{fieldsOf} :: \mt{Type} \to \{\mt{Type}\} \to \mt{Type} \\
adamc@785	1388 \mt{val} \; \mt{fieldsOf\_table} : \mt{fs} ::: \{\mt{Type}\} \to \mt{keys} ::: \{\{\mt{Unit}\}\} \to \mt{fieldsOf} \; (\mt{sql\_table} \; \mt{fs} \; \mt{keys}) \; \mt{fs} \\
adamc@785	1389 \mt{val} \; \mt{fieldsOf\_view} : \mt{fs} ::: \{\mt{Type}\} \to \mt{fieldsOf} \; (\mt{sql\_view} \; \mt{fs}) \; \mt{fs}
adamc@785	1390 \end{array}$$
adamc@785	1391
adamc@785	1392 \subsubsection{Table Constraints}
adamc@785	1393
adamc@785	1394 Tables may be declared with constraints, such that database modifications that violate the constraints are blocked. A table may have at most one \texttt{PRIMARY KEY} constraint, which gives the subset of columns that will most often be used to look up individual rows in the table.
adamc@785	1395
adamc@785	1396 $$\begin{array}{l}
adamc@785	1397 \mt{con} \; \mt{primary\_key} :: \{\mt{Type}\} \to \{\{\mt{Unit}\}\} \to \mt{Type} \\
adamc@785	1398 \mt{val} \; \mt{no\_primary\_key} : \mt{fs} ::: \{\mt{Type}\} \to \mt{primary\_key} \; \mt{fs} \; [] \\
adamc@785	1399 \mt{val} \; \mt{primary\_key} : \mt{rest} ::: \{\mt{Type}\} \to \mt{t} ::: \mt{Type} \to \mt{key1} :: \mt{Name} \to \mt{keys} :: \{\mt{Type}\} \\
adamc@785	1400 \hspace{.1in} \to [[\mt{key1}] \sim \mt{keys}] \Rightarrow [[\mt{key1} = \mt{t}] \rc \mt{keys} \sim \mt{rest}] \\
adamc@785	1401 \hspace{.1in} \Rightarrow \$([\mt{key1} = \mt{sql\_injectable\_prim} \; \mt{t}] \rc \mt{map} \; \mt{sql\_injectable\_prim} \; \mt{keys}) \\
adamc@785	1402 \hspace{.1in} \to \mt{primary\_key} \; ([\mt{key1} = \mt{t}] \rc \mt{keys} \rc \mt{rest}) \; [\mt{Pkey} = [\mt{key1}] \rc \mt{map} \; (\lambda \_ \Rightarrow ()) \; \mt{keys}]
adamc@785	1403 \end{array}$$
adamc@785	1404 The type class $\mt{sql\_injectable\_prim}$ characterizes which types are allowed in SQL and are not $\mt{option}$ types. In SQL, a \texttt{PRIMARY KEY} constraint enforces after-the-fact that a column may not contain \texttt{NULL}s, but Ur/Web forces that information to be included in table types from the beginning. Thus, the only effect of this kind of constraint in Ur/Web is to enforce uniqueness of the given key within the table.
adamc@785	1405
adamc@785	1406 A type family stands for sets of named constraints of the remaining varieties.
adamc@785	1407 $$\begin{array}{l}
adamc@785	1408 \mt{con} \; \mt{sql\_constraints} :: \{\mt{Type}\} \to \{\{\mt{Unit}\}\} \to \mt{Type}
adamc@785	1409 \end{array}$$
adamc@785	1410 The first argument gives the column types of the table being constrained, and the second argument maps constraint names to the keys that they define. Constraints that don't define keys are mapped to ``empty keys.''
adamc@785	1411
adamc@785	1412 There is a type family of individual, unnamed constraints.
adamc@785	1413 $$\begin{array}{l}
adamc@785	1414 \mt{con} \; \mt{sql\_constraint} :: \{\mt{Type}\} \to \{\mt{Unit}\} \to \mt{Type}
adamc@785	1415 \end{array}$$
adamc@785	1416 The first argument is the same as above, and the second argument gives the key columns for just this constraint.
adamc@785	1417
adamc@785	1418 We have operations for assembling constraints into constraint sets.
adamc@785	1419 $$\begin{array}{l}
adamc@785	1420 \mt{val} \; \mt{no\_constraint} : \mt{fs} ::: \{\mt{Type}\} \to \mt{sql\_constraints} \; \mt{fs} \; [] \\
adamc@785	1421 \mt{val} \; \mt{one\_constraint} : \mt{fs} ::: \{\mt{Type}\} \to \mt{unique} ::: \{\mt{Unit}\} \to \mt{name} :: \mt{Name} \\
adamc@785	1422 \hspace{.1in} \to \mt{sql\_constraint} \; \mt{fs} \; \mt{unique} \to \mt{sql\_constraints} \; \mt{fs} \; [\mt{name} = \mt{unique}] \\
adamc@785	1423 \mt{val} \; \mt{join\_constraints} : \mt{fs} ::: \{\mt{Type}\} \to \mt{uniques1} ::: \{\{\mt{Unit}\}\} \to \mt{uniques2} ::: \{\{\mt{Unit}\}\} \to [\mt{uniques1} \sim \mt{uniques2}] \\
adamc@785	1424 \hspace{.1in} \Rightarrow \mt{sql\_constraints} \; \mt{fs} \; \mt{uniques1} \to \mt{sql\_constraints} \; \mt{fs} \; \mt{uniques2} \to \mt{sql\_constraints} \; \mt{fs} \; (\mt{uniques1} \rc \mt{uniques2})
adamc@785	1425 \end{array}$$
adamc@785	1426
adamc@785	1427 A \texttt{UNIQUE} constraint forces a set of columns to be a key, which means that no combination of column values may occur more than once in the table. The $\mt{unique1}$ and $\mt{unique}$ arguments are separated out only to ensure that empty \texttt{UNIQUE} constraints are rejected.
adamc@785	1428 $$\begin{array}{l}
adamc@785	1429 \mt{val} \; \mt{unique} : \mt{rest} ::: \{\mt{Type}\} \to \mt{t} ::: \mt{Type} \to \mt{unique1} :: \mt{Name} \to \mt{unique} :: \{\mt{Type}\} \\
adamc@785	1430 \hspace{.1in} \to [[\mt{unique1}] \sim \mt{unique}] \Rightarrow [[\mt{unique1} = \mt{t}] \rc \mt{unique} \sim \mt{rest}] \\
adamc@785	1431 \hspace{.1in} \Rightarrow \mt{sql\_constraint} \; ([\mt{unique1} = \mt{t}] \rc \mt{unique} \rc \mt{rest}) \; ([\mt{unique1}] \rc \mt{map} \; (\lambda \_ \Rightarrow ()) \; \mt{unique})
adamc@785	1432 \end{array}$$
adamc@785	1433
adamc@785	1434 A \texttt{FOREIGN KEY} constraint connects a set of local columns to a local or remote key, enforcing that the local columns always reference an existent row of the foreign key's table. A local column of type $\mt{t}$ may be linked to a foreign column of type $\mt{option} \; \mt{t}$, and vice versa. We formalize that notion with a type class.
adamc@785	1435 $$\begin{array}{l}
adamc@785	1436 \mt{class} \; \mt{linkable} :: \mt{Type} \to \mt{Type} \to \mt{Type} \\
adamc@785	1437 \mt{val} \; \mt{linkable\_same} : \mt{t} ::: \mt{Type} \to \mt{linkable} \; \mt{t} \; \mt{t} \\
adamc@785	1438 \mt{val} \; \mt{linkable\_from\_nullable} : \mt{t} ::: \mt{Type} \to \mt{linkable} \; (\mt{option} \; \mt{t}) \; \mt{t} \\
adamc@785	1439 \mt{val} \; \mt{linkable\_to\_nullable} : \mt{t} ::: \mt{Type} \to \mt{linkable} \; \mt{t} \; (\mt{option} \; \mt{t})
adamc@785	1440 \end{array}$$
adamc@785	1441
adamc@785	1442 The $\mt{matching}$ type family uses $\mt{linkable}$ to define when two keys match up type-wise.
adamc@785	1443 $$\begin{array}{l}
adamc@785	1444 \mt{con} \; \mt{matching} :: \{\mt{Type}\} \to \{\mt{Type}\} \to \mt{Type} \\
adamc@785	1445 \mt{val} \; \mt{mat\_nil} : \mt{matching} \; [] \; [] \\
adamc@785	1446 \mt{val} \; \mt{mat\_cons} : \mt{t1} ::: \mt{Type} \to \mt{rest1} ::: \{\mt{Type}\} \to \mt{t2} ::: \mt{Type} \to \mt{rest2} ::: \{\mt{Type}\} \to \mt{nm1} :: \mt{Name} \to \mt{nm2} :: \mt{Name} \\
adamc@785	1447 \hspace{.1in} \to [[\mt{nm1}] \sim \mt{rest1}] \Rightarrow [[\mt{nm2}] \sim \mt{rest2}] \Rightarrow \mt{linkable} \; \mt{t1} \; \mt{t2} \to \mt{matching} \; \mt{rest1} \; \mt{rest2} \\
adamc@785	1448 \hspace{.1in} \to \mt{matching} \; ([\mt{nm1} = \mt{t1}] \rc \mt{rest1}) \; ([\mt{nm2} = \mt{t2}] \rc \mt{rest2})
adamc@785	1449 \end{array}$$
adamc@785	1450
adamc@785	1451 SQL provides a number of different propagation modes for \texttt{FOREIGN KEY} constraints, governing what happens when a row containing a still-referenced foreign key value is deleted or modified to have a different key value. The argument of a propagation mode's type gives the local key type.
adamc@785	1452 $$\begin{array}{l}
adamc@785	1453 \mt{con} \; \mt{propagation\_mode} :: \{\mt{Type}\} \to \mt{Type} \\
adamc@785	1454 \mt{val} \; \mt{restrict} : \mt{fs} ::: \{\mt{Type}\} \to \mt{propagation\_mode} \; \mt{fs} \\
adamc@785	1455 \mt{val} \; \mt{cascade} : \mt{fs} ::: \{\mt{Type}\} \to \mt{propagation\_mode} \; \mt{fs} \\
adamc@785	1456 \mt{val} \; \mt{no\_action} : \mt{fs} ::: \{\mt{Type}\} \to \mt{propagation\_mode} \; \mt{fs} \\
adamc@785	1457 \mt{val} \; \mt{set\_null} : \mt{fs} ::: \{\mt{Type}\} \to \mt{propagation\_mode} \; (\mt{map} \; \mt{option} \; \mt{fs})
adamc@785	1458 \end{array}$$
adamc@785	1459
adamc@785	1460 Finally, we put these ingredient together to define the \texttt{FOREIGN KEY} constraint function.
adamc@785	1461 $$\begin{array}{l}
adamc@785	1462 \mt{val} \; \mt{foreign\_key} : \mt{mine1} ::: \mt{Name} \to \mt{t} ::: \mt{Type} \to \mt{mine} ::: \{\mt{Type}\} \to \mt{munused} ::: \{\mt{Type}\} \to \mt{foreign} ::: \{\mt{Type}\} \\
adamc@785	1463 \hspace{.1in} \to \mt{funused} ::: \{\mt{Type}\} \to \mt{nm} ::: \mt{Name} \to \mt{uniques} ::: \{\{\mt{Unit}\}\} \\
adamc@785	1464 \hspace{.1in} \to [[\mt{mine1}] \sim \mt{mine}] \Rightarrow [[\mt{mine1} = \mt{t}] \rc \mt{mine} \sim \mt{munused}] \Rightarrow [\mt{foreign} \sim \mt{funused}] \Rightarrow [[\mt{nm}] \sim \mt{uniques}] \\
adamc@785	1465 \hspace{.1in} \Rightarrow \mt{matching} \; ([\mt{mine1} = \mt{t}] \rc \mt{mine}) \; \mt{foreign} \\
adamc@785	1466 \hspace{.1in} \to \mt{sql\_table} \; (\mt{foreign} \rc \mt{funused}) \; ([\mt{nm} = \mt{map} \; (\lambda \_ \Rightarrow ()) \; \mt{foreign}] \rc \mt{uniques}) \\
adamc@785	1467 \hspace{.1in} \to \{\mt{OnDelete} : \mt{propagation\_mode} \; ([\mt{mine1} = \mt{t}] \rc \mt{mine}), \\
adamc@785	1468 \hspace{.2in} \mt{OnUpdate} : \mt{propagation\_mode} \; ([\mt{mine1} = \mt{t}] \rc \mt{mine})\} \\
adamc@785	1469 \hspace{.1in} \to \mt{sql\_constraint} \; ([\mt{mine1} = \mt{t}] \rc \mt{mine} \rc \mt{munused}) \; []
adamc@785	1470 \end{array}$$
adamc@785	1471
adamc@785	1472 The last kind of constraint is a \texttt{CHECK} constraint, which attaches a boolean invariant over a row's contents. It is defined using the $\mt{sql\_exp}$ type family, which we discuss in more detail below.
adamc@785	1473 $$\begin{array}{l}
adamc@785	1474 \mt{val} \; \mt{check} : \mt{fs} ::: \{\mt{Type}\} \to \mt{sql\_exp} \; [] \; [] \; \mt{fs} \; \mt{bool} \to \mt{sql\_constraint} \; \mt{fs} \; []
adamc@785	1475 \end{array}$$
adamc@785	1476
adamc@785	1477 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.
adamc@785	1478
adamc@784	1479
adamc@543	1480 \subsubsection{Queries}
adamc@543	1481
adamc@543	1482 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.
adamc@543	1483 $$\begin{array}{l}
adamc@543	1484 \mt{con} \; \mt{sql\_query} :: \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \\
adamc@543	1485 \mt{val} \; \mt{sql\_query} : \mt{tables} ::: \{\{\mt{Type}\}\} \\
adamc@543	1486 \hspace{.1in} \to \mt{selectedFields} ::: \{\{\mt{Type}\}\} \\
adamc@543	1487 \hspace{.1in} \to \mt{selectedExps} ::: \{\mt{Type}\} \\
adamc@543	1488 \hspace{.1in} \to \{\mt{Rows} : \mt{sql\_query1} \; \mt{tables} \; \mt{selectedFields} \; \mt{selectedExps}, \\
adamc@543	1489 \hspace{.2in} \mt{OrderBy} : \mt{sql\_order\_by} \; \mt{tables} \; \mt{selectedExps}, \\
adamc@543	1490 \hspace{.2in} \mt{Limit} : \mt{sql\_limit}, \\
adamc@543	1491 \hspace{.2in} \mt{Offset} : \mt{sql\_offset}\} \\
adamc@543	1492 \hspace{.1in} \to \mt{sql\_query} \; \mt{selectedFields} \; \mt{selectedExps}
adamc@543	1493 \end{array}$$
adamc@543	1494
adamc@545	1495 Queries are used by folding over their results inside transactions.
adamc@545	1496 $$\begin{array}{l}
adamc@545	1497 \mt{val} \; \mt{query} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \lambda [\mt{tables} \sim \mt{exps}] \Rightarrow \mt{state} ::: \mt{Type} \to \mt{sql\_query} \; \mt{tables} \; \mt{exps} \\
adamc@658	1498 \hspace{.1in} \to (\$(\mt{exps} \rc \mt{map} \; (\lambda \mt{fields} :: \{\mt{Type}\} \Rightarrow \$\mt{fields}) \; \mt{tables}) \\
adamc@545	1499 \hspace{.2in} \to \mt{state} \to \mt{transaction} \; \mt{state}) \\
adamc@545	1500 \hspace{.1in} \to \mt{state} \to \mt{transaction} \; \mt{state}
adamc@545	1501 \end{array}$$
adamc@545	1502
adamc@543	1503 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 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.
adamc@543	1504 $$\begin{array}{l}
adamc@543	1505 \mt{con} \; \mt{sql\_query1} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \\
adamc@543	1506 \\
adamc@543	1507 \mt{type} \; \mt{sql\_relop} \\
adamc@543	1508 \mt{val} \; \mt{sql\_union} : \mt{sql\_relop} \\
adamc@543	1509 \mt{val} \; \mt{sql\_intersect} : \mt{sql\_relop} \\
adamc@543	1510 \mt{val} \; \mt{sql\_except} : \mt{sql\_relop} \\
adamc@543	1511 \mt{val} \; \mt{sql\_relop} : \mt{tables1} ::: \{\{\mt{Type}\}\} \\
adamc@543	1512 \hspace{.1in} \to \mt{tables2} ::: \{\{\mt{Type}\}\} \\
adamc@543	1513 \hspace{.1in} \to \mt{selectedFields} ::: \{\{\mt{Type}\}\} \\
adamc@543	1514 \hspace{.1in} \to \mt{selectedExps} ::: \{\mt{Type}\} \\
adamc@543	1515 \hspace{.1in} \to \mt{sql\_relop} \\
adamc@543	1516 \hspace{.1in} \to \mt{sql\_query1} \; \mt{tables1} \; \mt{selectedFields} \; \mt{selectedExps} \\
adamc@543	1517 \hspace{.1in} \to \mt{sql\_query1} \; \mt{tables2} \; \mt{selectedFields} \; \mt{selectedExps} \\
adamc@543	1518 \hspace{.1in} \to \mt{sql\_query1} \; \mt{selectedFields} \; \mt{selectedFields} \; \mt{selectedExps}
adamc@543	1519 \end{array}$$
adamc@543	1520
adamc@543	1521 $$\begin{array}{l}
adamc@543	1522 \mt{val} \; \mt{sql\_query1} : \mt{tables} ::: \{\{\mt{Type}\}\} \\
adamc@543	1523 \hspace{.1in} \to \mt{grouped} ::: \{\{\mt{Type}\}\} \\
adamc@543	1524 \hspace{.1in} \to \mt{selectedFields} ::: \{\{\mt{Type}\}\} \\
adamc@543	1525 \hspace{.1in} \to \mt{selectedExps} ::: \{\mt{Type}\} \\
adamc@1085	1526 \hspace{.1in} \to \mt{empties} :: \{\mt{Unit}\} \\
adamc@1085	1527 \hspace{.1in} \to [\mt{empties} \sim \mt{selectedFields}] \\
adamc@1085	1528 \hspace{.1in} \Rightarrow \{\mt{Distinct} : \mt{bool}, \\
adamc@994	1529 \hspace{.2in} \mt{From} : \mt{sql\_from\_items} \; \mt{tables}, \\
adamc@543	1530 \hspace{.2in} \mt{Where} : \mt{sql\_exp} \; \mt{tables} \; [] \; [] \; \mt{bool}, \\
adamc@543	1531 \hspace{.2in} \mt{GroupBy} : \mt{sql\_subset} \; \mt{tables} \; \mt{grouped}, \\
adamc@543	1532 \hspace{.2in} \mt{Having} : \mt{sql\_exp} \; \mt{grouped} \; \mt{tables} \; [] \; \mt{bool}, \\
adamc@1085	1533 \hspace{.2in} \mt{SelectFields} : \mt{sql\_subset} \; \mt{grouped} \; (\mt{map} \; (\lambda \_ \Rightarrow []) \; \mt{empties} \rc \mt{selectedFields}), \\
adamc@658	1534 \hspace{.2in} \mt {SelectExps} : \$(\mt{map} \; (\mt{sql\_exp} \; \mt{grouped} \; \mt{tables} \; []) \; \mt{selectedExps}) \} \\
adamc@543	1535 \hspace{.1in} \to \mt{sql\_query1} \; \mt{tables} \; \mt{selectedFields} \; \mt{selectedExps}
adamc@543	1536 \end{array}$$
adamc@543	1537
adamc@543	1538 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.
adamc@543	1539 $$\begin{array}{l}
adamc@543	1540 \mt{con} \; \mt{sql\_subset} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \mt{Type} \\
adamc@543	1541 \mt{val} \; \mt{sql\_subset} : \mt{keep\_drop} :: \{(\{\mt{Type}\} \times \{\mt{Type}\})\} \\
adamc@543	1542 \hspace{.1in} \to \mt{sql\_subset} \\
adamc@658	1543 \hspace{.2in} (\mt{map} \; (\lambda \mt{fields} :: (\{\mt{Type}\} \times \{\mt{Type}\}) \Rightarrow \mt{fields}.1 \rc \mt{fields}.2)\; \mt{keep\_drop}) \\
adamc@658	1544 \hspace{.2in} (\mt{map} \; (\lambda \mt{fields} :: (\{\mt{Type}\} \times \{\mt{Type}\}) \Rightarrow \mt{fields}.1) \; \mt{keep\_drop}) \\
adamc@543	1545 \mt{val} \; \mt{sql\_subset\_all} : \mt{tables} :: \{\{\mt{Type}\}\} \to \mt{sql\_subset} \; \mt{tables} \; \mt{tables}
adamc@543	1546 \end{array}$$
adamc@543	1547
adamc@560	1548 SQL expressions are used in several places, including $\mt{SELECT}$, $\mt{WHERE}$, $\mt{HAVING}$, and $\mt{ORDER} \; \mt{BY}$ clauses. They reify a fragment of the standard SQL expression language, while making it possible to inject ``native'' Ur values in some places. The arguments to the $\mt{sql\_exp}$ type family respectively give the unrestricted-availability table fields, the table fields that may only be used in arguments to aggregate functions, the available selected expressions, and the type of the expression.
adamc@543	1549 $$\begin{array}{l}
adamc@543	1550 \mt{con} \; \mt{sql\_exp} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \to \mt{Type}
adamc@543	1551 \end{array}$$
adamc@543	1552
adamc@543	1553 Any field in scope may be converted to an expression.
adamc@543	1554 $$\begin{array}{l}
adamc@543	1555 \mt{val} \; \mt{sql\_field} : \mt{otherTabs} ::: \{\{\mt{Type}\}\} \to \mt{otherFields} ::: \{\mt{Type}\} \\
adamc@543	1556 \hspace{.1in} \to \mt{fieldType} ::: \mt{Type} \to \mt{agg} ::: \{\{\mt{Type}\}\} \\
adamc@543	1557 \hspace{.1in} \to \mt{exps} ::: \{\mt{Type}\} \\
adamc@543	1558 \hspace{.1in} \to \mt{tab} :: \mt{Name} \to \mt{field} :: \mt{Name} \\
adamc@543	1559 \hspace{.1in} \to \mt{sql\_exp} \; ([\mt{tab} = [\mt{field} = \mt{fieldType}] \rc \mt{otherFields}] \rc \mt{otherTabs}) \; \mt{agg} \; \mt{exps} \; \mt{fieldType}
adamc@543	1560 \end{array}$$
adamc@543	1561
adamc@544	1562 There is an analogous function for referencing named expressions.
adamc@544	1563 $$\begin{array}{l}
adamc@544	1564 \mt{val} \; \mt{sql\_exp} : \mt{tabs} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{t} ::: \mt{Type} \to \mt{rest} ::: \{\mt{Type}\} \to \mt{nm} :: \mt{Name} \\
adamc@544	1565 \hspace{.1in} \to \mt{sql\_exp} \; \mt{tabs} \; \mt{agg} \; ([\mt{nm} = \mt{t}] \rc \mt{rest}) \; \mt{t}
adamc@544	1566 \end{array}$$
adamc@544	1567
adamc@544	1568 Ur values of appropriate types may be injected into SQL expressions.
adamc@544	1569 $$\begin{array}{l}
adamc@786	1570 \mt{class} \; \mt{sql\_injectable\_prim} \\
adamc@786	1571 \mt{val} \; \mt{sql\_bool} : \mt{sql\_injectable\_prim} \; \mt{bool} \\
adamc@786	1572 \mt{val} \; \mt{sql\_int} : \mt{sql\_injectable\_prim} \; \mt{int} \\
adamc@786	1573 \mt{val} \; \mt{sql\_float} : \mt{sql\_injectable\_prim} \; \mt{float} \\
adamc@786	1574 \mt{val} \; \mt{sql\_string} : \mt{sql\_injectable\_prim} \; \mt{string} \\
adamc@786	1575 \mt{val} \; \mt{sql\_time} : \mt{sql\_injectable\_prim} \; \mt{time} \\
adamc@786	1576 \mt{val} \; \mt{sql\_blob} : \mt{sql\_injectable\_prim} \; \mt{blob} \\
adamc@786	1577 \mt{val} \; \mt{sql\_channel} : \mt{t} ::: \mt{Type} \to \mt{sql\_injectable\_prim} \; (\mt{channel} \; \mt{t}) \\
adamc@786	1578 \mt{val} \; \mt{sql\_client} : \mt{sql\_injectable\_prim} \; \mt{client} \\
adamc@786	1579 \\
adamc@544	1580 \mt{class} \; \mt{sql\_injectable} \\
adamc@786	1581 \mt{val} \; \mt{sql\_prim} : \mt{t} ::: \mt{Type} \to \mt{sql\_injectable\_prim} \; \mt{t} \to \mt{sql\_injectable} \; \mt{t} \\
adamc@786	1582 \mt{val} \; \mt{sql\_option\_prim} : \mt{t} ::: \mt{Type} \to \mt{sql\_injectable\_prim} \; \mt{t} \to \mt{sql\_injectable} \; (\mt{option} \; \mt{t}) \\
adamc@786	1583 \\
adamc@544	1584 \mt{val} \; \mt{sql\_inject} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{t} ::: \mt{Type} \to \mt{sql\_injectable} \; \mt{t} \\
adamc@544	1585 \hspace{.1in} \to \mt{t} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t}
adamc@544	1586 \end{array}$$
adamc@544	1587
adamc@1123	1588 Additionally, most function-free types may be injected safely, via the $\mt{serialized}$ type family.
adamc@1123	1589 $$\begin{array}{l}
adamc@1123	1590 \mt{con} \; \mt{serialized} :: \mt{Type} \to \mt{Type} \\
adamc@1123	1591 \mt{val} \; \mt{serialize} : \mt{t} ::: \mt{Type} \to \mt{t} \to \mt{serialized} \; \mt{t} \\
adamc@1123	1592 \mt{val} \; \mt{deserialize} : \mt{t} ::: \mt{Type} \to \mt{serialized} \; \mt{t} \to \mt{t} \\
adamc@1123	1593 \mt{val} \; \mt{sql\_serialized} : \mt{t} ::: \mt{Type} \to \mt{sql\_injectable\_prim} \; (\mt{serialized} \; \mt{t})
adamc@1123	1594 \end{array}$$
adamc@1123	1595
adamc@544	1596 We have the SQL nullness test, which is necessary because of the strange SQL semantics of equality in the presence of null values.
adamc@544	1597 $$\begin{array}{l}
adamc@544	1598 \mt{val} \; \mt{sql\_is\_null} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{t} ::: \mt{Type} \\
adamc@544	1599 \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; (\mt{option} \; \mt{t}) \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{bool}
adamc@544	1600 \end{array}$$
adamc@544	1601
adamc@559	1602 We have generic nullary, unary, and binary operators.
adamc@544	1603 $$\begin{array}{l}
adamc@544	1604 \mt{con} \; \mt{sql\_nfunc} :: \mt{Type} \to \mt{Type} \\
adamc@544	1605 \mt{val} \; \mt{sql\_current\_timestamp} : \mt{sql\_nfunc} \; \mt{time} \\
adamc@544	1606 \mt{val} \; \mt{sql\_nfunc} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{t} ::: \mt{Type} \\
adamc@544	1607 \hspace{.1in} \to \mt{sql\_nfunc} \; \mt{t} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} \\\end{array}$$
adamc@544	1608
adamc@544	1609 $$\begin{array}{l}
adamc@544	1610 \mt{con} \; \mt{sql\_unary} :: \mt{Type} \to \mt{Type} \to \mt{Type} \\
adamc@544	1611 \mt{val} \; \mt{sql\_not} : \mt{sql\_unary} \; \mt{bool} \; \mt{bool} \\
adamc@544	1612 \mt{val} \; \mt{sql\_unary} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{arg} ::: \mt{Type} \to \mt{res} ::: \mt{Type} \\
adamc@544	1613 \hspace{.1in} \to \mt{sql\_unary} \; \mt{arg} \; \mt{res} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{arg} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{res} \\
adamc@544	1614 \end{array}$$
adamc@544	1615
adamc@544	1616 $$\begin{array}{l}
adamc@544	1617 \mt{con} \; \mt{sql\_binary} :: \mt{Type} \to \mt{Type} \to \mt{Type} \to \mt{Type} \\
adamc@544	1618 \mt{val} \; \mt{sql\_and} : \mt{sql\_binary} \; \mt{bool} \; \mt{bool} \; \mt{bool} \\
adamc@544	1619 \mt{val} \; \mt{sql\_or} : \mt{sql\_binary} \; \mt{bool} \; \mt{bool} \; \mt{bool} \\
adamc@544	1620 \mt{val} \; \mt{sql\_binary} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{arg_1} ::: \mt{Type} \to \mt{arg_2} ::: \mt{Type} \to \mt{res} ::: \mt{Type} \\
adamc@544	1621 \hspace{.1in} \to \mt{sql\_binary} \; \mt{arg_1} \; \mt{arg_2} \; \mt{res} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{arg_1} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{arg_2} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{res}
adamc@544	1622 \end{array}$$
adamc@544	1623
adamc@544	1624 $$\begin{array}{l}
adamc@559	1625 \mt{class} \; \mt{sql\_arith} \\
adamc@559	1626 \mt{val} \; \mt{sql\_int\_arith} : \mt{sql\_arith} \; \mt{int} \\
adamc@559	1627 \mt{val} \; \mt{sql\_float\_arith} : \mt{sql\_arith} \; \mt{float} \\
adamc@559	1628 \mt{val} \; \mt{sql\_neg} : \mt{t} ::: \mt{Type} \to \mt{sql\_arith} \; \mt{t} \to \mt{sql\_unary} \; \mt{t} \; \mt{t} \\
adamc@559	1629 \mt{val} \; \mt{sql\_plus} : \mt{t} ::: \mt{Type} \to \mt{sql\_arith} \; \mt{t} \to \mt{sql\_binary} \; \mt{t} \; \mt{t} \; \mt{t} \\
adamc@559	1630 \mt{val} \; \mt{sql\_minus} : \mt{t} ::: \mt{Type} \to \mt{sql\_arith} \; \mt{t} \to \mt{sql\_binary} \; \mt{t} \; \mt{t} \; \mt{t} \\
adamc@559	1631 \mt{val} \; \mt{sql\_times} : \mt{t} ::: \mt{Type} \to \mt{sql\_arith} \; \mt{t} \to \mt{sql\_binary} \; \mt{t} \; \mt{t} \; \mt{t} \\
adamc@559	1632 \mt{val} \; \mt{sql\_div} : \mt{t} ::: \mt{Type} \to \mt{sql\_arith} \; \mt{t} \to \mt{sql\_binary} \; \mt{t} \; \mt{t} \; \mt{t} \\
adamc@559	1633 \mt{val} \; \mt{sql\_mod} : \mt{sql\_binary} \; \mt{int} \; \mt{int} \; \mt{int}
adamc@559	1634 \end{array}$$
adamc@544	1635
adamc@656	1636 Finally, we have aggregate functions. The $\mt{COUNT(\ast)}$ syntax is handled specially, since it takes no real argument. The other aggregate functions are placed into a general type family, using constructor classes to restrict usage to properly-typed arguments. The key aspect of the $\mt{sql\_aggregate}$ function's type is the shift of aggregate-function-only fields into unrestricted fields.
adamc@544	1637 $$\begin{array}{l}
adamc@544	1638 \mt{val} \; \mt{sql\_count} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{int}
adamc@544	1639 \end{array}$$
adamc@544	1640
adamc@544	1641 $$\begin{array}{l}
adamc@544	1642 \mt{con} \; \mt{sql\_aggregate} :: \mt{Type} \to \mt{Type} \\
adamc@544	1643 \mt{val} \; \mt{sql\_aggregate} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{t} ::: \mt{Type} \\
adamc@544	1644 \hspace{.1in} \to \mt{sql\_aggregate} \; \mt{t} \to \mt{sql\_exp} \; \mt{agg} \; \mt{agg} \; \mt{exps} \; \mt{t} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t}
adamc@544	1645 \end{array}$$
adamc@544	1646
adamc@544	1647 $$\begin{array}{l}
adamc@544	1648 \mt{class} \; \mt{sql\_summable} \\
adamc@544	1649 \mt{val} \; \mt{sql\_summable\_int} : \mt{sql\_summable} \; \mt{int} \\
adamc@544	1650 \mt{val} \; \mt{sql\_summable\_float} : \mt{sql\_summable} \; \mt{float} \\
adamc@544	1651 \mt{val} \; \mt{sql\_avg} : \mt{t} ::: \mt{Type} \to \mt{sql\_summable} \; \mt{t} \to \mt{sql\_aggregate} \; \mt{t} \\
adamc@544	1652 \mt{val} \; \mt{sql\_sum} : \mt{t} ::: \mt{Type} \to \mt{sql\_summable} \mt{t} \to \mt{sql\_aggregate} \; \mt{t}
adamc@544	1653 \end{array}$$
adamc@544	1654
adamc@544	1655 $$\begin{array}{l}
adamc@544	1656 \mt{class} \; \mt{sql\_maxable} \\
adamc@544	1657 \mt{val} \; \mt{sql\_maxable\_int} : \mt{sql\_maxable} \; \mt{int} \\
adamc@544	1658 \mt{val} \; \mt{sql\_maxable\_float} : \mt{sql\_maxable} \; \mt{float} \\
adamc@544	1659 \mt{val} \; \mt{sql\_maxable\_string} : \mt{sql\_maxable} \; \mt{string} \\
adamc@544	1660 \mt{val} \; \mt{sql\_maxable\_time} : \mt{sql\_maxable} \; \mt{time} \\
adamc@544	1661 \mt{val} \; \mt{sql\_max} : \mt{t} ::: \mt{Type} \to \mt{sql\_maxable} \; \mt{t} \to \mt{sql\_aggregate} \; \mt{t} \\
adamc@544	1662 \mt{val} \; \mt{sql\_min} : \mt{t} ::: \mt{Type} \to \mt{sql\_maxable} \; \mt{t} \to \mt{sql\_aggregate} \; \mt{t}
adamc@544	1663 \end{array}$$
adamc@544	1664
adamc@786	1665 \texttt{FROM} clauses are specified using a type family.
adamc@786	1666 $$\begin{array}{l}
adamc@786	1667 \mt{con} \; \mt{sql\_from\_items} :: \{\{\mt{Type}\}\} \to \mt{Type} \\
adamc@786	1668 \mt{val} \; \mt{sql\_from\_table} : \mt{t} ::: \mt{Type} \to \mt{fs} ::: \{\mt{Type}\} \to \mt{fieldsOf} \; \mt{t} \; \mt{fs} \to \mt{name} :: \mt{Name} \to \mt{t} \to \mt{sql\_from\_items} \; [\mt{name} = \mt{fs}] \\
adamc@786	1669 \mt{val} \; \mt{sql\_from\_comma} : \mt{tabs1} ::: \{\{\mt{Type}\}\} \to \mt{tabs2} ::: \{\{\mt{Type}\}\} \to [\mt{tabs1} \sim \mt{tabs2}] \\
adamc@786	1670 \hspace{.1in} \Rightarrow \mt{sql\_from\_items} \; \mt{tabs1} \to \mt{sql\_from\_items} \; \mt{tabs2} \\
adamc@786	1671 \hspace{.1in} \to \mt{sql\_from\_items} \; (\mt{tabs1} \rc \mt{tabs2}) \\
adamc@786	1672 \mt{val} \; \mt{sql\_inner\_join} : \mt{tabs1} ::: \{\{\mt{Type}\}\} \to \mt{tabs2} ::: \{\{\mt{Type}\}\} \to [\mt{tabs1} \sim \mt{tabs2}] \\
adamc@786	1673 \hspace{.1in} \Rightarrow \mt{sql\_from\_items} \; \mt{tabs1} \to \mt{sql\_from\_items} \; \mt{tabs2} \\
adamc@786	1674 \hspace{.1in} \to \mt{sql\_exp} \; (\mt{tabs1} \rc \mt{tabs2}) \; [] \; [] \; \mt{bool} \\
adamc@786	1675 \hspace{.1in} \to \mt{sql\_from\_items} \; (\mt{tabs1} \rc \mt{tabs2})
adamc@786	1676 \end{array}$$
adamc@786	1677
adamc@786	1678 Besides these basic cases, outer joins are supported, which requires a type class for turning non-$\mt{option}$ columns into $\mt{option}$ columns.
adamc@786	1679 $$\begin{array}{l}
adamc@786	1680 \mt{class} \; \mt{nullify} :: \mt{Type} \to \mt{Type} \to \mt{Type} \\
adamc@786	1681 \mt{val} \; \mt{nullify\_option} : \mt{t} ::: \mt{Type} \to \mt{nullify} \; (\mt{option} \; \mt{t}) \; (\mt{option} \; \mt{t}) \\
adamc@786	1682 \mt{val} \; \mt{nullify\_prim} : \mt{t} ::: \mt{Type} \to \mt{sql\_injectable\_prim} \; \mt{t} \to \mt{nullify} \; \mt{t} \; (\mt{option} \; \mt{t})
adamc@786	1683 \end{array}$$
adamc@786	1684
adamc@786	1685 Left, right, and full outer joins can now be expressed using functions that accept records of $\mt{nullify}$ instances. Here, we give only the type for a left join as an example.
adamc@786	1686
adamc@786	1687 $$\begin{array}{l}
adamc@786	1688 \mt{val} \; \mt{sql\_left\_join} : \mt{tabs1} ::: \{\{\mt{Type}\}\} \to \mt{tabs2} ::: \{\{(\mt{Type} \times \mt{Type})\}\} \to [\mt{tabs1} \sim \mt{tabs2}] \\
adamc@786	1689 \hspace{.1in} \Rightarrow \$(\mt{map} \; (\lambda \mt{r} \Rightarrow \$(\mt{map} \; (\lambda \mt{p} :: (\mt{Type} \times \mt{Type}) \Rightarrow \mt{nullify} \; \mt{p}.1 \; \mt{p}.2) \; \mt{r})) \; \mt{tabs2}) \\
adamc@786	1690 \hspace{.1in} \to \mt{sql\_from\_items} \; \mt{tabs1} \to \mt{sql\_from\_items} \; (\mt{map} \; (\mt{map} \; (\lambda \mt{p} :: (\mt{Type} \times \mt{Type}) \Rightarrow \mt{p}.1)) \; \mt{tabs2}) \\
adamc@786	1691 \hspace{.1in} \to \mt{sql\_exp} \; (\mt{tabs1} \rc \mt{map} \; (\mt{map} \; (\lambda \mt{p} :: (\mt{Type} \times \mt{Type}) \Rightarrow \mt{p}.1)) \; \mt{tabs2}) \; [] \; [] \; \mt{bool} \\
adamc@786	1692 \hspace{.1in} \to \mt{sql\_from\_items} \; (\mt{tabs1} \rc \mt{map} \; (\mt{map} \; (\lambda \mt{p} :: (\mt{Type} \times \mt{Type}) \Rightarrow \mt{p}.2)) \; \mt{tabs2})
adamc@786	1693 \end{array}$$
adamc@786	1694
adamc@544	1695 We wrap up the definition of query syntax with the types used in representing $\mt{ORDER} \; \mt{BY}$, $\mt{LIMIT}$, and $\mt{OFFSET}$ clauses.
adamc@544	1696 $$\begin{array}{l}
adamc@544	1697 \mt{type} \; \mt{sql\_direction} \\
adamc@544	1698 \mt{val} \; \mt{sql\_asc} : \mt{sql\_direction} \\
adamc@544	1699 \mt{val} \; \mt{sql\_desc} : \mt{sql\_direction} \\
adamc@544	1700 \\
adamc@544	1701 \mt{con} \; \mt{sql\_order\_by} :: \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \\
adamc@544	1702 \mt{val} \; \mt{sql\_order\_by\_Nil} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{exps} :: \{\mt{Type}\} \to \mt{sql\_order\_by} \; \mt{tables} \; \mt{exps} \\
adamc@544	1703 \mt{val} \; \mt{sql\_order\_by\_Cons} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{t} ::: \mt{Type} \\
adamc@544	1704 \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; [] \; \mt{exps} \; \mt{t} \to \mt{sql\_direction} \to \mt{sql\_order\_by} \; \mt{tables} \; \mt{exps} \to \mt{sql\_order\_by} \; \mt{tables} \; \mt{exps} \\
adamc@544	1705 \\
adamc@544	1706 \mt{type} \; \mt{sql\_limit} \\
adamc@544	1707 \mt{val} \; \mt{sql\_no\_limit} : \mt{sql\_limit} \\
adamc@544	1708 \mt{val} \; \mt{sql\_limit} : \mt{int} \to \mt{sql\_limit} \\
adamc@544	1709 \\
adamc@544	1710 \mt{type} \; \mt{sql\_offset} \\
adamc@544	1711 \mt{val} \; \mt{sql\_no\_offset} : \mt{sql\_offset} \\
adamc@544	1712 \mt{val} \; \mt{sql\_offset} : \mt{int} \to \mt{sql\_offset}
adamc@544	1713 \end{array}$$
adamc@544	1714
adamc@545	1715
adamc@545	1716 \subsubsection{DML}
adamc@545	1717
adamc@545	1718 The Ur/Web library also includes an embedding of a fragment of SQL's DML, the Data Manipulation Language, for modifying database tables. Any piece of DML may be executed in a transaction.
adamc@545	1719
adamc@545	1720 $$\begin{array}{l}
adamc@545	1721 \mt{type} \; \mt{dml} \\
adamc@545	1722 \mt{val} \; \mt{dml} : \mt{dml} \to \mt{transaction} \; \mt{unit}
adamc@545	1723 \end{array}$$
adamc@545	1724
adamc@545	1725 Properly-typed records may be used to form $\mt{INSERT}$ commands.
adamc@545	1726 $$\begin{array}{l}
adamc@545	1727 \mt{val} \; \mt{insert} : \mt{fields} ::: \{\mt{Type}\} \to \mt{sql\_table} \; \mt{fields} \\
adamc@658	1728 \hspace{.1in} \to \$(\mt{map} \; (\mt{sql\_exp} \; [] \; [] \; []) \; \mt{fields}) \to \mt{dml}
adamc@545	1729 \end{array}$$
adamc@545	1730
adamc@545	1731 An $\mt{UPDATE}$ command is formed from a choice of which table fields to leave alone and which to change, along with an expression to use to compute the new value of each changed field and a $\mt{WHERE}$ clause.
adamc@545	1732 $$\begin{array}{l}
adamc@545	1733 \mt{val} \; \mt{update} : \mt{unchanged} ::: \{\mt{Type}\} \to \mt{changed} :: \{\mt{Type}\} \to \lambda [\mt{changed} \sim \mt{unchanged}] \\
adamc@658	1734 \hspace{.1in} \Rightarrow \$(\mt{map} \; (\mt{sql\_exp} \; [\mt{T} = \mt{changed} \rc \mt{unchanged}] \; [] \; []) \; \mt{changed}) \\
adamc@545	1735 \hspace{.1in} \to \mt{sql\_table} \; (\mt{changed} \rc \mt{unchanged}) \to \mt{sql\_exp} \; [\mt{T} = \mt{changed} \rc \mt{unchanged}] \; [] \; [] \; \mt{bool} \to \mt{dml}
adamc@545	1736 \end{array}$$
adamc@545	1737
adamc@545	1738 A $\mt{DELETE}$ command is formed from a table and a $\mt{WHERE}$ clause.
adamc@545	1739 $$\begin{array}{l}
adamc@545	1740 \mt{val} \; \mt{delete} : \mt{fields} ::: \{\mt{Type}\} \to \mt{sql\_table} \; \mt{fields} \to \mt{sql\_exp} \; [\mt{T} = \mt{fields}] \; [] \; [] \; \mt{bool} \to \mt{dml}
adamc@545	1741 \end{array}$$
adamc@545	1742
adamc@546	1743 \subsubsection{Sequences}
adamc@546	1744
adamc@546	1745 SQL sequences are counters with concurrency control, often used to assign unique IDs. Ur/Web supports them via a simple interface. The only way to create a sequence is with the $\mt{sequence}$ declaration form.
adamc@546	1746
adamc@546	1747 $$\begin{array}{l}
adamc@546	1748 \mt{type} \; \mt{sql\_sequence} \\
adamc@1085	1749 \mt{val} \; \mt{nextval} : \mt{sql\_sequence} \to \mt{transaction} \; \mt{int} \\
adamc@1085	1750 \mt{val} \; \mt{setval} : \mt{sql\_sequence} \to \mt{int} \to \mt{transaction} \; \mt{unit}
adamc@546	1751 \end{array}$$
adamc@546	1752
adamc@546	1753
adamc@547	1754 \subsection{XML}
adamc@547	1755
adamc@547	1756 Ur/Web's library contains an encoding of XML syntax and semantic constraints. We make no effort to follow the standards governing XML schemas. Rather, XML fragments are viewed more as values of ML datatypes, and we only track which tags are allowed inside which other tags.
adamc@547	1757
adamc@547	1758 The basic XML type family has arguments respectively indicating the \emph{context} of a fragment, the fields that the fragment expects to be bound on entry (and their types), and the fields that the fragment will bind (and their types). Contexts are a record-based ``poor man's subtyping'' encoding, with each possible set of valid tags corresponding to a different context record. The arguments dealing with field binding are only relevant to HTML forms.
adamc@547	1759 $$\begin{array}{l}
adamc@547	1760 \mt{con} \; \mt{xml} :: \{\mt{Unit}\} \to \{\mt{Type}\} \to \{\mt{Type}\} \to \mt{Type}
adamc@547	1761 \end{array}$$
adamc@547	1762
adamc@547	1763 We also have a type family of XML tags, indexed respectively by the record of optional attributes accepted by the tag, the context in which the tag may be placed, the context required of children of the tag, which form fields the tag uses, and which fields the tag defines.
adamc@547	1764 $$\begin{array}{l}
adamc@547	1765 \mt{con} \; \mt{tag} :: \{\mt{Type}\} \to \{\mt{Unit}\} \to \{\mt{Unit}\} \to \{\mt{Type}\} \to \{\mt{Type}\} \to \mt{Type}
adamc@547	1766 \end{array}$$
adamc@547	1767
adamc@547	1768 Literal text may be injected into XML as ``CDATA.''
adamc@547	1769 $$\begin{array}{l}
adamc@547	1770 \mt{val} \; \mt{cdata} : \mt{ctx} ::: \{\mt{Unit}\} \to \mt{use} ::: \{\mt{Type}\} \to \mt{string} \to \mt{xml} \; \mt{ctx} \; \mt{use} \; []
adamc@547	1771 \end{array}$$
adamc@547	1772
adamc@547	1773 There is a function for producing an XML tree with a particular tag at its root.
adamc@547	1774 $$\begin{array}{l}
adamc@547	1775 \mt{val} \; \mt{tag} : \mt{attrsGiven} ::: \{\mt{Type}\} \to \mt{attrsAbsent} ::: \{\mt{Type}\} \to \mt{ctxOuter} ::: \{\mt{Unit}\} \to \mt{ctxInner} ::: \{\mt{Unit}\} \\
adamc@547	1776 \hspace{.1in} \to \mt{useOuter} ::: \{\mt{Type}\} \to \mt{useInner} ::: \{\mt{Type}\} \to \mt{bindOuter} ::: \{\mt{Type}\} \to \mt{bindInner} ::: \{\mt{Type}\} \\
adamc@787	1777 \hspace{.1in} \to \lambda [\mt{attrsGiven} \sim \mt{attrsAbsent}] \; [\mt{useOuter} \sim \mt{useInner}] \; [\mt{bindOuter} \sim \mt{bindInner}] \\
adamc@787	1778 \hspace{.1in} \Rightarrow \mt{option} \; \mt{css\_class} \\
adamc@787	1779 \hspace{.1in} \to \$\mt{attrsGiven} \\
adamc@547	1780 \hspace{.1in} \to \mt{tag} \; (\mt{attrsGiven} \rc \mt{attrsAbsent}) \; \mt{ctxOuter} \; \mt{ctxInner} \; \mt{useOuter} \; \mt{bindOuter} \\
adamc@547	1781 \hspace{.1in} \to \mt{xml} \; \mt{ctxInner} \; \mt{useInner} \; \mt{bindInner} \to \mt{xml} \; \mt{ctxOuter} \; (\mt{useOuter} \rc \mt{useInner}) \; (\mt{bindOuter} \rc \mt{bindInner})
adamc@547	1782 \end{array}$$
adamc@787	1783 Note that any tag may be assigned a CSS class. This is the sole way of making use of the values produced by $\mt{style}$ declarations. Ur/Web itself doesn't deal with the syntax or semantics of style sheets; they can be linked via URLs with \texttt{link} tags. However, Ur/Web does make it easy to calculate upper bounds on usage of CSS classes through program analysis.
adamc@547	1784
adamc@547	1785 Two XML fragments may be concatenated.
adamc@547	1786 $$\begin{array}{l}
adamc@547	1787 \mt{val} \; \mt{join} : \mt{ctx} ::: \{\mt{Unit}\} \to \mt{use_1} ::: \{\mt{Type}\} \to \mt{bind_1} ::: \{\mt{Type}\} \to \mt{bind_2} ::: \{\mt{Type}\} \\
adamc@547	1788 \hspace{.1in} \to \lambda [\mt{use_1} \sim \mt{bind_1}] \; [\mt{bind_1} \sim \mt{bind_2}] \\
adamc@547	1789 \hspace{.1in} \Rightarrow \mt{xml} \; \mt{ctx} \; \mt{use_1} \; \mt{bind_1} \to \mt{xml} \; \mt{ctx} \; (\mt{use_1} \rc \mt{bind_1}) \; \mt{bind_2} \to \mt{xml} \; \mt{ctx} \; \mt{use_1} \; (\mt{bind_1} \rc \mt{bind_2})
adamc@547	1790 \end{array}$$
adamc@547	1791
adamc@547	1792 Finally, any XML fragment may be updated to ``claim'' to use more form fields than it does.
adamc@547	1793 $$\begin{array}{l}
adamc@547	1794 \mt{val} \; \mt{useMore} : \mt{ctx} ::: \{\mt{Unit}\} \to \mt{use_1} ::: \{\mt{Type}\} \to \mt{use_2} ::: \{\mt{Type}\} \to \mt{bind} ::: \{\mt{Type}\} \to \lambda [\mt{use_1} \sim \mt{use_2}] \\
adamc@547	1795 \hspace{.1in} \Rightarrow \mt{xml} \; \mt{ctx} \; \mt{use_1} \; \mt{bind} \to \mt{xml} \; \mt{ctx} \; (\mt{use_1} \rc \mt{use_2}) \; \mt{bind}
adamc@547	1796 \end{array}$$
adamc@547	1797
adamc@547	1798 We will not list here the different HTML tags and related functions from the standard library. They should be easy enough to understand from the code in \texttt{basis.urs}. The set of tags in the library is not yet claimed to be complete for HTML standards.
adamc@547	1799
adamc@547	1800 One last useful function is for aborting any page generation, returning some XML as an error message. This function takes the place of some uses of a general exception mechanism.
adamc@547	1801 $$\begin{array}{l}
adamc@547	1802 \mt{val} \; \mt{error} : \mt{t} ::: \mt{Type} \to \mt{xml} \; [\mt{Body}] \; [] \; [] \to \mt{t}
adamc@547	1803 \end{array}$$
adamc@547	1804
adamc@549	1805
adamc@701	1806 \subsection{Client-Side Programming}
adamc@659	1807
adamc@701	1808 Ur/Web supports running code on web browsers, via automatic compilation to JavaScript.
adamc@701	1809
adamc@701	1810 \subsubsection{The Basics}
adamc@701	1811
adamc@701	1812 Clients can open alert dialog boxes, in the usual annoying JavaScript way.
adamc@701	1813 $$\begin{array}{l}
adamc@701	1814 \mt{val} \; \mt{alert} : \mt{string} \to \mt{transaction} \; \mt{unit}
adamc@701	1815 \end{array}$$
adamc@701	1816
adamc@701	1817 Any transaction may be run in a new thread with the $\mt{spawn}$ function.
adamc@701	1818 $$\begin{array}{l}
adamc@701	1819 \mt{val} \; \mt{spawn} : \mt{transaction} \; \mt{unit} \to \mt{transaction} \; \mt{unit}
adamc@701	1820 \end{array}$$
adamc@701	1821
adamc@701	1822 The current thread can be paused for at least a specified number of milliseconds.
adamc@701	1823 $$\begin{array}{l}
adamc@701	1824 \mt{val} \; \mt{sleep} : \mt{int} \to \mt{transaction} \; \mt{unit}
adamc@701	1825 \end{array}$$
adamc@701	1826
adamc@787	1827 A few functions are available to registers callbacks for particular error events. Respectively, they are triggered on calls to $\mt{error}$, uncaught JavaScript exceptions, failure of remote procedure calls, the severance of the connection serving asynchronous messages, or the occurrence of some other error with that connection. If no handlers are registered for a kind of error, then occurrences of that error are ignored silently.
adamc@787	1828 $$\begin{array}{l}
adamc@787	1829 \mt{val} \; \mt{onError} : (\mt{xbody} \to \mt{transaction} \; \mt{unit}) \to \mt{transaction} \; \mt{unit} \\
adamc@787	1830 \mt{val} \; \mt{onFail} : (\mt{string} \to \mt{transaction} \; \mt{unit}) \to \mt{transaction} \; \mt{unit} \\
adamc@787	1831 \mt{val} \; \mt{onConnectFail} : \mt{transaction} \; \mt{unit} \to \mt{transaction} \; \mt{unit} \\
adamc@787	1832 \mt{val} \; \mt{onDisconnect} : \mt{transaction} \; \mt{unit} \to \mt{transaction} \; \mt{unit} \\
adamc@787	1833 \mt{val} \; \mt{onServerError} : (\mt{string} \to \mt{transaction} \; \mt{unit}) \to \mt{transaction} \; \mt{unit}
adamc@787	1834 \end{array}$$
adamc@787	1835
adamc@701	1836 \subsubsection{Functional-Reactive Page Generation}
adamc@701	1837
adamc@701	1838 Most approaches to ``AJAX''-style coding involve imperative manipulation of the DOM tree representing an HTML document's structure. Ur/Web follows the \emph{functional-reactive} approach instead. Programs may allocate mutable \emph{sources} of arbitrary types, and an HTML page is effectively a pure function over the latest values of the sources. The page is not mutated directly, but rather it changes automatically as the sources are mutated.
adamc@659	1839
adamc@659	1840 $$\begin{array}{l}
adamc@659	1841 \mt{con} \; \mt{source} :: \mt{Type} \to \mt{Type} \\
adamc@659	1842 \mt{val} \; \mt{source} : \mt{t} ::: \mt{Type} \to \mt{t} \to \mt{transaction} \; (\mt{source} \; \mt{t}) \\
adamc@659	1843 \mt{val} \; \mt{set} : \mt{t} ::: \mt{Type} \to \mt{source} \; \mt{t} \to \mt{t} \to \mt{transaction} \; \mt{unit} \\
adamc@659	1844 \mt{val} \; \mt{get} : \mt{t} ::: \mt{Type} \to \mt{source} \; \mt{t} \to \mt{transaction} \; \mt{t}
adamc@659	1845 \end{array}$$
adamc@659	1846
adamc@659	1847 Pure functions over sources are represented in a monad of \emph{signals}.
adamc@659	1848
adamc@659	1849 $$\begin{array}{l}
adamc@659	1850 \mt{con} \; \mt{signal} :: \mt{Type} \to \mt{Type} \\
adamc@659	1851 \mt{val} \; \mt{signal\_monad} : \mt{monad} \; \mt{signal} \\
adamc@659	1852 \mt{val} \; \mt{signal} : \mt{t} ::: \mt{Type} \to \mt{source} \; \mt{t} \to \mt{signal} \; \mt{t}
adamc@659	1853 \end{array}$$
adamc@659	1854
adamc@659	1855 A reactive portion of an HTML page is injected with a $\mt{dyn}$ tag, which has a signal-valued attribute $\mt{Signal}$.
adamc@659	1856
adamc@659	1857 $$\begin{array}{l}
adamc@701	1858 \mt{val} \; \mt{dyn} : \mt{use} ::: \{\mt{Type}\} \to \mt{bind} ::: \{\mt{Type}\} \to \mt{unit} \\
adamc@701	1859 \hspace{.1in} \to \mt{tag} \; [\mt{Signal} = \mt{signal} \; (\mt{xml} \; \mt{body} \; \mt{use} \; \mt{bind})] \; \mt{body} \; [] \; \mt{use} \; \mt{bind}
adamc@659	1860 \end{array}$$
adamc@659	1861
adamc@701	1862 Transactions can be run on the client by including them in attributes like the $\mt{Onclick}$ attribute of $\mt{button}$, and GUI widgets like $\mt{ctextbox}$ have $\mt{Source}$ attributes that can be used to connect them to sources, so that their values can be read by code running because of, e.g., an $\mt{Onclick}$ event.
adamc@701	1863
adamc@914	1864 \subsubsection{Remote Procedure Calls}
adamc@914	1865
adamc@914	1866 Any function call may be made a client-to-server ``remote procedure call'' if the function being called needs no features that are only available to client code. To make a function call an RPC, pass that function call as the argument to $\mt{Basis.rpc}$:
adamc@914	1867
adamc@914	1868 $$\begin{array}{l}
adamc@914	1869 \mt{val} \; \mt{rpc} : \mt{t} ::: \mt{Type} \to \mt{transaction} \; \mt{t} \to \mt{transaction} \; \mt{t}
adamc@914	1870 \end{array}$$
adamc@914	1871
adamc@701	1872 \subsubsection{Asynchronous Message-Passing}
adamc@701	1873
adamc@701	1874 To support asynchronous, ``server push'' delivery of messages to clients, any client that might need to receive an asynchronous message is assigned a unique ID. These IDs may be retrieved both on the client and on the server, during execution of code related to a client.
adamc@701	1875
adamc@701	1876 $$\begin{array}{l}
adamc@701	1877 \mt{type} \; \mt{client} \\
adamc@701	1878 \mt{val} \; \mt{self} : \mt{transaction} \; \mt{client}
adamc@701	1879 \end{array}$$
adamc@701	1880
adamc@701	1881 \emph{Channels} are the means of message-passing. Each channel is created in the context of a client and belongs to that client; no other client may receive the channel's messages. Each channel type includes the type of values that may be sent over the channel. Sending and receiving are asynchronous, in the sense that a client need not be ready to receive a message right away. Rather, sent messages may queue up, waiting to be processed.
adamc@701	1882
adamc@701	1883 $$\begin{array}{l}
adamc@701	1884 \mt{con} \; \mt{channel} :: \mt{Type} \to \mt{Type} \\
adamc@701	1885 \mt{val} \; \mt{channel} : \mt{t} ::: \mt{Type} \to \mt{transaction} \; (\mt{channel} \; \mt{t}) \\
adamc@701	1886 \mt{val} \; \mt{send} : \mt{t} ::: \mt{Type} \to \mt{channel} \; \mt{t} \to \mt{t} \to \mt{transaction} \; \mt{unit} \\
adamc@701	1887 \mt{val} \; \mt{recv} : \mt{t} ::: \mt{Type} \to \mt{channel} \; \mt{t} \to \mt{transaction} \; \mt{t}
adamc@701	1888 \end{array}$$
adamc@701	1889
adamc@701	1890 The $\mt{channel}$ and $\mt{send}$ operations may only be executed on the server, and $\mt{recv}$ may only be executed on a client. Neither clients nor channels may be passed as arguments from clients to server-side functions, so persistent channels can only be maintained by storing them in the database and looking them up using the current client ID or some application-specific value as a key.
adamc@701	1891
adamc@701	1892 Clients and channels live only as long as the web browser page views that they are associated with. When a user surfs away, his client and its channels will be garbage-collected, after that user is not heard from for the timeout period. Garbage collection deletes any database row that contains a client or channel directly. Any reference to one of these types inside an $\mt{option}$ is set to $\mt{None}$ instead. Both kinds of handling have the flavor of weak pointers, and that is a useful way to think about clients and channels in the database.
adamc@701	1893
adamc@659	1894
adamc@549	1895 \section{Ur/Web Syntax Extensions}
adamc@549	1896
adamc@549	1897 Ur/Web features some syntactic shorthands for building values using the functions from the last section. This section sketches the grammar of those extensions. We write spans of syntax inside brackets to indicate that they are optional.
adamc@549	1898
adamc@549	1899 \subsection{SQL}
adamc@549	1900
adamc@786	1901 \subsubsection{\label{tables}Table Declarations}
adamc@786	1902
adamc@788	1903 $\mt{table}$ declarations may include constraints, via these grammar rules.
adamc@788	1904 $$\begin{array}{rrcll}
adamc@788	1905 \textrm{Declarations} & d &::=& \mt{table} \; x : c \; [pk[,]] \; cts \\
adamc@788	1906 \textrm{Primary key constraints} & pk &::=& \mt{PRIMARY} \; \mt{KEY} \; K \\
adamc@788	1907 \textrm{Keys} & K &::=& f \mid (f, (f,)^+) \\
adamc@788	1908 \textrm{Constraint sets} & cts &::=& \mt{CONSTRAINT} f \; ct \mid cts, cts \mid \{\{e\}\} \\
adamc@788	1909 \textrm{Constraints} & ct &::=& \mt{UNIQUE} \; K \mid \mt{CHECK} \; E \\
adamc@788	1910 &&& \mid \mt{FOREIGN} \; \mt{KEY} \; K \; \mt{REFERENCES} \; F \; (K) \; [\mt{ON} \; \mt{DELETE} \; pr] \; [\mt{ON} \; \mt{UPDATE} \; pr] \\
adamc@788	1911 \textrm{Foreign tables} & F &::=& x \mid \{\{e\}\} \\
adamc@788	1912 \textrm{Propagation modes} & pr &::=& \mt{NO} \; \mt{ACTION} \mid \mt{RESTRICT} \mid \mt{CASCADE} \mid \mt{SET} \; \mt{NULL}
adamc@788	1913 \end{array}$$
adamc@788	1914
adamc@788	1915 A signature item $\mt{table} \; \mt{x} : \mt{c}$ is actually elaborated into two signature items: $\mt{con} \; \mt{x\_hidden\_constraints} :: \{\{\mt{Unit}\}\}$ and $\mt{val} \; \mt{x} : \mt{sql\_table} \; \mt{c} \; \mt{x\_hidden\_constraints}$. This is appropriate for common cases where client code doesn't care which keys a table has. It's also possible to include constraints after a $\mt{table}$ signature item, with the same syntax as for $\mt{table}$ declarations. This may look like dependent typing, but it's just a convenience. The constraints are type-checked to determine a constructor $u$ to include in $\mt{val} \; \mt{x} : \mt{sql\_table} \; \mt{c} \; (u \rc \mt{x\_hidden\_constraints})$, and then the expressions are thrown away. Nonetheless, it can be useful for documentation purposes to include table constraint details in signatures. Note that the automatic generation of $\mt{x\_hidden\_constraints}$ leads to a kind of free subtyping with respect to which constraints are defined.
adamc@788	1916
adamc@788	1917
adamc@549	1918 \subsubsection{Queries}
adamc@549	1919
adamc@550	1920 Queries $Q$ are added to the rules for expressions $e$.
adamc@550	1921
adamc@549	1922 $$\begin{array}{rrcll}
adamc@550	1923 \textrm{Queries} & Q &::=& (q \; [\mt{ORDER} \; \mt{BY} \; (E \; [o],)^+] \; [\mt{LIMIT} \; N] \; [\mt{OFFSET} \; N]) \\
adamc@1085	1924 \textrm{Pre-queries} & q &::=& \mt{SELECT} \; [\mt{DISTINCT}] \; P \; \mt{FROM} \; F,^+ \; [\mt{WHERE} \; E] \; [\mt{GROUP} \; \mt{BY} \; p,^+] \; [\mt{HAVING} \; E] \\
adamc@1085	1925 &&& \mid q \; R \; q \mid \{\{\{e\}\}\} \\
adamc@549	1926 \textrm{Relational operators} & R &::=& \mt{UNION} \mid \mt{INTERSECT} \mid \mt{EXCEPT}
adamc@549	1927 \end{array}$$
adamc@549	1928
adamc@549	1929 $$\begin{array}{rrcll}
adamc@549	1930 \textrm{Projections} & P &::=& \ast & \textrm{all columns} \\
adamc@549	1931 &&& p,^+ & \textrm{particular columns} \\
adamc@549	1932 \textrm{Pre-projections} & p &::=& t.f & \textrm{one column from a table} \\
adamc@558	1933 &&& t.\{\{c\}\} & \textrm{a record of columns from a table (of kind $\{\mt{Type}\}$)} \\
adamc@549	1934 \textrm{Table names} & t &::=& x & \textrm{constant table name (automatically capitalized)} \\
adamc@549	1935 &&& X & \textrm{constant table name} \\
adamc@549	1936 &&& \{\{c\}\} & \textrm{computed table name (of kind $\mt{Name}$)} \\
adamc@549	1937 \textrm{Column names} & f &::=& X & \textrm{constant column name} \\
adamc@549	1938 &&& \{c\} & \textrm{computed column name (of kind $\mt{Name}$)} \\
adamc@549	1939 \textrm{Tables} & T &::=& x & \textrm{table variable, named locally by its own capitalization} \\
adamc@549	1940 &&& x \; \mt{AS} \; t & \textrm{table variable, with local name} \\
adamc@549	1941 &&& \{\{e\}\} \; \mt{AS} \; t & \textrm{computed table expression, with local name} \\
adamc@1085	1942 \textrm{$\mt{FROM}$ items} & F &::=& T \mid \{\{e\}\} \mid F \; J \; \mt{JOIN} \; F \; \mt{ON} \; E \\
adamc@1085	1943 &&& \mid F \; \mt{CROSS} \; \mt{JOIN} \ F \\
adamc@1085	1944 \textrm{Joins} & J &::=& [\mt{INNER}] \\
adamc@1085	1945 &&& \mid [\mt{LEFT} \mid \mt{RIGHT} \mid \mt{FULL}] \; [\mt{OUTER}] \\
adamc@549	1946 \textrm{SQL expressions} & E &::=& p & \textrm{column references} \\
adamc@549	1947 &&& X & \textrm{named expression references} \\
adamc@549	1948 &&& \{\{e\}\} & \textrm{injected native Ur expressions} \\
adamc@549	1949 &&& \{e\} & \textrm{computed expressions, probably using $\mt{sql\_exp}$ directly} \\
adamc@549	1950 &&& \mt{TRUE} \mid \mt{FALSE} & \textrm{boolean constants} \\
adamc@549	1951 &&& \ell & \textrm{primitive type literals} \\
adamc@549	1952 &&& \mt{NULL} & \textrm{null value (injection of $\mt{None}$)} \\
adamc@549	1953 &&& E \; \mt{IS} \; \mt{NULL} & \textrm{nullness test} \\
adamc@549	1954 &&& n & \textrm{nullary operators} \\
adamc@549	1955 &&& u \; E & \textrm{unary operators} \\
adamc@549	1956 &&& E \; b \; E & \textrm{binary operators} \\
adamc@549	1957 &&& \mt{COUNT}(\ast) & \textrm{count number of rows} \\
adamc@549	1958 &&& a(E) & \textrm{other aggregate function} \\
adamc@549	1959 &&& (E) & \textrm{explicit precedence} \\
adamc@549	1960 \textrm{Nullary operators} & n &::=& \mt{CURRENT\_TIMESTAMP} \\
adamc@549	1961 \textrm{Unary operators} & u &::=& \mt{NOT} \\
adamc@549	1962 \textrm{Binary operators} & b &::=& \mt{AND} \mid \mt{OR} \mid \neq \mid < \mid \leq \mid > \mid \geq \\
adamc@549	1963 \textrm{Aggregate functions} & a &::=& \mt{AVG} \mid \mt{SUM} \mid \mt{MIN} \mid \mt{MAX} \\
adamc@550	1964 \textrm{Directions} & o &::=& \mt{ASC} \mid \mt{DESC} \\
adamc@549	1965 \textrm{SQL integer} & N &::=& n \mid \{e\} \\
adamc@549	1966 \end{array}$$
adamc@549	1967
adamc@1085	1968 Additionally, an SQL expression may be inserted into normal Ur code with the syntax $(\mt{SQL} \; E)$ or $(\mt{WHERE} \; E)$. Similar shorthands exist for other nonterminals, with the prefix $\mt{FROM}$ for $\mt{FROM}$ items and $\mt{SELECT1}$ for pre-queries.
adamc@549	1969
adamc@550	1970 \subsubsection{DML}
adamc@550	1971
adamc@550	1972 DML commands $D$ are added to the rules for expressions $e$.
adamc@550	1973
adamc@550	1974 $$\begin{array}{rrcll}
adamc@550	1975 \textrm{Commands} & D &::=& (\mt{INSERT} \; \mt{INTO} \; T^E \; (f,^+) \; \mt{VALUES} \; (E,^+)) \\
adamc@550	1976 &&& (\mt{UPDATE} \; T^E \; \mt{SET} \; (f = E,)^+ \; \mt{WHERE} \; E) \\
adamc@550	1977 &&& (\mt{DELETE} \; \mt{FROM} \; T^E \; \mt{WHERE} \; E) \\
adamc@550	1978 \textrm{Table expressions} & T^E &::=& x \mid \{\{e\}\}
adamc@550	1979 \end{array}$$
adamc@550	1980
adamc@550	1981 Inside $\mt{UPDATE}$ and $\mt{DELETE}$ commands, lone variables $X$ are interpreted as references to columns of the implicit table $\mt{T}$, rather than to named expressions.
adamc@549	1982
adamc@551	1983 \subsection{XML}
adamc@551	1984
adamc@551	1985 XML fragments $L$ are added to the rules for expressions $e$.
adamc@551	1986
adamc@551	1987 $$\begin{array}{rrcll}
adamc@551	1988 \textrm{XML fragments} & L &::=& \texttt{<xml/>} \mid \texttt{<xml>}l^*\texttt{</xml>} \\
adamc@551	1989 \textrm{XML pieces} & l &::=& \textrm{text} & \textrm{cdata} \\
adamc@551	1990 &&& \texttt{<}g\texttt{/>} & \textrm{tag with no children} \\
adamc@551	1991 &&& \texttt{<}g\texttt{>}l^*\texttt{</}x\texttt{>} & \textrm{tag with children} \\
adamc@559	1992 &&& \{e\} & \textrm{computed XML fragment} \\
adamc@559	1993 &&& \{[e]\} & \textrm{injection of an Ur expression, via the $\mt{Top}.\mt{txt}$ function} \\
adamc@551	1994 \textrm{Tag} & g &::=& h \; (x = v)^* \\
adamc@551	1995 \textrm{Tag head} & h &::=& x & \textrm{tag name} \\
adamc@551	1996 &&& h\{c\} & \textrm{constructor parameter} \\
adamc@551	1997 \textrm{Attribute value} & v &::=& \ell & \textrm{literal value} \\
adamc@551	1998 &&& \{e\} & \textrm{computed value} \\
adamc@551	1999 \end{array}$$
adamc@551	2000
adamc@552	2001
adamc@553	2002 \section{The Structure of Web Applications}
adamc@553	2003
adamc@1127	2004 A web application is built from a series of modules, with one module, the last one appearing in the \texttt{.urp} file, designated as the main module. The signature of the main module determines the URL entry points to the application. Such an entry point should have type $\mt{t1} \to \ldots \to \mt{tn} \to \mt{transaction} \; \mt{page}$, for any integer $n \geq 0$, where $\mt{page}$ is a type synonym for top-level HTML pages, defined in $\mt{Basis}$. If such a function is at the top level of main module $M$, with $n = 0$, it will be accessible at URI \texttt{/M/f}, and so on for more deeply-nested functions, as described in Section \ref{tag} below. Arguments to an entry-point function are deserialized from the part of the URI following \texttt{f}.
adamc@553	2005
adamc@553	2006 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.
adamc@553	2007
adamc@553	2008 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.
adamc@553	2009
adamc@558	2010 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.
adamc@553	2011
adamc@660	2012 Ur/Web programs generally mix server- and client-side code in a fairly transparent way. The one important restriction is that mixed client-server code must encapsulate all server-side pieces within named functions. This is because execution of such pieces will be implemented by explicit calls to the remote web server, and it is useful to get the programmer's help in designing the interface to be used. For example, this makes it easier to allow a client running an old version of an application to continue interacting with a server that has been upgraded to a new version, if the programmer took care to keep the interfaces of all of the old remote calls the same. The functions implementing these services are assigned names in the same way as normal web entry points, by using module structure.
adamc@660	2013
adamc@789	2014 \medskip
adamc@789	2015
adamc@789	2016 The HTTP standard suggests that GET requests only be used in ways that generate no side effects. Side effecting operations should use POST requests instead. The Ur/Web compiler enforces this rule strictly, via a simple conservative program analysis. Any page that may have a side effect must be accessed through a form, all of which use POST requests. A page is judged to have a side effect if its code depends syntactically on any of the side-effecting, server-side FFI functions. Links, forms, and most client-side event handlers are not followed during this syntactic traversal, but \texttt{<body onload=\{...\}>} handlers \emph{are} examined, since they run right away and could just as well be considered parts of main page handlers.
adamc@789	2017
adamc@789	2018 Ur/Web includes a kind of automatic protection against cross site request forgery attacks. Whenever any page execution can have side effects and can also read at least one cookie value, all cookie values must be signed cryptographically, to ensure that the user has come to the current page by submitting a form on a real page generated by the proper server. Signing and signature checking are inserted automatically by the compiler. This prevents attacks like phishing schemes where users are directed to counterfeit pages with forms that submit to your application, where a user's cookies might be submitted without his knowledge, causing some undesired side effect.
adamc@789	2019
adamc@553	2020
adamc@897	2021 \section{The Foreign Function Interface}
adamc@897	2022
adamc@897	2023 It is possible to call your own C and JavaScript code from Ur/Web applications, via the foreign function interface (FFI). The starting point for a new binding is a \texttt{.urs} signature file that presents your external library as a single Ur/Web module (with no nested modules). Compilation conventions map the types and values that you use into C and/or JavaScript types and values.
adamc@897	2024
adamc@897	2025 It is most convenient to encapsulate an FFI binding with a new \texttt{.urp} file, which applications can include with the \texttt{library} directive in their own \texttt{.urp} files. A number of directives are likely to show up in the library's project file.
adamc@897	2026
adamc@897	2027 \begin{itemize}
adamc@897	2028 \item \texttt{clientOnly Module.ident} registers a value as being allowed only in client-side code.
adamc@897	2029 \item \texttt{clientToServer Module.ident} declares a type as OK to marshal between clients and servers. By default, abstract FFI types are not allowed to be marshalled, since your library might be maintaining invariants that the simple serialization code doesn't check.
adamc@897	2030 \item \texttt{effectful Module.ident} registers a function that can have side effects. It is important to remember to use this directive for each such function, or else the optimizer might change program semantics.
adamc@897	2031 \item \texttt{ffi FILE.urs} names the file giving your library's signature. You can include multiple such files in a single \texttt{.urp} file, and each file \texttt{mod.urp} defines an FFI module \texttt{Mod}.
adamc@1099	2032 \item \texttt{include FILE} requests inclusion of a C header file.
adamc@897	2033 \item \texttt{jsFunc Module.ident=name} gives a mapping from an Ur name for a value to a JavaScript name.
adamc@897	2034 \item \texttt{link FILE} requests that \texttt{FILE} be linked into applications. It should be a C object or library archive file, and you are responsible for generating it with your own build process.
adamc@897	2035 \item \texttt{script URL} requests inclusion of a JavaScript source file within application HTML.
adamc@897	2036 \item \texttt{serverOnly Module.ident} registers a value as being allowed only in server-side code.
adamc@897	2037 \end{itemize}
adamc@897	2038
adamc@897	2039 \subsection{Writing C FFI Code}
adamc@897	2040
adamc@897	2041 A server-side FFI type or value \texttt{Module.ident} must have a corresponding type or value definition \texttt{uw\_Module\_ident} in C code. With the current Ur/Web version, it's not generally possible to work with Ur records or complex datatypes in C code, but most other kinds of types are fair game.
adamc@897	2042
adamc@897	2043 \begin{itemize}
adamc@897	2044 \item Primitive types defined in \texttt{Basis} are themselves using the standard FFI interface, so you may refer to them like \texttt{uw\_Basis\_t}. See \texttt{include/types.h} for their definitions.
adamc@897	2045 \item Enumeration datatypes, which have only constructors that take no arguments, should be defined using C \texttt{enum}s. The type is named as for any other type identifier, and each constructor \texttt{c} gets an enumeration constant named \texttt{uw\_Module\_c}.
adamc@897	2046 \item A datatype \texttt{dt} (such as \texttt{Basis.option}) that has one non-value-carrying constructor \texttt{NC} and one value-carrying constructor \texttt{C} gets special treatment. Where \texttt{T} is the type of \texttt{C}'s argument, and where we represent \texttt{T} as \texttt{t} in C, we represent \texttt{NC} with \texttt{NULL}. The representation of \texttt{C} depends on whether we're sure that we don't need to use \texttt{NULL} to represent \texttt{t} values; this condition holds only for strings and complex datatypes. For such types, \texttt{C v} is represented with the C encoding of \texttt{v}, such that the translation of \texttt{dt} is \texttt{t}. For other types, \texttt{C v} is represented with a pointer to the C encoding of v, such that the translation of \texttt{dt} is \texttt{t*}.
adamc@897	2047 \end{itemize}
adamc@897	2048
adamc@897	2049 The C FFI version of a Ur function with type \texttt{T1 -> ... -> TN -> R} or \texttt{T1 -> ... -> TN -> transaction R} has a C prototype like \texttt{R uw\_Module\_ident(uw\_context, T1, ..., TN)}. Only functions with types of the second form may have side effects. \texttt{uw\_context} is the type of state that persists across handling a client request. Many functions that operate on contexts are prototyped in \texttt{include/urweb.h}. Most should only be used internally by the compiler. A few are useful in general FFI implementation:
adamc@897	2050 \begin{itemize}
adamc@897	2051 \item \begin{verbatim}
adamc@897	2052 void uw_error(uw_context, failure_kind, const char *fmt, ...);
adamc@897	2053 \end{verbatim}
adamc@897	2054 Abort the current request processing, giving a \texttt{printf}-style format string and arguments for generating an error message. The \texttt{failure\_kind} argument can be \texttt{FATAL}, to abort the whole execution; \texttt{BOUNDED\_RETRY}, to try processing the request again from the beginning, but failing if this happens too many times; or \texttt{UNLIMITED\_RETRY}, to repeat processing, with no cap on how many times this can recur.
adamc@897	2055
adamc@897	2056 \item \begin{verbatim}
adamc@897	2057 void uw_push_cleanup(uw_context, void (func)(void ), void *arg);
adamc@897	2058 void uw_pop_cleanup(uw_context);
adamc@897	2059 \end{verbatim}
adamc@897	2060 Manipulate a stack of actions that should be taken if any kind of error condition arises. Calling the ``pop'' function both removes an action from the stack and executes it.
adamc@897	2061
adamc@897	2062 \item \begin{verbatim}
adamc@897	2063 void *uw_malloc(uw_context, size_t);
adamc@897	2064 \end{verbatim}
adamc@897	2065 A version of \texttt{malloc()} that allocates memory inside a context's heap, which is managed with region allocation. Thus, there is no \texttt{uw\_free()}, but you need to be careful not to keep ad-hoc C pointers to this area of memory.
adamc@897	2066
adamc@897	2067 For performance and correctness reasons, it is usually preferable to use \texttt{uw\_malloc()} instead of \texttt{malloc()}. The former manipulates a local heap that can be kept allocated across page requests, while the latter uses global data structures that may face contention during concurrent execution.
adamc@897	2068
adamc@897	2069 \item \begin{verbatim}
adamc@897	2070 typedef void (uw_callback)(void );
adamc@897	2071 void uw_register_transactional(uw_context, void *data, uw_callback commit,
adamc@897	2072 uw_callback rollback, uw_callback free);
adamc@897	2073 \end{verbatim}
adamc@897	2074 All side effects in Ur/Web programs need to be compatible with transactions, such that any set of actions can be undone at any time. Thus, you should not perform actions with non-local side effects directly; instead, register handlers to be called when the current transaction is committed or rolled back. The arguments here give an arbitary piece of data to be passed to callbacks, a function to call on commit, a function to call on rollback, and a function to call afterward in either case to clean up any allocated resources. A rollback handler may be called after the associated commit handler has already been called, if some later part of the commit process fails.
adamc@897	2075
adamc@1085	2076 Any of the callbacks may be \texttt{NULL}. To accommodate some stubbornly non-transactional real-world actions like sending an e-mail message, Ur/Web treats \texttt{NULL} \texttt{rollback} callbacks specially. When a transaction commits, all \texttt{commit} actions that have non-\texttt{NULL} rollback actions are tried before any \texttt{commit} actions that have \texttt{NULL} rollback actions. Thus, if a single execution uses only one non-transactional action, and if that action never fails partway through its execution while still causing an observable side effect, then Ur/Web can maintain the transactional abstraction.
adamc@1085	2077
adamc@1085	2078 \item \begin{verbatim}
adamc@1085	2079 void uw_get_global(uw_context, char name);
adamc@1085	2080 void uw_set_global(uw_context, char name, void data, uw_callback free);
adamc@1085	2081 \end{verbatim}
adamc@1085	2082 Different FFI-based extensions may want to associate their own pieces of data with contexts. The global interface provides a way of doing that, where each extension must come up with its own unique key. The \texttt{free} argument to \texttt{uw\_set\_global()} explains how to deallocate the saved data.
adamc@1085	2083
adamc@897	2084 \end{itemize}
adamc@897	2085
adamc@897	2086 \subsection{Writing JavaScript FFI Code}
adamc@897	2087
adamc@897	2088 JavaScript is dynamically typed, so Ur/Web type definitions imply no JavaScript code. The JavaScript identifier for each FFI function is set with the \texttt{jsFunc} directive. Each identifier can be defined in any JavaScript file that you ask to include with the \texttt{script} directive.
adamc@897	2089
adamc@897	2090 In contrast to C FFI code, JavaScript FFI functions take no extra context argument. Their argument lists are as you would expect from their Ur types. Only functions whose ranges take the form \texttt{transaction T} should have side effects; the JavaScript ``return type'' of such a function is \texttt{T}. Here are the conventions for representing Ur values in JavaScript.
adamc@897	2091
adamc@897	2092 \begin{itemize}
adamc@897	2093 \item Integers, floats, strings, characters, and booleans are represented in the usual JavaScript way.
adamc@985	2094 \item Ur functions are represented in an unspecified way. This means that you should not rely on any details of function representation. Named FFI functions are represented as JavaScript functions with as many arguments as their Ur types specify. To call a non-FFI function \texttt{f} on argument \texttt{x}, run \texttt{execF(f, x)}.
adamc@897	2095 \item An Ur record is represented with a JavaScript record, where Ur field name \texttt{N} translates to JavaScript field name \texttt{\_N}. An exception to this rule is that the empty record is encoded as \texttt{null}.
adamc@897	2096 \item \texttt{option}-like types receive special handling similar to their handling in C. The ``\texttt{None}'' constructor is \texttt{null}, and a use of the ``\texttt{Some}'' constructor on a value \texttt{v} is either \texttt{v}, if the underlying type doesn't need to use \texttt{null}; or \texttt{\{v:v\}} otherwise.
adamc@985	2097 \item Any other datatypes represent a non-value-carrying constructor \texttt{C} as \texttt{"C"} and an application of a constructor \texttt{C} to value \texttt{v} as \texttt{\{n:"C", v:v\}}. This rule only applies to datatypes defined in FFI module signatures; the compiler is free to optimize the representations of other, non-\texttt{option}-like datatypes in arbitrary ways.
adamc@897	2098 \end{itemize}
adamc@897	2099
adamc@897	2100 It is possible to write JavaScript FFI code that interacts with the functional-reactive structure of a document, but this version of the manual doesn't cover the details.
adamc@897	2101
adamc@897	2102
adamc@552	2103 \section{Compiler Phases}
adamc@552	2104
adamc@552	2105 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.
adamc@552	2106
adamc@552	2107 In this section, we step through the main phases of compilation, noting what consequences each phase has for effective programming.
adamc@552	2108
adamc@552	2109 \subsection{Parse}
adamc@552	2110
adamc@552	2111 The compiler reads a \texttt{.urp} file, figures out which \texttt{.urs} and \texttt{.ur} files it references, and combines them all into what is conceptually a single sequence of declarations in the core language of Section \ref{core}.
adamc@552	2112
adamc@552	2113 \subsection{Elaborate}
adamc@552	2114
adamc@552	2115 This is where type inference takes place, translating programs into an explicit form with no more wildcards. This phase is the most likely source of compiler error messages.
adamc@552	2116
adamc@552	2117 \subsection{Unnest}
adamc@552	2118
adamc@552	2119 Named local function definitions are moved to the top level, to avoid the need to generate closures.
adamc@552	2120
adamc@552	2121 \subsection{Corify}
adamc@552	2122
adamc@552	2123 Module system features are compiled away, through inlining of functor definitions at application sites. Afterward, most abstraction boundaries are broken, facilitating optimization.
adamc@552	2124
adamc@552	2125 \subsection{Especialize}
adamc@552	2126
adamc@552	2127 Functions are specialized to particular argument patterns. This is an important trick for avoiding the need to maintain any closures at runtime.
adamc@552	2128
adamc@552	2129 \subsection{Untangle}
adamc@552	2130
adamc@552	2131 Remove unnecessary mutual recursion, splitting recursive groups into strongly-connected components.
adamc@552	2132
adamc@552	2133 \subsection{Shake}
adamc@552	2134
adamc@552	2135 Remove all definitions not needed to run the page handlers that are visible in the signature of the last module listed in the \texttt{.urp} file.
adamc@552	2136
adamc@661	2137 \subsection{Rpcify}
adamc@661	2138
adamc@661	2139 Pieces of code are determined to be client-side, server-side, neither, or both, by figuring out which standard library functions might be needed to execute them. Calls to server-side functions (e.g., $\mt{query}$) within mixed client-server code are identified and replaced with explicit remote calls. Some mixed functions may be converted to continuation-passing style to facilitate this transformation.
adamc@661	2140
adamc@661	2141 \subsection{Untangle, Shake}
adamc@661	2142
adamc@661	2143 Repeat these simplifications.
adamc@661	2144
adamc@553	2145 \subsection{\label{tag}Tag}
adamc@552	2146
adamc@552	2147 Assign a URL name to each link and form action. It is important that these links and actions are written as applications of named functions, because such names are used to generate URL patterns. A URL pattern has a name built from the full module path of the named function, followed by the function name, with all pieces separated by slashes. The path of a functor application is based on the name given to the result, rather than the path of the functor itself.
adamc@552	2148
adamc@552	2149 \subsection{Reduce}
adamc@552	2150
adamc@552	2151 Apply definitional equality rules to simplify the program as much as possible. This effectively includes inlining of every non-recursive definition.
adamc@552	2152
adamc@552	2153 \subsection{Unpoly}
adamc@552	2154
adamc@552	2155 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.
adamc@552	2156
adamc@552	2157 \subsection{Specialize}
adamc@552	2158
adamc@558	2159 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.
adamc@552	2160
adamc@552	2161 \subsection{Shake}
adamc@552	2162
adamc@558	2163 Here the compiler repeats the earlier Shake phase.
adamc@552	2164
adamc@552	2165 \subsection{Monoize}
adamc@552	2166
adamc@552	2167 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.
adamc@552	2168
adamc@552	2169 This is the stage at which concrete names are generated for cookies, tables, and sequences. They are named following the same convention as for links and actions, based on module path information saved from earlier stages. Table and sequence names separate path elements with underscores instead of slashes, and they are prefixed by \texttt{uw\_}.
adamc@664	2170
adamc@552	2171 \subsection{MonoOpt}
adamc@552	2172
adamc@552	2173 Simple algebraic laws are applied to simplify the program, focusing especially on efficient imperative generation of HTML pages.
adamc@552	2174
adamc@552	2175 \subsection{MonoUntangle}
adamc@552	2176
adamc@552	2177 Unnecessary mutual recursion is broken up again.
adamc@552	2178
adamc@552	2179 \subsection{MonoReduce}
adamc@552	2180
adamc@552	2181 Equivalents of the definitional equality rules are applied to simplify programs, with inlining again playing a major role.
adamc@552	2182
adamc@552	2183 \subsection{MonoShake, MonoOpt}
adamc@552	2184
adamc@552	2185 Unneeded declarations are removed, and basic optimizations are repeated.
adamc@552	2186
adamc@552	2187 \subsection{Fuse}
adamc@552	2188
adamc@552	2189 The compiler tries to simplify calls to recursive functions whose results are immediately written as page output. The write action is pushed inside the function definitions to avoid allocation of intermediate results.
adamc@552	2190
adamc@552	2191 \subsection{MonoUntangle, MonoShake}
adamc@552	2192
adamc@552	2193 Fuse often creates more opportunities to remove spurious mutual recursion.
adamc@552	2194
adamc@552	2195 \subsection{Pathcheck}
adamc@552	2196
adamc@552	2197 The compiler checks that no link or action name has been used more than once.
adamc@552	2198
adamc@552	2199 \subsection{Cjrize}
adamc@552	2200
adamc@552	2201 The program is translated to what is more or less a subset of C. If any use of functions as data remains at this point, the compiler will complain.
adamc@552	2202
adamc@552	2203 \subsection{C Compilation and Linking}
adamc@552	2204
adamc@552	2205 The output of the last phase is pretty-printed as C source code and passed to GCC.
adamc@552	2206
adamc@552	2207
adamc@524	2208 \end{document}

Mercurial > urweb

annotate doc/manual.tex @ 1166:e1df4c63e336