Ur/Web: doc/manual.tex annotate

annotate doc/manual.tex @ 1163:6c507826fae9

Tips for CGI scripts without httpd.conf access

author	Adam Chlipala <adamc@hcoop.net>
date	Tue, 09 Feb 2010 20:08:59 -0500
parents	2ae57fa551be
children	8679ba87cf3c

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@783	155 \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	156 \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	157 \end{itemize}
adamc@701	158
adamc@701	159
adamc@557	160 \subsection{Building an Application}
adamc@557	161
adamc@557	162 To compile project \texttt{P.urp}, simply run
adamc@557	163 \begin{verbatim}
adamc@557	164 urweb P
adamc@557	165 \end{verbatim}
adamc@558	166 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	167
adamc@557	168 To time how long the different compiler phases run, without generating an executable, run
adamc@557	169 \begin{verbatim}
adamc@557	170 urweb -timing P
adamc@557	171 \end{verbatim}
adamc@557	172
adamc@1086	173 To stop the compilation process after type-checking, run
adamc@1086	174 \begin{verbatim}
adamc@1086	175 urweb -tc P
adamc@1086	176 \end{verbatim}
adamc@1086	177
adamc@896	178 Some other command-line parameters are accepted:
adamc@896	179 \begin{itemize}
adamc@896	180 \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	181
adamc@896	182 \item \texttt{-dbms [postgres\|mysql\|sqlite]}: Sets the database backend to use.
adamc@896	183 \begin{itemize}
adamc@896	184 \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	185
adamc@896	186 A command sequence like this can initialize a Postgres database, using a file \texttt{app.sql} generated by the compiler:
adamc@896	187 \begin{verbatim}
adamc@896	188 createdb app
adamc@896	189 psql -f app.sql app
adamc@896	190 \end{verbatim}
adamc@896	191
adamc@896	192 \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	193
adamc@896	194 A command sequence like this can initialize a MySQL database:
adamc@896	195 \begin{verbatim}
adamc@896	196 echo "CREATE DATABASE app" \| mysql
adamc@896	197 mysql -D app <app.sql
adamc@896	198 \end{verbatim}
adamc@896	199
adamc@896	200 \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	201
adamc@896	202 A command like this can initialize an SQLite database:
adamc@896	203 \begin{verbatim}
adamc@896	204 sqlite3 path/to/database/file <app.sql
adamc@896	205 \end{verbatim}
adamc@896	206 \end{itemize}
adamc@896	207
adamc@896	208 \item \texttt{-output FILENAME}: Set where the application executable is written.
adamc@896	209
adamc@1127	210 \item \texttt{-path NAME VALUE}: Set the value of path variable \texttt{\$NAME} to \texttt{VALUE}, for use in \texttt{.urp} files.
adamc@1127	211
adamc@896	212 \item \texttt{-protocol [http\|cgi\|fastcgi]}: Set the protocol that the generated application speaks.
adamc@896	213 \begin{itemize}
adamc@896	214 \item \texttt{http}: This is the default. It is for building standalone web servers that can be accessed by web browsers directly.
adamc@896	215
adamc@896	216 \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	217
adamc@896	218 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	219 \begin{verbatim}
adamc@896	220 ScriptAlias /Hello /path/to/hello.exe
adamc@896	221 \end{verbatim}
adamc@896	222
adamc@1163	223 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	224 \begin{verbatim}
adamc@1163	225 Options +ExecCGI
adamc@1163	226 AddHandler cgi-script .exe
adamc@1163	227 \end{verbatim}
adamc@1163	228
adamc@1163	229 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	230 \begin{verbatim}
adamc@1163	231 prefix /dir/script.exe/
adamc@1163	232 \end{verbatim}
adamc@1163	233
adamc@1163	234 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	235
adamc@896	236 \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	237
adamc@896	238 To configure a FastCGI program with Apache, one could combine the above \texttt{ScriptAlias} line with a line like this:
adamc@896	239 \begin{verbatim}
adamc@896	240 FastCgiServer /path/to/hello.exe -idle-timeout 99999
adamc@896	241 \end{verbatim}
adamc@896	242 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	243
adamc@896	244 Here is some lighttpd configuration for the same application.
adamc@896	245 \begin{verbatim}
adamc@896	246 fastcgi.server = (
adamc@896	247 "/Hello/" =>
adamc@896	248 (( "bin-path" => "/path/to/hello.exe",
adamc@896	249 "socket" => "/tmp/hello",
adamc@896	250 "check-local" => "disable",
adamc@896	251 "docroot" => "/",
adamc@896	252 "max-procs" => "1"
adamc@896	253 ))
adamc@896	254 )
adamc@896	255 \end{verbatim}
adamc@896	256 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	257
adamc@896	258 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	259 \end{itemize}
adamc@896	260
adamc@1127	261 \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	262
adamc@896	263 \item \texttt{-sql FILENAME}: Set where a database set-up SQL script is written.
adamc@1095	264
adamc@1095	265 \item \texttt{-static}: Link the runtime system statically. The default is to link against dynamic libraries.
adamc@896	266 \end{itemize}
adamc@896	267
adamc@556	268
adamc@529	269 \section{Ur Syntax}
adamc@529	270
adamc@784	271 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	272
adamc@524	273 \subsection{Lexical Conventions}
adamc@524	274
adamc@524	275 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	276
adamc@524	277 \begin{center}
adamc@524	278 \begin{tabular}{rl}
adamc@524	279 \textbf{\LaTeX} & \textbf{ASCII} \\
adamc@524	280 $\to$ & \cd{->} \\
adamc@652	281 $\longrightarrow$ & \cd{-->} \\
adamc@524	282 $\times$ & \cd{*} \\
adamc@524	283 $\lambda$ & \cd{fn} \\
adamc@524	284 $\Rightarrow$ & \cd{=>} \\
adamc@652	285 $\Longrightarrow$ & \cd{==>} \\
adamc@529	286 $\neq$ & \cd{<>} \\
adamc@529	287 $\leq$ & \cd{<=} \\
adamc@529	288 $\geq$ & \cd{>=} \\
adamc@524	289 \\
adamc@524	290 $x$ & Normal textual identifier, not beginning with an uppercase letter \\
adamc@525	291 $X$ & Normal textual identifier, beginning with an uppercase letter \\
adamc@524	292 \end{tabular}
adamc@524	293 \end{center}
adamc@524	294
adamc@525	295 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	296
adamc@873	297 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	298
adamc@527	299 This version of the manual doesn't include operator precedences; see \texttt{src/urweb.grm} for that.
adamc@527	300
adamc@552	301 \subsection{\label{core}Core Syntax}
adamc@524	302
adamc@524	303 \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	304 $$\begin{array}{rrcll}
adamc@524	305 \textrm{Kinds} & \kappa &::=& \mt{Type} & \textrm{proper types} \\
adamc@525	306 &&& \mt{Unit} & \textrm{the trivial constructor} \\
adamc@525	307 &&& \mt{Name} & \textrm{field names} \\
adamc@525	308 &&& \kappa \to \kappa & \textrm{type-level functions} \\
adamc@525	309 &&& \{\kappa\} & \textrm{type-level records} \\
adamc@525	310 &&& (\kappa\times^+) & \textrm{type-level tuples} \\
adamc@652	311 &&& X & \textrm{variable} \\
adamc@652	312 &&& X \longrightarrow k & \textrm{kind-polymorphic type-level function} \\
adamc@529	313 &&& \_\_ & \textrm{wildcard} \\
adamc@525	314 &&& (\kappa) & \textrm{explicit precedence} \\
adamc@524	315 \end{array}$$
adamc@524	316
adamc@524	317 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	318 $$\begin{array}{rrcll}
adamc@524	319 \textrm{Explicitness} & ? &::=& :: & \textrm{explicit} \\
adamc@558	320 &&& ::: & \textrm{implicit}
adamc@524	321 \end{array}$$
adamc@524	322
adamc@524	323 \emph{Constructors} are the main class of compile-time-only data. They include proper types and are classified by kinds.
adamc@524	324 $$\begin{array}{rrcll}
adamc@524	325 \textrm{Constructors} & c, \tau &::=& (c) :: \kappa & \textrm{kind annotation} \\
adamc@530	326 &&& \hat{x} & \textrm{constructor variable} \\
adamc@524	327 \\
adamc@525	328 &&& \tau \to \tau & \textrm{function type} \\
adamc@525	329 &&& x \; ? \; \kappa \to \tau & \textrm{polymorphic function type} \\
adamc@652	330 &&& X \longrightarrow \tau & \textrm{kind-polymorphic function type} \\
adamc@525	331 &&& \$ c & \textrm{record type} \\
adamc@524	332 \\
adamc@525	333 &&& c \; c & \textrm{type-level function application} \\
adamc@530	334 &&& \lambda x \; :: \; \kappa \Rightarrow c & \textrm{type-level function abstraction} \\
adamc@524	335 \\
adamc@652	336 &&& X \Longrightarrow c & \textrm{type-level kind-polymorphic function abstraction} \\
adamc@655	337 &&& c [\kappa] & \textrm{type-level kind-polymorphic function application} \\
adamc@652	338 \\
adamc@525	339 &&& () & \textrm{type-level unit} \\
adamc@525	340 &&& \#X & \textrm{field name} \\
adamc@524	341 \\
adamc@525	342 &&& [(c = c)^*] & \textrm{known-length type-level record} \\
adamc@525	343 &&& c \rc c & \textrm{type-level record concatenation} \\
adamc@652	344 &&& \mt{map} & \textrm{type-level record map} \\
adamc@524	345 \\
adamc@558	346 &&& (c,^+) & \textrm{type-level tuple} \\
adamc@525	347 &&& c.n & \textrm{type-level tuple projection ($n \in \mathbb N^+$)} \\
adamc@524	348 \\
adamc@652	349 &&& [c \sim c] \Rightarrow \tau & \textrm{guarded type} \\
adamc@524	350 \\
adamc@529	351 &&& \_ :: \kappa & \textrm{wildcard} \\
adamc@525	352 &&& (c) & \textrm{explicit precedence} \\
adamc@530	353 \\
adamc@530	354 \textrm{Qualified uncapitalized variables} & \hat{x} &::=& x & \textrm{not from a module} \\
adamc@530	355 &&& M.x & \textrm{projection from a module} \\
adamc@525	356 \end{array}$$
adamc@525	357
adamc@655	358 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	359
adamc@525	360 Modules of the module system are described by \emph{signatures}.
adamc@525	361 $$\begin{array}{rrcll}
adamc@525	362 \textrm{Signatures} & S &::=& \mt{sig} \; s^* \; \mt{end} & \textrm{constant} \\
adamc@525	363 &&& X & \textrm{variable} \\
adamc@525	364 &&& \mt{functor}(X : S) : S & \textrm{functor} \\
adamc@529	365 &&& S \; \mt{where} \; \mt{con} \; x = c & \textrm{concretizing an abstract constructor} \\
adamc@525	366 &&& M.X & \textrm{projection from a module} \\
adamc@525	367 \\
adamc@525	368 \textrm{Signature items} & s &::=& \mt{con} \; x :: \kappa & \textrm{abstract constructor} \\
adamc@525	369 &&& \mt{con} \; x :: \kappa = c & \textrm{concrete constructor} \\
adamc@528	370 &&& \mt{datatype} \; x \; x^* = dc\mid^+ & \textrm{algebraic datatype definition} \\
adamc@529	371 &&& \mt{datatype} \; x = \mt{datatype} \; M.x & \textrm{algebraic datatype import} \\
adamc@525	372 &&& \mt{val} \; x : \tau & \textrm{value} \\
adamc@525	373 &&& \mt{structure} \; X : S & \textrm{sub-module} \\
adamc@525	374 &&& \mt{signature} \; X = S & \textrm{sub-signature} \\
adamc@525	375 &&& \mt{include} \; S & \textrm{signature inclusion} \\
adamc@525	376 &&& \mt{constraint} \; c \sim c & \textrm{record disjointness constraint} \\
adamc@654	377 &&& \mt{class} \; x :: \kappa & \textrm{abstract constructor class} \\
adamc@654	378 &&& \mt{class} \; x :: \kappa = c & \textrm{concrete constructor class} \\
adamc@525	379 \\
adamc@525	380 \textrm{Datatype constructors} & dc &::=& X & \textrm{nullary constructor} \\
adamc@525	381 &&& X \; \mt{of} \; \tau & \textrm{unary constructor} \\
adamc@524	382 \end{array}$$
adamc@524	383
adamc@526	384 \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	385 $$\begin{array}{rrcll}
adamc@526	386 \textrm{Patterns} & p &::=& \_ & \textrm{wildcard} \\
adamc@526	387 &&& x & \textrm{variable} \\
adamc@526	388 &&& \ell & \textrm{constant} \\
adamc@526	389 &&& \hat{X} & \textrm{nullary constructor} \\
adamc@526	390 &&& \hat{X} \; p & \textrm{unary constructor} \\
adamc@526	391 &&& \{(x = p,)^*\} & \textrm{rigid record pattern} \\
adamc@526	392 &&& \{(x = p,)^+, \ldots\} & \textrm{flexible record pattern} \\
adamc@852	393 &&& p : \tau & \textrm{type annotation} \\
adamc@527	394 &&& (p) & \textrm{explicit precedence} \\
adamc@526	395 \\
adamc@529	396 \textrm{Qualified capitalized variables} & \hat{X} &::=& X & \textrm{not from a module} \\
adamc@526	397 &&& M.X & \textrm{projection from a module} \\
adamc@526	398 \end{array}$$
adamc@526	399
adamc@527	400 \emph{Expressions} are the main run-time entities, corresponding to both ``expressions'' and ``statements'' in mainstream imperative languages.
adamc@527	401 $$\begin{array}{rrcll}
adamc@527	402 \textrm{Expressions} & e &::=& e : \tau & \textrm{type annotation} \\
adamc@529	403 &&& \hat{x} & \textrm{variable} \\
adamc@529	404 &&& \hat{X} & \textrm{datatype constructor} \\
adamc@527	405 &&& \ell & \textrm{constant} \\
adamc@527	406 \\
adamc@527	407 &&& e \; e & \textrm{function application} \\
adamc@527	408 &&& \lambda x : \tau \Rightarrow e & \textrm{function abstraction} \\
adamc@527	409 &&& e [c] & \textrm{polymorphic function application} \\
adamc@852	410 &&& \lambda [x \; ? \; \kappa] \Rightarrow e & \textrm{polymorphic function abstraction} \\
adamc@655	411 &&& e [\kappa] & \textrm{kind-polymorphic function application} \\
adamc@652	412 &&& X \Longrightarrow e & \textrm{kind-polymorphic function abstraction} \\
adamc@527	413 \\
adamc@527	414 &&& \{(c = e,)^*\} & \textrm{known-length record} \\
adamc@527	415 &&& e.c & \textrm{record field projection} \\
adamc@527	416 &&& e \rc e & \textrm{record concatenation} \\
adamc@527	417 &&& e \rcut c & \textrm{removal of a single record field} \\
adamc@527	418 &&& e \rcutM c & \textrm{removal of multiple record fields} \\
adamc@527	419 \\
adamc@527	420 &&& \mt{let} \; ed^* \; \mt{in} \; e \; \mt{end} & \textrm{local definitions} \\
adamc@527	421 \\
adamc@527	422 &&& \mt{case} \; e \; \mt{of} \; (p \Rightarrow e\|)^+ & \textrm{pattern matching} \\
adamc@527	423 \\
adamc@654	424 &&& \lambda [c \sim c] \Rightarrow e & \textrm{guarded expression abstraction} \\
adamc@654	425 &&& e \; ! & \textrm{guarded expression application} \\
adamc@527	426 \\
adamc@527	427 &&& \_ & \textrm{wildcard} \\
adamc@527	428 &&& (e) & \textrm{explicit precedence} \\
adamc@527	429 \\
adamc@527	430 \textrm{Local declarations} & ed &::=& \cd{val} \; x : \tau = e & \textrm{non-recursive value} \\
adamc@527	431 &&& \cd{val} \; \cd{rec} \; (x : \tau = e \; \cd{and})^+ & \textrm{mutually-recursive values} \\
adamc@527	432 \end{array}$$
adamc@527	433
adamc@655	434 As with constructors, we include both abstraction and application for kind polymorphism, but applications are only inferred internally.
adamc@655	435
adamc@528	436 \emph{Declarations} primarily bring new symbols into context.
adamc@528	437 $$\begin{array}{rrcll}
adamc@528	438 \textrm{Declarations} & d &::=& \mt{con} \; x :: \kappa = c & \textrm{constructor synonym} \\
adamc@528	439 &&& \mt{datatype} \; x \; x^* = dc\mid^+ & \textrm{algebraic datatype definition} \\
adamc@529	440 &&& \mt{datatype} \; x = \mt{datatype} \; M.x & \textrm{algebraic datatype import} \\
adamc@528	441 &&& \mt{val} \; x : \tau = e & \textrm{value} \\
adamc@528	442 &&& \mt{val} \; \cd{rec} \; (x : \tau = e \; \mt{and})^+ & \textrm{mutually-recursive values} \\
adamc@528	443 &&& \mt{structure} \; X : S = M & \textrm{module definition} \\
adamc@528	444 &&& \mt{signature} \; X = S & \textrm{signature definition} \\
adamc@528	445 &&& \mt{open} \; M & \textrm{module inclusion} \\
adamc@528	446 &&& \mt{constraint} \; c \sim c & \textrm{record disjointness constraint} \\
adamc@528	447 &&& \mt{open} \; \mt{constraints} \; M & \textrm{inclusion of just the constraints from a module} \\
adamc@528	448 &&& \mt{table} \; x : c & \textrm{SQL table} \\
adamc@784	449 &&& \mt{view} \; x : c & \textrm{SQL view} \\
adamc@528	450 &&& \mt{sequence} \; x & \textrm{SQL sequence} \\
adamc@535	451 &&& \mt{cookie} \; x : \tau & \textrm{HTTP cookie} \\
adamc@784	452 &&& \mt{style} \; x : \tau & \textrm{CSS class} \\
adamc@654	453 &&& \mt{class} \; x :: \kappa = c & \textrm{concrete constructor class} \\
adamc@1085	454 &&& \mt{task} \; e = e & \textrm{recurring task} \\
adamc@528	455 \\
adamc@529	456 \textrm{Modules} & M &::=& \mt{struct} \; d^* \; \mt{end} & \textrm{constant} \\
adamc@529	457 &&& X & \textrm{variable} \\
adamc@529	458 &&& M.X & \textrm{projection} \\
adamc@529	459 &&& M(M) & \textrm{functor application} \\
adamc@529	460 &&& \mt{functor}(X : S) : S = M & \textrm{functor abstraction} \\
adamc@528	461 \end{array}$$
adamc@528	462
adamc@528	463 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	464
adamc@784	465 We omit some extra possibilities in $\mt{table}$ syntax, deferring them to Section \ref{tables}.
adamc@784	466
adamc@529	467 \subsection{Shorthands}
adamc@529	468
adamc@529	469 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	470
adamc@529	471 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	472
adamc@529	473 A record type may be written $\{(c = c,)^\}$, which elaborates to $\$[(c = c,)^]$.
adamc@529	474
adamc@533	475 The notation $[c_1, \ldots, c_n]$ is shorthand for $[c_1 = (), \ldots, c_n = ()]$.
adamc@533	476
adamc@529	477 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	478
adamc@852	479 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	480
adamc@529	481 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	482
adamc@529	483 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	484
adamc@654	485 A signature item or declaration $\mt{class} \; x = \lambda y \Rightarrow c$ may be abbreviated $\mt{class} \; x \; y = c$.
adamc@529	486
adamc@1102	487 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	488
adamc@852	489 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	490
adamc@852	491 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	492
adamc@852	493 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	494
adamc@529	495 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	496
adamc@852	497 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	498
adamc@853	499 A declaration $\mt{table} \; x : \{(c = c,)^\}$ is elaborated into $\mt{table} \; x : [(c = c,)^]$.
adamc@529	500
adamc@529	501 The syntax $\mt{where} \; \mt{type}$ is an alternate form of $\mt{where} \; \mt{con}$.
adamc@529	502
adamc@529	503 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	504
adamc@529	505 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	506
adamc@784	507 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	508
adamc@530	509
adamc@530	510 \section{Static Semantics}
adamc@530	511
adamc@530	512 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	513
adamc@530	514 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	515 \begin{itemize}
adamc@655	516 \item $\Gamma \vdash \kappa$ expresses kind well-formedness.
adamc@530	517 \item $\Gamma \vdash c :: \kappa$ assigns a kind to a constructor in a context.
adamc@530	518 \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	519 \item $\Gamma \vdash c \hookrightarrow C$ proves that record constructor $c$ decomposes into set $C$ of field names and record constructors.
adamc@530	520 \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	521 \item $\Gamma \vdash e : \tau$ is a standard typing judgment.
adamc@534	522 \item $\Gamma \vdash p \leadsto \Gamma; \tau$ combines typing of patterns with calculation of which new variables they bind.
adamc@537	523 \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	524 \item $\Gamma \vdash S \equiv S$ is the signature equivalence judgment.
adamc@536	525 \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	526 \item $\Gamma \vdash M : S$ is the module signature checking judgment.
adamc@537	527 \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	528 \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	529 \end{itemize}
adamc@530	530
adamc@655	531
adamc@655	532 \subsection{Kind Well-Formedness}
adamc@655	533
adamc@655	534 $$\infer{\Gamma \vdash \mt{Type}}{}
adamc@655	535 \quad \infer{\Gamma \vdash \mt{Unit}}{}
adamc@655	536 \quad \infer{\Gamma \vdash \mt{Name}}{}
adamc@655	537 \quad \infer{\Gamma \vdash \kappa_1 \to \kappa_2}{
adamc@655	538 \Gamma \vdash \kappa_1
adamc@655	539 & \Gamma \vdash \kappa_2
adamc@655	540 }
adamc@655	541 \quad \infer{\Gamma \vdash \{\kappa\}}{
adamc@655	542 \Gamma \vdash \kappa
adamc@655	543 }
adamc@655	544 \quad \infer{\Gamma \vdash (\kappa_1 \times \ldots \times \kappa_n)}{
adamc@655	545 \forall i: \Gamma \vdash \kappa_i
adamc@655	546 }$$
adamc@655	547
adamc@655	548 $$\infer{\Gamma \vdash X}{
adamc@655	549 X \in \Gamma
adamc@655	550 }
adamc@655	551 \quad \infer{\Gamma \vdash X \longrightarrow \kappa}{
adamc@655	552 \Gamma, X \vdash \kappa
adamc@655	553 }$$
adamc@655	554
adamc@530	555 \subsection{Kinding}
adamc@530	556
adamc@655	557 We write $[X \mapsto \kappa_1]\kappa_2$ for capture-avoiding substitution of $\kappa_1$ for $X$ in $\kappa_2$.
adamc@655	558
adamc@530	559 $$\infer{\Gamma \vdash (c) :: \kappa :: \kappa}{
adamc@530	560 \Gamma \vdash c :: \kappa
adamc@530	561 }
adamc@530	562 \quad \infer{\Gamma \vdash x :: \kappa}{
adamc@530	563 x :: \kappa \in \Gamma
adamc@530	564 }
adamc@530	565 \quad \infer{\Gamma \vdash x :: \kappa}{
adamc@530	566 x :: \kappa = c \in \Gamma
adamc@530	567 }$$
adamc@530	568
adamc@530	569 $$\infer{\Gamma \vdash M.x :: \kappa}{
adamc@537	570 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537	571 & \mt{proj}(M, \overline{s}, \mt{con} \; x) = \kappa
adamc@530	572 }
adamc@530	573 \quad \infer{\Gamma \vdash M.x :: \kappa}{
adamc@537	574 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537	575 & \mt{proj}(M, \overline{s}, \mt{con} \; x) = (\kappa, c)
adamc@530	576 }$$
adamc@530	577
adamc@530	578 $$\infer{\Gamma \vdash \tau_1 \to \tau_2 :: \mt{Type}}{
adamc@530	579 \Gamma \vdash \tau_1 :: \mt{Type}
adamc@530	580 & \Gamma \vdash \tau_2 :: \mt{Type}
adamc@530	581 }
adamc@530	582 \quad \infer{\Gamma \vdash x \; ? \: \kappa \to \tau :: \mt{Type}}{
adamc@530	583 \Gamma, x :: \kappa \vdash \tau :: \mt{Type}
adamc@530	584 }
adamc@655	585 \quad \infer{\Gamma \vdash X \longrightarrow \tau :: \mt{Type}}{
adamc@655	586 \Gamma, X \vdash \tau :: \mt{Type}
adamc@655	587 }
adamc@530	588 \quad \infer{\Gamma \vdash \$c :: \mt{Type}}{
adamc@530	589 \Gamma \vdash c :: \{\mt{Type}\}
adamc@530	590 }$$
adamc@530	591
adamc@530	592 $$\infer{\Gamma \vdash c_1 \; c_2 :: \kappa_2}{
adamc@530	593 \Gamma \vdash c_1 :: \kappa_1 \to \kappa_2
adamc@530	594 & \Gamma \vdash c_2 :: \kappa_1
adamc@530	595 }
adamc@530	596 \quad \infer{\Gamma \vdash \lambda x \; :: \; \kappa_1 \Rightarrow c :: \kappa_1 \to \kappa_2}{
adamc@530	597 \Gamma, x :: \kappa_1 \vdash c :: \kappa_2
adamc@530	598 }$$
adamc@530	599
adamc@655	600 $$\infer{\Gamma \vdash c[\kappa'] :: [X \mapsto \kappa']\kappa}{
adamc@655	601 \Gamma \vdash c :: X \to \kappa
adamc@655	602 & \Gamma \vdash \kappa'
adamc@655	603 }
adamc@655	604 \quad \infer{\Gamma \vdash X \Longrightarrow c :: X \to \kappa}{
adamc@655	605 \Gamma, X \vdash c :: \kappa
adamc@655	606 }$$
adamc@655	607
adamc@530	608 $$\infer{\Gamma \vdash () :: \mt{Unit}}{}
adamc@530	609 \quad \infer{\Gamma \vdash \#X :: \mt{Name}}{}$$
adamc@530	610
adamc@530	611 $$\infer{\Gamma \vdash [\overline{c_i = c'_i}] :: \{\kappa\}}{
adamc@530	612 \forall i: \Gamma \vdash c_i : \mt{Name}
adamc@530	613 & \Gamma \vdash c'_i :: \kappa
adamc@530	614 & \forall i \neq j: \Gamma \vdash c_i \sim c_j
adamc@530	615 }
adamc@530	616 \quad \infer{\Gamma \vdash c_1 \rc c_2 :: \{\kappa\}}{
adamc@530	617 \Gamma \vdash c_1 :: \{\kappa\}
adamc@530	618 & \Gamma \vdash c_2 :: \{\kappa\}
adamc@530	619 & \Gamma \vdash c_1 \sim c_2
adamc@530	620 }$$
adamc@530	621
adamc@655	622 $$\infer{\Gamma \vdash \mt{map} :: (\kappa_1 \to \kappa_2) \to \{\kappa_1\} \to \{\kappa_2\}}{}$$
adamc@530	623
adamc@573	624 $$\infer{\Gamma \vdash (\overline c) :: (\kappa_1 \times \ldots \times \kappa_n)}{
adamc@573	625 \forall i: \Gamma \vdash c_i :: \kappa_i
adamc@530	626 }
adamc@573	627 \quad \infer{\Gamma \vdash c.i :: \kappa_i}{
adamc@573	628 \Gamma \vdash c :: (\kappa_1 \times \ldots \times \kappa_n)
adamc@530	629 }$$
adamc@530	630
adamc@655	631 $$\infer{\Gamma \vdash \lambda [c_1 \sim c_2] \Rightarrow \tau :: \mt{Type}}{
adamc@655	632 \Gamma \vdash c_1 :: \{\kappa\}
adamc@530	633 & \Gamma \vdash c_2 :: \{\kappa'\}
adamc@655	634 & \Gamma, c_1 \sim c_2 \vdash \tau :: \mt{Type}
adamc@530	635 }$$
adamc@530	636
adamc@531	637 \subsection{Record Disjointness}
adamc@531	638
adamc@531	639 $$\infer{\Gamma \vdash c_1 \sim c_2}{
adamc@558	640 \Gamma \vdash c_1 \hookrightarrow C_1
adamc@558	641 & \Gamma \vdash c_2 \hookrightarrow C_2
adamc@558	642 & \forall c'_1 \in C_1, c'_2 \in C_2: \Gamma \vdash c'_1 \sim c'_2
adamc@531	643 }
adamc@531	644 \quad \infer{\Gamma \vdash X \sim X'}{
adamc@531	645 X \neq X'
adamc@531	646 }$$
adamc@531	647
adamc@531	648 $$\infer{\Gamma \vdash c_1 \sim c_2}{
adamc@531	649 c'_1 \sim c'_2 \in \Gamma
adamc@558	650 & \Gamma \vdash c'_1 \hookrightarrow C_1
adamc@558	651 & \Gamma \vdash c'_2 \hookrightarrow C_2
adamc@558	652 & c_1 \in C_1
adamc@558	653 & c_2 \in C_2
adamc@531	654 }$$
adamc@531	655
adamc@531	656 $$\infer{\Gamma \vdash c \hookrightarrow \{c\}}{}
adamc@531	657 \quad \infer{\Gamma \vdash [\overline{c = c'}] \hookrightarrow \{\overline{c}\}}{}
adamc@531	658 \quad \infer{\Gamma \vdash c_1 \rc c_2 \hookrightarrow C_1 \cup C_2}{
adamc@531	659 \Gamma \vdash c_1 \hookrightarrow C_1
adamc@531	660 & \Gamma \vdash c_2 \hookrightarrow C_2
adamc@531	661 }
adamc@531	662 \quad \infer{\Gamma \vdash c \hookrightarrow C}{
adamc@531	663 \Gamma \vdash c \equiv c'
adamc@531	664 & \Gamma \vdash c' \hookrightarrow C
adamc@531	665 }
adamc@531	666 \quad \infer{\Gamma \vdash \mt{map} \; f \; c \hookrightarrow C}{
adamc@531	667 \Gamma \vdash c \hookrightarrow C
adamc@531	668 }$$
adamc@531	669
adamc@541	670 \subsection{\label{definitional}Definitional Equality}
adamc@532	671
adamc@655	672 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	673
adamc@532	674 $$\infer{\Gamma \vdash c \equiv c}{}
adamc@532	675 \quad \infer{\Gamma \vdash c_1 \equiv c_2}{
adamc@532	676 \Gamma \vdash c_2 \equiv c_1
adamc@532	677 }
adamc@532	678 \quad \infer{\Gamma \vdash c_1 \equiv c_3}{
adamc@532	679 \Gamma \vdash c_1 \equiv c_2
adamc@532	680 & \Gamma \vdash c_2 \equiv c_3
adamc@532	681 }
adamc@532	682 \quad \infer{\Gamma \vdash \mathcal C[c_1] \equiv \mathcal C[c_2]}{
adamc@532	683 \Gamma \vdash c_1 \equiv c_2
adamc@532	684 }$$
adamc@532	685
adamc@532	686 $$\infer{\Gamma \vdash x \equiv c}{
adamc@532	687 x :: \kappa = c \in \Gamma
adamc@532	688 }
adamc@532	689 \quad \infer{\Gamma \vdash M.x \equiv c}{
adamc@537	690 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537	691 & \mt{proj}(M, \overline{s}, \mt{con} \; x) = (\kappa, c)
adamc@532	692 }
adamc@532	693 \quad \infer{\Gamma \vdash (\overline c).i \equiv c_i}{}$$
adamc@532	694
adamc@532	695 $$\infer{\Gamma \vdash (\lambda x :: \kappa \Rightarrow c) \; c' \equiv [x \mapsto c'] c}{}
adamc@655	696 \quad \infer{\Gamma \vdash (X \Longrightarrow c) [\kappa] \equiv [X \mapsto \kappa] c}{}$$
adamc@655	697
adamc@655	698 $$\infer{\Gamma \vdash c_1 \rc c_2 \equiv c_2 \rc c_1}{}
adamc@532	699 \quad \infer{\Gamma \vdash c_1 \rc (c_2 \rc c_3) \equiv (c_1 \rc c_2) \rc c_3}{}$$
adamc@532	700
adamc@532	701 $$\infer{\Gamma \vdash [] \rc c \equiv c}{}
adamc@532	702 \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	703
adamc@655	704 $$\infer{\Gamma \vdash \mt{map} \; f \; [] \equiv []}{}
adamc@655	705 \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	706
adamc@532	707 $$\infer{\Gamma \vdash \mt{map} \; (\lambda x \Rightarrow x) \; c \equiv c}{}
adamc@655	708 \quad \infer{\Gamma \vdash \mt{map} \; f \; (\mt{map} \; f' \; c)
adamc@655	709 \equiv \mt{map} \; (\lambda x \Rightarrow f \; (f' \; x)) \; c}{}$$
adamc@532	710
adamc@532	711 $$\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	712
adamc@534	713 \subsection{Expression Typing}
adamc@533	714
adamc@873	715 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	716
adamc@533	717 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	718
adamc@533	719 $$\infer{\Gamma \vdash e : \tau : \tau}{
adamc@533	720 \Gamma \vdash e : \tau
adamc@533	721 }
adamc@533	722 \quad \infer{\Gamma \vdash e : \tau}{
adamc@533	723 \Gamma \vdash e : \tau'
adamc@533	724 & \Gamma \vdash \tau' \equiv \tau
adamc@533	725 }
adamc@533	726 \quad \infer{\Gamma \vdash \ell : T(\ell)}{}$$
adamc@533	727
adamc@533	728 $$\infer{\Gamma \vdash x : \mathcal I(\tau)}{
adamc@533	729 x : \tau \in \Gamma
adamc@533	730 }
adamc@533	731 \quad \infer{\Gamma \vdash M.x : \mathcal I(\tau)}{
adamc@537	732 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537	733 & \mt{proj}(M, \overline{s}, \mt{val} \; x) = \tau
adamc@533	734 }
adamc@533	735 \quad \infer{\Gamma \vdash X : \mathcal I(\tau)}{
adamc@533	736 X : \tau \in \Gamma
adamc@533	737 }
adamc@533	738 \quad \infer{\Gamma \vdash M.X : \mathcal I(\tau)}{
adamc@537	739 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537	740 & \mt{proj}(M, \overline{s}, \mt{val} \; X) = \tau
adamc@533	741 }$$
adamc@533	742
adamc@533	743 $$\infer{\Gamma \vdash e_1 \; e_2 : \tau_2}{
adamc@533	744 \Gamma \vdash e_1 : \tau_1 \to \tau_2
adamc@533	745 & \Gamma \vdash e_2 : \tau_1
adamc@533	746 }
adamc@533	747 \quad \infer{\Gamma \vdash \lambda x : \tau_1 \Rightarrow e : \tau_1 \to \tau_2}{
adamc@533	748 \Gamma, x : \tau_1 \vdash e : \tau_2
adamc@533	749 }$$
adamc@533	750
adamc@533	751 $$\infer{\Gamma \vdash e [c] : [x \mapsto c]\tau}{
adamc@533	752 \Gamma \vdash e : x :: \kappa \to \tau
adamc@533	753 & \Gamma \vdash c :: \kappa
adamc@533	754 }
adamc@852	755 \quad \infer{\Gamma \vdash \lambda [x \; ? \; \kappa] \Rightarrow e : x \; ? \; \kappa \to \tau}{
adamc@533	756 \Gamma, x :: \kappa \vdash e : \tau
adamc@533	757 }$$
adamc@533	758
adamc@655	759 $$\infer{\Gamma \vdash e [\kappa] : [X \mapsto \kappa]\tau}{
adamc@655	760 \Gamma \vdash e : X \longrightarrow \tau
adamc@655	761 & \Gamma \vdash \kappa
adamc@655	762 }
adamc@655	763 \quad \infer{\Gamma \vdash X \Longrightarrow e : X \longrightarrow \tau}{
adamc@655	764 \Gamma, X \vdash e : \tau
adamc@655	765 }$$
adamc@655	766
adamc@533	767 $$\infer{\Gamma \vdash \{\overline{c = e}\} : \{\overline{c : \tau}\}}{
adamc@533	768 \forall i: \Gamma \vdash c_i :: \mt{Name}
adamc@533	769 & \Gamma \vdash e_i : \tau_i
adamc@533	770 & \forall i \neq j: \Gamma \vdash c_i \sim c_j
adamc@533	771 }
adamc@533	772 \quad \infer{\Gamma \vdash e.c : \tau}{
adamc@533	773 \Gamma \vdash e : \$([c = \tau] \rc c')
adamc@533	774 }
adamc@533	775 \quad \infer{\Gamma \vdash e_1 \rc e_2 : \$(c_1 \rc c_2)}{
adamc@533	776 \Gamma \vdash e_1 : \$c_1
adamc@533	777 & \Gamma \vdash e_2 : \$c_2
adamc@573	778 & \Gamma \vdash c_1 \sim c_2
adamc@533	779 }$$
adamc@533	780
adamc@533	781 $$\infer{\Gamma \vdash e \rcut c : \$c'}{
adamc@533	782 \Gamma \vdash e : \$([c = \tau] \rc c')
adamc@533	783 }
adamc@533	784 \quad \infer{\Gamma \vdash e \rcutM c : \$c'}{
adamc@533	785 \Gamma \vdash e : \$(c \rc c')
adamc@533	786 }$$
adamc@533	787
adamc@533	788 $$\infer{\Gamma \vdash \mt{let} \; \overline{ed} \; \mt{in} \; e \; \mt{end} : \tau}{
adamc@533	789 \Gamma \vdash \overline{ed} \leadsto \Gamma'
adamc@533	790 & \Gamma' \vdash e : \tau
adamc@533	791 }
adamc@533	792 \quad \infer{\Gamma \vdash \mt{case} \; e \; \mt{of} \; \overline{p \Rightarrow e} : \tau}{
adamc@533	793 \forall i: \Gamma \vdash p_i \leadsto \Gamma_i, \tau'
adamc@533	794 & \Gamma_i \vdash e_i : \tau
adamc@533	795 }$$
adamc@533	796
adamc@573	797 $$\infer{\Gamma \vdash \lambda [c_1 \sim c_2] \Rightarrow e : \lambda [c_1 \sim c_2] \Rightarrow \tau}{
adamc@533	798 \Gamma \vdash c_1 :: \{\kappa\}
adamc@655	799 & \Gamma \vdash c_2 :: \{\kappa'\}
adamc@533	800 & \Gamma, c_1 \sim c_2 \vdash e : \tau
adamc@662	801 }
adamc@662	802 \quad \infer{\Gamma \vdash e \; ! : \tau}{
adamc@662	803 \Gamma \vdash e : [c_1 \sim c_2] \Rightarrow \tau
adamc@662	804 & \Gamma \vdash c_1 \sim c_2
adamc@533	805 }$$
adamc@533	806
adamc@534	807 \subsection{Pattern Typing}
adamc@534	808
adamc@534	809 $$\infer{\Gamma \vdash \_ \leadsto \Gamma; \tau}{}
adamc@534	810 \quad \infer{\Gamma \vdash x \leadsto \Gamma, x : \tau; \tau}{}
adamc@534	811 \quad \infer{\Gamma \vdash \ell \leadsto \Gamma; T(\ell)}{}$$
adamc@534	812
adamc@534	813 $$\infer{\Gamma \vdash X \leadsto \Gamma; \overline{[x_i \mapsto \tau'_i]}\tau}{
adamc@534	814 X : \overline{x ::: \mt{Type}} \to \tau \in \Gamma
adamc@534	815 & \textrm{$\tau$ not a function type}
adamc@534	816 }
adamc@534	817 \quad \infer{\Gamma \vdash X \; p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau}{
adamc@534	818 X : \overline{x ::: \mt{Type}} \to \tau'' \to \tau \in \Gamma
adamc@534	819 & \Gamma \vdash p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau''
adamc@534	820 }$$
adamc@534	821
adamc@534	822 $$\infer{\Gamma \vdash M.X \leadsto \Gamma; \overline{[x_i \mapsto \tau'_i]}\tau}{
adamc@537	823 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537	824 & \mt{proj}(M, \overline{s}, \mt{val} \; X) = \overline{x ::: \mt{Type}} \to \tau
adamc@534	825 & \textrm{$\tau$ not a function type}
adamc@534	826 }$$
adamc@534	827
adamc@534	828 $$\infer{\Gamma \vdash M.X \; p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau}{
adamc@537	829 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537	830 & \mt{proj}(M, \overline{s}, \mt{val} \; X) = \overline{x ::: \mt{Type}} \to \tau'' \to \tau
adamc@534	831 & \Gamma \vdash p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau''
adamc@534	832 }$$
adamc@534	833
adamc@534	834 $$\infer{\Gamma \vdash \{\overline{x = p}\} \leadsto \Gamma_n; \{\overline{x = \tau}\}}{
adamc@534	835 \Gamma_0 = \Gamma
adamc@534	836 & \forall i: \Gamma_i \vdash p_i \leadsto \Gamma_{i+1}; \tau_i
adamc@534	837 }
adamc@534	838 \quad \infer{\Gamma \vdash \{\overline{x = p}, \ldots\} \leadsto \Gamma_n; \$([\overline{x = \tau}] \rc c)}{
adamc@534	839 \Gamma_0 = \Gamma
adamc@534	840 & \forall i: \Gamma_i \vdash p_i \leadsto \Gamma_{i+1}; \tau_i
adamc@534	841 }$$
adamc@534	842
adamc@852	843 $$\infer{\Gamma \vdash p : \tau \leadsto \Gamma'; \tau}{
adamc@852	844 \Gamma \vdash p \leadsto \Gamma'; \tau'
adamc@852	845 & \Gamma \vdash \tau' \equiv \tau
adamc@852	846 }$$
adamc@852	847
adamc@535	848 \subsection{Declaration Typing}
adamc@535	849
adamc@535	850 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	851
adamc@655	852 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	853
adamc@558	854 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	855 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	856
adamc@535	857 $$\infer{\Gamma \vdash \cdot \leadsto \Gamma}{}
adamc@535	858 \quad \infer{\Gamma \vdash d, \overline{d} \leadsto \Gamma''}{
adamc@535	859 \Gamma \vdash d \leadsto \Gamma'
adamc@535	860 & \Gamma' \vdash \overline{d} \leadsto \Gamma''
adamc@535	861 }$$
adamc@535	862
adamc@535	863 $$\infer{\Gamma \vdash \mt{con} \; x :: \kappa = c \leadsto \Gamma, x :: \kappa = c}{
adamc@535	864 \Gamma \vdash c :: \kappa
adamc@535	865 }
adamc@535	866 \quad \infer{\Gamma \vdash \mt{datatype} \; x \; \overline{y} = \overline{dc} \leadsto \Gamma'}{
adamc@535	867 \overline{y}; x; \Gamma, x :: \mt{Type}^{\mt{len}(\overline y)} \to \mt{Type} \vdash \overline{dc} \leadsto \Gamma'
adamc@535	868 }$$
adamc@535	869
adamc@535	870 $$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leadsto \Gamma'}{
adamc@537	871 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537	872 & \mt{proj}(M, \overline{s}, \mt{datatype} \; z) = (\overline{y}, \overline{dc})
adamc@535	873 & \overline{y}; x; \Gamma, x :: \mt{Type}^{\mt{len}(\overline y)} \to \mt{Type} = M.z \vdash \overline{dc} \leadsto \Gamma'
adamc@535	874 }$$
adamc@535	875
adamc@535	876 $$\infer{\Gamma \vdash \mt{val} \; x : \tau = e \leadsto \Gamma, x : \tau}{
adamc@535	877 \Gamma \vdash e : \tau
adamc@535	878 }$$
adamc@535	879
adamc@535	880 $$\infer{\Gamma \vdash \mt{val} \; \mt{rec} \; \overline{x : \tau = e} \leadsto \Gamma, \overline{x : \tau}}{
adamc@535	881 \forall i: \Gamma, \overline{x : \tau} \vdash e_i : \tau_i
adamc@535	882 & \textrm{$e_i$ starts with an expression $\lambda$, optionally preceded by constructor and disjointness $\lambda$s}
adamc@535	883 }$$
adamc@535	884
adamc@535	885 $$\infer{\Gamma \vdash \mt{structure} \; X : S = M \leadsto \Gamma, X : S}{
adamc@535	886 \Gamma \vdash M : S
adamc@558	887 & \textrm{ $M$ not a constant or application}
adamc@535	888 }
adamc@558	889 \quad \infer{\Gamma \vdash \mt{structure} \; X : S = M \leadsto \Gamma, X : \mt{selfify}(X, \overline{s})}{
adamc@558	890 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@539	891 }$$
adamc@539	892
adamc@539	893 $$\infer{\Gamma \vdash \mt{signature} \; X = S \leadsto \Gamma, X = S}{
adamc@535	894 \Gamma \vdash S
adamc@535	895 }$$
adamc@535	896
adamc@537	897 $$\infer{\Gamma \vdash \mt{open} \; M \leadsto \Gamma, \mathcal O(M, \overline{s})}{
adamc@537	898 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@535	899 }$$
adamc@535	900
adamc@535	901 $$\infer{\Gamma \vdash \mt{constraint} \; c_1 \sim c_2 \leadsto \Gamma}{
adamc@535	902 \Gamma \vdash c_1 :: \{\kappa\}
adamc@535	903 & \Gamma \vdash c_2 :: \{\kappa\}
adamc@535	904 & \Gamma \vdash c_1 \sim c_2
adamc@535	905 }
adamc@537	906 \quad \infer{\Gamma \vdash \mt{open} \; \mt{constraints} \; M \leadsto \Gamma, \mathcal O_c(M, \overline{s})}{
adamc@537	907 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@535	908 }$$
adamc@535	909
adamc@784	910 $$\infer{\Gamma \vdash \mt{table} \; x : c \leadsto \Gamma, x : \mt{Basis}.\mt{sql\_table} \; c \; []}{
adamc@535	911 \Gamma \vdash c :: \{\mt{Type}\}
adamc@535	912 }
adamc@784	913 \quad \infer{\Gamma \vdash \mt{view} \; x : c \leadsto \Gamma, x : \mt{Basis}.\mt{sql\_view} \; c}{
adamc@784	914 \Gamma \vdash c :: \{\mt{Type}\}
adamc@784	915 }$$
adamc@784	916
adamc@784	917 $$\infer{\Gamma \vdash \mt{sequence} \; x \leadsto \Gamma, x : \mt{Basis}.\mt{sql\_sequence}}{}$$
adamc@535	918
adamc@535	919 $$\infer{\Gamma \vdash \mt{cookie} \; x : \tau \leadsto \Gamma, x : \mt{Basis}.\mt{http\_cookie} \; \tau}{
adamc@535	920 \Gamma \vdash \tau :: \mt{Type}
adamc@784	921 }
adamc@784	922 \quad \infer{\Gamma \vdash \mt{style} \; x \leadsto \Gamma, x : \mt{Basis}.\mt{css\_class}}{}$$
adamc@535	923
adamc@1085	924 $$\infer{\Gamma \vdash \mt{task} \; e_1 = e_2 \leadsto \Gamma}{
adamc@1085	925 \Gamma \vdash e_1 :: \mt{Basis}.\mt{task\_kind}
adamc@1085	926 & \Gamma \vdash e_2 :: \mt{Basis}.\mt{transaction} \; \{\}
adamc@1085	927 }$$
adamc@1085	928
adamc@784	929 $$\infer{\Gamma \vdash \mt{class} \; x :: \kappa = c \leadsto \Gamma, x :: \kappa = c}{
adamc@784	930 \Gamma \vdash c :: \kappa
adamc@535	931 }$$
adamc@535	932
adamc@535	933 $$\infer{\overline{y}; x; \Gamma \vdash \cdot \leadsto \Gamma}{}
adamc@535	934 \quad \infer{\overline{y}; x; \Gamma \vdash X \mid \overline{dc} \leadsto \Gamma', X : \overline{y ::: \mt{Type}} \to x \; \overline{y}}{
adamc@535	935 \overline{y}; x; \Gamma \vdash \overline{dc} \leadsto \Gamma'
adamc@535	936 }
adamc@535	937 \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	938 \overline{y}; x; \Gamma \vdash \overline{dc} \leadsto \Gamma'
adamc@535	939 }$$
adamc@535	940
adamc@537	941 \subsection{Signature Item Typing}
adamc@537	942
adamc@537	943 We appeal to a signature item analogue of the $\mathcal O$ function from the last subsection.
adamc@537	944
adamc@537	945 $$\infer{\Gamma \vdash \cdot \leadsto \Gamma}{}
adamc@537	946 \quad \infer{\Gamma \vdash s, \overline{s} \leadsto \Gamma''}{
adamc@537	947 \Gamma \vdash s \leadsto \Gamma'
adamc@537	948 & \Gamma' \vdash \overline{s} \leadsto \Gamma''
adamc@537	949 }$$
adamc@537	950
adamc@537	951 $$\infer{\Gamma \vdash \mt{con} \; x :: \kappa \leadsto \Gamma, x :: \kappa}{}
adamc@537	952 \quad \infer{\Gamma \vdash \mt{con} \; x :: \kappa = c \leadsto \Gamma, x :: \kappa = c}{
adamc@537	953 \Gamma \vdash c :: \kappa
adamc@537	954 }
adamc@537	955 \quad \infer{\Gamma \vdash \mt{datatype} \; x \; \overline{y} = \overline{dc} \leadsto \Gamma'}{
adamc@537	956 \overline{y}; x; \Gamma, x :: \mt{Type}^{\mt{len}(\overline y)} \to \mt{Type} \vdash \overline{dc} \leadsto \Gamma'
adamc@537	957 }$$
adamc@537	958
adamc@537	959 $$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leadsto \Gamma'}{
adamc@537	960 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537	961 & \mt{proj}(M, \overline{s}, \mt{datatype} \; z) = (\overline{y}, \overline{dc})
adamc@537	962 & \overline{y}; x; \Gamma, x :: \mt{Type}^{\mt{len}(\overline y)} \to \mt{Type} = M.z \vdash \overline{dc} \leadsto \Gamma'
adamc@537	963 }$$
adamc@537	964
adamc@537	965 $$\infer{\Gamma \vdash \mt{val} \; x : \tau \leadsto \Gamma, x : \tau}{
adamc@537	966 \Gamma \vdash \tau :: \mt{Type}
adamc@537	967 }$$
adamc@537	968
adamc@537	969 $$\infer{\Gamma \vdash \mt{structure} \; X : S \leadsto \Gamma, X : S}{
adamc@537	970 \Gamma \vdash S
adamc@537	971 }
adamc@537	972 \quad \infer{\Gamma \vdash \mt{signature} \; X = S \leadsto \Gamma, X = S}{
adamc@537	973 \Gamma \vdash S
adamc@537	974 }$$
adamc@537	975
adamc@537	976 $$\infer{\Gamma \vdash \mt{include} \; S \leadsto \Gamma, \mathcal O(\overline{s})}{
adamc@537	977 \Gamma \vdash S
adamc@537	978 & \Gamma \vdash S \equiv \mt{sig} \; \overline{s} \; \mt{end}
adamc@537	979 }$$
adamc@537	980
adamc@537	981 $$\infer{\Gamma \vdash \mt{constraint} \; c_1 \sim c_2 \leadsto \Gamma, c_1 \sim c_2}{
adamc@537	982 \Gamma \vdash c_1 :: \{\kappa\}
adamc@537	983 & \Gamma \vdash c_2 :: \{\kappa\}
adamc@537	984 }$$
adamc@537	985
adamc@784	986 $$\infer{\Gamma \vdash \mt{class} \; x :: \kappa = c \leadsto \Gamma, x :: \kappa = c}{
adamc@784	987 \Gamma \vdash c :: \kappa
adamc@537	988 }
adamc@784	989 \quad \infer{\Gamma \vdash \mt{class} \; x :: \kappa \leadsto \Gamma, x :: \kappa}{}$$
adamc@537	990
adamc@536	991 \subsection{Signature Compatibility}
adamc@536	992
adamc@558	993 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	994
adamc@537	995 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	996
adamc@536	997 $$\infer{\Gamma \vdash S \equiv S}{}
adamc@536	998 \quad \infer{\Gamma \vdash S_1 \equiv S_2}{
adamc@536	999 \Gamma \vdash S_2 \equiv S_1
adamc@536	1000 }
adamc@536	1001 \quad \infer{\Gamma \vdash X \equiv S}{
adamc@536	1002 X = S \in \Gamma
adamc@536	1003 }
adamc@536	1004 \quad \infer{\Gamma \vdash M.X \equiv S}{
adamc@537	1005 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537	1006 & \mt{proj}(M, \overline{s}, \mt{signature} \; X) = S
adamc@536	1007 }$$
adamc@536	1008
adamc@536	1009 $$\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	1010 \Gamma \vdash S \equiv \mt{sig} \; \overline{s^1} \; \mt{con} \; x :: \kappa \; \overline{s_2} \; \mt{end}
adamc@536	1011 & \Gamma \vdash c :: \kappa
adamc@537	1012 }
adamc@537	1013 \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	1014 \Gamma \vdash S \equiv \mt{sig} \; \overline{s} \; \mt{end}
adamc@536	1015 }$$
adamc@536	1016
adamc@536	1017 $$\infer{\Gamma \vdash S_1 \leq S_2}{
adamc@536	1018 \Gamma \vdash S_1 \equiv S_2
adamc@536	1019 }
adamc@536	1020 \quad \infer{\Gamma \vdash \mt{sig} \; \overline{s} \; \mt{end} \leq \mt{sig} \; \mt{end}}{}
adamc@537	1021 \quad \infer{\Gamma \vdash \mt{sig} \; \overline{s} \; \mt{end} \leq \mt{sig} \; s' \; \overline{s'} \; \mt{end}}{
adamc@537	1022 \Gamma \vdash \overline{s} \leq s'
adamc@537	1023 & \Gamma \vdash s' \leadsto \Gamma'
adamc@537	1024 & \Gamma' \vdash \mt{sig} \; \overline{s} \; \mt{end} \leq \mt{sig} \; \overline{s'} \; \mt{end}
adamc@537	1025 }$$
adamc@537	1026
adamc@537	1027 $$\infer{\Gamma \vdash s \; \overline{s} \leq s'}{
adamc@537	1028 \Gamma \vdash s \leq s'
adamc@537	1029 }
adamc@537	1030 \quad \infer{\Gamma \vdash s \; \overline{s} \leq s'}{
adamc@537	1031 \Gamma \vdash s \leadsto \Gamma'
adamc@537	1032 & \Gamma' \vdash \overline{s} \leq s'
adamc@536	1033 }$$
adamc@536	1034
adamc@536	1035 $$\infer{\Gamma \vdash \mt{functor} (X : S_1) : S_2 \leq \mt{functor} (X : S'_1) : S'_2}{
adamc@536	1036 \Gamma \vdash S'_1 \leq S_1
adamc@536	1037 & \Gamma, X : S'_1 \vdash S_2 \leq S'_2
adamc@536	1038 }$$
adamc@536	1039
adamc@537	1040 $$\infer{\Gamma \vdash \mt{con} \; x :: \kappa \leq \mt{con} \; x :: \kappa}{}
adamc@537	1041 \quad \infer{\Gamma \vdash \mt{con} \; x :: \kappa = c \leq \mt{con} \; x :: \kappa}{}
adamc@558	1042 \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	1043
adamc@537	1044 $$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leq \mt{con} \; x :: \mt{Type}^{\mt{len}(y)} \to \mt{Type}}{
adamc@537	1045 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537	1046 & \mt{proj}(M, \overline{s}, \mt{datatype} \; z) = (\overline{y}, \overline{dc})
adamc@537	1047 }$$
adamc@537	1048
adamc@784	1049 $$\infer{\Gamma \vdash \mt{class} \; x :: \kappa \leq \mt{con} \; x :: \kappa}{}
adamc@784	1050 \quad \infer{\Gamma \vdash \mt{class} \; x :: \kappa = c \leq \mt{con} \; x :: \kappa}{}$$
adamc@537	1051
adamc@537	1052 $$\infer{\Gamma \vdash \mt{con} \; x :: \kappa = c_1 \leq \mt{con} \; x :: \mt{\kappa} = c_2}{
adamc@537	1053 \Gamma \vdash c_1 \equiv c_2
adamc@537	1054 }
adamc@784	1055 \quad \infer{\Gamma \vdash \mt{class} \; x :: \kappa = c_1 \leq \mt{con} \; x :: \kappa = c_2}{
adamc@537	1056 \Gamma \vdash c_1 \equiv c_2
adamc@537	1057 }$$
adamc@537	1058
adamc@537	1059 $$\infer{\Gamma \vdash \mt{datatype} \; x \; \overline{y} = \overline{dc} \leq \mt{datatype} \; x \; \overline{y} = \overline{dc'}}{
adamc@537	1060 \Gamma, \overline{y :: \mt{Type}} \vdash \overline{dc} \leq \overline{dc'}
adamc@537	1061 }$$
adamc@537	1062
adamc@537	1063 $$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leq \mt{datatype} \; x \; \overline{y} = \overline{dc'}}{
adamc@537	1064 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537	1065 & \mt{proj}(M, \overline{s}, \mt{datatype} \; z) = (\overline{y}, \overline{dc})
adamc@537	1066 & \Gamma, \overline{y :: \mt{Type}} \vdash \overline{dc} \leq \overline{dc'}
adamc@537	1067 }$$
adamc@537	1068
adamc@537	1069 $$\infer{\Gamma \vdash \cdot \leq \cdot}{}
adamc@537	1070 \quad \infer{\Gamma \vdash X; \overline{dc} \leq X; \overline{dc'}}{
adamc@537	1071 \Gamma \vdash \overline{dc} \leq \overline{dc'}
adamc@537	1072 }
adamc@537	1073 \quad \infer{\Gamma \vdash X \; \mt{of} \; \tau_1; \overline{dc} \leq X \; \mt{of} \; \tau_2; \overline{dc'}}{
adamc@537	1074 \Gamma \vdash \tau_1 \equiv \tau_2
adamc@537	1075 & \Gamma \vdash \overline{dc} \leq \overline{dc'}
adamc@537	1076 }$$
adamc@537	1077
adamc@537	1078 $$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leq \mt{datatype} \; x = \mt{datatype} \; M'.z'}{
adamc@537	1079 \Gamma \vdash M.z \equiv M'.z'
adamc@537	1080 }$$
adamc@537	1081
adamc@537	1082 $$\infer{\Gamma \vdash \mt{val} \; x : \tau_1 \leq \mt{val} \; x : \tau_2}{
adamc@537	1083 \Gamma \vdash \tau_1 \equiv \tau_2
adamc@537	1084 }
adamc@537	1085 \quad \infer{\Gamma \vdash \mt{structure} \; X : S_1 \leq \mt{structure} \; X : S_2}{
adamc@537	1086 \Gamma \vdash S_1 \leq S_2
adamc@537	1087 }
adamc@537	1088 \quad \infer{\Gamma \vdash \mt{signature} \; X = S_1 \leq \mt{signature} \; X = S_2}{
adamc@537	1089 \Gamma \vdash S_1 \leq S_2
adamc@537	1090 & \Gamma \vdash S_2 \leq S_1
adamc@537	1091 }$$
adamc@537	1092
adamc@537	1093 $$\infer{\Gamma \vdash \mt{constraint} \; c_1 \sim c_2 \leq \mt{constraint} \; c'_1 \sim c'_2}{
adamc@537	1094 \Gamma \vdash c_1 \equiv c'_1
adamc@537	1095 & \Gamma \vdash c_2 \equiv c'_2
adamc@537	1096 }$$
adamc@537	1097
adamc@655	1098 $$\infer{\Gamma \vdash \mt{class} \; x :: \kappa \leq \mt{class} \; x :: \kappa}{}
adamc@655	1099 \quad \infer{\Gamma \vdash \mt{class} \; x :: \kappa = c \leq \mt{class} \; x :: \kappa}{}
adamc@655	1100 \quad \infer{\Gamma \vdash \mt{class} \; x :: \kappa = c_1 \leq \mt{class} \; x :: \kappa = c_2}{
adamc@537	1101 \Gamma \vdash c_1 \equiv c_2
adamc@537	1102 }$$
adamc@537	1103
adamc@538	1104 \subsection{Module Typing}
adamc@538	1105
adamc@538	1106 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	1107
adamc@538	1108 $$\infer{\Gamma \vdash M : S}{
adamc@538	1109 \Gamma \vdash M : S'
adamc@538	1110 & \Gamma \vdash S' \leq S
adamc@538	1111 }
adamc@538	1112 \quad \infer{\Gamma \vdash \mt{struct} \; \overline{d} \; \mt{end} : \mt{sig} \; \mt{sigOf}(\overline{d}) \; \mt{end}}{
adamc@538	1113 \Gamma \vdash \overline{d} \leadsto \Gamma'
adamc@538	1114 }
adamc@538	1115 \quad \infer{\Gamma \vdash X : S}{
adamc@538	1116 X : S \in \Gamma
adamc@538	1117 }$$
adamc@538	1118
adamc@538	1119 $$\infer{\Gamma \vdash M.X : S}{
adamc@538	1120 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@538	1121 & \mt{proj}(M, \overline{s}, \mt{structure} \; X) = S
adamc@538	1122 }$$
adamc@538	1123
adamc@538	1124 $$\infer{\Gamma \vdash M_1(M_2) : [X \mapsto M_2]S_2}{
adamc@538	1125 \Gamma \vdash M_1 : \mt{functor}(X : S_1) : S_2
adamc@538	1126 & \Gamma \vdash M_2 : S_1
adamc@538	1127 }
adamc@538	1128 \quad \infer{\Gamma \vdash \mt{functor} (X : S_1) : S_2 = M : \mt{functor} (X : S_1) : S_2}{
adamc@538	1129 \Gamma \vdash S_1
adamc@538	1130 & \Gamma, X : S_1 \vdash S_2
adamc@538	1131 & \Gamma, X : S_1 \vdash M : S_2
adamc@538	1132 }$$
adamc@538	1133
adamc@538	1134 \begin{eqnarray*}
adamc@538	1135 \mt{sigOf}(\cdot) &=& \cdot \\
adamc@538	1136 \mt{sigOf}(s \; \overline{s'}) &=& \mt{sigOf}(s) \; \mt{sigOf}(\overline{s'}) \\
adamc@538	1137 \\
adamc@538	1138 \mt{sigOf}(\mt{con} \; x :: \kappa = c) &=& \mt{con} \; x :: \kappa = c \\
adamc@538	1139 \mt{sigOf}(\mt{datatype} \; x \; \overline{y} = \overline{dc}) &=& \mt{datatype} \; x \; \overline{y} = \overline{dc} \\
adamc@538	1140 \mt{sigOf}(\mt{datatype} \; x = \mt{datatype} \; M.z) &=& \mt{datatype} \; x = \mt{datatype} \; M.z \\
adamc@538	1141 \mt{sigOf}(\mt{val} \; x : \tau = e) &=& \mt{val} \; x : \tau \\
adamc@538	1142 \mt{sigOf}(\mt{val} \; \mt{rec} \; \overline{x : \tau = e}) &=& \overline{\mt{val} \; x : \tau} \\
adamc@538	1143 \mt{sigOf}(\mt{structure} \; X : S = M) &=& \mt{structure} \; X : S \\
adamc@538	1144 \mt{sigOf}(\mt{signature} \; X = S) &=& \mt{signature} \; X = S \\
adamc@538	1145 \mt{sigOf}(\mt{open} \; M) &=& \mt{include} \; S \textrm{ (where $\Gamma \vdash M : S$)} \\
adamc@538	1146 \mt{sigOf}(\mt{constraint} \; c_1 \sim c_2) &=& \mt{constraint} \; c_1 \sim c_2 \\
adamc@538	1147 \mt{sigOf}(\mt{open} \; \mt{constraints} \; M) &=& \cdot \\
adamc@538	1148 \mt{sigOf}(\mt{table} \; x : c) &=& \mt{table} \; x : c \\
adamc@784	1149 \mt{sigOf}(\mt{view} \; x : c) &=& \mt{view} \; x : c \\
adamc@538	1150 \mt{sigOf}(\mt{sequence} \; x) &=& \mt{sequence} \; x \\
adamc@538	1151 \mt{sigOf}(\mt{cookie} \; x : \tau) &=& \mt{cookie} \; x : \tau \\
adamc@784	1152 \mt{sigOf}(\mt{style} \; x) &=& \mt{style} \; x \\
adamc@655	1153 \mt{sigOf}(\mt{class} \; x :: \kappa = c) &=& \mt{class} \; x :: \kappa = c \\
adamc@538	1154 \end{eqnarray*}
adamc@539	1155 \begin{eqnarray*}
adamc@539	1156 \mt{selfify}(M, \cdot) &=& \cdot \\
adamc@558	1157 \mt{selfify}(M, s \; \overline{s'}) &=& \mt{selfify}(M, s) \; \mt{selfify}(M, \overline{s'}) \\
adamc@539	1158 \\
adamc@539	1159 \mt{selfify}(M, \mt{con} \; x :: \kappa) &=& \mt{con} \; x :: \kappa = M.x \\
adamc@539	1160 \mt{selfify}(M, \mt{con} \; x :: \kappa = c) &=& \mt{con} \; x :: \kappa = c \\
adamc@539	1161 \mt{selfify}(M, \mt{datatype} \; x \; \overline{y} = \overline{dc}) &=& \mt{datatype} \; x \; \overline{y} = \mt{datatype} \; M.x \\
adamc@539	1162 \mt{selfify}(M, \mt{datatype} \; x = \mt{datatype} \; M'.z) &=& \mt{datatype} \; x = \mt{datatype} \; M'.z \\
adamc@539	1163 \mt{selfify}(M, \mt{val} \; x : \tau) &=& \mt{val} \; x : \tau \\
adamc@539	1164 \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	1165 \mt{selfify}(M, \mt{signature} \; X = S) &=& \mt{signature} \; X = S \\
adamc@539	1166 \mt{selfify}(M, \mt{include} \; S) &=& \mt{include} \; S \\
adamc@539	1167 \mt{selfify}(M, \mt{constraint} \; c_1 \sim c_2) &=& \mt{constraint} \; c_1 \sim c_2 \\
adamc@655	1168 \mt{selfify}(M, \mt{class} \; x :: \kappa) &=& \mt{class} \; x :: \kappa = M.x \\
adamc@655	1169 \mt{selfify}(M, \mt{class} \; x :: \kappa = c) &=& \mt{class} \; x :: \kappa = c \\
adamc@539	1170 \end{eqnarray*}
adamc@539	1171
adamc@540	1172 \subsection{Module Projection}
adamc@540	1173
adamc@540	1174 \begin{eqnarray*}
adamc@540	1175 \mt{proj}(M, \mt{con} \; x :: \kappa \; \overline{s}, \mt{con} \; x) &=& \kappa \\
adamc@540	1176 \mt{proj}(M, \mt{con} \; x :: \kappa = c \; \overline{s}, \mt{con} \; x) &=& (\kappa, c) \\
adamc@540	1177 \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	1178 \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	1179 && \textrm{and $\mt{proj}(M', \overline{s'}, \mt{datatype} \; z) = (\overline{y}, \overline{dc})$)} \\
adamc@655	1180 \mt{proj}(M, \mt{class} \; x :: \kappa \; \overline{s}, \mt{con} \; x) &=& \kappa \to \mt{Type} \\
adamc@655	1181 \mt{proj}(M, \mt{class} \; x :: \kappa = c \; \overline{s}, \mt{con} \; x) &=& (\kappa \to \mt{Type}, c) \\
adamc@540	1182 \\
adamc@540	1183 \mt{proj}(M, \mt{datatype} \; x \; \overline{y} = \overline{dc} \; \overline{s}, \mt{datatype} \; x) &=& (\overline{y}, \overline{dc}) \\
adamc@540	1184 \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	1185 \\
adamc@540	1186 \mt{proj}(M, \mt{val} \; x : \tau \; \overline{s}, \mt{val} \; x) &=& \tau \\
adamc@540	1187 \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	1188 \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	1189 \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	1190 && \textrm{and $\mt{proj}(M', \overline{s'}, \mt{datatype} \; z = (\overline{y}, \overline{dc})$ and $X \in \overline{dc}$)} \\
adamc@540	1191 \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	1192 && \textrm{and $\mt{proj}(M', \overline{s'}, \mt{datatype} \; z = (\overline{y}, \overline{dc})$ and $X \; \mt{of} \; \tau \in \overline{dc}$)} \\
adamc@540	1193 \\
adamc@540	1194 \mt{proj}(M, \mt{structure} \; X : S \; \overline{s}, \mt{structure} \; X) &=& S \\
adamc@540	1195 \\
adamc@540	1196 \mt{proj}(M, \mt{signature} \; X = S \; \overline{s}, \mt{signature} \; X) &=& S \\
adamc@540	1197 \\
adamc@540	1198 \mt{proj}(M, \mt{con} \; x :: \kappa \; \overline{s}, V) &=& [x \mapsto M.x]\mt{proj}(M, \overline{s}, V) \\
adamc@540	1199 \mt{proj}(M, \mt{con} \; x :: \kappa = c \; \overline{s}, V) &=& [x \mapsto M.x]\mt{proj}(M, \overline{s}, V) \\
adamc@540	1200 \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	1201 \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	1202 \mt{proj}(M, \mt{val} \; x : \tau \; \overline{s}, V) &=& \mt{proj}(M, \overline{s}, V) \\
adamc@540	1203 \mt{proj}(M, \mt{structure} \; X : S \; \overline{s}, V) &=& [X \mapsto M.X]\mt{proj}(M, \overline{s}, V) \\
adamc@540	1204 \mt{proj}(M, \mt{signature} \; X = S \; \overline{s}, V) &=& [X \mapsto M.X]\mt{proj}(M, \overline{s}, V) \\
adamc@540	1205 \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	1206 \mt{proj}(M, \mt{constraint} \; c_1 \sim c_2 \; \overline{s}, V) &=& \mt{proj}(M, \overline{s}, V) \\
adamc@655	1207 \mt{proj}(M, \mt{class} \; x :: \kappa \; \overline{s}, V) &=& [x \mapsto M.x]\mt{proj}(M, \overline{s}, V) \\
adamc@655	1208 \mt{proj}(M, \mt{class} \; x :: \kappa = c \; \overline{s}, V) &=& [x \mapsto M.x]\mt{proj}(M, \overline{s}, V) \\
adamc@540	1209 \end{eqnarray*}
adamc@540	1210
adamc@541	1211
adamc@541	1212 \section{Type Inference}
adamc@541	1213
adamc@541	1214 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	1215
adamc@541	1216 \subsection{Basic Unification}
adamc@541	1217
adamc@560	1218 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	1219
adamc@656	1220 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	1221
adamc@541	1222 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	1223
adamc@541	1224 \subsection{Unifying Record Types}
adamc@541	1225
adamc@570	1226 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	1227
adamc@656	1228 \subsection{\label{typeclasses}Constructor Classes}
adamc@541	1229
adamc@784	1230 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	1231
adamc@784	1232 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	1233
adamc@656	1234 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	1235
adamc@656	1236 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	1237
adamc@541	1238 \subsection{Reverse-Engineering Record Types}
adamc@541	1239
adamc@656	1240 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	1241
adamc@541	1242 \subsection{Implicit Arguments in Functor Applications}
adamc@541	1243
adamc@656	1244 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	1245
adamc@541	1246
adamc@542	1247 \section{The Ur Standard Library}
adamc@542	1248
adamc@542	1249 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	1250
adamc@542	1251 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	1252
adamc@542	1253 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	1254 $$\begin{array}{l}
adamc@542	1255 \mt{type} \; \mt{int} \\
adamc@542	1256 \mt{type} \; \mt{float} \\
adamc@873	1257 \mt{type} \; \mt{char} \\
adamc@542	1258 \mt{type} \; \mt{string} \\
adamc@542	1259 \mt{type} \; \mt{time} \\
adamc@785	1260 \mt{type} \; \mt{blob} \\
adamc@542	1261 \\
adamc@542	1262 \mt{type} \; \mt{unit} = \{\} \\
adamc@542	1263 \\
adamc@542	1264 \mt{datatype} \; \mt{bool} = \mt{False} \mid \mt{True} \\
adamc@542	1265 \\
adamc@785	1266 \mt{datatype} \; \mt{option} \; \mt{t} = \mt{None} \mid \mt{Some} \; \mt{of} \; \mt{t} \\
adamc@785	1267 \\
adamc@785	1268 \mt{datatype} \; \mt{list} \; \mt{t} = \mt{Nil} \mid \mt{Cons} \; \mt{of} \; \mt{t} \times \mt{list} \; \mt{t}
adamc@542	1269 \end{array}$$
adamc@542	1270
adamc@1123	1271 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	1272
adamc@657	1273 Another important generic Ur element comes at the beginning of \texttt{top.urs}.
adamc@657	1274
adamc@657	1275 $$\begin{array}{l}
adamc@657	1276 \mt{con} \; \mt{folder} :: \mt{K} \longrightarrow \{\mt{K}\} \to \mt{Type} \\
adamc@657	1277 \\
adamc@657	1278 \mt{val} \; \mt{fold} : \mt{K} \longrightarrow \mt{tf} :: (\{\mt{K}\} \to \mt{Type}) \\
adamc@657	1279 \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	1280 \hspace{.2in} \mt{tf} \; \mt{r} \to \mt{tf} \; ([\mt{nm} = \mt{v}] \rc \mt{r})) \\
adamc@657	1281 \hspace{.1in} \to \mt{tf} \; [] \\
adamc@657	1282 \hspace{.1in} \to \mt{r} :: \{\mt{K}\} \to \mt{folder} \; \mt{r} \to \mt{tf} \; \mt{r}
adamc@657	1283 \end{array}$$
adamc@657	1284
adamc@657	1285 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	1286
adamc@664	1287 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	1288
adamc@542	1289
adamc@542	1290 \section{The Ur/Web Standard Library}
adamc@542	1291
adamc@658	1292 \subsection{Monads}
adamc@658	1293
adamc@658	1294 The Ur Basis defines the monad constructor class from Haskell.
adamc@658	1295
adamc@658	1296 $$\begin{array}{l}
adamc@658	1297 \mt{class} \; \mt{monad} :: \mt{Type} \to \mt{Type} \\
adamc@658	1298 \mt{val} \; \mt{return} : \mt{m} ::: (\mt{Type} \to \mt{Type}) \to \mt{t} ::: \mt{Type} \\
adamc@658	1299 \hspace{.1in} \to \mt{monad} \; \mt{m} \\
adamc@658	1300 \hspace{.1in} \to \mt{t} \to \mt{m} \; \mt{t} \\
adamc@658	1301 \mt{val} \; \mt{bind} : \mt{m} ::: (\mt{Type} \to \mt{Type}) \to \mt{t1} ::: \mt{Type} \to \mt{t2} ::: \mt{Type} \\
adamc@658	1302 \hspace{.1in} \to \mt{monad} \; \mt{m} \\
adamc@658	1303 \hspace{.1in} \to \mt{m} \; \mt{t1} \to (\mt{t1} \to \mt{m} \; \mt{t2}) \\
adamc@658	1304 \hspace{.1in} \to \mt{m} \; \mt{t2}
adamc@658	1305 \end{array}$$
adamc@658	1306
adamc@542	1307 \subsection{Transactions}
adamc@542	1308
adamc@542	1309 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	1310 $$\begin{array}{l}
adamc@542	1311 \mt{con} \; \mt{transaction} :: \mt{Type} \to \mt{Type} \\
adamc@658	1312 \mt{val} \; \mt{transaction\_monad} : \mt{monad} \; \mt{transaction}
adamc@542	1313 \end{array}$$
adamc@542	1314
adamc@1123	1315 For debugging purposes, a transactional function is provided for outputting a string on the server process' \texttt{stderr}.
adamc@1123	1316 $$\begin{array}{l}
adamc@1123	1317 \mt{val} \; \mt{debug} : \mt{string} \to \mt{transaction} \; \mt{unit}
adamc@1123	1318 \end{array}$$
adamc@1123	1319
adamc@542	1320 \subsection{HTTP}
adamc@542	1321
adamc@542	1322 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	1323 $$\begin{array}{l}
adamc@786	1324 \mt{val} \; \mt{requestHeader} : \mt{string} \to \mt{transaction} \; (\mt{option} \; \mt{string}) \\
adamc@786	1325 \\
adamc@786	1326 \mt{con} \; \mt{http\_cookie} :: \mt{Type} \to \mt{Type} \\
adamc@786	1327 \mt{val} \; \mt{getCookie} : \mt{t} ::: \mt{Type} \to \mt{http\_cookie} \; \mt{t} \to \mt{transaction} \; (\mt{option} \; \mt{t}) \\
adamc@1050	1328 \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	1329 \mt{val} \; \mt{clearCookie} : \mt{t} ::: \mt{Type} \to \mt{http\_cookie} \; \mt{t} \to \mt{transaction} \; \mt{unit}
adamc@786	1330 \end{array}$$
adamc@786	1331
adamc@786	1332 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	1333 $$\begin{array}{l}
adamc@786	1334 \mt{type} \; \mt{url} \\
adamc@786	1335 \mt{val} \; \mt{bless} : \mt{string} \to \mt{url} \\
adamc@786	1336 \mt{val} \; \mt{checkUrl} : \mt{string} \to \mt{option} \; \mt{url}
adamc@786	1337 \end{array}$$
adamc@786	1338 $\mt{bless}$ raises a runtime error if the string passed to it fails the URL policy.
adamc@786	1339
adamc@1085	1340 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	1341 $$\begin{array}{l}
adamc@1085	1342 \mt{val} \; \mt{currentUrl} : \mt{transaction} \; \mt{url} \\
adamc@1085	1343 \mt{val} \; \mt{url} : \mt{transaction} \; \mt{page} \to \mt{url}
adamc@1085	1344 \end{array}$$
adamc@1085	1345
adamc@1085	1346 Page generation may be interrupted at any time with a request to redirect to a particular URL instead.
adamc@1085	1347 $$\begin{array}{l}
adamc@1085	1348 \mt{val} \; \mt{redirect} : \mt{t} ::: \mt{Type} \to \mt{url} \to \mt{transaction} \; \mt{t}
adamc@1085	1349 \end{array}$$
adamc@1085	1350
adamc@786	1351 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	1352 $$\begin{array}{l}
adamc@786	1353 \mt{type} \; \mt{file} \\
adamc@786	1354 \mt{val} \; \mt{fileName} : \mt{file} \to \mt{option} \; \mt{string} \\
adamc@786	1355 \mt{val} \; \mt{fileMimeType} : \mt{file} \to \mt{string} \\
adamc@786	1356 \mt{val} \; \mt{fileData} : \mt{file} \to \mt{blob}
adamc@786	1357 \end{array}$$
adamc@786	1358
adamc@786	1359 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	1360 $$\begin{array}{l}
adamc@786	1361 \mt{type} \; \mt{mimeType} \\
adamc@786	1362 \mt{val} \; \mt{blessMime} : \mt{string} \to \mt{mimeType} \\
adamc@786	1363 \mt{val} \; \mt{checkMime} : \mt{string} \to \mt{option} \; \mt{mimeType} \\
adamc@786	1364 \mt{val} \; \mt{returnBlob} : \mt{t} ::: \mt{Type} \to \mt{blob} \to \mt{mimeType} \to \mt{transaction} \; \mt{t}
adamc@542	1365 \end{array}$$
adamc@542	1366
adamc@543	1367 \subsection{SQL}
adamc@543	1368
adamc@543	1369 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	1370 $$\begin{array}{l}
adamc@785	1371 \mt{con} \; \mt{sql\_table} :: \{\mt{Type}\} \to \{\{\mt{Unit}\}\} \to \mt{Type}
adamc@785	1372 \end{array}$$
adamc@785	1373 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	1374
adamc@785	1375 We also have the simpler type family of SQL views, which have no keys.
adamc@785	1376 $$\begin{array}{l}
adamc@785	1377 \mt{con} \; \mt{sql\_view} :: \{\mt{Type}\} \to \mt{Type}
adamc@543	1378 \end{array}$$
adamc@543	1379
adamc@785	1380 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	1381 $$\begin{array}{l}
adamc@785	1382 \mt{class} \; \mt{fieldsOf} :: \mt{Type} \to \{\mt{Type}\} \to \mt{Type} \\
adamc@785	1383 \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	1384 \mt{val} \; \mt{fieldsOf\_view} : \mt{fs} ::: \{\mt{Type}\} \to \mt{fieldsOf} \; (\mt{sql\_view} \; \mt{fs}) \; \mt{fs}
adamc@785	1385 \end{array}$$
adamc@785	1386
adamc@785	1387 \subsubsection{Table Constraints}
adamc@785	1388
adamc@785	1389 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	1390
adamc@785	1391 $$\begin{array}{l}
adamc@785	1392 \mt{con} \; \mt{primary\_key} :: \{\mt{Type}\} \to \{\{\mt{Unit}\}\} \to \mt{Type} \\
adamc@785	1393 \mt{val} \; \mt{no\_primary\_key} : \mt{fs} ::: \{\mt{Type}\} \to \mt{primary\_key} \; \mt{fs} \; [] \\
adamc@785	1394 \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	1395 \hspace{.1in} \to [[\mt{key1}] \sim \mt{keys}] \Rightarrow [[\mt{key1} = \mt{t}] \rc \mt{keys} \sim \mt{rest}] \\
adamc@785	1396 \hspace{.1in} \Rightarrow \$([\mt{key1} = \mt{sql\_injectable\_prim} \; \mt{t}] \rc \mt{map} \; \mt{sql\_injectable\_prim} \; \mt{keys}) \\
adamc@785	1397 \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	1398 \end{array}$$
adamc@785	1399 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	1400
adamc@785	1401 A type family stands for sets of named constraints of the remaining varieties.
adamc@785	1402 $$\begin{array}{l}
adamc@785	1403 \mt{con} \; \mt{sql\_constraints} :: \{\mt{Type}\} \to \{\{\mt{Unit}\}\} \to \mt{Type}
adamc@785	1404 \end{array}$$
adamc@785	1405 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	1406
adamc@785	1407 There is a type family of individual, unnamed constraints.
adamc@785	1408 $$\begin{array}{l}
adamc@785	1409 \mt{con} \; \mt{sql\_constraint} :: \{\mt{Type}\} \to \{\mt{Unit}\} \to \mt{Type}
adamc@785	1410 \end{array}$$
adamc@785	1411 The first argument is the same as above, and the second argument gives the key columns for just this constraint.
adamc@785	1412
adamc@785	1413 We have operations for assembling constraints into constraint sets.
adamc@785	1414 $$\begin{array}{l}
adamc@785	1415 \mt{val} \; \mt{no\_constraint} : \mt{fs} ::: \{\mt{Type}\} \to \mt{sql\_constraints} \; \mt{fs} \; [] \\
adamc@785	1416 \mt{val} \; \mt{one\_constraint} : \mt{fs} ::: \{\mt{Type}\} \to \mt{unique} ::: \{\mt{Unit}\} \to \mt{name} :: \mt{Name} \\
adamc@785	1417 \hspace{.1in} \to \mt{sql\_constraint} \; \mt{fs} \; \mt{unique} \to \mt{sql\_constraints} \; \mt{fs} \; [\mt{name} = \mt{unique}] \\
adamc@785	1418 \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	1419 \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	1420 \end{array}$$
adamc@785	1421
adamc@785	1422 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	1423 $$\begin{array}{l}
adamc@785	1424 \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	1425 \hspace{.1in} \to [[\mt{unique1}] \sim \mt{unique}] \Rightarrow [[\mt{unique1} = \mt{t}] \rc \mt{unique} \sim \mt{rest}] \\
adamc@785	1426 \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	1427 \end{array}$$
adamc@785	1428
adamc@785	1429 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	1430 $$\begin{array}{l}
adamc@785	1431 \mt{class} \; \mt{linkable} :: \mt{Type} \to \mt{Type} \to \mt{Type} \\
adamc@785	1432 \mt{val} \; \mt{linkable\_same} : \mt{t} ::: \mt{Type} \to \mt{linkable} \; \mt{t} \; \mt{t} \\
adamc@785	1433 \mt{val} \; \mt{linkable\_from\_nullable} : \mt{t} ::: \mt{Type} \to \mt{linkable} \; (\mt{option} \; \mt{t}) \; \mt{t} \\
adamc@785	1434 \mt{val} \; \mt{linkable\_to\_nullable} : \mt{t} ::: \mt{Type} \to \mt{linkable} \; \mt{t} \; (\mt{option} \; \mt{t})
adamc@785	1435 \end{array}$$
adamc@785	1436
adamc@785	1437 The $\mt{matching}$ type family uses $\mt{linkable}$ to define when two keys match up type-wise.
adamc@785	1438 $$\begin{array}{l}
adamc@785	1439 \mt{con} \; \mt{matching} :: \{\mt{Type}\} \to \{\mt{Type}\} \to \mt{Type} \\
adamc@785	1440 \mt{val} \; \mt{mat\_nil} : \mt{matching} \; [] \; [] \\
adamc@785	1441 \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	1442 \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	1443 \hspace{.1in} \to \mt{matching} \; ([\mt{nm1} = \mt{t1}] \rc \mt{rest1}) \; ([\mt{nm2} = \mt{t2}] \rc \mt{rest2})
adamc@785	1444 \end{array}$$
adamc@785	1445
adamc@785	1446 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	1447 $$\begin{array}{l}
adamc@785	1448 \mt{con} \; \mt{propagation\_mode} :: \{\mt{Type}\} \to \mt{Type} \\
adamc@785	1449 \mt{val} \; \mt{restrict} : \mt{fs} ::: \{\mt{Type}\} \to \mt{propagation\_mode} \; \mt{fs} \\
adamc@785	1450 \mt{val} \; \mt{cascade} : \mt{fs} ::: \{\mt{Type}\} \to \mt{propagation\_mode} \; \mt{fs} \\
adamc@785	1451 \mt{val} \; \mt{no\_action} : \mt{fs} ::: \{\mt{Type}\} \to \mt{propagation\_mode} \; \mt{fs} \\
adamc@785	1452 \mt{val} \; \mt{set\_null} : \mt{fs} ::: \{\mt{Type}\} \to \mt{propagation\_mode} \; (\mt{map} \; \mt{option} \; \mt{fs})
adamc@785	1453 \end{array}$$
adamc@785	1454
adamc@785	1455 Finally, we put these ingredient together to define the \texttt{FOREIGN KEY} constraint function.
adamc@785	1456 $$\begin{array}{l}
adamc@785	1457 \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	1458 \hspace{.1in} \to \mt{funused} ::: \{\mt{Type}\} \to \mt{nm} ::: \mt{Name} \to \mt{uniques} ::: \{\{\mt{Unit}\}\} \\
adamc@785	1459 \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	1460 \hspace{.1in} \Rightarrow \mt{matching} \; ([\mt{mine1} = \mt{t}] \rc \mt{mine}) \; \mt{foreign} \\
adamc@785	1461 \hspace{.1in} \to \mt{sql\_table} \; (\mt{foreign} \rc \mt{funused}) \; ([\mt{nm} = \mt{map} \; (\lambda \_ \Rightarrow ()) \; \mt{foreign}] \rc \mt{uniques}) \\
adamc@785	1462 \hspace{.1in} \to \{\mt{OnDelete} : \mt{propagation\_mode} \; ([\mt{mine1} = \mt{t}] \rc \mt{mine}), \\
adamc@785	1463 \hspace{.2in} \mt{OnUpdate} : \mt{propagation\_mode} \; ([\mt{mine1} = \mt{t}] \rc \mt{mine})\} \\
adamc@785	1464 \hspace{.1in} \to \mt{sql\_constraint} \; ([\mt{mine1} = \mt{t}] \rc \mt{mine} \rc \mt{munused}) \; []
adamc@785	1465 \end{array}$$
adamc@785	1466
adamc@785	1467 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	1468 $$\begin{array}{l}
adamc@785	1469 \mt{val} \; \mt{check} : \mt{fs} ::: \{\mt{Type}\} \to \mt{sql\_exp} \; [] \; [] \; \mt{fs} \; \mt{bool} \to \mt{sql\_constraint} \; \mt{fs} \; []
adamc@785	1470 \end{array}$$
adamc@785	1471
adamc@785	1472 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	1473
adamc@784	1474
adamc@543	1475 \subsubsection{Queries}
adamc@543	1476
adamc@543	1477 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	1478 $$\begin{array}{l}
adamc@543	1479 \mt{con} \; \mt{sql\_query} :: \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \\
adamc@543	1480 \mt{val} \; \mt{sql\_query} : \mt{tables} ::: \{\{\mt{Type}\}\} \\
adamc@543	1481 \hspace{.1in} \to \mt{selectedFields} ::: \{\{\mt{Type}\}\} \\
adamc@543	1482 \hspace{.1in} \to \mt{selectedExps} ::: \{\mt{Type}\} \\
adamc@543	1483 \hspace{.1in} \to \{\mt{Rows} : \mt{sql\_query1} \; \mt{tables} \; \mt{selectedFields} \; \mt{selectedExps}, \\
adamc@543	1484 \hspace{.2in} \mt{OrderBy} : \mt{sql\_order\_by} \; \mt{tables} \; \mt{selectedExps}, \\
adamc@543	1485 \hspace{.2in} \mt{Limit} : \mt{sql\_limit}, \\
adamc@543	1486 \hspace{.2in} \mt{Offset} : \mt{sql\_offset}\} \\
adamc@543	1487 \hspace{.1in} \to \mt{sql\_query} \; \mt{selectedFields} \; \mt{selectedExps}
adamc@543	1488 \end{array}$$
adamc@543	1489
adamc@545	1490 Queries are used by folding over their results inside transactions.
adamc@545	1491 $$\begin{array}{l}
adamc@545	1492 \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	1493 \hspace{.1in} \to (\$(\mt{exps} \rc \mt{map} \; (\lambda \mt{fields} :: \{\mt{Type}\} \Rightarrow \$\mt{fields}) \; \mt{tables}) \\
adamc@545	1494 \hspace{.2in} \to \mt{state} \to \mt{transaction} \; \mt{state}) \\
adamc@545	1495 \hspace{.1in} \to \mt{state} \to \mt{transaction} \; \mt{state}
adamc@545	1496 \end{array}$$
adamc@545	1497
adamc@543	1498 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	1499 $$\begin{array}{l}
adamc@543	1500 \mt{con} \; \mt{sql\_query1} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \\
adamc@543	1501 \\
adamc@543	1502 \mt{type} \; \mt{sql\_relop} \\
adamc@543	1503 \mt{val} \; \mt{sql\_union} : \mt{sql\_relop} \\
adamc@543	1504 \mt{val} \; \mt{sql\_intersect} : \mt{sql\_relop} \\
adamc@543	1505 \mt{val} \; \mt{sql\_except} : \mt{sql\_relop} \\
adamc@543	1506 \mt{val} \; \mt{sql\_relop} : \mt{tables1} ::: \{\{\mt{Type}\}\} \\
adamc@543	1507 \hspace{.1in} \to \mt{tables2} ::: \{\{\mt{Type}\}\} \\
adamc@543	1508 \hspace{.1in} \to \mt{selectedFields} ::: \{\{\mt{Type}\}\} \\
adamc@543	1509 \hspace{.1in} \to \mt{selectedExps} ::: \{\mt{Type}\} \\
adamc@543	1510 \hspace{.1in} \to \mt{sql\_relop} \\
adamc@543	1511 \hspace{.1in} \to \mt{sql\_query1} \; \mt{tables1} \; \mt{selectedFields} \; \mt{selectedExps} \\
adamc@543	1512 \hspace{.1in} \to \mt{sql\_query1} \; \mt{tables2} \; \mt{selectedFields} \; \mt{selectedExps} \\
adamc@543	1513 \hspace{.1in} \to \mt{sql\_query1} \; \mt{selectedFields} \; \mt{selectedFields} \; \mt{selectedExps}
adamc@543	1514 \end{array}$$
adamc@543	1515
adamc@543	1516 $$\begin{array}{l}
adamc@543	1517 \mt{val} \; \mt{sql\_query1} : \mt{tables} ::: \{\{\mt{Type}\}\} \\
adamc@543	1518 \hspace{.1in} \to \mt{grouped} ::: \{\{\mt{Type}\}\} \\
adamc@543	1519 \hspace{.1in} \to \mt{selectedFields} ::: \{\{\mt{Type}\}\} \\
adamc@543	1520 \hspace{.1in} \to \mt{selectedExps} ::: \{\mt{Type}\} \\
adamc@1085	1521 \hspace{.1in} \to \mt{empties} :: \{\mt{Unit}\} \\
adamc@1085	1522 \hspace{.1in} \to [\mt{empties} \sim \mt{selectedFields}] \\
adamc@1085	1523 \hspace{.1in} \Rightarrow \{\mt{Distinct} : \mt{bool}, \\
adamc@994	1524 \hspace{.2in} \mt{From} : \mt{sql\_from\_items} \; \mt{tables}, \\
adamc@543	1525 \hspace{.2in} \mt{Where} : \mt{sql\_exp} \; \mt{tables} \; [] \; [] \; \mt{bool}, \\
adamc@543	1526 \hspace{.2in} \mt{GroupBy} : \mt{sql\_subset} \; \mt{tables} \; \mt{grouped}, \\
adamc@543	1527 \hspace{.2in} \mt{Having} : \mt{sql\_exp} \; \mt{grouped} \; \mt{tables} \; [] \; \mt{bool}, \\
adamc@1085	1528 \hspace{.2in} \mt{SelectFields} : \mt{sql\_subset} \; \mt{grouped} \; (\mt{map} \; (\lambda \_ \Rightarrow []) \; \mt{empties} \rc \mt{selectedFields}), \\
adamc@658	1529 \hspace{.2in} \mt {SelectExps} : \$(\mt{map} \; (\mt{sql\_exp} \; \mt{grouped} \; \mt{tables} \; []) \; \mt{selectedExps}) \} \\
adamc@543	1530 \hspace{.1in} \to \mt{sql\_query1} \; \mt{tables} \; \mt{selectedFields} \; \mt{selectedExps}
adamc@543	1531 \end{array}$$
adamc@543	1532
adamc@543	1533 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	1534 $$\begin{array}{l}
adamc@543	1535 \mt{con} \; \mt{sql\_subset} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \mt{Type} \\
adamc@543	1536 \mt{val} \; \mt{sql\_subset} : \mt{keep\_drop} :: \{(\{\mt{Type}\} \times \{\mt{Type}\})\} \\
adamc@543	1537 \hspace{.1in} \to \mt{sql\_subset} \\
adamc@658	1538 \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	1539 \hspace{.2in} (\mt{map} \; (\lambda \mt{fields} :: (\{\mt{Type}\} \times \{\mt{Type}\}) \Rightarrow \mt{fields}.1) \; \mt{keep\_drop}) \\
adamc@543	1540 \mt{val} \; \mt{sql\_subset\_all} : \mt{tables} :: \{\{\mt{Type}\}\} \to \mt{sql\_subset} \; \mt{tables} \; \mt{tables}
adamc@543	1541 \end{array}$$
adamc@543	1542
adamc@560	1543 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	1544 $$\begin{array}{l}
adamc@543	1545 \mt{con} \; \mt{sql\_exp} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \to \mt{Type}
adamc@543	1546 \end{array}$$
adamc@543	1547
adamc@543	1548 Any field in scope may be converted to an expression.
adamc@543	1549 $$\begin{array}{l}
adamc@543	1550 \mt{val} \; \mt{sql\_field} : \mt{otherTabs} ::: \{\{\mt{Type}\}\} \to \mt{otherFields} ::: \{\mt{Type}\} \\
adamc@543	1551 \hspace{.1in} \to \mt{fieldType} ::: \mt{Type} \to \mt{agg} ::: \{\{\mt{Type}\}\} \\
adamc@543	1552 \hspace{.1in} \to \mt{exps} ::: \{\mt{Type}\} \\
adamc@543	1553 \hspace{.1in} \to \mt{tab} :: \mt{Name} \to \mt{field} :: \mt{Name} \\
adamc@543	1554 \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	1555 \end{array}$$
adamc@543	1556
adamc@544	1557 There is an analogous function for referencing named expressions.
adamc@544	1558 $$\begin{array}{l}
adamc@544	1559 \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	1560 \hspace{.1in} \to \mt{sql\_exp} \; \mt{tabs} \; \mt{agg} \; ([\mt{nm} = \mt{t}] \rc \mt{rest}) \; \mt{t}
adamc@544	1561 \end{array}$$
adamc@544	1562
adamc@544	1563 Ur values of appropriate types may be injected into SQL expressions.
adamc@544	1564 $$\begin{array}{l}
adamc@786	1565 \mt{class} \; \mt{sql\_injectable\_prim} \\
adamc@786	1566 \mt{val} \; \mt{sql\_bool} : \mt{sql\_injectable\_prim} \; \mt{bool} \\
adamc@786	1567 \mt{val} \; \mt{sql\_int} : \mt{sql\_injectable\_prim} \; \mt{int} \\
adamc@786	1568 \mt{val} \; \mt{sql\_float} : \mt{sql\_injectable\_prim} \; \mt{float} \\
adamc@786	1569 \mt{val} \; \mt{sql\_string} : \mt{sql\_injectable\_prim} \; \mt{string} \\
adamc@786	1570 \mt{val} \; \mt{sql\_time} : \mt{sql\_injectable\_prim} \; \mt{time} \\
adamc@786	1571 \mt{val} \; \mt{sql\_blob} : \mt{sql\_injectable\_prim} \; \mt{blob} \\
adamc@786	1572 \mt{val} \; \mt{sql\_channel} : \mt{t} ::: \mt{Type} \to \mt{sql\_injectable\_prim} \; (\mt{channel} \; \mt{t}) \\
adamc@786	1573 \mt{val} \; \mt{sql\_client} : \mt{sql\_injectable\_prim} \; \mt{client} \\
adamc@786	1574 \\
adamc@544	1575 \mt{class} \; \mt{sql\_injectable} \\
adamc@786	1576 \mt{val} \; \mt{sql\_prim} : \mt{t} ::: \mt{Type} \to \mt{sql\_injectable\_prim} \; \mt{t} \to \mt{sql\_injectable} \; \mt{t} \\
adamc@786	1577 \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	1578 \\
adamc@544	1579 \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	1580 \hspace{.1in} \to \mt{t} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t}
adamc@544	1581 \end{array}$$
adamc@544	1582
adamc@1123	1583 Additionally, most function-free types may be injected safely, via the $\mt{serialized}$ type family.
adamc@1123	1584 $$\begin{array}{l}
adamc@1123	1585 \mt{con} \; \mt{serialized} :: \mt{Type} \to \mt{Type} \\
adamc@1123	1586 \mt{val} \; \mt{serialize} : \mt{t} ::: \mt{Type} \to \mt{t} \to \mt{serialized} \; \mt{t} \\
adamc@1123	1587 \mt{val} \; \mt{deserialize} : \mt{t} ::: \mt{Type} \to \mt{serialized} \; \mt{t} \to \mt{t} \\
adamc@1123	1588 \mt{val} \; \mt{sql\_serialized} : \mt{t} ::: \mt{Type} \to \mt{sql\_injectable\_prim} \; (\mt{serialized} \; \mt{t})
adamc@1123	1589 \end{array}$$
adamc@1123	1590
adamc@544	1591 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	1592 $$\begin{array}{l}
adamc@544	1593 \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	1594 \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	1595 \end{array}$$
adamc@544	1596
adamc@559	1597 We have generic nullary, unary, and binary operators.
adamc@544	1598 $$\begin{array}{l}
adamc@544	1599 \mt{con} \; \mt{sql\_nfunc} :: \mt{Type} \to \mt{Type} \\
adamc@544	1600 \mt{val} \; \mt{sql\_current\_timestamp} : \mt{sql\_nfunc} \; \mt{time} \\
adamc@544	1601 \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	1602 \hspace{.1in} \to \mt{sql\_nfunc} \; \mt{t} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} \\\end{array}$$
adamc@544	1603
adamc@544	1604 $$\begin{array}{l}
adamc@544	1605 \mt{con} \; \mt{sql\_unary} :: \mt{Type} \to \mt{Type} \to \mt{Type} \\
adamc@544	1606 \mt{val} \; \mt{sql\_not} : \mt{sql\_unary} \; \mt{bool} \; \mt{bool} \\
adamc@544	1607 \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	1608 \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	1609 \end{array}$$
adamc@544	1610
adamc@544	1611 $$\begin{array}{l}
adamc@544	1612 \mt{con} \; \mt{sql\_binary} :: \mt{Type} \to \mt{Type} \to \mt{Type} \to \mt{Type} \\
adamc@544	1613 \mt{val} \; \mt{sql\_and} : \mt{sql\_binary} \; \mt{bool} \; \mt{bool} \; \mt{bool} \\
adamc@544	1614 \mt{val} \; \mt{sql\_or} : \mt{sql\_binary} \; \mt{bool} \; \mt{bool} \; \mt{bool} \\
adamc@544	1615 \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	1616 \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	1617 \end{array}$$
adamc@544	1618
adamc@544	1619 $$\begin{array}{l}
adamc@559	1620 \mt{class} \; \mt{sql\_arith} \\
adamc@559	1621 \mt{val} \; \mt{sql\_int\_arith} : \mt{sql\_arith} \; \mt{int} \\
adamc@559	1622 \mt{val} \; \mt{sql\_float\_arith} : \mt{sql\_arith} \; \mt{float} \\
adamc@559	1623 \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	1624 \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	1625 \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	1626 \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	1627 \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	1628 \mt{val} \; \mt{sql\_mod} : \mt{sql\_binary} \; \mt{int} \; \mt{int} \; \mt{int}
adamc@559	1629 \end{array}$$
adamc@544	1630
adamc@656	1631 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	1632 $$\begin{array}{l}
adamc@544	1633 \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	1634 \end{array}$$
adamc@544	1635
adamc@544	1636 $$\begin{array}{l}
adamc@544	1637 \mt{con} \; \mt{sql\_aggregate} :: \mt{Type} \to \mt{Type} \\
adamc@544	1638 \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	1639 \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	1640 \end{array}$$
adamc@544	1641
adamc@544	1642 $$\begin{array}{l}
adamc@544	1643 \mt{class} \; \mt{sql\_summable} \\
adamc@544	1644 \mt{val} \; \mt{sql\_summable\_int} : \mt{sql\_summable} \; \mt{int} \\
adamc@544	1645 \mt{val} \; \mt{sql\_summable\_float} : \mt{sql\_summable} \; \mt{float} \\
adamc@544	1646 \mt{val} \; \mt{sql\_avg} : \mt{t} ::: \mt{Type} \to \mt{sql\_summable} \; \mt{t} \to \mt{sql\_aggregate} \; \mt{t} \\
adamc@544	1647 \mt{val} \; \mt{sql\_sum} : \mt{t} ::: \mt{Type} \to \mt{sql\_summable} \mt{t} \to \mt{sql\_aggregate} \; \mt{t}
adamc@544	1648 \end{array}$$
adamc@544	1649
adamc@544	1650 $$\begin{array}{l}
adamc@544	1651 \mt{class} \; \mt{sql\_maxable} \\
adamc@544	1652 \mt{val} \; \mt{sql\_maxable\_int} : \mt{sql\_maxable} \; \mt{int} \\
adamc@544	1653 \mt{val} \; \mt{sql\_maxable\_float} : \mt{sql\_maxable} \; \mt{float} \\
adamc@544	1654 \mt{val} \; \mt{sql\_maxable\_string} : \mt{sql\_maxable} \; \mt{string} \\
adamc@544	1655 \mt{val} \; \mt{sql\_maxable\_time} : \mt{sql\_maxable} \; \mt{time} \\
adamc@544	1656 \mt{val} \; \mt{sql\_max} : \mt{t} ::: \mt{Type} \to \mt{sql\_maxable} \; \mt{t} \to \mt{sql\_aggregate} \; \mt{t} \\
adamc@544	1657 \mt{val} \; \mt{sql\_min} : \mt{t} ::: \mt{Type} \to \mt{sql\_maxable} \; \mt{t} \to \mt{sql\_aggregate} \; \mt{t}
adamc@544	1658 \end{array}$$
adamc@544	1659
adamc@786	1660 \texttt{FROM} clauses are specified using a type family.
adamc@786	1661 $$\begin{array}{l}
adamc@786	1662 \mt{con} \; \mt{sql\_from\_items} :: \{\{\mt{Type}\}\} \to \mt{Type} \\
adamc@786	1663 \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	1664 \mt{val} \; \mt{sql\_from\_comma} : \mt{tabs1} ::: \{\{\mt{Type}\}\} \to \mt{tabs2} ::: \{\{\mt{Type}\}\} \to [\mt{tabs1} \sim \mt{tabs2}] \\
adamc@786	1665 \hspace{.1in} \Rightarrow \mt{sql\_from\_items} \; \mt{tabs1} \to \mt{sql\_from\_items} \; \mt{tabs2} \\
adamc@786	1666 \hspace{.1in} \to \mt{sql\_from\_items} \; (\mt{tabs1} \rc \mt{tabs2}) \\
adamc@786	1667 \mt{val} \; \mt{sql\_inner\_join} : \mt{tabs1} ::: \{\{\mt{Type}\}\} \to \mt{tabs2} ::: \{\{\mt{Type}\}\} \to [\mt{tabs1} \sim \mt{tabs2}] \\
adamc@786	1668 \hspace{.1in} \Rightarrow \mt{sql\_from\_items} \; \mt{tabs1} \to \mt{sql\_from\_items} \; \mt{tabs2} \\
adamc@786	1669 \hspace{.1in} \to \mt{sql\_exp} \; (\mt{tabs1} \rc \mt{tabs2}) \; [] \; [] \; \mt{bool} \\
adamc@786	1670 \hspace{.1in} \to \mt{sql\_from\_items} \; (\mt{tabs1} \rc \mt{tabs2})
adamc@786	1671 \end{array}$$
adamc@786	1672
adamc@786	1673 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	1674 $$\begin{array}{l}
adamc@786	1675 \mt{class} \; \mt{nullify} :: \mt{Type} \to \mt{Type} \to \mt{Type} \\
adamc@786	1676 \mt{val} \; \mt{nullify\_option} : \mt{t} ::: \mt{Type} \to \mt{nullify} \; (\mt{option} \; \mt{t}) \; (\mt{option} \; \mt{t}) \\
adamc@786	1677 \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	1678 \end{array}$$
adamc@786	1679
adamc@786	1680 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	1681
adamc@786	1682 $$\begin{array}{l}
adamc@786	1683 \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	1684 \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	1685 \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	1686 \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	1687 \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	1688 \end{array}$$
adamc@786	1689
adamc@544	1690 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	1691 $$\begin{array}{l}
adamc@544	1692 \mt{type} \; \mt{sql\_direction} \\
adamc@544	1693 \mt{val} \; \mt{sql\_asc} : \mt{sql\_direction} \\
adamc@544	1694 \mt{val} \; \mt{sql\_desc} : \mt{sql\_direction} \\
adamc@544	1695 \\
adamc@544	1696 \mt{con} \; \mt{sql\_order\_by} :: \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \\
adamc@544	1697 \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	1698 \mt{val} \; \mt{sql\_order\_by\_Cons} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{t} ::: \mt{Type} \\
adamc@544	1699 \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	1700 \\
adamc@544	1701 \mt{type} \; \mt{sql\_limit} \\
adamc@544	1702 \mt{val} \; \mt{sql\_no\_limit} : \mt{sql\_limit} \\
adamc@544	1703 \mt{val} \; \mt{sql\_limit} : \mt{int} \to \mt{sql\_limit} \\
adamc@544	1704 \\
adamc@544	1705 \mt{type} \; \mt{sql\_offset} \\
adamc@544	1706 \mt{val} \; \mt{sql\_no\_offset} : \mt{sql\_offset} \\
adamc@544	1707 \mt{val} \; \mt{sql\_offset} : \mt{int} \to \mt{sql\_offset}
adamc@544	1708 \end{array}$$
adamc@544	1709
adamc@545	1710
adamc@545	1711 \subsubsection{DML}
adamc@545	1712
adamc@545	1713 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	1714
adamc@545	1715 $$\begin{array}{l}
adamc@545	1716 \mt{type} \; \mt{dml} \\
adamc@545	1717 \mt{val} \; \mt{dml} : \mt{dml} \to \mt{transaction} \; \mt{unit}
adamc@545	1718 \end{array}$$
adamc@545	1719
adamc@545	1720 Properly-typed records may be used to form $\mt{INSERT}$ commands.
adamc@545	1721 $$\begin{array}{l}
adamc@545	1722 \mt{val} \; \mt{insert} : \mt{fields} ::: \{\mt{Type}\} \to \mt{sql\_table} \; \mt{fields} \\
adamc@658	1723 \hspace{.1in} \to \$(\mt{map} \; (\mt{sql\_exp} \; [] \; [] \; []) \; \mt{fields}) \to \mt{dml}
adamc@545	1724 \end{array}$$
adamc@545	1725
adamc@545	1726 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	1727 $$\begin{array}{l}
adamc@545	1728 \mt{val} \; \mt{update} : \mt{unchanged} ::: \{\mt{Type}\} \to \mt{changed} :: \{\mt{Type}\} \to \lambda [\mt{changed} \sim \mt{unchanged}] \\
adamc@658	1729 \hspace{.1in} \Rightarrow \$(\mt{map} \; (\mt{sql\_exp} \; [\mt{T} = \mt{changed} \rc \mt{unchanged}] \; [] \; []) \; \mt{changed}) \\
adamc@545	1730 \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	1731 \end{array}$$
adamc@545	1732
adamc@545	1733 A $\mt{DELETE}$ command is formed from a table and a $\mt{WHERE}$ clause.
adamc@545	1734 $$\begin{array}{l}
adamc@545	1735 \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	1736 \end{array}$$
adamc@545	1737
adamc@546	1738 \subsubsection{Sequences}
adamc@546	1739
adamc@546	1740 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	1741
adamc@546	1742 $$\begin{array}{l}
adamc@546	1743 \mt{type} \; \mt{sql\_sequence} \\
adamc@1085	1744 \mt{val} \; \mt{nextval} : \mt{sql\_sequence} \to \mt{transaction} \; \mt{int} \\
adamc@1085	1745 \mt{val} \; \mt{setval} : \mt{sql\_sequence} \to \mt{int} \to \mt{transaction} \; \mt{unit}
adamc@546	1746 \end{array}$$
adamc@546	1747
adamc@546	1748
adamc@547	1749 \subsection{XML}
adamc@547	1750
adamc@547	1751 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	1752
adamc@547	1753 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	1754 $$\begin{array}{l}
adamc@547	1755 \mt{con} \; \mt{xml} :: \{\mt{Unit}\} \to \{\mt{Type}\} \to \{\mt{Type}\} \to \mt{Type}
adamc@547	1756 \end{array}$$
adamc@547	1757
adamc@547	1758 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	1759 $$\begin{array}{l}
adamc@547	1760 \mt{con} \; \mt{tag} :: \{\mt{Type}\} \to \{\mt{Unit}\} \to \{\mt{Unit}\} \to \{\mt{Type}\} \to \{\mt{Type}\} \to \mt{Type}
adamc@547	1761 \end{array}$$
adamc@547	1762
adamc@547	1763 Literal text may be injected into XML as ``CDATA.''
adamc@547	1764 $$\begin{array}{l}
adamc@547	1765 \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	1766 \end{array}$$
adamc@547	1767
adamc@547	1768 There is a function for producing an XML tree with a particular tag at its root.
adamc@547	1769 $$\begin{array}{l}
adamc@547	1770 \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	1771 \hspace{.1in} \to \mt{useOuter} ::: \{\mt{Type}\} \to \mt{useInner} ::: \{\mt{Type}\} \to \mt{bindOuter} ::: \{\mt{Type}\} \to \mt{bindInner} ::: \{\mt{Type}\} \\
adamc@787	1772 \hspace{.1in} \to \lambda [\mt{attrsGiven} \sim \mt{attrsAbsent}] \; [\mt{useOuter} \sim \mt{useInner}] \; [\mt{bindOuter} \sim \mt{bindInner}] \\
adamc@787	1773 \hspace{.1in} \Rightarrow \mt{option} \; \mt{css\_class} \\
adamc@787	1774 \hspace{.1in} \to \$\mt{attrsGiven} \\
adamc@547	1775 \hspace{.1in} \to \mt{tag} \; (\mt{attrsGiven} \rc \mt{attrsAbsent}) \; \mt{ctxOuter} \; \mt{ctxInner} \; \mt{useOuter} \; \mt{bindOuter} \\
adamc@547	1776 \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	1777 \end{array}$$
adamc@787	1778 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	1779
adamc@547	1780 Two XML fragments may be concatenated.
adamc@547	1781 $$\begin{array}{l}
adamc@547	1782 \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	1783 \hspace{.1in} \to \lambda [\mt{use_1} \sim \mt{bind_1}] \; [\mt{bind_1} \sim \mt{bind_2}] \\
adamc@547	1784 \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	1785 \end{array}$$
adamc@547	1786
adamc@547	1787 Finally, any XML fragment may be updated to ``claim'' to use more form fields than it does.
adamc@547	1788 $$\begin{array}{l}
adamc@547	1789 \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	1790 \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	1791 \end{array}$$
adamc@547	1792
adamc@547	1793 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	1794
adamc@547	1795 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	1796 $$\begin{array}{l}
adamc@547	1797 \mt{val} \; \mt{error} : \mt{t} ::: \mt{Type} \to \mt{xml} \; [\mt{Body}] \; [] \; [] \to \mt{t}
adamc@547	1798 \end{array}$$
adamc@547	1799
adamc@549	1800
adamc@701	1801 \subsection{Client-Side Programming}
adamc@659	1802
adamc@701	1803 Ur/Web supports running code on web browsers, via automatic compilation to JavaScript.
adamc@701	1804
adamc@701	1805 \subsubsection{The Basics}
adamc@701	1806
adamc@701	1807 Clients can open alert dialog boxes, in the usual annoying JavaScript way.
adamc@701	1808 $$\begin{array}{l}
adamc@701	1809 \mt{val} \; \mt{alert} : \mt{string} \to \mt{transaction} \; \mt{unit}
adamc@701	1810 \end{array}$$
adamc@701	1811
adamc@701	1812 Any transaction may be run in a new thread with the $\mt{spawn}$ function.
adamc@701	1813 $$\begin{array}{l}
adamc@701	1814 \mt{val} \; \mt{spawn} : \mt{transaction} \; \mt{unit} \to \mt{transaction} \; \mt{unit}
adamc@701	1815 \end{array}$$
adamc@701	1816
adamc@701	1817 The current thread can be paused for at least a specified number of milliseconds.
adamc@701	1818 $$\begin{array}{l}
adamc@701	1819 \mt{val} \; \mt{sleep} : \mt{int} \to \mt{transaction} \; \mt{unit}
adamc@701	1820 \end{array}$$
adamc@701	1821
adamc@787	1822 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	1823 $$\begin{array}{l}
adamc@787	1824 \mt{val} \; \mt{onError} : (\mt{xbody} \to \mt{transaction} \; \mt{unit}) \to \mt{transaction} \; \mt{unit} \\
adamc@787	1825 \mt{val} \; \mt{onFail} : (\mt{string} \to \mt{transaction} \; \mt{unit}) \to \mt{transaction} \; \mt{unit} \\
adamc@787	1826 \mt{val} \; \mt{onConnectFail} : \mt{transaction} \; \mt{unit} \to \mt{transaction} \; \mt{unit} \\
adamc@787	1827 \mt{val} \; \mt{onDisconnect} : \mt{transaction} \; \mt{unit} \to \mt{transaction} \; \mt{unit} \\
adamc@787	1828 \mt{val} \; \mt{onServerError} : (\mt{string} \to \mt{transaction} \; \mt{unit}) \to \mt{transaction} \; \mt{unit}
adamc@787	1829 \end{array}$$
adamc@787	1830
adamc@701	1831 \subsubsection{Functional-Reactive Page Generation}
adamc@701	1832
adamc@701	1833 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	1834
adamc@659	1835 $$\begin{array}{l}
adamc@659	1836 \mt{con} \; \mt{source} :: \mt{Type} \to \mt{Type} \\
adamc@659	1837 \mt{val} \; \mt{source} : \mt{t} ::: \mt{Type} \to \mt{t} \to \mt{transaction} \; (\mt{source} \; \mt{t}) \\
adamc@659	1838 \mt{val} \; \mt{set} : \mt{t} ::: \mt{Type} \to \mt{source} \; \mt{t} \to \mt{t} \to \mt{transaction} \; \mt{unit} \\
adamc@659	1839 \mt{val} \; \mt{get} : \mt{t} ::: \mt{Type} \to \mt{source} \; \mt{t} \to \mt{transaction} \; \mt{t}
adamc@659	1840 \end{array}$$
adamc@659	1841
adamc@659	1842 Pure functions over sources are represented in a monad of \emph{signals}.
adamc@659	1843
adamc@659	1844 $$\begin{array}{l}
adamc@659	1845 \mt{con} \; \mt{signal} :: \mt{Type} \to \mt{Type} \\
adamc@659	1846 \mt{val} \; \mt{signal\_monad} : \mt{monad} \; \mt{signal} \\
adamc@659	1847 \mt{val} \; \mt{signal} : \mt{t} ::: \mt{Type} \to \mt{source} \; \mt{t} \to \mt{signal} \; \mt{t}
adamc@659	1848 \end{array}$$
adamc@659	1849
adamc@659	1850 A reactive portion of an HTML page is injected with a $\mt{dyn}$ tag, which has a signal-valued attribute $\mt{Signal}$.
adamc@659	1851
adamc@659	1852 $$\begin{array}{l}
adamc@701	1853 \mt{val} \; \mt{dyn} : \mt{use} ::: \{\mt{Type}\} \to \mt{bind} ::: \{\mt{Type}\} \to \mt{unit} \\
adamc@701	1854 \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	1855 \end{array}$$
adamc@659	1856
adamc@701	1857 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	1858
adamc@914	1859 \subsubsection{Remote Procedure Calls}
adamc@914	1860
adamc@914	1861 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	1862
adamc@914	1863 $$\begin{array}{l}
adamc@914	1864 \mt{val} \; \mt{rpc} : \mt{t} ::: \mt{Type} \to \mt{transaction} \; \mt{t} \to \mt{transaction} \; \mt{t}
adamc@914	1865 \end{array}$$
adamc@914	1866
adamc@701	1867 \subsubsection{Asynchronous Message-Passing}
adamc@701	1868
adamc@701	1869 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	1870
adamc@701	1871 $$\begin{array}{l}
adamc@701	1872 \mt{type} \; \mt{client} \\
adamc@701	1873 \mt{val} \; \mt{self} : \mt{transaction} \; \mt{client}
adamc@701	1874 \end{array}$$
adamc@701	1875
adamc@701	1876 \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	1877
adamc@701	1878 $$\begin{array}{l}
adamc@701	1879 \mt{con} \; \mt{channel} :: \mt{Type} \to \mt{Type} \\
adamc@701	1880 \mt{val} \; \mt{channel} : \mt{t} ::: \mt{Type} \to \mt{transaction} \; (\mt{channel} \; \mt{t}) \\
adamc@701	1881 \mt{val} \; \mt{send} : \mt{t} ::: \mt{Type} \to \mt{channel} \; \mt{t} \to \mt{t} \to \mt{transaction} \; \mt{unit} \\
adamc@701	1882 \mt{val} \; \mt{recv} : \mt{t} ::: \mt{Type} \to \mt{channel} \; \mt{t} \to \mt{transaction} \; \mt{t}
adamc@701	1883 \end{array}$$
adamc@701	1884
adamc@701	1885 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	1886
adamc@701	1887 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	1888
adamc@659	1889
adamc@549	1890 \section{Ur/Web Syntax Extensions}
adamc@549	1891
adamc@549	1892 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	1893
adamc@549	1894 \subsection{SQL}
adamc@549	1895
adamc@786	1896 \subsubsection{\label{tables}Table Declarations}
adamc@786	1897
adamc@788	1898 $\mt{table}$ declarations may include constraints, via these grammar rules.
adamc@788	1899 $$\begin{array}{rrcll}
adamc@788	1900 \textrm{Declarations} & d &::=& \mt{table} \; x : c \; [pk[,]] \; cts \\
adamc@788	1901 \textrm{Primary key constraints} & pk &::=& \mt{PRIMARY} \; \mt{KEY} \; K \\
adamc@788	1902 \textrm{Keys} & K &::=& f \mid (f, (f,)^+) \\
adamc@788	1903 \textrm{Constraint sets} & cts &::=& \mt{CONSTRAINT} f \; ct \mid cts, cts \mid \{\{e\}\} \\
adamc@788	1904 \textrm{Constraints} & ct &::=& \mt{UNIQUE} \; K \mid \mt{CHECK} \; E \\
adamc@788	1905 &&& \mid \mt{FOREIGN} \; \mt{KEY} \; K \; \mt{REFERENCES} \; F \; (K) \; [\mt{ON} \; \mt{DELETE} \; pr] \; [\mt{ON} \; \mt{UPDATE} \; pr] \\
adamc@788	1906 \textrm{Foreign tables} & F &::=& x \mid \{\{e\}\} \\
adamc@788	1907 \textrm{Propagation modes} & pr &::=& \mt{NO} \; \mt{ACTION} \mid \mt{RESTRICT} \mid \mt{CASCADE} \mid \mt{SET} \; \mt{NULL}
adamc@788	1908 \end{array}$$
adamc@788	1909
adamc@788	1910 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	1911
adamc@788	1912
adamc@549	1913 \subsubsection{Queries}
adamc@549	1914
adamc@550	1915 Queries $Q$ are added to the rules for expressions $e$.
adamc@550	1916
adamc@549	1917 $$\begin{array}{rrcll}
adamc@550	1918 \textrm{Queries} & Q &::=& (q \; [\mt{ORDER} \; \mt{BY} \; (E \; [o],)^+] \; [\mt{LIMIT} \; N] \; [\mt{OFFSET} \; N]) \\
adamc@1085	1919 \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	1920 &&& \mid q \; R \; q \mid \{\{\{e\}\}\} \\
adamc@549	1921 \textrm{Relational operators} & R &::=& \mt{UNION} \mid \mt{INTERSECT} \mid \mt{EXCEPT}
adamc@549	1922 \end{array}$$
adamc@549	1923
adamc@549	1924 $$\begin{array}{rrcll}
adamc@549	1925 \textrm{Projections} & P &::=& \ast & \textrm{all columns} \\
adamc@549	1926 &&& p,^+ & \textrm{particular columns} \\
adamc@549	1927 \textrm{Pre-projections} & p &::=& t.f & \textrm{one column from a table} \\
adamc@558	1928 &&& t.\{\{c\}\} & \textrm{a record of columns from a table (of kind $\{\mt{Type}\}$)} \\
adamc@549	1929 \textrm{Table names} & t &::=& x & \textrm{constant table name (automatically capitalized)} \\
adamc@549	1930 &&& X & \textrm{constant table name} \\
adamc@549	1931 &&& \{\{c\}\} & \textrm{computed table name (of kind $\mt{Name}$)} \\
adamc@549	1932 \textrm{Column names} & f &::=& X & \textrm{constant column name} \\
adamc@549	1933 &&& \{c\} & \textrm{computed column name (of kind $\mt{Name}$)} \\
adamc@549	1934 \textrm{Tables} & T &::=& x & \textrm{table variable, named locally by its own capitalization} \\
adamc@549	1935 &&& x \; \mt{AS} \; t & \textrm{table variable, with local name} \\
adamc@549	1936 &&& \{\{e\}\} \; \mt{AS} \; t & \textrm{computed table expression, with local name} \\
adamc@1085	1937 \textrm{$\mt{FROM}$ items} & F &::=& T \mid \{\{e\}\} \mid F \; J \; \mt{JOIN} \; F \; \mt{ON} \; E \\
adamc@1085	1938 &&& \mid F \; \mt{CROSS} \; \mt{JOIN} \ F \\
adamc@1085	1939 \textrm{Joins} & J &::=& [\mt{INNER}] \\
adamc@1085	1940 &&& \mid [\mt{LEFT} \mid \mt{RIGHT} \mid \mt{FULL}] \; [\mt{OUTER}] \\
adamc@549	1941 \textrm{SQL expressions} & E &::=& p & \textrm{column references} \\
adamc@549	1942 &&& X & \textrm{named expression references} \\
adamc@549	1943 &&& \{\{e\}\} & \textrm{injected native Ur expressions} \\
adamc@549	1944 &&& \{e\} & \textrm{computed expressions, probably using $\mt{sql\_exp}$ directly} \\
adamc@549	1945 &&& \mt{TRUE} \mid \mt{FALSE} & \textrm{boolean constants} \\
adamc@549	1946 &&& \ell & \textrm{primitive type literals} \\
adamc@549	1947 &&& \mt{NULL} & \textrm{null value (injection of $\mt{None}$)} \\
adamc@549	1948 &&& E \; \mt{IS} \; \mt{NULL} & \textrm{nullness test} \\
adamc@549	1949 &&& n & \textrm{nullary operators} \\
adamc@549	1950 &&& u \; E & \textrm{unary operators} \\
adamc@549	1951 &&& E \; b \; E & \textrm{binary operators} \\
adamc@549	1952 &&& \mt{COUNT}(\ast) & \textrm{count number of rows} \\
adamc@549	1953 &&& a(E) & \textrm{other aggregate function} \\
adamc@549	1954 &&& (E) & \textrm{explicit precedence} \\
adamc@549	1955 \textrm{Nullary operators} & n &::=& \mt{CURRENT\_TIMESTAMP} \\
adamc@549	1956 \textrm{Unary operators} & u &::=& \mt{NOT} \\
adamc@549	1957 \textrm{Binary operators} & b &::=& \mt{AND} \mid \mt{OR} \mid \neq \mid < \mid \leq \mid > \mid \geq \\
adamc@549	1958 \textrm{Aggregate functions} & a &::=& \mt{AVG} \mid \mt{SUM} \mid \mt{MIN} \mid \mt{MAX} \\
adamc@550	1959 \textrm{Directions} & o &::=& \mt{ASC} \mid \mt{DESC} \\
adamc@549	1960 \textrm{SQL integer} & N &::=& n \mid \{e\} \\
adamc@549	1961 \end{array}$$
adamc@549	1962
adamc@1085	1963 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	1964
adamc@550	1965 \subsubsection{DML}
adamc@550	1966
adamc@550	1967 DML commands $D$ are added to the rules for expressions $e$.
adamc@550	1968
adamc@550	1969 $$\begin{array}{rrcll}
adamc@550	1970 \textrm{Commands} & D &::=& (\mt{INSERT} \; \mt{INTO} \; T^E \; (f,^+) \; \mt{VALUES} \; (E,^+)) \\
adamc@550	1971 &&& (\mt{UPDATE} \; T^E \; \mt{SET} \; (f = E,)^+ \; \mt{WHERE} \; E) \\
adamc@550	1972 &&& (\mt{DELETE} \; \mt{FROM} \; T^E \; \mt{WHERE} \; E) \\
adamc@550	1973 \textrm{Table expressions} & T^E &::=& x \mid \{\{e\}\}
adamc@550	1974 \end{array}$$
adamc@550	1975
adamc@550	1976 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	1977
adamc@551	1978 \subsection{XML}
adamc@551	1979
adamc@551	1980 XML fragments $L$ are added to the rules for expressions $e$.
adamc@551	1981
adamc@551	1982 $$\begin{array}{rrcll}
adamc@551	1983 \textrm{XML fragments} & L &::=& \texttt{<xml/>} \mid \texttt{<xml>}l^*\texttt{</xml>} \\
adamc@551	1984 \textrm{XML pieces} & l &::=& \textrm{text} & \textrm{cdata} \\
adamc@551	1985 &&& \texttt{<}g\texttt{/>} & \textrm{tag with no children} \\
adamc@551	1986 &&& \texttt{<}g\texttt{>}l^*\texttt{</}x\texttt{>} & \textrm{tag with children} \\
adamc@559	1987 &&& \{e\} & \textrm{computed XML fragment} \\
adamc@559	1988 &&& \{[e]\} & \textrm{injection of an Ur expression, via the $\mt{Top}.\mt{txt}$ function} \\
adamc@551	1989 \textrm{Tag} & g &::=& h \; (x = v)^* \\
adamc@551	1990 \textrm{Tag head} & h &::=& x & \textrm{tag name} \\
adamc@551	1991 &&& h\{c\} & \textrm{constructor parameter} \\
adamc@551	1992 \textrm{Attribute value} & v &::=& \ell & \textrm{literal value} \\
adamc@551	1993 &&& \{e\} & \textrm{computed value} \\
adamc@551	1994 \end{array}$$
adamc@551	1995
adamc@552	1996
adamc@553	1997 \section{The Structure of Web Applications}
adamc@553	1998
adamc@1127	1999 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	2000
adamc@553	2001 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	2002
adamc@553	2003 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	2004
adamc@558	2005 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	2006
adamc@660	2007 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	2008
adamc@789	2009 \medskip
adamc@789	2010
adamc@789	2011 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	2012
adamc@789	2013 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	2014
adamc@553	2015
adamc@897	2016 \section{The Foreign Function Interface}
adamc@897	2017
adamc@897	2018 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	2019
adamc@897	2020 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	2021
adamc@897	2022 \begin{itemize}
adamc@897	2023 \item \texttt{clientOnly Module.ident} registers a value as being allowed only in client-side code.
adamc@897	2024 \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	2025 \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	2026 \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	2027 \item \texttt{include FILE} requests inclusion of a C header file.
adamc@897	2028 \item \texttt{jsFunc Module.ident=name} gives a mapping from an Ur name for a value to a JavaScript name.
adamc@897	2029 \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	2030 \item \texttt{script URL} requests inclusion of a JavaScript source file within application HTML.
adamc@897	2031 \item \texttt{serverOnly Module.ident} registers a value as being allowed only in server-side code.
adamc@897	2032 \end{itemize}
adamc@897	2033
adamc@897	2034 \subsection{Writing C FFI Code}
adamc@897	2035
adamc@897	2036 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	2037
adamc@897	2038 \begin{itemize}
adamc@897	2039 \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	2040 \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	2041 \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	2042 \end{itemize}
adamc@897	2043
adamc@897	2044 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	2045 \begin{itemize}
adamc@897	2046 \item \begin{verbatim}
adamc@897	2047 void uw_error(uw_context, failure_kind, const char *fmt, ...);
adamc@897	2048 \end{verbatim}
adamc@897	2049 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	2050
adamc@897	2051 \item \begin{verbatim}
adamc@897	2052 void uw_push_cleanup(uw_context, void (func)(void ), void *arg);
adamc@897	2053 void uw_pop_cleanup(uw_context);
adamc@897	2054 \end{verbatim}
adamc@897	2055 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	2056
adamc@897	2057 \item \begin{verbatim}
adamc@897	2058 void *uw_malloc(uw_context, size_t);
adamc@897	2059 \end{verbatim}
adamc@897	2060 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	2061
adamc@897	2062 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	2063
adamc@897	2064 \item \begin{verbatim}
adamc@897	2065 typedef void (uw_callback)(void );
adamc@897	2066 void uw_register_transactional(uw_context, void *data, uw_callback commit,
adamc@897	2067 uw_callback rollback, uw_callback free);
adamc@897	2068 \end{verbatim}
adamc@897	2069 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	2070
adamc@1085	2071 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	2072
adamc@1085	2073 \item \begin{verbatim}
adamc@1085	2074 void uw_get_global(uw_context, char name);
adamc@1085	2075 void uw_set_global(uw_context, char name, void data, uw_callback free);
adamc@1085	2076 \end{verbatim}
adamc@1085	2077 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	2078
adamc@897	2079 \end{itemize}
adamc@897	2080
adamc@897	2081 \subsection{Writing JavaScript FFI Code}
adamc@897	2082
adamc@897	2083 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	2084
adamc@897	2085 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	2086
adamc@897	2087 \begin{itemize}
adamc@897	2088 \item Integers, floats, strings, characters, and booleans are represented in the usual JavaScript way.
adamc@985	2089 \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	2090 \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	2091 \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	2092 \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	2093 \end{itemize}
adamc@897	2094
adamc@897	2095 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	2096
adamc@897	2097
adamc@552	2098 \section{Compiler Phases}
adamc@552	2099
adamc@552	2100 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	2101
adamc@552	2102 In this section, we step through the main phases of compilation, noting what consequences each phase has for effective programming.
adamc@552	2103
adamc@552	2104 \subsection{Parse}
adamc@552	2105
adamc@552	2106 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	2107
adamc@552	2108 \subsection{Elaborate}
adamc@552	2109
adamc@552	2110 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	2111
adamc@552	2112 \subsection{Unnest}
adamc@552	2113
adamc@552	2114 Named local function definitions are moved to the top level, to avoid the need to generate closures.
adamc@552	2115
adamc@552	2116 \subsection{Corify}
adamc@552	2117
adamc@552	2118 Module system features are compiled away, through inlining of functor definitions at application sites. Afterward, most abstraction boundaries are broken, facilitating optimization.
adamc@552	2119
adamc@552	2120 \subsection{Especialize}
adamc@552	2121
adamc@552	2122 Functions are specialized to particular argument patterns. This is an important trick for avoiding the need to maintain any closures at runtime.
adamc@552	2123
adamc@552	2124 \subsection{Untangle}
adamc@552	2125
adamc@552	2126 Remove unnecessary mutual recursion, splitting recursive groups into strongly-connected components.
adamc@552	2127
adamc@552	2128 \subsection{Shake}
adamc@552	2129
adamc@552	2130 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	2131
adamc@661	2132 \subsection{Rpcify}
adamc@661	2133
adamc@661	2134 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	2135
adamc@661	2136 \subsection{Untangle, Shake}
adamc@661	2137
adamc@661	2138 Repeat these simplifications.
adamc@661	2139
adamc@553	2140 \subsection{\label{tag}Tag}
adamc@552	2141
adamc@552	2142 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	2143
adamc@552	2144 \subsection{Reduce}
adamc@552	2145
adamc@552	2146 Apply definitional equality rules to simplify the program as much as possible. This effectively includes inlining of every non-recursive definition.
adamc@552	2147
adamc@552	2148 \subsection{Unpoly}
adamc@552	2149
adamc@552	2150 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	2151
adamc@552	2152 \subsection{Specialize}
adamc@552	2153
adamc@558	2154 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	2155
adamc@552	2156 \subsection{Shake}
adamc@552	2157
adamc@558	2158 Here the compiler repeats the earlier Shake phase.
adamc@552	2159
adamc@552	2160 \subsection{Monoize}
adamc@552	2161
adamc@552	2162 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	2163
adamc@552	2164 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	2165
adamc@552	2166 \subsection{MonoOpt}
adamc@552	2167
adamc@552	2168 Simple algebraic laws are applied to simplify the program, focusing especially on efficient imperative generation of HTML pages.
adamc@552	2169
adamc@552	2170 \subsection{MonoUntangle}
adamc@552	2171
adamc@552	2172 Unnecessary mutual recursion is broken up again.
adamc@552	2173
adamc@552	2174 \subsection{MonoReduce}
adamc@552	2175
adamc@552	2176 Equivalents of the definitional equality rules are applied to simplify programs, with inlining again playing a major role.
adamc@552	2177
adamc@552	2178 \subsection{MonoShake, MonoOpt}
adamc@552	2179
adamc@552	2180 Unneeded declarations are removed, and basic optimizations are repeated.
adamc@552	2181
adamc@552	2182 \subsection{Fuse}
adamc@552	2183
adamc@552	2184 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	2185
adamc@552	2186 \subsection{MonoUntangle, MonoShake}
adamc@552	2187
adamc@552	2188 Fuse often creates more opportunities to remove spurious mutual recursion.
adamc@552	2189
adamc@552	2190 \subsection{Pathcheck}
adamc@552	2191
adamc@552	2192 The compiler checks that no link or action name has been used more than once.
adamc@552	2193
adamc@552	2194 \subsection{Cjrize}
adamc@552	2195
adamc@552	2196 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	2197
adamc@552	2198 \subsection{C Compilation and Linking}
adamc@552	2199
adamc@552	2200 The output of the last phase is pretty-printed as C source code and passed to GCC.
adamc@552	2201
adamc@552	2202
adamc@524	2203 \end{document}

Mercurial > urweb

annotate doc/manual.tex @ 1163:6c507826fae9