Ur/Web: doc/manual.tex annotate

annotate doc/manual.tex @ 1086:99aebdf30257

-tc flag

author	Adam Chlipala <adamc@hcoop.net>
date	Thu, 24 Dec 2009 10:02:48 -0500
parents	ae885ad70d83
children	f1647f16097d

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

Mercurial > urweb

annotate doc/manual.tex @ 1086:99aebdf30257