adamc@524: \documentclass{article} adamc@554: \usepackage{fullpage,amsmath,amssymb,proof,url} rmbruijn@1568: \usepackage[T1]{fontenc} adamc@524: \newcommand{\cd}[1]{\texttt{#1}} adamc@524: \newcommand{\mt}[1]{\mathsf{#1}} adamc@524: adamc@524: \newcommand{\rc}{+ \hspace{-.075in} + \;} adamc@527: \newcommand{\rcut}{\; \texttt{--} \;} adamc@527: \newcommand{\rcutM}{\; \texttt{---} \;} adamc@524: adamc@524: \begin{document} adamc@524: adamc@524: \title{The Ur/Web Manual} adamc@524: \author{Adam Chlipala} adamc@524: adamc@524: \maketitle adamc@524: adamc@540: \tableofcontents adamc@540: adamc@554: adamc@554: \section{Introduction} adamc@554: adamc@1160: \emph{Ur} is a programming language designed to introduce richer type system features into functional programming in the tradition of ML and Haskell. Ur is functional, pure, statically-typed, and strict. Ur supports a powerful kind of \emph{metaprogramming} based on \emph{type-level computation with type-level records}. adamc@554: adamc@554: \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: adamc@554: \begin{itemize} adamc@554: \item Suffer from any kinds of code-injection attacks adamc@554: \item Return invalid HTML adamc@554: \item Contain dead intra-application links adamc@554: \item Have mismatches between HTML forms and the fields expected by their handlers adamc@652: \item Include client-side code that makes incorrect assumptions about the ``AJAX''-style services that the remote web server provides adamc@554: \item Attempt invalid SQL queries adamc@652: \item Use improper marshaling or unmarshaling in communication with SQL databases or between browsers and web servers adamc@554: \end{itemize} adamc@554: adamc@554: 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: adamc@652: 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: adamc@554: \medskip adamc@554: adamc@554: The official web site for Ur is: adamc@554: \begin{center} adamc@554: \url{http://www.impredicative.com/ur/} adamc@554: \end{center} adamc@554: adamc@555: adamc@555: \section{Installation} adamc@555: adamc@555: 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: adamc@555: \begin{verbatim} adamc@555: ./configure adamc@555: make adamc@555: sudo make install adamc@555: \end{verbatim} adamc@555: adam@1523: 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 (or an alternate C compiler) in your execution path; MLton, the whole-program optimizing compiler for Standard ML; and the development files for the OpenSSL 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: \begin{verbatim} adam@1368: apt-get install mlton libssl-dev adamc@896: \end{verbatim} adamc@555: adamc@896: To build programs that access SQL databases, you also need one of these client libraries for supported backends. adamc@555: \begin{verbatim} adamc@896: apt-get install libpq-dev libmysqlclient15-dev libsqlite3-dev adamc@555: \end{verbatim} adamc@555: adamc@555: 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: \begin{verbatim} adamc@555: apt-get install smlnj libsmlnj-smlnj ml-yacc ml-lpt adamc@555: \end{verbatim} adamc@555: adamc@555: 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: adamc@896: To run an SQL-backed application with a backend besides SQLite, you will probably want to install one of these servers. adamc@555: adamc@555: \begin{verbatim} adam@1400: apt-get install postgresql-8.4 mysql-server-5.1 adamc@555: \end{verbatim} adamc@555: adamc@555: 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: adamc@555: \begin{verbatim} adamc@555: apt-get install emacs-goodies-el adamc@555: \end{verbatim} adamc@555: adam@1441: If you don't want to install the Emacs mode, run \texttt{./configure} with the argument \texttt{--without-emacs}. adam@1441: adam@1523: 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 the C compiler and linker on every invocation. Some older GCC versions need this setting to mask a bug in function inlining. adamc@555: adamc@555: \begin{verbatim} adam@1523: CCARGS=-fno-inline ./configure adamc@555: \end{verbatim} adamc@555: adam@1523: Since the author is still getting a handle on the GNU Autotools that provide the build system, you may need to do some further work to get started, especially in environments with significant differences from Linux (where most testing is done). The variables \texttt{PGHEADER}, \texttt{MSHEADER}, and \texttt{SQHEADER} may be used to set the proper C header files to include for the development libraries of PostgreSQL, MySQL, and SQLite, respectively. To get libpq to link, one OS X user reported setting \texttt{CCARGS="-I/opt/local/include -L/opt/local/lib/postgresql84"}, after creating a symbolic link with \texttt{ln -s /opt/local/include/postgresql84 /opt/local/include/postgresql}. adamc@555: adamc@555: The Emacs mode can be set to autoload by adding the following to your \texttt{.emacs} file. adamc@555: adamc@555: \begin{verbatim} adamc@555: (add-to-list 'load-path "/usr/local/share/emacs/site-lisp/urweb-mode") adamc@555: (load "urweb-mode-startup") adamc@555: \end{verbatim} adamc@555: adamc@555: Change the path in the first line if you chose a different Emacs installation path during configuration. adamc@555: adamc@555: adamc@556: \section{Command-Line Compiler} adamc@556: adamc@556: \subsection{Project Files} adamc@556: adamc@556: 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: adamc@556: \begin{verbatim} adamc@556: database dbname=test adamc@556: sql crud1.sql adamc@556: adamc@556: crud adamc@556: crud1 adamc@556: \end{verbatim} adamc@556: adamc@556: 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: adamc@556: 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: adamc@556: \begin{verbatim} adamc@556: createdb test adamc@556: psql -f crud1.sql test adamc@556: \end{verbatim} adamc@556: adam@1331: A blank line separates the named directives from a list of modules to include in the project. Any line may contain a shell-script-style comment, where any suffix of a line starting at a hash character \texttt{\#} is ignored. adamc@556: adamc@556: 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: adamc@783: 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: \begin{itemize} adam@1465: \item \texttt{[allow|deny] [url|mime|requestHeader|responseHeader] PATTERN} registers a rule governing which URLs, MIME types, HTTP request headers, or HTTP response headers are allowed to appear explicitly in this application. The first such rule to match a name determines the verdict. If \texttt{PATTERN} ends in \texttt{*}, it is interpreted as a prefix rule. Otherwise, a string must match it exactly. adam@1400: \item \texttt{alwaysInline PATH} requests that every call to the referenced function be inlined. Section \ref{structure} explains how functions are assigned path strings. adam@1462: \item \texttt{benignEffectful Module.ident} registers an FFI function or transaction as having side effects. The optimizer avoids removing, moving, or duplicating calls to such functions. Every effectful FFI function must be registered, or the optimizer may make invalid transformations. This version of the \texttt{effectful} directive registers that this function only has side effects that remain local to a single page generation. adamc@783: \item \texttt{clientOnly Module.ident} registers an FFI function or transaction that may only be run in client browsers. adamc@783: \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: \item \texttt{database DBSTRING} sets the string to pass to libpq to open a database connection. adamc@783: \item \texttt{debug} saves some intermediate C files, which is mostly useful to help in debugging the compiler itself. adamc@783: \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: \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: \item \texttt{ffi FILENAME} reads the file \texttt{FILENAME.urs} to determine the interface to a new FFI module. The name of the module is calculated from \texttt{FILENAME} in the same way as for normal source files. See the files \texttt{include/urweb.h} and \texttt{src/c/urweb.c} for examples of C headers and implementations for FFI modules. In general, every type or value \texttt{Module.ident} becomes \texttt{uw\_Module\_ident} in C. adamc@1099: \item \texttt{include FILENAME} adds \texttt{FILENAME} to the list of files to be \texttt{\#include}d in C sources. This is most useful for interfacing with new FFI modules. adamc@783: \item \texttt{jsFunc Module.ident=name} gives the JavaScript name of an FFI value. adamc@1089: \item \texttt{library FILENAME} parses \texttt{FILENAME.urp} and merges its contents with the rest of the current file's contents. If \texttt{FILENAME.urp} doesn't exist, the compiler also tries \texttt{FILENAME/lib.urp}. adam@1309: \item \texttt{limit class num} sets a resource usage limit for generated applications. The limit \texttt{class} will be set to the non-negative integer \texttt{num}. The classes are: adam@1309: \begin{itemize} adam@1309: \item \texttt{cleanup}: maximum number of cleanup operations (e.g., entries recording the need to deallocate certain temporary objects) that may be active at once per request adam@1309: \item \texttt{database}: maximum size of database files (currently only used by SQLite) adam@1309: \item \texttt{deltas}: maximum number of messages sendable in a single request handler with \texttt{Basis.send} adam@1309: \item \texttt{globals}: maximum number of global variables that FFI libraries may set in a single request context adam@1309: \item \texttt{headers}: maximum size (in bytes) of per-request buffer used to hold HTTP headers for generated pages adam@1309: \item \texttt{heap}: maximum size (in bytes) of per-request heap for dynamically-allocated data adam@1309: \item \texttt{inputs}: maximum number of top-level form fields per request adam@1309: \item \texttt{messages}: maximum size (in bytes) of per-request buffer used to hold a single outgoing message sent with \texttt{Basis.send} adam@1309: \item \texttt{page}: maximum size (in bytes) of per-request buffer used to hold HTML content of generated pages adam@1309: \item \texttt{script}: maximum size (in bytes) of per-request buffer used to hold JavaScript content of generated pages adam@1309: \item \texttt{subinputs}: maximum number of form fields per request, excluding top-level fields adam@1309: \item \texttt{time}: maximum running time of a single page request, in units of approximately 0.1 seconds adam@1309: \item \texttt{transactionals}: maximum number of custom transactional actions (e.g., sending an e-mail) that may be run in a single page generation adam@1309: \end{itemize} adam@1523: \item \texttt{link FILENAME} adds \texttt{FILENAME} to the list of files to be passed to the linker at the end of compilation. This is most useful for importing extra libraries needed by new FFI modules. adam@1332: \item \texttt{minHeap NUMBYTES} sets the initial size for thread-local heaps used in handling requests. These heaps grow automatically as needed (up to any maximum set with \texttt{limit}), but each regrow requires restarting the request handling process. adam@1478: \item \texttt{noXsrfProtection URIPREFIX} turns off automatic cross-site request forgery protection for the page handler identified by the given URI prefix. This will avoid checking cryptographic signatures on cookies, which is generally a reasonable idea for some pages, such as login pages that are going to discard all old cookie values, anyway. adam@1297: \item \texttt{onError Module.var} changes the handling of fatal application errors. Instead of displaying a default, ugly error 500 page, the error page will be generated by calling function \texttt{Module.var} on a piece of XML representing the error message. The error handler should have type $\mt{xbody} \to \mt{transaction} \; \mt{page}$. Note that the error handler \emph{cannot} be in the application's main module, since that would register it as explicitly callable via URLs. adamc@852: \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: \item \texttt{prefix PREFIX} sets the prefix included before every URI within the generated application. The default is \texttt{/}. adamc@783: \item \texttt{profile} generates an executable that may be used with gprof. adam@1300: \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}. The \texttt{TO} field may be left empty to express the idea of deleting a prefix. For instance, \texttt{rewrite url Main/*} will strip all \texttt{Main/} prefixes from URLs. 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@1183: \item \texttt{safeGet URI} asks to allow the page handler assigned this canonical URI prefix to cause persistent side effects, even if accessed via an HTTP \cd{GET} request. adamc@783: \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: \item \texttt{serverOnly Module.ident} registers an FFI function or transaction that may only be run on the server. adamc@1164: \item \texttt{sigfile PATH} sets a path where your application should look for a key to use in cryptographic signing. This is used to prevent cross-site request forgery attacks for any form handler that both reads a cookie and creates side effects. If the referenced file doesn't exist, an application will create it and read its saved data on future invocations. You can also initialize the file manually with any contents at least 16 bytes long; the first 16 bytes will be treated as the key. adamc@783: \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: \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: \end{itemize} adamc@701: adamc@701: adamc@557: \subsection{Building an Application} adamc@557: adamc@557: To compile project \texttt{P.urp}, simply run adamc@557: \begin{verbatim} adamc@557: urweb P adamc@557: \end{verbatim} adamc@1198: 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. See Section \ref{structure} for an explanation of the URI mapping convention, which determines how each page of your application may be accessed via URLs. adamc@557: adamc@557: To time how long the different compiler phases run, without generating an executable, run adamc@557: \begin{verbatim} adamc@557: urweb -timing P adamc@557: \end{verbatim} adamc@557: adamc@1086: To stop the compilation process after type-checking, run adamc@1086: \begin{verbatim} adamc@1086: urweb -tc P adamc@1086: \end{verbatim} adam@1530: It is often worthwhile to run \cd{urweb} in this mode, because later phases of compilation can take significantly longer than type-checking alone, and the type checker catches many errors that would traditionally be found through debugging a running application. adamc@1086: adam@1531: A related option is \cd{-dumpTypes}, which, as long as parsing succeeds, outputs to stdout a summary of the kinds of all identifiers declared with \cd{con} and the types of all identifiers declared with \cd{val} or \cd{val rec}. This information is dumped even if there are errors during type inference. Compiler error messages go to stderr, not stdout, so it is easy to distinguish the two kinds of output programmatically. adam@1531: adamc@1170: To output information relevant to CSS stylesheets (and not finish regular compilation), run adamc@1170: \begin{verbatim} adamc@1170: urweb -css P adamc@1170: \end{verbatim} adamc@1170: The first output line is a list of categories of CSS properties that would be worth setting on the document body. The remaining lines are space-separated pairs of CSS class names and categories of properties that would be worth setting for that class. The category codes are divided into two varieties. Codes that reveal properties of a tag or its (recursive) children are \cd{B} for block-level elements, \cd{C} for table captions, \cd{D} for table cells, \cd{L} for lists, and \cd{T} for tables. Codes that reveal properties of the precise tag that uses a class are \cd{b} for block-level elements, \cd{t} for tables, \cd{d} for table cells, \cd{-} for table rows, \cd{H} for the possibility to set a height, \cd{N} for non-replaced inline-level elements, \cd{R} for replaced inline elements, and \cd{W} for the possibility to set a width. adamc@1170: adamc@896: Some other command-line parameters are accepted: adamc@896: \begin{itemize} adamc@896: \item \texttt{-db }: 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: adamc@896: \item \texttt{-dbms [postgres|mysql|sqlite]}: Sets the database backend to use. adamc@896: \begin{itemize} adamc@896: \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: adamc@896: A command sequence like this can initialize a Postgres database, using a file \texttt{app.sql} generated by the compiler: adamc@896: \begin{verbatim} adamc@896: createdb app adamc@896: psql -f app.sql app adamc@896: \end{verbatim} adamc@896: adamc@896: \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: adamc@896: A command sequence like this can initialize a MySQL database: adamc@896: \begin{verbatim} adamc@896: echo "CREATE DATABASE app" | mysql adamc@896: mysql -D app adamc@896: (( "bin-path" => "/path/to/hello.exe", adamc@896: "socket" => "/tmp/hello", adamc@896: "check-local" => "disable", adamc@896: "docroot" => "/", adamc@896: "max-procs" => "1" adamc@896: )) adamc@896: ) adamc@896: \end{verbatim} adamc@896: 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: adamc@896: 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. adam@1509: adam@1509: \item \texttt{static}: This protocol may be used to generate static web pages from Ur/Web code. The output executable expects a single command-line argument, giving the URI of a page to generate. For instance, this argument might be \cd{/main}, in which case a static HTTP response for that page will be written to stdout. adamc@896: \end{itemize} adamc@896: adamc@1127: \item \texttt{-root Name PATH}: Trigger an alternate module convention for all source files found in directory \texttt{PATH} or any of its subdirectories. Any file \texttt{PATH/foo.ur} defines a module \texttt{Name.Foo} instead of the usual \texttt{Foo}. Any file \texttt{PATH/subdir/foo.ur} defines a module \texttt{Name.Subdir.Foo}, and so on for arbitrary nesting of subdirectories. adamc@1127: adamc@1164: \item \texttt{-sigfile PATH}: Same as the \texttt{sigfile} directive in \texttt{.urp} files adamc@1164: adamc@896: \item \texttt{-sql FILENAME}: Set where a database set-up SQL script is written. adamc@1095: adamc@1095: \item \texttt{-static}: Link the runtime system statically. The default is to link against dynamic libraries. adamc@896: \end{itemize} adamc@896: adam@1297: There is an additional convenience method for invoking \texttt{urweb}. If the main argument is \texttt{FOO}, and \texttt{FOO.ur} exists but \texttt{FOO.urp} doesn't, then the invocation is interpreted as if called on a \texttt{.urp} file containing \texttt{FOO} as its only main entry, with an additional \texttt{rewrite all FOO/*} directive. adamc@556: adam@1509: \subsection{Tutorial Formatting} adam@1509: adam@1509: The Ur/Web compiler also supports rendering of nice HTML tutorials from Ur source files, when invoked like \cd{urweb -tutorial DIR}. The directory \cd{DIR} is examined for files whose names end in \cd{.ur}. Every such file is translated into a \cd{.html} version. adam@1509: adam@1509: These input files follow normal Ur syntax, with a few exceptions: adam@1509: \begin{itemize} adam@1509: \item The first line must be a comment like \cd{(* TITLE *)}, where \cd{TITLE} is a string of your choice that will be used as the title of the output page. adam@1509: \item While most code in the output HTML will be formatted as a monospaced code listing, text in regular Ur comments is formatted as normal English text. adam@1509: \item A comment like \cd{(* * HEADING *)} introduces a section heading, with text \cd{HEADING} of your choice. adam@1509: \item To include both a rendering of an Ur expression and a pretty-printed version of its value, bracket the expression with \cd{(* begin eval *)} and \cd{(* end *)}. The result of expression evaluation is pretty-printed with \cd{show}, so the expression type must belong to that type class. adam@1509: \item To include code that should not be shown in the tutorial (e.g., to add a \cd{show} instance to use with \cd{eval}), bracket the code with \cd{(* begin hide *)} and \cd{(* end *)}. adam@1509: \end{itemize} adam@1509: adam@1509: A word of warning: as for demo generation, tutorial generation calls Emacs to syntax-highlight Ur code. adam@1509: adam@1522: \subsection{Run-Time Options} adam@1522: adam@1522: Compiled applications consult a few environment variables to modify their behavior: adam@1522: adam@1522: \begin{itemize} adam@1522: \item \cd{URWEB\_NUM\_THREADS}: alternative to the \cd{-t} command-line argument (currently used only by FastCGI) adam@1522: \item \cd{URWEB\_STACK\_SIZE}: size of per-thread stacks, in bytes as@1564: \item \cd{URWEB\_PQ\_CON}: when using PostgreSQL, overrides the compiled-in connection string adam@1522: \end{itemize} adam@1522: adam@1509: adamc@529: \section{Ur Syntax} adamc@529: adamc@784: 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: adamc@524: \subsection{Lexical Conventions} adamc@524: adamc@524: 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: adamc@524: \begin{center} adamc@524: \begin{tabular}{rl} adamc@524: \textbf{\LaTeX} & \textbf{ASCII} \\ adamc@524: $\to$ & \cd{->} \\ adamc@652: $\longrightarrow$ & \cd{-->} \\ adamc@524: $\times$ & \cd{*} \\ adamc@524: $\lambda$ & \cd{fn} \\ adamc@524: $\Rightarrow$ & \cd{=>} \\ adamc@652: $\Longrightarrow$ & \cd{==>} \\ adamc@529: $\neq$ & \cd{<>} \\ adamc@529: $\leq$ & \cd{<=} \\ adamc@529: $\geq$ & \cd{>=} \\ adamc@524: \\ adamc@524: $x$ & Normal textual identifier, not beginning with an uppercase letter \\ adamc@525: $X$ & Normal textual identifier, beginning with an uppercase letter \\ adamc@524: \end{tabular} adamc@524: \end{center} adamc@524: adamc@525: 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: adamc@873: 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: adamc@527: This version of the manual doesn't include operator precedences; see \texttt{src/urweb.grm} for that. adamc@527: adam@1297: As in the ML language family, the syntax \texttt{(* ... *)} is used for (nestable) comments. Within XML literals, Ur/Web also supports the usual \texttt{} XML comments. adam@1297: adamc@552: \subsection{\label{core}Core Syntax} adamc@524: adamc@524: \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: $$\begin{array}{rrcll} adamc@524: \textrm{Kinds} & \kappa &::=& \mt{Type} & \textrm{proper types} \\ adamc@525: &&& \mt{Unit} & \textrm{the trivial constructor} \\ adamc@525: &&& \mt{Name} & \textrm{field names} \\ adamc@525: &&& \kappa \to \kappa & \textrm{type-level functions} \\ adamc@525: &&& \{\kappa\} & \textrm{type-level records} \\ adamc@525: &&& (\kappa\times^+) & \textrm{type-level tuples} \\ adamc@652: &&& X & \textrm{variable} \\ adam@1574: &&& X \longrightarrow \kappa & \textrm{kind-polymorphic type-level function} \\ adamc@529: &&& \_\_ & \textrm{wildcard} \\ adamc@525: &&& (\kappa) & \textrm{explicit precedence} \\ adamc@524: \end{array}$$ adamc@524: adamc@524: 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: $$\begin{array}{rrcll} adamc@524: \textrm{Explicitness} & ? &::=& :: & \textrm{explicit} \\ adamc@558: &&& ::: & \textrm{implicit} adamc@524: \end{array}$$ adamc@524: adamc@524: \emph{Constructors} are the main class of compile-time-only data. They include proper types and are classified by kinds. adamc@524: $$\begin{array}{rrcll} adamc@524: \textrm{Constructors} & c, \tau &::=& (c) :: \kappa & \textrm{kind annotation} \\ adamc@530: &&& \hat{x} & \textrm{constructor variable} \\ adamc@524: \\ adamc@525: &&& \tau \to \tau & \textrm{function type} \\ adamc@525: &&& x \; ? \; \kappa \to \tau & \textrm{polymorphic function type} \\ adamc@652: &&& X \longrightarrow \tau & \textrm{kind-polymorphic function type} \\ adamc@525: &&& \$ c & \textrm{record type} \\ adamc@524: \\ adamc@525: &&& c \; c & \textrm{type-level function application} \\ adamc@530: &&& \lambda x \; :: \; \kappa \Rightarrow c & \textrm{type-level function abstraction} \\ adamc@524: \\ adamc@652: &&& X \Longrightarrow c & \textrm{type-level kind-polymorphic function abstraction} \\ adamc@655: &&& c [\kappa] & \textrm{type-level kind-polymorphic function application} \\ adamc@652: \\ adamc@525: &&& () & \textrm{type-level unit} \\ adamc@525: &&& \#X & \textrm{field name} \\ adamc@524: \\ adamc@525: &&& [(c = c)^*] & \textrm{known-length type-level record} \\ adamc@525: &&& c \rc c & \textrm{type-level record concatenation} \\ adamc@652: &&& \mt{map} & \textrm{type-level record map} \\ adamc@524: \\ adamc@558: &&& (c,^+) & \textrm{type-level tuple} \\ adamc@525: &&& c.n & \textrm{type-level tuple projection ($n \in \mathbb N^+$)} \\ adamc@524: \\ adamc@652: &&& [c \sim c] \Rightarrow \tau & \textrm{guarded type} \\ adamc@524: \\ adamc@529: &&& \_ :: \kappa & \textrm{wildcard} \\ adamc@525: &&& (c) & \textrm{explicit precedence} \\ adamc@530: \\ adamc@530: \textrm{Qualified uncapitalized variables} & \hat{x} &::=& x & \textrm{not from a module} \\ adamc@530: &&& M.x & \textrm{projection from a module} \\ adamc@525: \end{array}$$ adamc@525: adam@1579: We include both abstraction and application for kind polymorphism, but applications are only inferred internally; they may not be written explicitly in source programs. Also, in the ``known-length type-level record'' form, in $c_1 = c_2$ terms, the parser currently only allows $c_1$ to be of the forms $X$ (as a shorthand for $\#X$) or $x$, or a natural number to stand for the corresponding field name (e.g., for tuples). adamc@655: adamc@525: Modules of the module system are described by \emph{signatures}. adamc@525: $$\begin{array}{rrcll} adamc@525: \textrm{Signatures} & S &::=& \mt{sig} \; s^* \; \mt{end} & \textrm{constant} \\ adamc@525: &&& X & \textrm{variable} \\ adamc@525: &&& \mt{functor}(X : S) : S & \textrm{functor} \\ adamc@529: &&& S \; \mt{where} \; \mt{con} \; x = c & \textrm{concretizing an abstract constructor} \\ adamc@525: &&& M.X & \textrm{projection from a module} \\ adamc@525: \\ adamc@525: \textrm{Signature items} & s &::=& \mt{con} \; x :: \kappa & \textrm{abstract constructor} \\ adamc@525: &&& \mt{con} \; x :: \kappa = c & \textrm{concrete constructor} \\ adamc@528: &&& \mt{datatype} \; x \; x^* = dc\mid^+ & \textrm{algebraic datatype definition} \\ adamc@529: &&& \mt{datatype} \; x = \mt{datatype} \; M.x & \textrm{algebraic datatype import} \\ adamc@525: &&& \mt{val} \; x : \tau & \textrm{value} \\ adamc@525: &&& \mt{structure} \; X : S & \textrm{sub-module} \\ adamc@525: &&& \mt{signature} \; X = S & \textrm{sub-signature} \\ adamc@525: &&& \mt{include} \; S & \textrm{signature inclusion} \\ adamc@525: &&& \mt{constraint} \; c \sim c & \textrm{record disjointness constraint} \\ adamc@654: &&& \mt{class} \; x :: \kappa & \textrm{abstract constructor class} \\ adamc@654: &&& \mt{class} \; x :: \kappa = c & \textrm{concrete constructor class} \\ adamc@525: \\ adamc@525: \textrm{Datatype constructors} & dc &::=& X & \textrm{nullary constructor} \\ adamc@525: &&& X \; \mt{of} \; \tau & \textrm{unary constructor} \\ adamc@524: \end{array}$$ adamc@524: adamc@526: \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: $$\begin{array}{rrcll} adamc@526: \textrm{Patterns} & p &::=& \_ & \textrm{wildcard} \\ adamc@526: &&& x & \textrm{variable} \\ adamc@526: &&& \ell & \textrm{constant} \\ adamc@526: &&& \hat{X} & \textrm{nullary constructor} \\ adamc@526: &&& \hat{X} \; p & \textrm{unary constructor} \\ adamc@526: &&& \{(x = p,)^*\} & \textrm{rigid record pattern} \\ adamc@526: &&& \{(x = p,)^+, \ldots\} & \textrm{flexible record pattern} \\ adamc@852: &&& p : \tau & \textrm{type annotation} \\ adamc@527: &&& (p) & \textrm{explicit precedence} \\ adamc@526: \\ adamc@529: \textrm{Qualified capitalized variables} & \hat{X} &::=& X & \textrm{not from a module} \\ adamc@526: &&& M.X & \textrm{projection from a module} \\ adamc@526: \end{array}$$ adamc@526: adamc@527: \emph{Expressions} are the main run-time entities, corresponding to both ``expressions'' and ``statements'' in mainstream imperative languages. adamc@527: $$\begin{array}{rrcll} adamc@527: \textrm{Expressions} & e &::=& e : \tau & \textrm{type annotation} \\ adamc@529: &&& \hat{x} & \textrm{variable} \\ adamc@529: &&& \hat{X} & \textrm{datatype constructor} \\ adamc@527: &&& \ell & \textrm{constant} \\ adamc@527: \\ adamc@527: &&& e \; e & \textrm{function application} \\ adamc@527: &&& \lambda x : \tau \Rightarrow e & \textrm{function abstraction} \\ adamc@527: &&& e [c] & \textrm{polymorphic function application} \\ adamc@852: &&& \lambda [x \; ? \; \kappa] \Rightarrow e & \textrm{polymorphic function abstraction} \\ adamc@655: &&& e [\kappa] & \textrm{kind-polymorphic function application} \\ adamc@652: &&& X \Longrightarrow e & \textrm{kind-polymorphic function abstraction} \\ adamc@527: \\ adamc@527: &&& \{(c = e,)^*\} & \textrm{known-length record} \\ adamc@527: &&& e.c & \textrm{record field projection} \\ adamc@527: &&& e \rc e & \textrm{record concatenation} \\ adamc@527: &&& e \rcut c & \textrm{removal of a single record field} \\ adamc@527: &&& e \rcutM c & \textrm{removal of multiple record fields} \\ adamc@527: \\ adamc@527: &&& \mt{let} \; ed^* \; \mt{in} \; e \; \mt{end} & \textrm{local definitions} \\ adamc@527: \\ adamc@527: &&& \mt{case} \; e \; \mt{of} \; (p \Rightarrow e|)^+ & \textrm{pattern matching} \\ adamc@527: \\ adamc@654: &&& \lambda [c \sim c] \Rightarrow e & \textrm{guarded expression abstraction} \\ adamc@654: &&& e \; ! & \textrm{guarded expression application} \\ adamc@527: \\ adamc@527: &&& \_ & \textrm{wildcard} \\ adamc@527: &&& (e) & \textrm{explicit precedence} \\ adamc@527: \\ adamc@527: \textrm{Local declarations} & ed &::=& \cd{val} \; x : \tau = e & \textrm{non-recursive value} \\ adamc@527: &&& \cd{val} \; \cd{rec} \; (x : \tau = e \; \cd{and})^+ & \textrm{mutually-recursive values} \\ adamc@527: \end{array}$$ adamc@527: adamc@655: As with constructors, we include both abstraction and application for kind polymorphism, but applications are only inferred internally. adamc@655: adamc@528: \emph{Declarations} primarily bring new symbols into context. adamc@528: $$\begin{array}{rrcll} adamc@528: \textrm{Declarations} & d &::=& \mt{con} \; x :: \kappa = c & \textrm{constructor synonym} \\ adamc@528: &&& \mt{datatype} \; x \; x^* = dc\mid^+ & \textrm{algebraic datatype definition} \\ adamc@529: &&& \mt{datatype} \; x = \mt{datatype} \; M.x & \textrm{algebraic datatype import} \\ adamc@528: &&& \mt{val} \; x : \tau = e & \textrm{value} \\ adamc@528: &&& \mt{val} \; \cd{rec} \; (x : \tau = e \; \mt{and})^+ & \textrm{mutually-recursive values} \\ adamc@528: &&& \mt{structure} \; X : S = M & \textrm{module definition} \\ adamc@528: &&& \mt{signature} \; X = S & \textrm{signature definition} \\ adamc@528: &&& \mt{open} \; M & \textrm{module inclusion} \\ adamc@528: &&& \mt{constraint} \; c \sim c & \textrm{record disjointness constraint} \\ adamc@528: &&& \mt{open} \; \mt{constraints} \; M & \textrm{inclusion of just the constraints from a module} \\ adamc@528: &&& \mt{table} \; x : c & \textrm{SQL table} \\ adam@1594: &&& \mt{view} \; x = e & \textrm{SQL view} \\ adamc@528: &&& \mt{sequence} \; x & \textrm{SQL sequence} \\ adamc@535: &&& \mt{cookie} \; x : \tau & \textrm{HTTP cookie} \\ adamc@784: &&& \mt{style} \; x : \tau & \textrm{CSS class} \\ adamc@654: &&& \mt{class} \; x :: \kappa = c & \textrm{concrete constructor class} \\ adamc@1085: &&& \mt{task} \; e = e & \textrm{recurring task} \\ adamc@528: \\ adamc@529: \textrm{Modules} & M &::=& \mt{struct} \; d^* \; \mt{end} & \textrm{constant} \\ adamc@529: &&& X & \textrm{variable} \\ adamc@529: &&& M.X & \textrm{projection} \\ adamc@529: &&& M(M) & \textrm{functor application} \\ adamc@529: &&& \mt{functor}(X : S) : S = M & \textrm{functor abstraction} \\ adamc@528: \end{array}$$ adamc@528: adamc@528: 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: adam@1594: We omit some extra possibilities in $\mt{table}$ syntax, deferring them to Section \ref{tables}. The concrete syntax of $\mt{view}$ declarations is also more complex than shown in the table above, with details deferred to Section \ref{tables}. adamc@784: adamc@529: \subsection{Shorthands} adamc@529: adamc@529: 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: adamc@529: 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: adamc@529: A record type may be written $\{(c = c,)^*\}$, which elaborates to $\$[(c = c,)^*]$. adamc@529: adamc@533: The notation $[c_1, \ldots, c_n]$ is shorthand for $[c_1 = (), \ldots, c_n = ()]$. adamc@533: adam@1350: A tuple type $\tau_1 \times \ldots \times \tau_n$ expands to a record type $\{1 : \tau_1, \ldots, n : \tau_n\}$, with natural numbers as field names. A tuple expression $(e_1, \ldots, e_n)$ expands to a record expression $\{1 = e_1, \ldots, n = e_n\}$. 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: adamc@852: 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: adam@1574: Further, the signature item or declaration syntax $\mt{con} \; x \; b^+ = c$ is shorthand for wrapping of the appropriate $\lambda$s around the righthand side $c$. The $b$ elements may not include $X$, and there may also be an optional $:: \kappa$ before the $=$. adam@1574: adam@1306: In some contexts, the parser isn't happy with token sequences like $x :: \_$, to indicate a constructor variable of wildcard kind. In such cases, write the second two tokens as $::\hspace{-.05in}\_$, with no intervening spaces. Analogous syntax $:::\hspace{-.05in}\_$ is available for implicit constructor arguments. adam@1302: adamc@529: 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: adamc@529: 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: adamc@654: A signature item or declaration $\mt{class} \; x = \lambda y \Rightarrow c$ may be abbreviated $\mt{class} \; x \; y = c$. adamc@529: adam@1482: 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 type class instance and disjointness arguments have been made explicit. (For the purposes of this paragraph, the type family $\mt{Top.folder}$ is a type class, though it isn't marked as one by the usual means.) An expression $@@x$ achieves the same effect, additionally making explicit all implicit constructor arguments. The default is that implicit arguments are inserted automatically after any reference to a variable, or after any application of a variable to one or more arguments. For such an expression, implicit wildcard arguments are added for the longest prefix of the expression's type consisting only of implicit polymorphism, type class instances, and disjointness obligations. The same syntax works for variables projected out of modules and for capitalized variables (datatype constructors). adamc@529: adamc@852: 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: adamc@852: 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: adamc@852: 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: adamc@529: 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: adamc@852: 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: adamc@853: A declaration $\mt{table} \; x : \{(c = c,)^*\}$ is elaborated into $\mt{table} \; x : [(c = c,)^*]$. adamc@529: adamc@529: The syntax $\mt{where} \; \mt{type}$ is an alternate form of $\mt{where} \; \mt{con}$. adamc@529: adamc@529: 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: adamc@529: 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: adamc@784: 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: adamc@530: adamc@530: \section{Static Semantics} adamc@530: adamc@530: 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: adamc@530: 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: \begin{itemize} adamc@655: \item $\Gamma \vdash \kappa$ expresses kind well-formedness. adamc@530: \item $\Gamma \vdash c :: \kappa$ assigns a kind to a constructor in a context. adamc@530: \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: \item $\Gamma \vdash c \hookrightarrow C$ proves that record constructor $c$ decomposes into set $C$ of field names and record constructors. adamc@530: \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: \item $\Gamma \vdash e : \tau$ is a standard typing judgment. adamc@534: \item $\Gamma \vdash p \leadsto \Gamma; \tau$ combines typing of patterns with calculation of which new variables they bind. adamc@537: \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: \item $\Gamma \vdash S \equiv S$ is the signature equivalence judgment. adamc@536: \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: \item $\Gamma \vdash M : S$ is the module signature checking judgment. adamc@537: \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: \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: \end{itemize} adamc@530: adamc@655: adamc@655: \subsection{Kind Well-Formedness} adamc@655: adamc@655: $$\infer{\Gamma \vdash \mt{Type}}{} adamc@655: \quad \infer{\Gamma \vdash \mt{Unit}}{} adamc@655: \quad \infer{\Gamma \vdash \mt{Name}}{} adamc@655: \quad \infer{\Gamma \vdash \kappa_1 \to \kappa_2}{ adamc@655: \Gamma \vdash \kappa_1 adamc@655: & \Gamma \vdash \kappa_2 adamc@655: } adamc@655: \quad \infer{\Gamma \vdash \{\kappa\}}{ adamc@655: \Gamma \vdash \kappa adamc@655: } adamc@655: \quad \infer{\Gamma \vdash (\kappa_1 \times \ldots \times \kappa_n)}{ adamc@655: \forall i: \Gamma \vdash \kappa_i adamc@655: }$$ adamc@655: adamc@655: $$\infer{\Gamma \vdash X}{ adamc@655: X \in \Gamma adamc@655: } adamc@655: \quad \infer{\Gamma \vdash X \longrightarrow \kappa}{ adamc@655: \Gamma, X \vdash \kappa adamc@655: }$$ adamc@655: adamc@530: \subsection{Kinding} adamc@530: adamc@655: We write $[X \mapsto \kappa_1]\kappa_2$ for capture-avoiding substitution of $\kappa_1$ for $X$ in $\kappa_2$. adamc@655: adamc@530: $$\infer{\Gamma \vdash (c) :: \kappa :: \kappa}{ adamc@530: \Gamma \vdash c :: \kappa adamc@530: } adamc@530: \quad \infer{\Gamma \vdash x :: \kappa}{ adamc@530: x :: \kappa \in \Gamma adamc@530: } adamc@530: \quad \infer{\Gamma \vdash x :: \kappa}{ adamc@530: x :: \kappa = c \in \Gamma adamc@530: }$$ adamc@530: adamc@530: $$\infer{\Gamma \vdash M.x :: \kappa}{ adamc@537: \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end} adamc@537: & \mt{proj}(M, \overline{s}, \mt{con} \; x) = \kappa adamc@530: } adamc@530: \quad \infer{\Gamma \vdash M.x :: \kappa}{ adamc@537: \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end} adamc@537: & \mt{proj}(M, \overline{s}, \mt{con} \; x) = (\kappa, c) adamc@530: }$$ adamc@530: adamc@530: $$\infer{\Gamma \vdash \tau_1 \to \tau_2 :: \mt{Type}}{ adamc@530: \Gamma \vdash \tau_1 :: \mt{Type} adamc@530: & \Gamma \vdash \tau_2 :: \mt{Type} adamc@530: } adamc@530: \quad \infer{\Gamma \vdash x \; ? \: \kappa \to \tau :: \mt{Type}}{ adamc@530: \Gamma, x :: \kappa \vdash \tau :: \mt{Type} adamc@530: } adamc@655: \quad \infer{\Gamma \vdash X \longrightarrow \tau :: \mt{Type}}{ adamc@655: \Gamma, X \vdash \tau :: \mt{Type} adamc@655: } adamc@530: \quad \infer{\Gamma \vdash \$c :: \mt{Type}}{ adamc@530: \Gamma \vdash c :: \{\mt{Type}\} adamc@530: }$$ adamc@530: adamc@530: $$\infer{\Gamma \vdash c_1 \; c_2 :: \kappa_2}{ adamc@530: \Gamma \vdash c_1 :: \kappa_1 \to \kappa_2 adamc@530: & \Gamma \vdash c_2 :: \kappa_1 adamc@530: } adamc@530: \quad \infer{\Gamma \vdash \lambda x \; :: \; \kappa_1 \Rightarrow c :: \kappa_1 \to \kappa_2}{ adamc@530: \Gamma, x :: \kappa_1 \vdash c :: \kappa_2 adamc@530: }$$ adamc@530: adamc@655: $$\infer{\Gamma \vdash c[\kappa'] :: [X \mapsto \kappa']\kappa}{ adamc@655: \Gamma \vdash c :: X \to \kappa adamc@655: & \Gamma \vdash \kappa' adamc@655: } adamc@655: \quad \infer{\Gamma \vdash X \Longrightarrow c :: X \to \kappa}{ adamc@655: \Gamma, X \vdash c :: \kappa adamc@655: }$$ adamc@655: adamc@530: $$\infer{\Gamma \vdash () :: \mt{Unit}}{} adamc@530: \quad \infer{\Gamma \vdash \#X :: \mt{Name}}{}$$ adamc@530: adamc@530: $$\infer{\Gamma \vdash [\overline{c_i = c'_i}] :: \{\kappa\}}{ adamc@530: \forall i: \Gamma \vdash c_i : \mt{Name} adamc@530: & \Gamma \vdash c'_i :: \kappa adamc@530: & \forall i \neq j: \Gamma \vdash c_i \sim c_j adamc@530: } adamc@530: \quad \infer{\Gamma \vdash c_1 \rc c_2 :: \{\kappa\}}{ adamc@530: \Gamma \vdash c_1 :: \{\kappa\} adamc@530: & \Gamma \vdash c_2 :: \{\kappa\} adamc@530: & \Gamma \vdash c_1 \sim c_2 adamc@530: }$$ adamc@530: adamc@655: $$\infer{\Gamma \vdash \mt{map} :: (\kappa_1 \to \kappa_2) \to \{\kappa_1\} \to \{\kappa_2\}}{}$$ adamc@530: adamc@573: $$\infer{\Gamma \vdash (\overline c) :: (\kappa_1 \times \ldots \times \kappa_n)}{ adamc@573: \forall i: \Gamma \vdash c_i :: \kappa_i adamc@530: } adamc@573: \quad \infer{\Gamma \vdash c.i :: \kappa_i}{ adamc@573: \Gamma \vdash c :: (\kappa_1 \times \ldots \times \kappa_n) adamc@530: }$$ adamc@530: adamc@655: $$\infer{\Gamma \vdash \lambda [c_1 \sim c_2] \Rightarrow \tau :: \mt{Type}}{ adamc@655: \Gamma \vdash c_1 :: \{\kappa\} adamc@530: & \Gamma \vdash c_2 :: \{\kappa'\} adamc@655: & \Gamma, c_1 \sim c_2 \vdash \tau :: \mt{Type} adamc@530: }$$ adamc@530: adamc@531: \subsection{Record Disjointness} adamc@531: adamc@531: $$\infer{\Gamma \vdash c_1 \sim c_2}{ adamc@558: \Gamma \vdash c_1 \hookrightarrow C_1 adamc@558: & \Gamma \vdash c_2 \hookrightarrow C_2 adamc@558: & \forall c'_1 \in C_1, c'_2 \in C_2: \Gamma \vdash c'_1 \sim c'_2 adamc@531: } adamc@531: \quad \infer{\Gamma \vdash X \sim X'}{ adamc@531: X \neq X' adamc@531: }$$ adamc@531: adamc@531: $$\infer{\Gamma \vdash c_1 \sim c_2}{ adamc@531: c'_1 \sim c'_2 \in \Gamma adamc@558: & \Gamma \vdash c'_1 \hookrightarrow C_1 adamc@558: & \Gamma \vdash c'_2 \hookrightarrow C_2 adamc@558: & c_1 \in C_1 adamc@558: & c_2 \in C_2 adamc@531: }$$ adamc@531: adamc@531: $$\infer{\Gamma \vdash c \hookrightarrow \{c\}}{} adamc@531: \quad \infer{\Gamma \vdash [\overline{c = c'}] \hookrightarrow \{\overline{c}\}}{} adamc@531: \quad \infer{\Gamma \vdash c_1 \rc c_2 \hookrightarrow C_1 \cup C_2}{ adamc@531: \Gamma \vdash c_1 \hookrightarrow C_1 adamc@531: & \Gamma \vdash c_2 \hookrightarrow C_2 adamc@531: } adamc@531: \quad \infer{\Gamma \vdash c \hookrightarrow C}{ adamc@531: \Gamma \vdash c \equiv c' adamc@531: & \Gamma \vdash c' \hookrightarrow C adamc@531: } adamc@531: \quad \infer{\Gamma \vdash \mt{map} \; f \; c \hookrightarrow C}{ adamc@531: \Gamma \vdash c \hookrightarrow C adamc@531: }$$ adamc@531: adamc@541: \subsection{\label{definitional}Definitional Equality} adamc@532: adamc@655: 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: adamc@532: $$\infer{\Gamma \vdash c \equiv c}{} adamc@532: \quad \infer{\Gamma \vdash c_1 \equiv c_2}{ adamc@532: \Gamma \vdash c_2 \equiv c_1 adamc@532: } adamc@532: \quad \infer{\Gamma \vdash c_1 \equiv c_3}{ adamc@532: \Gamma \vdash c_1 \equiv c_2 adamc@532: & \Gamma \vdash c_2 \equiv c_3 adamc@532: } adamc@532: \quad \infer{\Gamma \vdash \mathcal C[c_1] \equiv \mathcal C[c_2]}{ adamc@532: \Gamma \vdash c_1 \equiv c_2 adamc@532: }$$ adamc@532: adamc@532: $$\infer{\Gamma \vdash x \equiv c}{ adamc@532: x :: \kappa = c \in \Gamma adamc@532: } adamc@532: \quad \infer{\Gamma \vdash M.x \equiv c}{ adamc@537: \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end} adamc@537: & \mt{proj}(M, \overline{s}, \mt{con} \; x) = (\kappa, c) adamc@532: } adamc@532: \quad \infer{\Gamma \vdash (\overline c).i \equiv c_i}{}$$ adamc@532: adamc@532: $$\infer{\Gamma \vdash (\lambda x :: \kappa \Rightarrow c) \; c' \equiv [x \mapsto c'] c}{} adamc@655: \quad \infer{\Gamma \vdash (X \Longrightarrow c) [\kappa] \equiv [X \mapsto \kappa] c}{}$$ adamc@655: adamc@655: $$\infer{\Gamma \vdash c_1 \rc c_2 \equiv c_2 \rc c_1}{} adamc@532: \quad \infer{\Gamma \vdash c_1 \rc (c_2 \rc c_3) \equiv (c_1 \rc c_2) \rc c_3}{}$$ adamc@532: adamc@532: $$\infer{\Gamma \vdash [] \rc c \equiv c}{} adamc@532: \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: adamc@655: $$\infer{\Gamma \vdash \mt{map} \; f \; [] \equiv []}{} adamc@655: \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: adamc@532: $$\infer{\Gamma \vdash \mt{map} \; (\lambda x \Rightarrow x) \; c \equiv c}{} adamc@655: \quad \infer{\Gamma \vdash \mt{map} \; f \; (\mt{map} \; f' \; c) adamc@655: \equiv \mt{map} \; (\lambda x \Rightarrow f \; (f' \; x)) \; c}{}$$ adamc@532: adamc@532: $$\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: adamc@534: \subsection{Expression Typing} adamc@533: adamc@873: 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: adamc@533: 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: adamc@533: $$\infer{\Gamma \vdash e : \tau : \tau}{ adamc@533: \Gamma \vdash e : \tau adamc@533: } adamc@533: \quad \infer{\Gamma \vdash e : \tau}{ adamc@533: \Gamma \vdash e : \tau' adamc@533: & \Gamma \vdash \tau' \equiv \tau adamc@533: } adamc@533: \quad \infer{\Gamma \vdash \ell : T(\ell)}{}$$ adamc@533: adamc@533: $$\infer{\Gamma \vdash x : \mathcal I(\tau)}{ adamc@533: x : \tau \in \Gamma adamc@533: } adamc@533: \quad \infer{\Gamma \vdash M.x : \mathcal I(\tau)}{ adamc@537: \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end} adamc@537: & \mt{proj}(M, \overline{s}, \mt{val} \; x) = \tau adamc@533: } adamc@533: \quad \infer{\Gamma \vdash X : \mathcal I(\tau)}{ adamc@533: X : \tau \in \Gamma adamc@533: } adamc@533: \quad \infer{\Gamma \vdash M.X : \mathcal I(\tau)}{ adamc@537: \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end} adamc@537: & \mt{proj}(M, \overline{s}, \mt{val} \; X) = \tau adamc@533: }$$ adamc@533: adamc@533: $$\infer{\Gamma \vdash e_1 \; e_2 : \tau_2}{ adamc@533: \Gamma \vdash e_1 : \tau_1 \to \tau_2 adamc@533: & \Gamma \vdash e_2 : \tau_1 adamc@533: } adamc@533: \quad \infer{\Gamma \vdash \lambda x : \tau_1 \Rightarrow e : \tau_1 \to \tau_2}{ adamc@533: \Gamma, x : \tau_1 \vdash e : \tau_2 adamc@533: }$$ adamc@533: adamc@533: $$\infer{\Gamma \vdash e [c] : [x \mapsto c]\tau}{ adamc@533: \Gamma \vdash e : x :: \kappa \to \tau adamc@533: & \Gamma \vdash c :: \kappa adamc@533: } adamc@852: \quad \infer{\Gamma \vdash \lambda [x \; ? \; \kappa] \Rightarrow e : x \; ? \; \kappa \to \tau}{ adamc@533: \Gamma, x :: \kappa \vdash e : \tau adamc@533: }$$ adamc@533: adamc@655: $$\infer{\Gamma \vdash e [\kappa] : [X \mapsto \kappa]\tau}{ adamc@655: \Gamma \vdash e : X \longrightarrow \tau adamc@655: & \Gamma \vdash \kappa adamc@655: } adamc@655: \quad \infer{\Gamma \vdash X \Longrightarrow e : X \longrightarrow \tau}{ adamc@655: \Gamma, X \vdash e : \tau adamc@655: }$$ adamc@655: adamc@533: $$\infer{\Gamma \vdash \{\overline{c = e}\} : \{\overline{c : \tau}\}}{ adamc@533: \forall i: \Gamma \vdash c_i :: \mt{Name} adamc@533: & \Gamma \vdash e_i : \tau_i adamc@533: & \forall i \neq j: \Gamma \vdash c_i \sim c_j adamc@533: } adamc@533: \quad \infer{\Gamma \vdash e.c : \tau}{ adamc@533: \Gamma \vdash e : \$([c = \tau] \rc c') adamc@533: } adamc@533: \quad \infer{\Gamma \vdash e_1 \rc e_2 : \$(c_1 \rc c_2)}{ adamc@533: \Gamma \vdash e_1 : \$c_1 adamc@533: & \Gamma \vdash e_2 : \$c_2 adamc@573: & \Gamma \vdash c_1 \sim c_2 adamc@533: }$$ adamc@533: adamc@533: $$\infer{\Gamma \vdash e \rcut c : \$c'}{ adamc@533: \Gamma \vdash e : \$([c = \tau] \rc c') adamc@533: } adamc@533: \quad \infer{\Gamma \vdash e \rcutM c : \$c'}{ adamc@533: \Gamma \vdash e : \$(c \rc c') adamc@533: }$$ adamc@533: adamc@533: $$\infer{\Gamma \vdash \mt{let} \; \overline{ed} \; \mt{in} \; e \; \mt{end} : \tau}{ adamc@533: \Gamma \vdash \overline{ed} \leadsto \Gamma' adamc@533: & \Gamma' \vdash e : \tau adamc@533: } adamc@533: \quad \infer{\Gamma \vdash \mt{case} \; e \; \mt{of} \; \overline{p \Rightarrow e} : \tau}{ adamc@533: \forall i: \Gamma \vdash p_i \leadsto \Gamma_i, \tau' adamc@533: & \Gamma_i \vdash e_i : \tau adamc@533: }$$ adamc@533: adamc@573: $$\infer{\Gamma \vdash \lambda [c_1 \sim c_2] \Rightarrow e : \lambda [c_1 \sim c_2] \Rightarrow \tau}{ adamc@533: \Gamma \vdash c_1 :: \{\kappa\} adamc@655: & \Gamma \vdash c_2 :: \{\kappa'\} adamc@533: & \Gamma, c_1 \sim c_2 \vdash e : \tau adamc@662: } adamc@662: \quad \infer{\Gamma \vdash e \; ! : \tau}{ adamc@662: \Gamma \vdash e : [c_1 \sim c_2] \Rightarrow \tau adamc@662: & \Gamma \vdash c_1 \sim c_2 adamc@533: }$$ adamc@533: adamc@534: \subsection{Pattern Typing} adamc@534: adamc@534: $$\infer{\Gamma \vdash \_ \leadsto \Gamma; \tau}{} adamc@534: \quad \infer{\Gamma \vdash x \leadsto \Gamma, x : \tau; \tau}{} adamc@534: \quad \infer{\Gamma \vdash \ell \leadsto \Gamma; T(\ell)}{}$$ adamc@534: adamc@534: $$\infer{\Gamma \vdash X \leadsto \Gamma; \overline{[x_i \mapsto \tau'_i]}\tau}{ adamc@534: X : \overline{x ::: \mt{Type}} \to \tau \in \Gamma adamc@534: & \textrm{$\tau$ not a function type} adamc@534: } adamc@534: \quad \infer{\Gamma \vdash X \; p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau}{ adamc@534: X : \overline{x ::: \mt{Type}} \to \tau'' \to \tau \in \Gamma adamc@534: & \Gamma \vdash p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau'' adamc@534: }$$ adamc@534: adamc@534: $$\infer{\Gamma \vdash M.X \leadsto \Gamma; \overline{[x_i \mapsto \tau'_i]}\tau}{ adamc@537: \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end} adamc@537: & \mt{proj}(M, \overline{s}, \mt{val} \; X) = \overline{x ::: \mt{Type}} \to \tau adamc@534: & \textrm{$\tau$ not a function type} adamc@534: }$$ adamc@534: adamc@534: $$\infer{\Gamma \vdash M.X \; p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau}{ adamc@537: \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end} adamc@537: & \mt{proj}(M, \overline{s}, \mt{val} \; X) = \overline{x ::: \mt{Type}} \to \tau'' \to \tau adamc@534: & \Gamma \vdash p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau'' adamc@534: }$$ adamc@534: adamc@534: $$\infer{\Gamma \vdash \{\overline{x = p}\} \leadsto \Gamma_n; \{\overline{x = \tau}\}}{ adamc@534: \Gamma_0 = \Gamma adamc@534: & \forall i: \Gamma_i \vdash p_i \leadsto \Gamma_{i+1}; \tau_i adamc@534: } adamc@534: \quad \infer{\Gamma \vdash \{\overline{x = p}, \ldots\} \leadsto \Gamma_n; \$([\overline{x = \tau}] \rc c)}{ adamc@534: \Gamma_0 = \Gamma adamc@534: & \forall i: \Gamma_i \vdash p_i \leadsto \Gamma_{i+1}; \tau_i adamc@534: }$$ adamc@534: adamc@852: $$\infer{\Gamma \vdash p : \tau \leadsto \Gamma'; \tau}{ adamc@852: \Gamma \vdash p \leadsto \Gamma'; \tau' adamc@852: & \Gamma \vdash \tau' \equiv \tau adamc@852: }$$ adamc@852: adamc@535: \subsection{Declaration Typing} adamc@535: adamc@535: 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: adamc@655: 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: adamc@558: 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: 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: adamc@535: $$\infer{\Gamma \vdash \cdot \leadsto \Gamma}{} adamc@535: \quad \infer{\Gamma \vdash d, \overline{d} \leadsto \Gamma''}{ adamc@535: \Gamma \vdash d \leadsto \Gamma' adamc@535: & \Gamma' \vdash \overline{d} \leadsto \Gamma'' adamc@535: }$$ adamc@535: adamc@535: $$\infer{\Gamma \vdash \mt{con} \; x :: \kappa = c \leadsto \Gamma, x :: \kappa = c}{ adamc@535: \Gamma \vdash c :: \kappa adamc@535: } adamc@535: \quad \infer{\Gamma \vdash \mt{datatype} \; x \; \overline{y} = \overline{dc} \leadsto \Gamma'}{ adamc@535: \overline{y}; x; \Gamma, x :: \mt{Type}^{\mt{len}(\overline y)} \to \mt{Type} \vdash \overline{dc} \leadsto \Gamma' adamc@535: }$$ adamc@535: adamc@535: $$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leadsto \Gamma'}{ adamc@537: \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end} adamc@537: & \mt{proj}(M, \overline{s}, \mt{datatype} \; z) = (\overline{y}, \overline{dc}) adamc@535: & \overline{y}; x; \Gamma, x :: \mt{Type}^{\mt{len}(\overline y)} \to \mt{Type} = M.z \vdash \overline{dc} \leadsto \Gamma' adamc@535: }$$ adamc@535: adamc@535: $$\infer{\Gamma \vdash \mt{val} \; x : \tau = e \leadsto \Gamma, x : \tau}{ adamc@535: \Gamma \vdash e : \tau adamc@535: }$$ adamc@535: adamc@535: $$\infer{\Gamma \vdash \mt{val} \; \mt{rec} \; \overline{x : \tau = e} \leadsto \Gamma, \overline{x : \tau}}{ adamc@535: \forall i: \Gamma, \overline{x : \tau} \vdash e_i : \tau_i adamc@535: & \textrm{$e_i$ starts with an expression $\lambda$, optionally preceded by constructor and disjointness $\lambda$s} adamc@535: }$$ adamc@535: adamc@535: $$\infer{\Gamma \vdash \mt{structure} \; X : S = M \leadsto \Gamma, X : S}{ adamc@535: \Gamma \vdash M : S adamc@558: & \textrm{ $M$ not a constant or application} adamc@535: } adamc@558: \quad \infer{\Gamma \vdash \mt{structure} \; X : S = M \leadsto \Gamma, X : \mt{selfify}(X, \overline{s})}{ adamc@558: \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end} adamc@539: }$$ adamc@539: adamc@539: $$\infer{\Gamma \vdash \mt{signature} \; X = S \leadsto \Gamma, X = S}{ adamc@535: \Gamma \vdash S adamc@535: }$$ adamc@535: adamc@537: $$\infer{\Gamma \vdash \mt{open} \; M \leadsto \Gamma, \mathcal O(M, \overline{s})}{ adamc@537: \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end} adamc@535: }$$ adamc@535: adamc@535: $$\infer{\Gamma \vdash \mt{constraint} \; c_1 \sim c_2 \leadsto \Gamma}{ adamc@535: \Gamma \vdash c_1 :: \{\kappa\} adamc@535: & \Gamma \vdash c_2 :: \{\kappa\} adamc@535: & \Gamma \vdash c_1 \sim c_2 adamc@535: } adamc@537: \quad \infer{\Gamma \vdash \mt{open} \; \mt{constraints} \; M \leadsto \Gamma, \mathcal O_c(M, \overline{s})}{ adamc@537: \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end} adamc@535: }$$ adamc@535: adamc@784: $$\infer{\Gamma \vdash \mt{table} \; x : c \leadsto \Gamma, x : \mt{Basis}.\mt{sql\_table} \; c \; []}{ adamc@535: \Gamma \vdash c :: \{\mt{Type}\} adamc@535: } adam@1594: \quad \infer{\Gamma \vdash \mt{view} \; x = e \leadsto \Gamma, x : \mt{Basis}.\mt{sql\_view} \; c}{ adam@1594: \Gamma \vdash e :: \mt{Basis}.\mt{sql\_query} \; [] \; [] \; (\mt{map} \; (\lambda \_ \Rightarrow []) \; c') \; c adamc@784: }$$ adamc@784: adamc@784: $$\infer{\Gamma \vdash \mt{sequence} \; x \leadsto \Gamma, x : \mt{Basis}.\mt{sql\_sequence}}{}$$ adamc@535: adamc@535: $$\infer{\Gamma \vdash \mt{cookie} \; x : \tau \leadsto \Gamma, x : \mt{Basis}.\mt{http\_cookie} \; \tau}{ adamc@535: \Gamma \vdash \tau :: \mt{Type} adamc@784: } adamc@784: \quad \infer{\Gamma \vdash \mt{style} \; x \leadsto \Gamma, x : \mt{Basis}.\mt{css\_class}}{}$$ adamc@535: adamc@1085: $$\infer{\Gamma \vdash \mt{task} \; e_1 = e_2 \leadsto \Gamma}{ adam@1348: \Gamma \vdash e_1 :: \mt{Basis}.\mt{task\_kind} \; \tau adam@1348: & \Gamma \vdash e_2 :: \tau \to \mt{Basis}.\mt{transaction} \; \{\} adamc@1085: }$$ adamc@1085: adamc@784: $$\infer{\Gamma \vdash \mt{class} \; x :: \kappa = c \leadsto \Gamma, x :: \kappa = c}{ adamc@784: \Gamma \vdash c :: \kappa adamc@535: }$$ adamc@535: adamc@535: $$\infer{\overline{y}; x; \Gamma \vdash \cdot \leadsto \Gamma}{} adamc@535: \quad \infer{\overline{y}; x; \Gamma \vdash X \mid \overline{dc} \leadsto \Gamma', X : \overline{y ::: \mt{Type}} \to x \; \overline{y}}{ adamc@535: \overline{y}; x; \Gamma \vdash \overline{dc} \leadsto \Gamma' adamc@535: } adamc@535: \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: \overline{y}; x; \Gamma \vdash \overline{dc} \leadsto \Gamma' adamc@535: }$$ adamc@535: adamc@537: \subsection{Signature Item Typing} adamc@537: adamc@537: We appeal to a signature item analogue of the $\mathcal O$ function from the last subsection. adamc@537: adamc@537: $$\infer{\Gamma \vdash \cdot \leadsto \Gamma}{} adamc@537: \quad \infer{\Gamma \vdash s, \overline{s} \leadsto \Gamma''}{ adamc@537: \Gamma \vdash s \leadsto \Gamma' adamc@537: & \Gamma' \vdash \overline{s} \leadsto \Gamma'' adamc@537: }$$ adamc@537: adamc@537: $$\infer{\Gamma \vdash \mt{con} \; x :: \kappa \leadsto \Gamma, x :: \kappa}{} adamc@537: \quad \infer{\Gamma \vdash \mt{con} \; x :: \kappa = c \leadsto \Gamma, x :: \kappa = c}{ adamc@537: \Gamma \vdash c :: \kappa adamc@537: } adamc@537: \quad \infer{\Gamma \vdash \mt{datatype} \; x \; \overline{y} = \overline{dc} \leadsto \Gamma'}{ adamc@537: \overline{y}; x; \Gamma, x :: \mt{Type}^{\mt{len}(\overline y)} \to \mt{Type} \vdash \overline{dc} \leadsto \Gamma' adamc@537: }$$ adamc@537: adamc@537: $$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leadsto \Gamma'}{ adamc@537: \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end} adamc@537: & \mt{proj}(M, \overline{s}, \mt{datatype} \; z) = (\overline{y}, \overline{dc}) adamc@537: & \overline{y}; x; \Gamma, x :: \mt{Type}^{\mt{len}(\overline y)} \to \mt{Type} = M.z \vdash \overline{dc} \leadsto \Gamma' adamc@537: }$$ adamc@537: adamc@537: $$\infer{\Gamma \vdash \mt{val} \; x : \tau \leadsto \Gamma, x : \tau}{ adamc@537: \Gamma \vdash \tau :: \mt{Type} adamc@537: }$$ adamc@537: adamc@537: $$\infer{\Gamma \vdash \mt{structure} \; X : S \leadsto \Gamma, X : S}{ adamc@537: \Gamma \vdash S adamc@537: } adamc@537: \quad \infer{\Gamma \vdash \mt{signature} \; X = S \leadsto \Gamma, X = S}{ adamc@537: \Gamma \vdash S adamc@537: }$$ adamc@537: adamc@537: $$\infer{\Gamma \vdash \mt{include} \; S \leadsto \Gamma, \mathcal O(\overline{s})}{ adamc@537: \Gamma \vdash S adamc@537: & \Gamma \vdash S \equiv \mt{sig} \; \overline{s} \; \mt{end} adamc@537: }$$ adamc@537: adamc@537: $$\infer{\Gamma \vdash \mt{constraint} \; c_1 \sim c_2 \leadsto \Gamma, c_1 \sim c_2}{ adamc@537: \Gamma \vdash c_1 :: \{\kappa\} adamc@537: & \Gamma \vdash c_2 :: \{\kappa\} adamc@537: }$$ adamc@537: adamc@784: $$\infer{\Gamma \vdash \mt{class} \; x :: \kappa = c \leadsto \Gamma, x :: \kappa = c}{ adamc@784: \Gamma \vdash c :: \kappa adamc@537: } adamc@784: \quad \infer{\Gamma \vdash \mt{class} \; x :: \kappa \leadsto \Gamma, x :: \kappa}{}$$ adamc@537: adamc@536: \subsection{Signature Compatibility} adamc@536: adamc@558: 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: adamc@537: 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: adamc@536: $$\infer{\Gamma \vdash S \equiv S}{} adamc@536: \quad \infer{\Gamma \vdash S_1 \equiv S_2}{ adamc@536: \Gamma \vdash S_2 \equiv S_1 adamc@536: } adamc@536: \quad \infer{\Gamma \vdash X \equiv S}{ adamc@536: X = S \in \Gamma adamc@536: } adamc@536: \quad \infer{\Gamma \vdash M.X \equiv S}{ adamc@537: \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end} adamc@537: & \mt{proj}(M, \overline{s}, \mt{signature} \; X) = S adamc@536: }$$ adamc@536: adamc@536: $$\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: \Gamma \vdash S \equiv \mt{sig} \; \overline{s^1} \; \mt{con} \; x :: \kappa \; \overline{s_2} \; \mt{end} adamc@536: & \Gamma \vdash c :: \kappa adamc@537: } adamc@537: \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: \Gamma \vdash S \equiv \mt{sig} \; \overline{s} \; \mt{end} adamc@536: }$$ adamc@536: adamc@536: $$\infer{\Gamma \vdash S_1 \leq S_2}{ adamc@536: \Gamma \vdash S_1 \equiv S_2 adamc@536: } adamc@536: \quad \infer{\Gamma \vdash \mt{sig} \; \overline{s} \; \mt{end} \leq \mt{sig} \; \mt{end}}{} adamc@537: \quad \infer{\Gamma \vdash \mt{sig} \; \overline{s} \; \mt{end} \leq \mt{sig} \; s' \; \overline{s'} \; \mt{end}}{ adamc@537: \Gamma \vdash \overline{s} \leq s' adamc@537: & \Gamma \vdash s' \leadsto \Gamma' adamc@537: & \Gamma' \vdash \mt{sig} \; \overline{s} \; \mt{end} \leq \mt{sig} \; \overline{s'} \; \mt{end} adamc@537: }$$ adamc@537: adamc@537: $$\infer{\Gamma \vdash s \; \overline{s} \leq s'}{ adamc@537: \Gamma \vdash s \leq s' adamc@537: } adamc@537: \quad \infer{\Gamma \vdash s \; \overline{s} \leq s'}{ adamc@537: \Gamma \vdash s \leadsto \Gamma' adamc@537: & \Gamma' \vdash \overline{s} \leq s' adamc@536: }$$ adamc@536: adamc@536: $$\infer{\Gamma \vdash \mt{functor} (X : S_1) : S_2 \leq \mt{functor} (X : S'_1) : S'_2}{ adamc@536: \Gamma \vdash S'_1 \leq S_1 adamc@536: & \Gamma, X : S'_1 \vdash S_2 \leq S'_2 adamc@536: }$$ adamc@536: adamc@537: $$\infer{\Gamma \vdash \mt{con} \; x :: \kappa \leq \mt{con} \; x :: \kappa}{} adamc@537: \quad \infer{\Gamma \vdash \mt{con} \; x :: \kappa = c \leq \mt{con} \; x :: \kappa}{} adamc@558: \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: adamc@537: $$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leq \mt{con} \; x :: \mt{Type}^{\mt{len}(y)} \to \mt{Type}}{ adamc@537: \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end} adamc@537: & \mt{proj}(M, \overline{s}, \mt{datatype} \; z) = (\overline{y}, \overline{dc}) adamc@537: }$$ adamc@537: adamc@784: $$\infer{\Gamma \vdash \mt{class} \; x :: \kappa \leq \mt{con} \; x :: \kappa}{} adamc@784: \quad \infer{\Gamma \vdash \mt{class} \; x :: \kappa = c \leq \mt{con} \; x :: \kappa}{}$$ adamc@537: adamc@537: $$\infer{\Gamma \vdash \mt{con} \; x :: \kappa = c_1 \leq \mt{con} \; x :: \mt{\kappa} = c_2}{ adamc@537: \Gamma \vdash c_1 \equiv c_2 adamc@537: } adamc@784: \quad \infer{\Gamma \vdash \mt{class} \; x :: \kappa = c_1 \leq \mt{con} \; x :: \kappa = c_2}{ adamc@537: \Gamma \vdash c_1 \equiv c_2 adamc@537: }$$ adamc@537: adamc@537: $$\infer{\Gamma \vdash \mt{datatype} \; x \; \overline{y} = \overline{dc} \leq \mt{datatype} \; x \; \overline{y} = \overline{dc'}}{ adamc@537: \Gamma, \overline{y :: \mt{Type}} \vdash \overline{dc} \leq \overline{dc'} adamc@537: }$$ adamc@537: adamc@537: $$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leq \mt{datatype} \; x \; \overline{y} = \overline{dc'}}{ adamc@537: \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end} adamc@537: & \mt{proj}(M, \overline{s}, \mt{datatype} \; z) = (\overline{y}, \overline{dc}) adamc@537: & \Gamma, \overline{y :: \mt{Type}} \vdash \overline{dc} \leq \overline{dc'} adamc@537: }$$ adamc@537: adamc@537: $$\infer{\Gamma \vdash \cdot \leq \cdot}{} adamc@537: \quad \infer{\Gamma \vdash X; \overline{dc} \leq X; \overline{dc'}}{ adamc@537: \Gamma \vdash \overline{dc} \leq \overline{dc'} adamc@537: } adamc@537: \quad \infer{\Gamma \vdash X \; \mt{of} \; \tau_1; \overline{dc} \leq X \; \mt{of} \; \tau_2; \overline{dc'}}{ adamc@537: \Gamma \vdash \tau_1 \equiv \tau_2 adamc@537: & \Gamma \vdash \overline{dc} \leq \overline{dc'} adamc@537: }$$ adamc@537: adamc@537: $$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leq \mt{datatype} \; x = \mt{datatype} \; M'.z'}{ adamc@537: \Gamma \vdash M.z \equiv M'.z' adamc@537: }$$ adamc@537: adamc@537: $$\infer{\Gamma \vdash \mt{val} \; x : \tau_1 \leq \mt{val} \; x : \tau_2}{ adamc@537: \Gamma \vdash \tau_1 \equiv \tau_2 adamc@537: } adamc@537: \quad \infer{\Gamma \vdash \mt{structure} \; X : S_1 \leq \mt{structure} \; X : S_2}{ adamc@537: \Gamma \vdash S_1 \leq S_2 adamc@537: } adamc@537: \quad \infer{\Gamma \vdash \mt{signature} \; X = S_1 \leq \mt{signature} \; X = S_2}{ adamc@537: \Gamma \vdash S_1 \leq S_2 adamc@537: & \Gamma \vdash S_2 \leq S_1 adamc@537: }$$ adamc@537: adamc@537: $$\infer{\Gamma \vdash \mt{constraint} \; c_1 \sim c_2 \leq \mt{constraint} \; c'_1 \sim c'_2}{ adamc@537: \Gamma \vdash c_1 \equiv c'_1 adamc@537: & \Gamma \vdash c_2 \equiv c'_2 adamc@537: }$$ adamc@537: adamc@655: $$\infer{\Gamma \vdash \mt{class} \; x :: \kappa \leq \mt{class} \; x :: \kappa}{} adamc@655: \quad \infer{\Gamma \vdash \mt{class} \; x :: \kappa = c \leq \mt{class} \; x :: \kappa}{} adamc@655: \quad \infer{\Gamma \vdash \mt{class} \; x :: \kappa = c_1 \leq \mt{class} \; x :: \kappa = c_2}{ adamc@537: \Gamma \vdash c_1 \equiv c_2 adamc@537: }$$ adamc@537: adamc@538: \subsection{Module Typing} adamc@538: adamc@538: 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: adamc@538: $$\infer{\Gamma \vdash M : S}{ adamc@538: \Gamma \vdash M : S' adamc@538: & \Gamma \vdash S' \leq S adamc@538: } adamc@538: \quad \infer{\Gamma \vdash \mt{struct} \; \overline{d} \; \mt{end} : \mt{sig} \; \mt{sigOf}(\overline{d}) \; \mt{end}}{ adamc@538: \Gamma \vdash \overline{d} \leadsto \Gamma' adamc@538: } adamc@538: \quad \infer{\Gamma \vdash X : S}{ adamc@538: X : S \in \Gamma adamc@538: }$$ adamc@538: adamc@538: $$\infer{\Gamma \vdash M.X : S}{ adamc@538: \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end} adamc@538: & \mt{proj}(M, \overline{s}, \mt{structure} \; X) = S adamc@538: }$$ adamc@538: adamc@538: $$\infer{\Gamma \vdash M_1(M_2) : [X \mapsto M_2]S_2}{ adamc@538: \Gamma \vdash M_1 : \mt{functor}(X : S_1) : S_2 adamc@538: & \Gamma \vdash M_2 : S_1 adamc@538: } adamc@538: \quad \infer{\Gamma \vdash \mt{functor} (X : S_1) : S_2 = M : \mt{functor} (X : S_1) : S_2}{ adamc@538: \Gamma \vdash S_1 adamc@538: & \Gamma, X : S_1 \vdash S_2 adamc@538: & \Gamma, X : S_1 \vdash M : S_2 adamc@538: }$$ adamc@538: adamc@538: \begin{eqnarray*} adamc@538: \mt{sigOf}(\cdot) &=& \cdot \\ adamc@538: \mt{sigOf}(s \; \overline{s'}) &=& \mt{sigOf}(s) \; \mt{sigOf}(\overline{s'}) \\ adamc@538: \\ adamc@538: \mt{sigOf}(\mt{con} \; x :: \kappa = c) &=& \mt{con} \; x :: \kappa = c \\ adamc@538: \mt{sigOf}(\mt{datatype} \; x \; \overline{y} = \overline{dc}) &=& \mt{datatype} \; x \; \overline{y} = \overline{dc} \\ adamc@538: \mt{sigOf}(\mt{datatype} \; x = \mt{datatype} \; M.z) &=& \mt{datatype} \; x = \mt{datatype} \; M.z \\ adamc@538: \mt{sigOf}(\mt{val} \; x : \tau = e) &=& \mt{val} \; x : \tau \\ adamc@538: \mt{sigOf}(\mt{val} \; \mt{rec} \; \overline{x : \tau = e}) &=& \overline{\mt{val} \; x : \tau} \\ adamc@538: \mt{sigOf}(\mt{structure} \; X : S = M) &=& \mt{structure} \; X : S \\ adamc@538: \mt{sigOf}(\mt{signature} \; X = S) &=& \mt{signature} \; X = S \\ adamc@538: \mt{sigOf}(\mt{open} \; M) &=& \mt{include} \; S \textrm{ (where $\Gamma \vdash M : S$)} \\ adamc@538: \mt{sigOf}(\mt{constraint} \; c_1 \sim c_2) &=& \mt{constraint} \; c_1 \sim c_2 \\ adamc@538: \mt{sigOf}(\mt{open} \; \mt{constraints} \; M) &=& \cdot \\ adamc@538: \mt{sigOf}(\mt{table} \; x : c) &=& \mt{table} \; x : c \\ adam@1594: \mt{sigOf}(\mt{view} \; x = e) &=& \mt{view} \; x : c \textrm{ (where $\Gamma \vdash e : \mt{Basis}.\mt{sql\_query} \; [] \; [] \; (\mt{map} \; (\lambda \_ \Rightarrow []) \; c') \; c$)} \\ adamc@538: \mt{sigOf}(\mt{sequence} \; x) &=& \mt{sequence} \; x \\ adamc@538: \mt{sigOf}(\mt{cookie} \; x : \tau) &=& \mt{cookie} \; x : \tau \\ adamc@784: \mt{sigOf}(\mt{style} \; x) &=& \mt{style} \; x \\ adamc@655: \mt{sigOf}(\mt{class} \; x :: \kappa = c) &=& \mt{class} \; x :: \kappa = c \\ adamc@538: \end{eqnarray*} adamc@539: \begin{eqnarray*} adamc@539: \mt{selfify}(M, \cdot) &=& \cdot \\ adamc@558: \mt{selfify}(M, s \; \overline{s'}) &=& \mt{selfify}(M, s) \; \mt{selfify}(M, \overline{s'}) \\ adamc@539: \\ adamc@539: \mt{selfify}(M, \mt{con} \; x :: \kappa) &=& \mt{con} \; x :: \kappa = M.x \\ adamc@539: \mt{selfify}(M, \mt{con} \; x :: \kappa = c) &=& \mt{con} \; x :: \kappa = c \\ adamc@539: \mt{selfify}(M, \mt{datatype} \; x \; \overline{y} = \overline{dc}) &=& \mt{datatype} \; x \; \overline{y} = \mt{datatype} \; M.x \\ adamc@539: \mt{selfify}(M, \mt{datatype} \; x = \mt{datatype} \; M'.z) &=& \mt{datatype} \; x = \mt{datatype} \; M'.z \\ adamc@539: \mt{selfify}(M, \mt{val} \; x : \tau) &=& \mt{val} \; x : \tau \\ adamc@539: \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: \mt{selfify}(M, \mt{signature} \; X = S) &=& \mt{signature} \; X = S \\ adamc@539: \mt{selfify}(M, \mt{include} \; S) &=& \mt{include} \; S \\ adamc@539: \mt{selfify}(M, \mt{constraint} \; c_1 \sim c_2) &=& \mt{constraint} \; c_1 \sim c_2 \\ adamc@655: \mt{selfify}(M, \mt{class} \; x :: \kappa) &=& \mt{class} \; x :: \kappa = M.x \\ adamc@655: \mt{selfify}(M, \mt{class} \; x :: \kappa = c) &=& \mt{class} \; x :: \kappa = c \\ adamc@539: \end{eqnarray*} adamc@539: adamc@540: \subsection{Module Projection} adamc@540: adamc@540: \begin{eqnarray*} adamc@540: \mt{proj}(M, \mt{con} \; x :: \kappa \; \overline{s}, \mt{con} \; x) &=& \kappa \\ adamc@540: \mt{proj}(M, \mt{con} \; x :: \kappa = c \; \overline{s}, \mt{con} \; x) &=& (\kappa, c) \\ adamc@540: \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: \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: && \textrm{and $\mt{proj}(M', \overline{s'}, \mt{datatype} \; z) = (\overline{y}, \overline{dc})$)} \\ adamc@655: \mt{proj}(M, \mt{class} \; x :: \kappa \; \overline{s}, \mt{con} \; x) &=& \kappa \to \mt{Type} \\ adamc@655: \mt{proj}(M, \mt{class} \; x :: \kappa = c \; \overline{s}, \mt{con} \; x) &=& (\kappa \to \mt{Type}, c) \\ adamc@540: \\ adamc@540: \mt{proj}(M, \mt{datatype} \; x \; \overline{y} = \overline{dc} \; \overline{s}, \mt{datatype} \; x) &=& (\overline{y}, \overline{dc}) \\ adamc@540: \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: \\ adamc@540: \mt{proj}(M, \mt{val} \; x : \tau \; \overline{s}, \mt{val} \; x) &=& \tau \\ adamc@540: \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: \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: \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: && \textrm{and $\mt{proj}(M', \overline{s'}, \mt{datatype} \; z = (\overline{y}, \overline{dc})$ and $X \in \overline{dc}$)} \\ adamc@540: \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: && \textrm{and $\mt{proj}(M', \overline{s'}, \mt{datatype} \; z = (\overline{y}, \overline{dc})$ and $X \; \mt{of} \; \tau \in \overline{dc}$)} \\ adamc@540: \\ adamc@540: \mt{proj}(M, \mt{structure} \; X : S \; \overline{s}, \mt{structure} \; X) &=& S \\ adamc@540: \\ adamc@540: \mt{proj}(M, \mt{signature} \; X = S \; \overline{s}, \mt{signature} \; X) &=& S \\ adamc@540: \\ adamc@540: \mt{proj}(M, \mt{con} \; x :: \kappa \; \overline{s}, V) &=& [x \mapsto M.x]\mt{proj}(M, \overline{s}, V) \\ adamc@540: \mt{proj}(M, \mt{con} \; x :: \kappa = c \; \overline{s}, V) &=& [x \mapsto M.x]\mt{proj}(M, \overline{s}, V) \\ adamc@540: \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: \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: \mt{proj}(M, \mt{val} \; x : \tau \; \overline{s}, V) &=& \mt{proj}(M, \overline{s}, V) \\ adamc@540: \mt{proj}(M, \mt{structure} \; X : S \; \overline{s}, V) &=& [X \mapsto M.X]\mt{proj}(M, \overline{s}, V) \\ adamc@540: \mt{proj}(M, \mt{signature} \; X = S \; \overline{s}, V) &=& [X \mapsto M.X]\mt{proj}(M, \overline{s}, V) \\ adamc@540: \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: \mt{proj}(M, \mt{constraint} \; c_1 \sim c_2 \; \overline{s}, V) &=& \mt{proj}(M, \overline{s}, V) \\ adamc@655: \mt{proj}(M, \mt{class} \; x :: \kappa \; \overline{s}, V) &=& [x \mapsto M.x]\mt{proj}(M, \overline{s}, V) \\ adamc@655: \mt{proj}(M, \mt{class} \; x :: \kappa = c \; \overline{s}, V) &=& [x \mapsto M.x]\mt{proj}(M, \overline{s}, V) \\ adamc@540: \end{eqnarray*} adamc@540: adamc@541: adamc@541: \section{Type Inference} adamc@541: adamc@541: 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: adamc@541: \subsection{Basic Unification} adamc@541: adamc@560: 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: adamc@656: 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: adamc@541: 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: adamc@541: \subsection{Unifying Record Types} adamc@541: adamc@570: 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: adamc@656: \subsection{\label{typeclasses}Constructor Classes} adamc@541: adamc@784: 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: adamc@784: 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: adamc@656: 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: adamc@656: 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: adamc@541: \subsection{Reverse-Engineering Record Types} adamc@541: adamc@656: 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: adamc@541: \subsection{Implicit Arguments in Functor Applications} adamc@541: adamc@656: 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: adamc@541: adamc@542: \section{The Ur Standard Library} adamc@542: adamc@542: 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: adamc@542: 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: adamc@542: 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: $$\begin{array}{l} adamc@542: \mt{type} \; \mt{int} \\ adamc@542: \mt{type} \; \mt{float} \\ adamc@873: \mt{type} \; \mt{char} \\ adamc@542: \mt{type} \; \mt{string} \\ adamc@542: \mt{type} \; \mt{time} \\ adamc@785: \mt{type} \; \mt{blob} \\ adamc@542: \\ adamc@542: \mt{type} \; \mt{unit} = \{\} \\ adamc@542: \\ adamc@542: \mt{datatype} \; \mt{bool} = \mt{False} \mid \mt{True} \\ adamc@542: \\ adamc@785: \mt{datatype} \; \mt{option} \; \mt{t} = \mt{None} \mid \mt{Some} \; \mt{of} \; \mt{t} \\ adamc@785: \\ adamc@785: \mt{datatype} \; \mt{list} \; \mt{t} = \mt{Nil} \mid \mt{Cons} \; \mt{of} \; \mt{t} \times \mt{list} \; \mt{t} adamc@542: \end{array}$$ adamc@542: adamc@1123: The only unusual element of this list is the $\mt{blob}$ type, which stands for binary sequences. Simple blobs can be created from strings via $\mt{Basis.textBlob}$. Blobs will also be generated from HTTP file uploads. adamc@785: adam@1297: Ur also supports \emph{polymorphic variants}, a dual to extensible records that has been popularized by OCaml. A type $\mt{variant} \; r$ represents an $n$-ary sum type, with one constructor for each field of record $r$. Each constructor $c$ takes an argument of type $r.c$; the type $\{\}$ can be used to ``simulate'' a nullary constructor. The \cd{make} function builds a variant value, while \cd{match} implements pattern-matching, with match cases represented as records of functions. adam@1297: $$\begin{array}{l} adam@1297: \mt{con} \; \mt{variant} :: \{\mt{Type}\} \to \mt{Type} \\ adam@1297: \mt{val} \; \mt{make} : \mt{nm} :: \mt{Name} \to \mt{t} ::: \mt{Type} \to \mt{ts} ::: \{\mt{Type}\} \to [[\mt{nm}] \sim \mt{ts}] \Rightarrow \mt{t} \to \mt{variant} \; ([\mt{nm} = \mt{t}] \rc \mt{ts}) \\ adam@1297: \mt{val} \; \mt{match} : \mt{ts} ::: \{\mt{Type}\} \to \mt{t} ::: \mt{Type} \to \mt{variant} \; \mt{ts} \to \$(\mt{map} \; (\lambda \mt{t'} \Rightarrow \mt{t'} \to \mt{t}) \; \mt{ts}) \to \mt{t} adam@1297: \end{array}$$ adam@1297: adamc@657: Another important generic Ur element comes at the beginning of \texttt{top.urs}. adamc@657: adamc@657: $$\begin{array}{l} adamc@657: \mt{con} \; \mt{folder} :: \mt{K} \longrightarrow \{\mt{K}\} \to \mt{Type} \\ adamc@657: \\ adamc@657: \mt{val} \; \mt{fold} : \mt{K} \longrightarrow \mt{tf} :: (\{\mt{K}\} \to \mt{Type}) \\ adamc@657: \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: \hspace{.2in} \mt{tf} \; \mt{r} \to \mt{tf} \; ([\mt{nm} = \mt{v}] \rc \mt{r})) \\ adamc@657: \hspace{.1in} \to \mt{tf} \; [] \\ adamc@657: \hspace{.1in} \to \mt{r} :: \{\mt{K}\} \to \mt{folder} \; \mt{r} \to \mt{tf} \; \mt{r} adamc@657: \end{array}$$ adamc@657: adamc@657: 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: adamc@664: 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: adamc@542: adamc@542: \section{The Ur/Web Standard Library} adamc@542: adam@1400: Some operations are only allowed in server-side code or only in client-side code. The type system does not enforce such restrictions, but the compiler enforces them in the process of whole-program compilation. In the discussion below, we note when a set of operations has a location restriction. adam@1400: adamc@658: \subsection{Monads} adamc@658: adamc@658: The Ur Basis defines the monad constructor class from Haskell. adamc@658: adamc@658: $$\begin{array}{l} adamc@658: \mt{class} \; \mt{monad} :: \mt{Type} \to \mt{Type} \\ adamc@658: \mt{val} \; \mt{return} : \mt{m} ::: (\mt{Type} \to \mt{Type}) \to \mt{t} ::: \mt{Type} \\ adamc@658: \hspace{.1in} \to \mt{monad} \; \mt{m} \\ adamc@658: \hspace{.1in} \to \mt{t} \to \mt{m} \; \mt{t} \\ adamc@658: \mt{val} \; \mt{bind} : \mt{m} ::: (\mt{Type} \to \mt{Type}) \to \mt{t1} ::: \mt{Type} \to \mt{t2} ::: \mt{Type} \\ adamc@658: \hspace{.1in} \to \mt{monad} \; \mt{m} \\ adamc@658: \hspace{.1in} \to \mt{m} \; \mt{t1} \to (\mt{t1} \to \mt{m} \; \mt{t2}) \\ adam@1544: \hspace{.1in} \to \mt{m} \; \mt{t2} \\ adam@1544: \mt{val} \; \mt{mkMonad} : \mt{m} ::: (\mt{Type} \to \mt{Type}) \\ adam@1544: \hspace{.1in} \to \{\mt{Return} : \mt{t} ::: \mt{Type} \to \mt{t} \to \mt{m} \; \mt{t}, \\ adam@1544: \hspace{.3in} \mt{Bind} : \mt{t1} ::: \mt{Type} \to \mt{t2} ::: \mt{Type} \to \mt{m} \; \mt{t1} \to (\mt{t1} \to \mt{m} \; \mt{t2}) \to \mt{m} \; \mt{t2}\} \\ adam@1544: \hspace{.1in} \to \mt{monad} \; \mt{m} adamc@658: \end{array}$$ adamc@658: adam@1548: The Ur/Web compiler provides syntactic sugar for monads, similar to Haskell's \cd{do} notation. An expression $x \leftarrow e_1; e_2$ is desugarded to $\mt{bind} \; e_1 \; (\lambda x \Rightarrow e_2)$, and an expression $e_1; e_2$ is desugared to $\mt{bind} \; e_1 \; (\lambda () \Rightarrow e_2)$. adam@1548: adamc@542: \subsection{Transactions} adamc@542: adamc@542: 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: $$\begin{array}{l} adamc@542: \mt{con} \; \mt{transaction} :: \mt{Type} \to \mt{Type} \\ adamc@658: \mt{val} \; \mt{transaction\_monad} : \mt{monad} \; \mt{transaction} adamc@542: \end{array}$$ adamc@542: adamc@1123: For debugging purposes, a transactional function is provided for outputting a string on the server process' \texttt{stderr}. adamc@1123: $$\begin{array}{l} adamc@1123: \mt{val} \; \mt{debug} : \mt{string} \to \mt{transaction} \; \mt{unit} adamc@1123: \end{array}$$ adamc@1123: adamc@542: \subsection{HTTP} adamc@542: adam@1400: There are transactions for reading an HTTP header by name and for getting and setting strongly-typed cookies. Cookies may only be created by the $\mt{cookie}$ declaration form, ensuring that they be named consistently based on module structure. For now, cookie operations are server-side only. adamc@542: $$\begin{array}{l} adamc@786: \mt{con} \; \mt{http\_cookie} :: \mt{Type} \to \mt{Type} \\ adamc@786: \mt{val} \; \mt{getCookie} : \mt{t} ::: \mt{Type} \to \mt{http\_cookie} \; \mt{t} \to \mt{transaction} \; (\mt{option} \; \mt{t}) \\ adamc@1050: \mt{val} \; \mt{setCookie} : \mt{t} ::: \mt{Type} \to \mt{http\_cookie} \; \mt{t} \to \{\mt{Value} : \mt{t}, \mt{Expires} : \mt{option} \; \mt{time}, \mt{Secure} : \mt{bool}\} \to \mt{transaction} \; \mt{unit} \\ adamc@1050: \mt{val} \; \mt{clearCookie} : \mt{t} ::: \mt{Type} \to \mt{http\_cookie} \; \mt{t} \to \mt{transaction} \; \mt{unit} adamc@786: \end{array}$$ adamc@786: adamc@786: 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: $$\begin{array}{l} adamc@786: \mt{type} \; \mt{url} \\ adamc@786: \mt{val} \; \mt{bless} : \mt{string} \to \mt{url} \\ adamc@786: \mt{val} \; \mt{checkUrl} : \mt{string} \to \mt{option} \; \mt{url} adamc@786: \end{array}$$ adamc@786: $\mt{bless}$ raises a runtime error if the string passed to it fails the URL policy. adamc@786: adam@1400: It is possible to grab the current page's URL or to build a URL for an arbitrary transaction that would also be an acceptable value of a \texttt{link} attribute of the \texttt{a} tag. These are server-side operations. adamc@1085: $$\begin{array}{l} adamc@1085: \mt{val} \; \mt{currentUrl} : \mt{transaction} \; \mt{url} \\ adamc@1085: \mt{val} \; \mt{url} : \mt{transaction} \; \mt{page} \to \mt{url} adamc@1085: \end{array}$$ adamc@1085: adamc@1085: Page generation may be interrupted at any time with a request to redirect to a particular URL instead. adamc@1085: $$\begin{array}{l} adamc@1085: \mt{val} \; \mt{redirect} : \mt{t} ::: \mt{Type} \to \mt{url} \to \mt{transaction} \; \mt{t} adamc@1085: \end{array}$$ adamc@1085: adam@1400: It's possible for pages to return files of arbitrary MIME types. A file can be input from the user using this data type, along with the $\mt{upload}$ form tag. These functions and those described in the following paragraph are server-side. adamc@786: $$\begin{array}{l} adamc@786: \mt{type} \; \mt{file} \\ adamc@786: \mt{val} \; \mt{fileName} : \mt{file} \to \mt{option} \; \mt{string} \\ adamc@786: \mt{val} \; \mt{fileMimeType} : \mt{file} \to \mt{string} \\ adamc@786: \mt{val} \; \mt{fileData} : \mt{file} \to \mt{blob} adamc@786: \end{array}$$ adamc@786: adam@1465: It is also possible to get HTTP request headers and set HTTP response headers, using abstract types similar to the one for URLs. adam@1465: adam@1465: $$\begin{array}{l} adam@1465: \mt{type} \; \mt{requestHeader} \\ adam@1465: \mt{val} \; \mt{blessRequestHeader} : \mt{string} \to \mt{requestHeader} \\ adam@1465: \mt{val} \; \mt{checkRequestHeader} : \mt{string} \to \mt{option} \; \mt{requestHeader} \\ adam@1465: \mt{val} \; \mt{getHeader} : \mt{requestHeader} \to \mt{transaction} \; (\mt{option} \; \mt{string}) \\ adam@1465: \\ adam@1465: \mt{type} \; \mt{responseHeader} \\ adam@1465: \mt{val} \; \mt{blessResponseHeader} : \mt{string} \to \mt{responseHeader} \\ adam@1465: \mt{val} \; \mt{checkResponseHeader} : \mt{string} \to \mt{option} \; \mt{responseHeader} \\ adam@1465: \mt{val} \; \mt{setHeader} : \mt{responseHeader} \to \mt{string} \to \mt{transaction} \; \mt{unit} adam@1465: \end{array}$$ adam@1465: adamc@786: 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: $$\begin{array}{l} adamc@786: \mt{type} \; \mt{mimeType} \\ adamc@786: \mt{val} \; \mt{blessMime} : \mt{string} \to \mt{mimeType} \\ adamc@786: \mt{val} \; \mt{checkMime} : \mt{string} \to \mt{option} \; \mt{mimeType} \\ adamc@786: \mt{val} \; \mt{returnBlob} : \mt{t} ::: \mt{Type} \to \mt{blob} \to \mt{mimeType} \to \mt{transaction} \; \mt{t} adamc@542: \end{array}$$ adamc@542: adamc@543: \subsection{SQL} adamc@543: adam@1400: Everything about SQL database access is restricted to server-side code. adam@1400: adamc@543: 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: $$\begin{array}{l} adamc@785: \mt{con} \; \mt{sql\_table} :: \{\mt{Type}\} \to \{\{\mt{Unit}\}\} \to \mt{Type} adamc@785: \end{array}$$ adamc@785: 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: adamc@785: We also have the simpler type family of SQL views, which have no keys. adamc@785: $$\begin{array}{l} adamc@785: \mt{con} \; \mt{sql\_view} :: \{\mt{Type}\} \to \mt{Type} adamc@543: \end{array}$$ adamc@543: adamc@785: 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: $$\begin{array}{l} adamc@785: \mt{class} \; \mt{fieldsOf} :: \mt{Type} \to \{\mt{Type}\} \to \mt{Type} \\ adamc@785: \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: \mt{val} \; \mt{fieldsOf\_view} : \mt{fs} ::: \{\mt{Type}\} \to \mt{fieldsOf} \; (\mt{sql\_view} \; \mt{fs}) \; \mt{fs} adamc@785: \end{array}$$ adamc@785: adamc@785: \subsubsection{Table Constraints} adamc@785: adamc@785: 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: adamc@785: $$\begin{array}{l} adamc@785: \mt{con} \; \mt{primary\_key} :: \{\mt{Type}\} \to \{\{\mt{Unit}\}\} \to \mt{Type} \\ adamc@785: \mt{val} \; \mt{no\_primary\_key} : \mt{fs} ::: \{\mt{Type}\} \to \mt{primary\_key} \; \mt{fs} \; [] \\ adamc@785: \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: \hspace{.1in} \to [[\mt{key1}] \sim \mt{keys}] \Rightarrow [[\mt{key1} = \mt{t}] \rc \mt{keys} \sim \mt{rest}] \\ adamc@785: \hspace{.1in} \Rightarrow \$([\mt{key1} = \mt{sql\_injectable\_prim} \; \mt{t}] \rc \mt{map} \; \mt{sql\_injectable\_prim} \; \mt{keys}) \\ adamc@785: \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: \end{array}$$ adamc@785: 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: adamc@785: A type family stands for sets of named constraints of the remaining varieties. adamc@785: $$\begin{array}{l} adamc@785: \mt{con} \; \mt{sql\_constraints} :: \{\mt{Type}\} \to \{\{\mt{Unit}\}\} \to \mt{Type} adamc@785: \end{array}$$ adamc@785: 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: adamc@785: There is a type family of individual, unnamed constraints. adamc@785: $$\begin{array}{l} adamc@785: \mt{con} \; \mt{sql\_constraint} :: \{\mt{Type}\} \to \{\mt{Unit}\} \to \mt{Type} adamc@785: \end{array}$$ adamc@785: The first argument is the same as above, and the second argument gives the key columns for just this constraint. adamc@785: adamc@785: We have operations for assembling constraints into constraint sets. adamc@785: $$\begin{array}{l} adamc@785: \mt{val} \; \mt{no\_constraint} : \mt{fs} ::: \{\mt{Type}\} \to \mt{sql\_constraints} \; \mt{fs} \; [] \\ adamc@785: \mt{val} \; \mt{one\_constraint} : \mt{fs} ::: \{\mt{Type}\} \to \mt{unique} ::: \{\mt{Unit}\} \to \mt{name} :: \mt{Name} \\ adamc@785: \hspace{.1in} \to \mt{sql\_constraint} \; \mt{fs} \; \mt{unique} \to \mt{sql\_constraints} \; \mt{fs} \; [\mt{name} = \mt{unique}] \\ adamc@785: \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: \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: \end{array}$$ adamc@785: adamc@785: 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: $$\begin{array}{l} adamc@785: \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: \hspace{.1in} \to [[\mt{unique1}] \sim \mt{unique}] \Rightarrow [[\mt{unique1} = \mt{t}] \rc \mt{unique} \sim \mt{rest}] \\ adamc@785: \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: \end{array}$$ adamc@785: adamc@785: 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: $$\begin{array}{l} adamc@785: \mt{class} \; \mt{linkable} :: \mt{Type} \to \mt{Type} \to \mt{Type} \\ adamc@785: \mt{val} \; \mt{linkable\_same} : \mt{t} ::: \mt{Type} \to \mt{linkable} \; \mt{t} \; \mt{t} \\ adamc@785: \mt{val} \; \mt{linkable\_from\_nullable} : \mt{t} ::: \mt{Type} \to \mt{linkable} \; (\mt{option} \; \mt{t}) \; \mt{t} \\ adamc@785: \mt{val} \; \mt{linkable\_to\_nullable} : \mt{t} ::: \mt{Type} \to \mt{linkable} \; \mt{t} \; (\mt{option} \; \mt{t}) adamc@785: \end{array}$$ adamc@785: adamc@785: The $\mt{matching}$ type family uses $\mt{linkable}$ to define when two keys match up type-wise. adamc@785: $$\begin{array}{l} adamc@785: \mt{con} \; \mt{matching} :: \{\mt{Type}\} \to \{\mt{Type}\} \to \mt{Type} \\ adamc@785: \mt{val} \; \mt{mat\_nil} : \mt{matching} \; [] \; [] \\ adamc@785: \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: \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: \hspace{.1in} \to \mt{matching} \; ([\mt{nm1} = \mt{t1}] \rc \mt{rest1}) \; ([\mt{nm2} = \mt{t2}] \rc \mt{rest2}) adamc@785: \end{array}$$ adamc@785: adamc@785: 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: $$\begin{array}{l} adamc@785: \mt{con} \; \mt{propagation\_mode} :: \{\mt{Type}\} \to \mt{Type} \\ adamc@785: \mt{val} \; \mt{restrict} : \mt{fs} ::: \{\mt{Type}\} \to \mt{propagation\_mode} \; \mt{fs} \\ adamc@785: \mt{val} \; \mt{cascade} : \mt{fs} ::: \{\mt{Type}\} \to \mt{propagation\_mode} \; \mt{fs} \\ adamc@785: \mt{val} \; \mt{no\_action} : \mt{fs} ::: \{\mt{Type}\} \to \mt{propagation\_mode} \; \mt{fs} \\ adamc@785: \mt{val} \; \mt{set\_null} : \mt{fs} ::: \{\mt{Type}\} \to \mt{propagation\_mode} \; (\mt{map} \; \mt{option} \; \mt{fs}) adamc@785: \end{array}$$ adamc@785: adamc@785: Finally, we put these ingredient together to define the \texttt{FOREIGN KEY} constraint function. adamc@785: $$\begin{array}{l} adamc@785: \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: \hspace{.1in} \to \mt{funused} ::: \{\mt{Type}\} \to \mt{nm} ::: \mt{Name} \to \mt{uniques} ::: \{\{\mt{Unit}\}\} \\ adamc@785: \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: \hspace{.1in} \Rightarrow \mt{matching} \; ([\mt{mine1} = \mt{t}] \rc \mt{mine}) \; \mt{foreign} \\ adamc@785: \hspace{.1in} \to \mt{sql\_table} \; (\mt{foreign} \rc \mt{funused}) \; ([\mt{nm} = \mt{map} \; (\lambda \_ \Rightarrow ()) \; \mt{foreign}] \rc \mt{uniques}) \\ adamc@785: \hspace{.1in} \to \{\mt{OnDelete} : \mt{propagation\_mode} \; ([\mt{mine1} = \mt{t}] \rc \mt{mine}), \\ adamc@785: \hspace{.2in} \mt{OnUpdate} : \mt{propagation\_mode} \; ([\mt{mine1} = \mt{t}] \rc \mt{mine})\} \\ adamc@785: \hspace{.1in} \to \mt{sql\_constraint} \; ([\mt{mine1} = \mt{t}] \rc \mt{mine} \rc \mt{munused}) \; [] adamc@785: \end{array}$$ adamc@785: adamc@785: 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: $$\begin{array}{l} adamc@785: \mt{val} \; \mt{check} : \mt{fs} ::: \{\mt{Type}\} \to \mt{sql\_exp} \; [] \; [] \; \mt{fs} \; \mt{bool} \to \mt{sql\_constraint} \; \mt{fs} \; [] adamc@785: \end{array}$$ adamc@785: adamc@785: 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: adamc@784: adamc@543: \subsubsection{Queries} adamc@543: adam@1400: A final query is constructed via the $\mt{sql\_query}$ function. Constructor arguments respectively specify the unrestricted free table variables (which will only be available in subqueries), the free table variables that may only be mentioned within arguments to aggregate functions, table fields we select (as records mapping tables to the subsets of their fields that we choose), and the (always named) extra expressions that we select. adamc@543: $$\begin{array}{l} adam@1400: \mt{con} \; \mt{sql\_query} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \\ adamc@1193: \mt{val} \; \mt{sql\_query} : \mt{free} ::: \{\{\mt{Type}\}\} \\ adam@1400: \hspace{.1in} \to \mt{afree} ::: \{\{\mt{Type}\}\} \\ adamc@1193: \hspace{.1in} \to \mt{tables} ::: \{\{\mt{Type}\}\} \\ adamc@543: \hspace{.1in} \to \mt{selectedFields} ::: \{\{\mt{Type}\}\} \\ adamc@543: \hspace{.1in} \to \mt{selectedExps} ::: \{\mt{Type}\} \\ adamc@1193: \hspace{.1in} \to [\mt{free} \sim \mt{tables}] \\ adam@1400: \hspace{.1in} \Rightarrow \{\mt{Rows} : \mt{sql\_query1} \; \mt{free} \; \mt{afree} \; \mt{tables} \; \mt{selectedFields} \; \mt{selectedExps}, \\ adamc@1193: \hspace{.2in} \mt{OrderBy} : \mt{sql\_order\_by} \; (\mt{free} \rc \mt{tables}) \; \mt{selectedExps}, \\ adamc@543: \hspace{.2in} \mt{Limit} : \mt{sql\_limit}, \\ adamc@543: \hspace{.2in} \mt{Offset} : \mt{sql\_offset}\} \\ adam@1400: \hspace{.1in} \to \mt{sql\_query} \; \mt{free} \; \mt{afree} \; \mt{selectedFields} \; \mt{selectedExps} adamc@543: \end{array}$$ adamc@543: adamc@545: Queries are used by folding over their results inside transactions. adamc@545: $$\begin{array}{l} adam@1400: \mt{val} \; \mt{query} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to [\mt{tables} \sim \mt{exps}] \Rightarrow \mt{state} ::: \mt{Type} \to \mt{sql\_query} \; [] \; [] \; \mt{tables} \; \mt{exps} \\ adamc@658: \hspace{.1in} \to (\$(\mt{exps} \rc \mt{map} \; (\lambda \mt{fields} :: \{\mt{Type}\} \Rightarrow \$\mt{fields}) \; \mt{tables}) \\ adamc@545: \hspace{.2in} \to \mt{state} \to \mt{transaction} \; \mt{state}) \\ adamc@545: \hspace{.1in} \to \mt{state} \to \mt{transaction} \; \mt{state} adamc@545: \end{array}$$ adamc@545: adam@1400: Most of the complexity of the query encoding is in the type $\mt{sql\_query1}$, which includes simple queries and derived queries based on relational operators. Constructor arguments respectively specify the unrestricted free table veriables, the aggregate-only free table variables, the tables we select from, the subset of fields that we keep from each table for the result rows, and the extra expressions that we select. adamc@543: $$\begin{array}{l} adam@1400: \mt{con} \; \mt{sql\_query1} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \\ adamc@543: \\ adamc@543: \mt{type} \; \mt{sql\_relop} \\ adamc@543: \mt{val} \; \mt{sql\_union} : \mt{sql\_relop} \\ adamc@543: \mt{val} \; \mt{sql\_intersect} : \mt{sql\_relop} \\ adamc@543: \mt{val} \; \mt{sql\_except} : \mt{sql\_relop} \\ adam@1400: \mt{val} \; \mt{sql\_relop} : \mt{free} ::: \{\{\mt{Type}\}\} \\ adam@1400: \hspace{.1in} \to \mt{afree} ::: \{\{\mt{Type}\}\} \\ adam@1400: \hspace{.1in} \to \mt{tables1} ::: \{\{\mt{Type}\}\} \\ adamc@543: \hspace{.1in} \to \mt{tables2} ::: \{\{\mt{Type}\}\} \\ adamc@543: \hspace{.1in} \to \mt{selectedFields} ::: \{\{\mt{Type}\}\} \\ adamc@543: \hspace{.1in} \to \mt{selectedExps} ::: \{\mt{Type}\} \\ adamc@543: \hspace{.1in} \to \mt{sql\_relop} \\ adam@1458: \hspace{.1in} \to \mt{bool} \; (* \; \mt{ALL} \; *) \\ adam@1400: \hspace{.1in} \to \mt{sql\_query1} \; \mt{free} \; \mt{afree} \; \mt{tables1} \; \mt{selectedFields} \; \mt{selectedExps} \\ adam@1400: \hspace{.1in} \to \mt{sql\_query1} \; \mt{free} \; \mt{afree} \; \mt{tables2} \; \mt{selectedFields} \; \mt{selectedExps} \\ adam@1400: \hspace{.1in} \to \mt{sql\_query1} \; \mt{free} \; \mt{afree} \; \mt{selectedFields} \; \mt{selectedFields} \; \mt{selectedExps} adamc@543: \end{array}$$ adamc@543: adamc@543: $$\begin{array}{l} adamc@1193: \mt{val} \; \mt{sql\_query1} : \mt{free} ::: \{\{\mt{Type}\}\} \\ adam@1400: \hspace{.1in} \to \mt{afree} ::: \{\{\mt{Type}\}\} \\ adamc@1193: \hspace{.1in} \to \mt{tables} ::: \{\{\mt{Type}\}\} \\ adamc@543: \hspace{.1in} \to \mt{grouped} ::: \{\{\mt{Type}\}\} \\ adamc@543: \hspace{.1in} \to \mt{selectedFields} ::: \{\{\mt{Type}\}\} \\ adamc@543: \hspace{.1in} \to \mt{selectedExps} ::: \{\mt{Type}\} \\ adamc@1085: \hspace{.1in} \to \mt{empties} :: \{\mt{Unit}\} \\ adamc@1193: \hspace{.1in} \to [\mt{free} \sim \mt{tables}] \\ adamc@1193: \hspace{.1in} \Rightarrow [\mt{free} \sim \mt{grouped}] \\ adam@1400: \hspace{.1in} \Rightarrow [\mt{afree} \sim \mt{tables}] \\ adamc@1193: \hspace{.1in} \Rightarrow [\mt{empties} \sim \mt{selectedFields}] \\ adamc@1085: \hspace{.1in} \Rightarrow \{\mt{Distinct} : \mt{bool}, \\ adamc@1193: \hspace{.2in} \mt{From} : \mt{sql\_from\_items} \; \mt{free} \; \mt{tables}, \\ adam@1400: \hspace{.2in} \mt{Where} : \mt{sql\_exp} \; (\mt{free} \rc \mt{tables}) \; \mt{afree} \; [] \; \mt{bool}, \\ adamc@543: \hspace{.2in} \mt{GroupBy} : \mt{sql\_subset} \; \mt{tables} \; \mt{grouped}, \\ adam@1400: \hspace{.2in} \mt{Having} : \mt{sql\_exp} \; (\mt{free} \rc \mt{grouped}) \; (\mt{afree} \rc \mt{tables}) \; [] \; \mt{bool}, \\ adamc@1085: \hspace{.2in} \mt{SelectFields} : \mt{sql\_subset} \; \mt{grouped} \; (\mt{map} \; (\lambda \_ \Rightarrow []) \; \mt{empties} \rc \mt{selectedFields}), \\ adam@1400: \hspace{.2in} \mt {SelectExps} : \$(\mt{map} \; (\mt{sql\_exp} \; (\mt{free} \rc \mt{grouped}) \; (\mt{afree} \rc \mt{tables}) \; []) \; \mt{selectedExps}) \} \\ adam@1400: \hspace{.1in} \to \mt{sql\_query1} \; \mt{free} \; \mt{afree} \; \mt{tables} \; \mt{selectedFields} \; \mt{selectedExps} adamc@543: \end{array}$$ adamc@543: adamc@543: 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: $$\begin{array}{l} adamc@543: \mt{con} \; \mt{sql\_subset} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \mt{Type} \\ adamc@543: \mt{val} \; \mt{sql\_subset} : \mt{keep\_drop} :: \{(\{\mt{Type}\} \times \{\mt{Type}\})\} \\ adamc@543: \hspace{.1in} \to \mt{sql\_subset} \\ adamc@658: \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: \hspace{.2in} (\mt{map} \; (\lambda \mt{fields} :: (\{\mt{Type}\} \times \{\mt{Type}\}) \Rightarrow \mt{fields}.1) \; \mt{keep\_drop}) \\ adamc@543: \mt{val} \; \mt{sql\_subset\_all} : \mt{tables} :: \{\{\mt{Type}\}\} \to \mt{sql\_subset} \; \mt{tables} \; \mt{tables} adamc@543: \end{array}$$ adamc@543: adamc@560: 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: $$\begin{array}{l} adamc@543: \mt{con} \; \mt{sql\_exp} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \to \mt{Type} adamc@543: \end{array}$$ adamc@543: adamc@543: Any field in scope may be converted to an expression. adamc@543: $$\begin{array}{l} adamc@543: \mt{val} \; \mt{sql\_field} : \mt{otherTabs} ::: \{\{\mt{Type}\}\} \to \mt{otherFields} ::: \{\mt{Type}\} \\ adamc@543: \hspace{.1in} \to \mt{fieldType} ::: \mt{Type} \to \mt{agg} ::: \{\{\mt{Type}\}\} \\ adamc@543: \hspace{.1in} \to \mt{exps} ::: \{\mt{Type}\} \\ adamc@543: \hspace{.1in} \to \mt{tab} :: \mt{Name} \to \mt{field} :: \mt{Name} \\ adamc@543: \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: \end{array}$$ adamc@543: adamc@544: There is an analogous function for referencing named expressions. adamc@544: $$\begin{array}{l} adamc@544: \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: \hspace{.1in} \to \mt{sql\_exp} \; \mt{tabs} \; \mt{agg} \; ([\mt{nm} = \mt{t}] \rc \mt{rest}) \; \mt{t} adamc@544: \end{array}$$ adamc@544: adamc@544: Ur values of appropriate types may be injected into SQL expressions. adamc@544: $$\begin{array}{l} adamc@786: \mt{class} \; \mt{sql\_injectable\_prim} \\ adamc@786: \mt{val} \; \mt{sql\_bool} : \mt{sql\_injectable\_prim} \; \mt{bool} \\ adamc@786: \mt{val} \; \mt{sql\_int} : \mt{sql\_injectable\_prim} \; \mt{int} \\ adamc@786: \mt{val} \; \mt{sql\_float} : \mt{sql\_injectable\_prim} \; \mt{float} \\ adamc@786: \mt{val} \; \mt{sql\_string} : \mt{sql\_injectable\_prim} \; \mt{string} \\ adamc@786: \mt{val} \; \mt{sql\_time} : \mt{sql\_injectable\_prim} \; \mt{time} \\ adamc@786: \mt{val} \; \mt{sql\_blob} : \mt{sql\_injectable\_prim} \; \mt{blob} \\ adamc@786: \mt{val} \; \mt{sql\_channel} : \mt{t} ::: \mt{Type} \to \mt{sql\_injectable\_prim} \; (\mt{channel} \; \mt{t}) \\ adamc@786: \mt{val} \; \mt{sql\_client} : \mt{sql\_injectable\_prim} \; \mt{client} \\ adamc@786: \\ adamc@544: \mt{class} \; \mt{sql\_injectable} \\ adamc@786: \mt{val} \; \mt{sql\_prim} : \mt{t} ::: \mt{Type} \to \mt{sql\_injectable\_prim} \; \mt{t} \to \mt{sql\_injectable} \; \mt{t} \\ adamc@786: \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: \\ adamc@544: \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: \hspace{.1in} \to \mt{t} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} adamc@544: \end{array}$$ adamc@544: adamc@1123: Additionally, most function-free types may be injected safely, via the $\mt{serialized}$ type family. adamc@1123: $$\begin{array}{l} adamc@1123: \mt{con} \; \mt{serialized} :: \mt{Type} \to \mt{Type} \\ adamc@1123: \mt{val} \; \mt{serialize} : \mt{t} ::: \mt{Type} \to \mt{t} \to \mt{serialized} \; \mt{t} \\ adamc@1123: \mt{val} \; \mt{deserialize} : \mt{t} ::: \mt{Type} \to \mt{serialized} \; \mt{t} \to \mt{t} \\ adamc@1123: \mt{val} \; \mt{sql\_serialized} : \mt{t} ::: \mt{Type} \to \mt{sql\_injectable\_prim} \; (\mt{serialized} \; \mt{t}) adamc@1123: \end{array}$$ adamc@1123: adamc@544: 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: $$\begin{array}{l} adamc@544: \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: \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: \end{array}$$ adamc@544: adamc@559: We have generic nullary, unary, and binary operators. adamc@544: $$\begin{array}{l} adamc@544: \mt{con} \; \mt{sql\_nfunc} :: \mt{Type} \to \mt{Type} \\ adamc@544: \mt{val} \; \mt{sql\_current\_timestamp} : \mt{sql\_nfunc} \; \mt{time} \\ adamc@544: \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: \hspace{.1in} \to \mt{sql\_nfunc} \; \mt{t} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} \\\end{array}$$ adamc@544: adamc@544: $$\begin{array}{l} adamc@544: \mt{con} \; \mt{sql\_unary} :: \mt{Type} \to \mt{Type} \to \mt{Type} \\ adamc@544: \mt{val} \; \mt{sql\_not} : \mt{sql\_unary} \; \mt{bool} \; \mt{bool} \\ adamc@544: \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: \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: \end{array}$$ adamc@544: adamc@544: $$\begin{array}{l} adamc@544: \mt{con} \; \mt{sql\_binary} :: \mt{Type} \to \mt{Type} \to \mt{Type} \to \mt{Type} \\ adamc@544: \mt{val} \; \mt{sql\_and} : \mt{sql\_binary} \; \mt{bool} \; \mt{bool} \; \mt{bool} \\ adamc@544: \mt{val} \; \mt{sql\_or} : \mt{sql\_binary} \; \mt{bool} \; \mt{bool} \; \mt{bool} \\ adamc@544: \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: \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: \end{array}$$ adamc@544: adamc@544: $$\begin{array}{l} adamc@559: \mt{class} \; \mt{sql\_arith} \\ adamc@559: \mt{val} \; \mt{sql\_int\_arith} : \mt{sql\_arith} \; \mt{int} \\ adamc@559: \mt{val} \; \mt{sql\_float\_arith} : \mt{sql\_arith} \; \mt{float} \\ adamc@559: \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: \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: \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: \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: \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: \mt{val} \; \mt{sql\_mod} : \mt{sql\_binary} \; \mt{int} \; \mt{int} \; \mt{int} adamc@559: \end{array}$$ adamc@544: adamc@656: 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: $$\begin{array}{l} adamc@544: \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: \end{array}$$ adamc@544: adamc@544: $$\begin{array}{l} adamc@1188: \mt{con} \; \mt{sql\_aggregate} :: \mt{Type} \to \mt{Type} \to \mt{Type} \\ adamc@1188: \mt{val} \; \mt{sql\_aggregate} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{dom} ::: \mt{Type} \to \mt{ran} ::: \mt{Type} \\ adamc@1188: \hspace{.1in} \to \mt{sql\_aggregate} \; \mt{dom} \; \mt{ran} \to \mt{sql\_exp} \; \mt{agg} \; \mt{agg} \; \mt{exps} \; \mt{dom} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{ran} adamc@1188: \end{array}$$ adamc@1188: adamc@1188: $$\begin{array}{l} adamc@1188: \mt{val} \; \mt{sql\_count\_col} : \mt{t} ::: \mt{Type} \to \mt{sql\_aggregate} \; (\mt{option} \; \mt{t}) \; \mt{int} adamc@544: \end{array}$$ adam@1400: adam@1400: Most aggregate functions are typed using a two-parameter constructor class $\mt{nullify}$ which maps $\mt{option}$ types to themselves and adds $\mt{option}$ to others. That is, this constructor class represents the process of making an SQL type ``nullable.'' adamc@544: adamc@544: $$\begin{array}{l} adamc@544: \mt{class} \; \mt{sql\_summable} \\ adamc@544: \mt{val} \; \mt{sql\_summable\_int} : \mt{sql\_summable} \; \mt{int} \\ adamc@544: \mt{val} \; \mt{sql\_summable\_float} : \mt{sql\_summable} \; \mt{float} \\ adam@1400: \mt{val} \; \mt{sql\_avg} : \mt{t} ::: \mt{Type} \to \mt{nt} ::: \mt{Type} \to \mt{sql\_summable} \; \mt{t} \to \mt{nullify} \; \mt{t} \; \mt{nt} \to \mt{sql\_aggregate} \; \mt{t} \; \mt{nt} \\ adam@1400: \mt{val} \; \mt{sql\_sum} : \mt{t} ::: \mt{Type} \to \mt{nt} ::: \mt{Type} \to \mt{sql\_summable} \; \mt{t} \to \mt{nullify} \; \mt{t} \; \mt{nt} \to \mt{sql\_aggregate} \; \mt{t} \; \mt{nt} adamc@544: \end{array}$$ adamc@544: adamc@544: $$\begin{array}{l} adamc@544: \mt{class} \; \mt{sql\_maxable} \\ adamc@544: \mt{val} \; \mt{sql\_maxable\_int} : \mt{sql\_maxable} \; \mt{int} \\ adamc@544: \mt{val} \; \mt{sql\_maxable\_float} : \mt{sql\_maxable} \; \mt{float} \\ adamc@544: \mt{val} \; \mt{sql\_maxable\_string} : \mt{sql\_maxable} \; \mt{string} \\ adamc@544: \mt{val} \; \mt{sql\_maxable\_time} : \mt{sql\_maxable} \; \mt{time} \\ adam@1400: \mt{val} \; \mt{sql\_max} : \mt{t} ::: \mt{Type} \to \mt{nt} ::: \mt{Type} \to \mt{sql\_maxable} \; \mt{t} \to \mt{nullify} \; \mt{t} \; \mt{nt} \to \mt{sql\_aggregate} \; \mt{t} \; \mt{nt} \\ adam@1400: \mt{val} \; \mt{sql\_min} : \mt{t} ::: \mt{Type} \to \mt{nt} ::: \mt{Type} \to \mt{sql\_maxable} \; \mt{t} \to \mt{nullify} \; \mt{t} \; \mt{nt} \to \mt{sql\_aggregate} \; \mt{t} \; \mt{nt} adamc@544: \end{array}$$ adamc@544: adamc@1193: Any SQL query that returns single columns may be turned into a subquery expression. adamc@1193: adamc@786: $$\begin{array}{l} adam@1421: \mt{val} \; \mt{sql\_subquery} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{nm} ::: \mt{Name} \to \mt{t} ::: \mt{Type} \to \mt{nt} ::: \mt{Type} \\ adam@1421: \hspace{.1in} \to \mt{nullify} \; \mt{t} \; \mt{nt} \to \mt{sql\_query} \; \mt{tables} \; \mt{agg} \; [\mt{nm} = \mt{t}] \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{nt} adamc@1193: \end{array}$$ adamc@1193: adam@1573: There is also an \cd{IF..THEN..ELSE..} construct that is compiled into standard SQL \cd{CASE} expressions. adam@1573: $$\begin{array}{l} adam@1573: \mt{val} \; \mt{sql\_if\_then\_else} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{t} ::: \mt{Type} \\ adam@1573: \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{bool} \\ adam@1573: \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} \\ adam@1573: \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} \\ adam@1573: \hspace{.1in} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} adam@1573: \end{array}$$ adam@1573: adamc@1193: \texttt{FROM} clauses are specified using a type family, whose arguments are the free table variables and the table variables bound by this clause. adamc@1193: $$\begin{array}{l} adamc@1193: \mt{con} \; \mt{sql\_from\_items} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \mt{Type} \\ adamc@1193: \mt{val} \; \mt{sql\_from\_table} : \mt{free} ::: \{\{\mt{Type}\}\} \\ adamc@1193: \hspace{.1in} \to \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{free} \; [\mt{name} = \mt{fs}] \\ adamc@1193: \mt{val} \; \mt{sql\_from\_query} : \mt{free} ::: \{\{\mt{Type}\}\} \to \mt{fs} ::: \{\mt{Type}\} \to \mt{name} :: \mt{Name} \to \mt{sql\_query} \; \mt{free} \; [] \; \mt{fs} \to \mt{sql\_from\_items} \; \mt{free} \; [\mt{name} = \mt{fs}] \\ adamc@1193: \mt{val} \; \mt{sql\_from\_comma} : \mt{free} ::: \mt{tabs1} ::: \{\{\mt{Type}\}\} \to \mt{tabs2} ::: \{\{\mt{Type}\}\} \to [\mt{tabs1} \sim \mt{tabs2}] \\ adamc@1193: \hspace{.1in} \Rightarrow \mt{sql\_from\_items} \; \mt{free} \; \mt{tabs1} \to \mt{sql\_from\_items} \; \mt{free} \; \mt{tabs2} \\ adamc@1193: \hspace{.1in} \to \mt{sql\_from\_items} \; \mt{free} \; (\mt{tabs1} \rc \mt{tabs2}) \\ adamc@1193: \mt{val} \; \mt{sql\_inner\_join} : \mt{free} ::: \{\{\mt{Type}\}\} \to \mt{tabs1} ::: \{\{\mt{Type}\}\} \to \mt{tabs2} ::: \{\{\mt{Type}\}\} \\ adamc@1193: \hspace{.1in} \to [\mt{free} \sim \mt{tabs1}] \Rightarrow [\mt{free} \sim \mt{tabs2}] \Rightarrow [\mt{tabs1} \sim \mt{tabs2}] \\ adamc@1193: \hspace{.1in} \Rightarrow \mt{sql\_from\_items} \; \mt{free} \; \mt{tabs1} \to \mt{sql\_from\_items} \; \mt{free} \; \mt{tabs2} \\ adamc@1193: \hspace{.1in} \to \mt{sql\_exp} \; (\mt{free} \rc \mt{tabs1} \rc \mt{tabs2}) \; [] \; [] \; \mt{bool} \\ adamc@1193: \hspace{.1in} \to \mt{sql\_from\_items} \; \mt{free} \; (\mt{tabs1} \rc \mt{tabs2}) adamc@786: \end{array}$$ adamc@786: adamc@786: 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: $$\begin{array}{l} adamc@786: \mt{class} \; \mt{nullify} :: \mt{Type} \to \mt{Type} \to \mt{Type} \\ adamc@786: \mt{val} \; \mt{nullify\_option} : \mt{t} ::: \mt{Type} \to \mt{nullify} \; (\mt{option} \; \mt{t}) \; (\mt{option} \; \mt{t}) \\ adamc@786: \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: \end{array}$$ adamc@786: adamc@786: 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: adamc@786: $$\begin{array}{l} adamc@1193: \mt{val} \; \mt{sql\_left\_join} : \mt{free} ::: \{\{\mt{Type}\}\} \to \mt{tabs1} ::: \{\{\mt{Type}\}\} \to \mt{tabs2} ::: \{\{(\mt{Type} \times \mt{Type})\}\} \\ adamc@1193: \hspace{.1in} \to [\mt{free} \sim \mt{tabs1}] \Rightarrow [\mt{free} \sim \mt{tabs2}] \Rightarrow [\mt{tabs1} \sim \mt{tabs2}] \\ adamc@786: \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@1193: \hspace{.1in} \to \mt{sql\_from\_items} \; \mt{free} \; \mt{tabs1} \to \mt{sql\_from\_items} \; \mt{free} \; (\mt{map} \; (\mt{map} \; (\lambda \mt{p} :: (\mt{Type} \times \mt{Type}) \Rightarrow \mt{p}.1)) \; \mt{tabs2}) \\ adamc@1193: \hspace{.1in} \to \mt{sql\_exp} \; (\mt{free} \rc \mt{tabs1} \rc \mt{map} \; (\mt{map} \; (\lambda \mt{p} :: (\mt{Type} \times \mt{Type}) \Rightarrow \mt{p}.1)) \; \mt{tabs2}) \; [] \; [] \; \mt{bool} \\ adamc@1193: \hspace{.1in} \to \mt{sql\_from\_items} \; \mt{free} \; (\mt{tabs1} \rc \mt{map} \; (\mt{map} \; (\lambda \mt{p} :: (\mt{Type} \times \mt{Type}) \Rightarrow \mt{p}.2)) \; \mt{tabs2}) adamc@786: \end{array}$$ adamc@786: adamc@544: 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: $$\begin{array}{l} adamc@544: \mt{type} \; \mt{sql\_direction} \\ adamc@544: \mt{val} \; \mt{sql\_asc} : \mt{sql\_direction} \\ adamc@544: \mt{val} \; \mt{sql\_desc} : \mt{sql\_direction} \\ adamc@544: \\ adamc@544: \mt{con} \; \mt{sql\_order\_by} :: \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \\ adamc@544: \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: \mt{val} \; \mt{sql\_order\_by\_Cons} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{t} ::: \mt{Type} \\ adamc@544: \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: \\ adamc@544: \mt{type} \; \mt{sql\_limit} \\ adamc@544: \mt{val} \; \mt{sql\_no\_limit} : \mt{sql\_limit} \\ adamc@544: \mt{val} \; \mt{sql\_limit} : \mt{int} \to \mt{sql\_limit} \\ adamc@544: \\ adamc@544: \mt{type} \; \mt{sql\_offset} \\ adamc@544: \mt{val} \; \mt{sql\_no\_offset} : \mt{sql\_offset} \\ adamc@544: \mt{val} \; \mt{sql\_offset} : \mt{int} \to \mt{sql\_offset} adamc@544: \end{array}$$ adamc@544: adamc@545: adamc@545: \subsubsection{DML} adamc@545: adamc@545: 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: adamc@545: $$\begin{array}{l} adamc@545: \mt{type} \; \mt{dml} \\ adamc@545: \mt{val} \; \mt{dml} : \mt{dml} \to \mt{transaction} \; \mt{unit} adamc@545: \end{array}$$ adamc@545: adam@1297: The function $\mt{Basis.dml}$ will trigger a fatal application error if the command fails, for instance, because a data integrity constraint is violated. An alternate function returns an error message as a string instead. adam@1297: adam@1297: $$\begin{array}{l} adam@1297: \mt{val} \; \mt{tryDml} : \mt{dml} \to \mt{transaction} \; (\mt{option} \; \mt{string}) adam@1297: \end{array}$$ adam@1297: adamc@545: Properly-typed records may be used to form $\mt{INSERT}$ commands. adamc@545: $$\begin{array}{l} adamc@545: \mt{val} \; \mt{insert} : \mt{fields} ::: \{\mt{Type}\} \to \mt{sql\_table} \; \mt{fields} \\ adamc@658: \hspace{.1in} \to \$(\mt{map} \; (\mt{sql\_exp} \; [] \; [] \; []) \; \mt{fields}) \to \mt{dml} adamc@545: \end{array}$$ adamc@545: adam@1578: 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. Note that, in the table environment applied to expressions, the table being updated is hardcoded at the name $\mt{T}$. The parsing extension for $\mt{UPDATE}$ will elaborate all table-free field references to use table variable $\mt{T}$. adamc@545: $$\begin{array}{l} adam@1380: \mt{val} \; \mt{update} : \mt{unchanged} ::: \{\mt{Type}\} \to \mt{changed} :: \{\mt{Type}\} \to [\mt{changed} \sim \mt{unchanged}] \\ adamc@658: \hspace{.1in} \Rightarrow \$(\mt{map} \; (\mt{sql\_exp} \; [\mt{T} = \mt{changed} \rc \mt{unchanged}] \; [] \; []) \; \mt{changed}) \\ adamc@545: \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: \end{array}$$ adamc@545: adam@1578: A $\mt{DELETE}$ command is formed from a table and a $\mt{WHERE}$ clause. The above use of $\mt{T}$ is repeated. adamc@545: $$\begin{array}{l} adamc@545: \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: \end{array}$$ adamc@545: adamc@546: \subsubsection{Sequences} adamc@546: adamc@546: 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: adamc@546: $$\begin{array}{l} adamc@546: \mt{type} \; \mt{sql\_sequence} \\ adamc@1085: \mt{val} \; \mt{nextval} : \mt{sql\_sequence} \to \mt{transaction} \; \mt{int} \\ adamc@1085: \mt{val} \; \mt{setval} : \mt{sql\_sequence} \to \mt{int} \to \mt{transaction} \; \mt{unit} adamc@546: \end{array}$$ adamc@546: adamc@546: adamc@547: \subsection{XML} adamc@547: adam@1333: 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. The Ur/Web standard library encodes a very loose version of XHTML, where it is very easy to produce documents which are invalid XHTML, but which still display properly in all major browsers. The main purposes of the invariants that are enforced are first, to provide some documentation about the places where it would make sense to insert XML fragments; and second, to rule out code injection attacks and other abstraction violations related to HTML syntax. adamc@547: adam@1345: 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. For instance, the context for the \texttt{} tag is $[\mt{Body}, \mt{Tr}]$, to indicate a kind of nesting inside \texttt{} and \texttt{}. Contexts are maintained in a somewhat ad-hoc way; the only definitive reference for their meanings is the types of the tag values in \texttt{basis.urs}. The arguments dealing with field binding are only relevant to HTML forms. adamc@547: $$\begin{array}{l} adamc@547: \mt{con} \; \mt{xml} :: \{\mt{Unit}\} \to \{\mt{Type}\} \to \{\mt{Type}\} \to \mt{Type} adamc@547: \end{array}$$ adamc@547: adamc@547: 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: $$\begin{array}{l} adamc@547: \mt{con} \; \mt{tag} :: \{\mt{Type}\} \to \{\mt{Unit}\} \to \{\mt{Unit}\} \to \{\mt{Type}\} \to \{\mt{Type}\} \to \mt{Type} adamc@547: \end{array}$$ adamc@547: adamc@547: Literal text may be injected into XML as ``CDATA.'' adamc@547: $$\begin{array}{l} adamc@547: \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: \end{array}$$ adamc@547: adam@1358: There is also a function to insert the literal value of a character. Since Ur/Web uses the UTF-8 text encoding, the $\mt{cdata}$ function is only sufficient to encode characters with ASCII codes below 128. Higher codes have alternate meanings in UTF-8 than in usual ASCII, so this alternate function should be used with them. adam@1358: $$\begin{array}{l} adam@1358: \mt{val} \; \mt{cdataChar} : \mt{ctx} ::: \{\mt{Unit}\} \to \mt{use} ::: \{\mt{Type}\} \to \mt{char} \to \mt{xml} \; \mt{ctx} \; \mt{use} \; [] adam@1358: \end{array}$$ adam@1358: adamc@547: There is a function for producing an XML tree with a particular tag at its root. adamc@547: $$\begin{array}{l} adamc@547: \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: \hspace{.1in} \to \mt{useOuter} ::: \{\mt{Type}\} \to \mt{useInner} ::: \{\mt{Type}\} \to \mt{bindOuter} ::: \{\mt{Type}\} \to \mt{bindInner} ::: \{\mt{Type}\} \\ adam@1380: \hspace{.1in} \to [\mt{attrsGiven} \sim \mt{attrsAbsent}] \Rightarrow [\mt{useOuter} \sim \mt{useInner}] \Rightarrow [\mt{bindOuter} \sim \mt{bindInner}] \\ adamc@787: \hspace{.1in} \Rightarrow \mt{option} \; \mt{css\_class} \\ adamc@787: \hspace{.1in} \to \$\mt{attrsGiven} \\ adamc@547: \hspace{.1in} \to \mt{tag} \; (\mt{attrsGiven} \rc \mt{attrsAbsent}) \; \mt{ctxOuter} \; \mt{ctxInner} \; \mt{useOuter} \; \mt{bindOuter} \\ adamc@547: \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: \end{array}$$ adam@1297: 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. The function $\mt{Basis.classes}$ can be used to specify a list of CSS classes for a single tag. adamc@547: adamc@547: Two XML fragments may be concatenated. adamc@547: $$\begin{array}{l} adamc@547: \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}\} \\ adam@1380: \hspace{.1in} \to [\mt{use_1} \sim \mt{bind_1}] \Rightarrow [\mt{bind_1} \sim \mt{bind_2}] \\ adamc@547: \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: \end{array}$$ adamc@547: adamc@547: Finally, any XML fragment may be updated to ``claim'' to use more form fields than it does. adamc@547: $$\begin{array}{l} adam@1380: \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 [\mt{use_1} \sim \mt{use_2}] \\ adamc@547: \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: \end{array}$$ adamc@547: adam@1344: 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. Also note that there is currently no way for the programmer to add his own tags. It \emph{is} possible to add new tags directly to \texttt{basis.urs}, but this should only be done as a prelude to suggesting a patch to the main distribution. adamc@547: adamc@547: 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: $$\begin{array}{l} adamc@547: \mt{val} \; \mt{error} : \mt{t} ::: \mt{Type} \to \mt{xml} \; [\mt{Body}] \; [] \; [] \to \mt{t} adamc@547: \end{array}$$ adamc@547: adamc@549: adamc@701: \subsection{Client-Side Programming} adamc@659: adamc@701: Ur/Web supports running code on web browsers, via automatic compilation to JavaScript. adamc@701: adamc@701: \subsubsection{The Basics} adamc@701: adam@1400: All of the functions in this subsection are client-side only. adam@1400: adam@1297: Clients can open alert and confirm dialog boxes, in the usual annoying JavaScript way. adamc@701: $$\begin{array}{l} adam@1297: \mt{val} \; \mt{alert} : \mt{string} \to \mt{transaction} \; \mt{unit} \\ adam@1297: \mt{val} \; \mt{confirm} : \mt{string} \to \mt{transaction} \; \mt{bool} adamc@701: \end{array}$$ adamc@701: adamc@701: Any transaction may be run in a new thread with the $\mt{spawn}$ function. adamc@701: $$\begin{array}{l} adamc@701: \mt{val} \; \mt{spawn} : \mt{transaction} \; \mt{unit} \to \mt{transaction} \; \mt{unit} adamc@701: \end{array}$$ adamc@701: adamc@701: The current thread can be paused for at least a specified number of milliseconds. adamc@701: $$\begin{array}{l} adamc@701: \mt{val} \; \mt{sleep} : \mt{int} \to \mt{transaction} \; \mt{unit} adamc@701: \end{array}$$ adamc@701: adamc@787: 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: $$\begin{array}{l} adamc@787: \mt{val} \; \mt{onError} : (\mt{xbody} \to \mt{transaction} \; \mt{unit}) \to \mt{transaction} \; \mt{unit} \\ adamc@787: \mt{val} \; \mt{onFail} : (\mt{string} \to \mt{transaction} \; \mt{unit}) \to \mt{transaction} \; \mt{unit} \\ adamc@787: \mt{val} \; \mt{onConnectFail} : \mt{transaction} \; \mt{unit} \to \mt{transaction} \; \mt{unit} \\ adamc@787: \mt{val} \; \mt{onDisconnect} : \mt{transaction} \; \mt{unit} \to \mt{transaction} \; \mt{unit} \\ adamc@787: \mt{val} \; \mt{onServerError} : (\mt{string} \to \mt{transaction} \; \mt{unit}) \to \mt{transaction} \; \mt{unit} adamc@787: \end{array}$$ adamc@787: adam@1555: There are also functions to register standard document-level event handlers. adam@1555: adam@1555: $$\begin{array}{l} adam@1555: \mt{val} \; \mt{onClick} : \mt{transaction} \; \mt{unit} \to \mt{transaction} \; \mt{unit} \\ adam@1555: \mt{val} \; \mt{onDblclick} : \mt{transaction} \; \mt{unit} \to \mt{transaction} \; \mt{unit} \\ adam@1555: \mt{val} \; \mt{onKeydown} : (\mt{int} \to \mt{transaction} \; \mt{unit}) \to \mt{transaction} \; \mt{unit} \\ adam@1555: \mt{val} \; \mt{onKeypress} : (\mt{int} \to \mt{transaction} \; \mt{unit}) \to \mt{transaction} \; \mt{unit} \\ adam@1555: \mt{val} \; \mt{onKeyup} : (\mt{int} \to \mt{transaction} \; \mt{unit}) \to \mt{transaction} \; \mt{unit} \\ adam@1555: \mt{val} \; \mt{onMousedown} : \mt{transaction} \; \mt{unit} \to \mt{transaction} \; \mt{unit} \\ adam@1555: \mt{val} \; \mt{onMouseup} : \mt{transaction} \; \mt{unit} \to \mt{transaction} \; \mt{unit} adam@1555: \end{array}$$ adam@1555: adam@1559: Versions of standard JavaScript functions are provided that event handlers may call to mask default handling or prevent bubbling of events up to parent DOM nodes, respectively. adam@1559: adam@1559: $$\begin{array}{l} adam@1559: \mt{val} \; \mt{preventDefault} : \mt{transaction} \; \mt{unit} \\ adam@1559: \mt{val} \; \mt{stopPropagation} : \mt{transaction} \; \mt{unit} adam@1559: \end{array}$$ adam@1559: adam@1556: \subsubsection{Node IDs} adam@1556: adam@1556: There is an abstract type of node IDs that may be assigned to \cd{id} attributes of most HTML tags. adam@1556: adam@1556: $$\begin{array}{l} adam@1556: \mt{type} \; \mt{id} \\ adam@1556: \mt{val} \; \mt{fresh} : \mt{transaction} \; \mt{id} adam@1556: \end{array}$$ adam@1556: adam@1556: The \cd{fresh} function is allowed on both server and client, but there is no other way to create IDs, which includes lack of a way to force an ID to match a particular string. The only semantic importance of IDs within Ur/Web is in uses of the HTML \cd{