Ur/Web: doc/manual.tex annotate

annotate doc/manual.tex @ 897:2faf558b2d05

FFI manual section

author	Adam Chlipala <adamc@hcoop.net>
date	Sat, 18 Jul 2009 15:08:21 -0400
parents	0ae8894d5c97
children	782f0b4eea67

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

Mercurial > urweb

annotate doc/manual.tex @ 897:2faf558b2d05