annotate doc/manual.tex @ 852:4d4c62d95b9c

New release
author Adam Chlipala <adamc@hcoop.net>
date Tue, 23 Jun 2009 12:53:47 -0400
parents d18f6f0bcf60
children 19fdeef40ada
rev   line source
adamc@524 1 \documentclass{article}
adamc@554 2 \usepackage{fullpage,amsmath,amssymb,proof,url}
adamc@524 3
adamc@524 4 \newcommand{\cd}[1]{\texttt{#1}}
adamc@524 5 \newcommand{\mt}[1]{\mathsf{#1}}
adamc@524 6
adamc@524 7 \newcommand{\rc}{+ \hspace{-.075in} + \;}
adamc@527 8 \newcommand{\rcut}{\; \texttt{--} \;}
adamc@527 9 \newcommand{\rcutM}{\; \texttt{---} \;}
adamc@524 10
adamc@524 11 \begin{document}
adamc@524 12
adamc@524 13 \title{The Ur/Web Manual}
adamc@524 14 \author{Adam Chlipala}
adamc@524 15
adamc@524 16 \maketitle
adamc@524 17
adamc@540 18 \tableofcontents
adamc@540 19
adamc@554 20
adamc@554 21 \section{Introduction}
adamc@554 22
adamc@554 23 \emph{Ur} is a programming language designed to introduce richer type system features into functional programming in the tradition of ML and Haskell. Ur is functional, pure, statically-typed, and strict. Ur supports a powerful kind of \emph{metaprogramming} based on \emph{row types}.
adamc@554 24
adamc@554 25 \emph{Ur/Web} is Ur plus a special standard library and associated rules for parsing and optimization. Ur/Web supports construction of dynamic web applications backed by SQL databases. The signature of the standard library is such that well-typed Ur/Web programs ``don't go wrong'' in a very broad sense. Not only do they not crash during particular page generations, but they also may not:
adamc@554 26
adamc@554 27 \begin{itemize}
adamc@554 28 \item Suffer from any kinds of code-injection attacks
adamc@554 29 \item Return invalid HTML
adamc@554 30 \item Contain dead intra-application links
adamc@554 31 \item Have mismatches between HTML forms and the fields expected by their handlers
adamc@652 32 \item Include client-side code that makes incorrect assumptions about the ``AJAX''-style services that the remote web server provides
adamc@554 33 \item Attempt invalid SQL queries
adamc@652 34 \item Use improper marshaling or unmarshaling in communication with SQL databases or between browsers and web servers
adamc@554 35 \end{itemize}
adamc@554 36
adamc@554 37 This type safety is just the foundation of the Ur/Web methodology. It is also possible to use metaprogramming to build significant application pieces by analysis of type structure. For instance, the demo includes an ML-style functor for building an admin interface for an arbitrary SQL table. The type system guarantees that the admin interface sub-application that comes out will always be free of the above-listed bugs, no matter which well-typed table description is given as input.
adamc@554 38
adamc@652 39 The Ur/Web compiler also produces very efficient object code that does not use garbage collection. These compiled programs will often be even more efficient than what most programmers would bother to write in C. The compiler also generates JavaScript versions of client-side code, with no need to write those parts of applications in a different language.
adamc@554 40
adamc@554 41 \medskip
adamc@554 42
adamc@554 43 The official web site for Ur is:
adamc@554 44 \begin{center}
adamc@554 45 \url{http://www.impredicative.com/ur/}
adamc@554 46 \end{center}
adamc@554 47
adamc@555 48
adamc@555 49 \section{Installation}
adamc@555 50
adamc@555 51 If you are lucky, then the following standard command sequence will suffice for installation, in a directory to which you have unpacked the latest distribution tarball.
adamc@555 52
adamc@555 53 \begin{verbatim}
adamc@555 54 ./configure
adamc@555 55 make
adamc@555 56 sudo make install
adamc@555 57 \end{verbatim}
adamc@555 58
adamc@783 59 Some other packages must be installed for the above to work. At a minimum, you need a standard UNIX shell, with standard UNIX tools like sed and GCC in your execution path; MLton, the whole-program optimizing compiler for Standard ML; and the mhash C library. To build programs that access SQL databases, you also need libpq, the PostgreSQL client library. As of this writing, in the ``testing'' version of Debian Linux, this command will install the more uncommon of these dependencies:
adamc@555 60
adamc@555 61 \begin{verbatim}
adamc@783 62 apt-get install mlton libmhash-dev libpq-dev
adamc@555 63 \end{verbatim}
adamc@555 64
adamc@555 65 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 66
adamc@555 67 \begin{verbatim}
adamc@555 68 apt-get install smlnj libsmlnj-smlnj ml-yacc ml-lpt
adamc@555 69 \end{verbatim}
adamc@555 70
adamc@555 71 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 72
adamc@555 73 To run an SQL-backed application, you will probably want to install the PostgreSQL server. Version 8.3 or higher is required.
adamc@555 74
adamc@555 75 \begin{verbatim}
adamc@555 76 apt-get install postgresql-8.3
adamc@555 77 \end{verbatim}
adamc@555 78
adamc@555 79 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 80
adamc@555 81 \begin{verbatim}
adamc@555 82 apt-get install emacs-goodies-el
adamc@555 83 \end{verbatim}
adamc@555 84
adamc@555 85 Even with the right packages installed, configuration and building might fail to work. After you run \texttt{./configure}, you will see the values of some named environment variables printed. You may need to adjust these values to get proper installation for your system. To change a value, store your preferred alternative in the corresponding UNIX environment variable, before running \texttt{./configure}. For instance, here is how to change the list of extra arguments that the Ur/Web compiler will pass to GCC on every invocation.
adamc@555 86
adamc@555 87 \begin{verbatim}
adamc@555 88 GCCARGS=-fnested-functions ./configure
adamc@555 89 \end{verbatim}
adamc@555 90
adamc@555 91 Some OSX users have reported needing to use this particular GCCARGS value.
adamc@555 92
adamc@555 93 The Emacs mode can be set to autoload by adding the following to your \texttt{.emacs} file.
adamc@555 94
adamc@555 95 \begin{verbatim}
adamc@555 96 (add-to-list 'load-path "/usr/local/share/emacs/site-lisp/urweb-mode")
adamc@555 97 (load "urweb-mode-startup")
adamc@555 98 \end{verbatim}
adamc@555 99
adamc@555 100 Change the path in the first line if you chose a different Emacs installation path during configuration.
adamc@555 101
adamc@555 102
adamc@556 103 \section{Command-Line Compiler}
adamc@556 104
adamc@556 105 \subsection{Project Files}
adamc@556 106
adamc@556 107 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 108
adamc@556 109 \begin{verbatim}
adamc@556 110 database dbname=test
adamc@556 111 sql crud1.sql
adamc@556 112
adamc@556 113 crud
adamc@556 114 crud1
adamc@556 115 \end{verbatim}
adamc@556 116
adamc@556 117 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 118
adamc@556 119 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 120
adamc@556 121 \begin{verbatim}
adamc@556 122 createdb test
adamc@556 123 psql -f crud1.sql test
adamc@556 124 \end{verbatim}
adamc@556 125
adamc@556 126 A blank line always separates the named directives from a list of modules to include in the project; if there are no named directives, a blank line must begin the file.
adamc@556 127
adamc@556 128 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 129
adamc@783 130 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 131 \begin{itemize}
adamc@783 132 \item \texttt{[allow|deny] [url|mime] PATTERN} registers a rule governing which URLs or MIME types are allowed in this application. The first such rule to match a URL or MIME type determines the verdict. If \texttt{PATTERN} ends in \texttt{*}, it is interpreted as a prefix rule. Otherwise, a string must match it exactly.
adamc@783 133 \item \texttt{clientOnly Module.ident} registers an FFI function or transaction that may only be run in client browsers.
adamc@783 134 \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 135 \item \texttt{database DBSTRING} sets the string to pass to libpq to open a database connection.
adamc@783 136 \item \texttt{debug} saves some intermediate C files, which is mostly useful to help in debugging the compiler itself.
adamc@783 137 \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 138 \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 139 \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@783 140 \item \texttt{jsFunc Module.ident=name} gives the JavaScript name of an FFI value.
adamc@783 141 \item \texttt{library FILENAME} parses \texttt{FILENAME.urp} and merges its contents with the rest of the current file's contents.
adamc@783 142 \item \texttt{link FILENAME} adds \texttt{FILENAME} to the list of files to be passed to the GCC linker at the end of compilation. This is most useful for importing extra libraries needed by new FFI modules.
adamc@852 143 \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 144 \item \texttt{prefix PREFIX} sets the prefix included before every URI within the generated application. The default is \texttt{/}.
adamc@783 145 \item \texttt{profile} generates an executable that may be used with gprof.
adamc@783 146 \item \texttt{rewrite KIND FROM TO} gives a rule for rewriting canonical module paths. For instance, the canonical path of a page may be \texttt{Mod1.Mod2.mypage}, while you would rather the page were accessed via a URL containing only \texttt{page}. The directive \texttt{rewrite url Mod1/Mod2/mypage page} would accomplish that. The possible values of \texttt{KIND} determine which kinds of objects are affected. The kind \texttt{all} matches any object, and \texttt{url} matches page URLs. The kinds \texttt{table}, \texttt{sequence}, and \texttt{view} match those sorts of SQL entities, and \texttt{relation} matches any of those three. \texttt{cookie} matches HTTP cookies, and \texttt{style} matches CSS class names. If \texttt{FROM} ends in \texttt{/*}, it is interpreted as a prefix matching rule, and rewriting occurs by replacing only the appropriate prefix of a path with \texttt{TO}. While the actual external names of relations and styles have parts separated by underscores instead of slashes, all rewrite rules must be written in terms of slashes.
adamc@783 147 \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 148 \item \texttt{serverOnly Module.ident} registers an FFI function or transaction that may only be run on the server.
adamc@783 149 \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 150 \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 151 \end{itemize}
adamc@701 152
adamc@701 153
adamc@557 154 \subsection{Building an Application}
adamc@557 155
adamc@557 156 To compile project \texttt{P.urp}, simply run
adamc@557 157 \begin{verbatim}
adamc@557 158 urweb P
adamc@557 159 \end{verbatim}
adamc@558 160 The output executable is a standalone web server. Run it with the command-line argument \texttt{-h} to see which options it takes. If the project file lists a database, the web server will attempt to connect to that database on startup.
adamc@557 161
adamc@557 162 To time how long the different compiler phases run, without generating an executable, run
adamc@557 163 \begin{verbatim}
adamc@557 164 urweb -timing P
adamc@557 165 \end{verbatim}
adamc@557 166
adamc@556 167
adamc@529 168 \section{Ur Syntax}
adamc@529 169
adamc@784 170 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 171
adamc@524 172 \subsection{Lexical Conventions}
adamc@524 173
adamc@524 174 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 175
adamc@524 176 \begin{center}
adamc@524 177 \begin{tabular}{rl}
adamc@524 178 \textbf{\LaTeX} & \textbf{ASCII} \\
adamc@524 179 $\to$ & \cd{->} \\
adamc@652 180 $\longrightarrow$ & \cd{-->} \\
adamc@524 181 $\times$ & \cd{*} \\
adamc@524 182 $\lambda$ & \cd{fn} \\
adamc@524 183 $\Rightarrow$ & \cd{=>} \\
adamc@652 184 $\Longrightarrow$ & \cd{==>} \\
adamc@529 185 $\neq$ & \cd{<>} \\
adamc@529 186 $\leq$ & \cd{<=} \\
adamc@529 187 $\geq$ & \cd{>=} \\
adamc@524 188 \\
adamc@524 189 $x$ & Normal textual identifier, not beginning with an uppercase letter \\
adamc@525 190 $X$ & Normal textual identifier, beginning with an uppercase letter \\
adamc@524 191 \end{tabular}
adamc@524 192 \end{center}
adamc@524 193
adamc@525 194 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 195
adamc@526 196 We write $\ell$ for literals of the primitive types, for the most part following C conventions. There are $\mt{int}$, $\mt{float}$, and $\mt{string}$ literals.
adamc@526 197
adamc@527 198 This version of the manual doesn't include operator precedences; see \texttt{src/urweb.grm} for that.
adamc@527 199
adamc@552 200 \subsection{\label{core}Core Syntax}
adamc@524 201
adamc@524 202 \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 203 $$\begin{array}{rrcll}
adamc@524 204 \textrm{Kinds} & \kappa &::=& \mt{Type} & \textrm{proper types} \\
adamc@525 205 &&& \mt{Unit} & \textrm{the trivial constructor} \\
adamc@525 206 &&& \mt{Name} & \textrm{field names} \\
adamc@525 207 &&& \kappa \to \kappa & \textrm{type-level functions} \\
adamc@525 208 &&& \{\kappa\} & \textrm{type-level records} \\
adamc@525 209 &&& (\kappa\times^+) & \textrm{type-level tuples} \\
adamc@652 210 &&& X & \textrm{variable} \\
adamc@652 211 &&& X \longrightarrow k & \textrm{kind-polymorphic type-level function} \\
adamc@529 212 &&& \_\_ & \textrm{wildcard} \\
adamc@525 213 &&& (\kappa) & \textrm{explicit precedence} \\
adamc@524 214 \end{array}$$
adamc@524 215
adamc@524 216 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 217 $$\begin{array}{rrcll}
adamc@524 218 \textrm{Explicitness} & ? &::=& :: & \textrm{explicit} \\
adamc@558 219 &&& ::: & \textrm{implicit}
adamc@524 220 \end{array}$$
adamc@524 221
adamc@524 222 \emph{Constructors} are the main class of compile-time-only data. They include proper types and are classified by kinds.
adamc@524 223 $$\begin{array}{rrcll}
adamc@524 224 \textrm{Constructors} & c, \tau &::=& (c) :: \kappa & \textrm{kind annotation} \\
adamc@530 225 &&& \hat{x} & \textrm{constructor variable} \\
adamc@524 226 \\
adamc@525 227 &&& \tau \to \tau & \textrm{function type} \\
adamc@525 228 &&& x \; ? \; \kappa \to \tau & \textrm{polymorphic function type} \\
adamc@652 229 &&& X \longrightarrow \tau & \textrm{kind-polymorphic function type} \\
adamc@525 230 &&& \$ c & \textrm{record type} \\
adamc@524 231 \\
adamc@525 232 &&& c \; c & \textrm{type-level function application} \\
adamc@530 233 &&& \lambda x \; :: \; \kappa \Rightarrow c & \textrm{type-level function abstraction} \\
adamc@524 234 \\
adamc@652 235 &&& X \Longrightarrow c & \textrm{type-level kind-polymorphic function abstraction} \\
adamc@655 236 &&& c [\kappa] & \textrm{type-level kind-polymorphic function application} \\
adamc@652 237 \\
adamc@525 238 &&& () & \textrm{type-level unit} \\
adamc@525 239 &&& \#X & \textrm{field name} \\
adamc@524 240 \\
adamc@525 241 &&& [(c = c)^*] & \textrm{known-length type-level record} \\
adamc@525 242 &&& c \rc c & \textrm{type-level record concatenation} \\
adamc@652 243 &&& \mt{map} & \textrm{type-level record map} \\
adamc@524 244 \\
adamc@558 245 &&& (c,^+) & \textrm{type-level tuple} \\
adamc@525 246 &&& c.n & \textrm{type-level tuple projection ($n \in \mathbb N^+$)} \\
adamc@524 247 \\
adamc@652 248 &&& [c \sim c] \Rightarrow \tau & \textrm{guarded type} \\
adamc@524 249 \\
adamc@529 250 &&& \_ :: \kappa & \textrm{wildcard} \\
adamc@525 251 &&& (c) & \textrm{explicit precedence} \\
adamc@530 252 \\
adamc@530 253 \textrm{Qualified uncapitalized variables} & \hat{x} &::=& x & \textrm{not from a module} \\
adamc@530 254 &&& M.x & \textrm{projection from a module} \\
adamc@525 255 \end{array}$$
adamc@525 256
adamc@655 257 We include both abstraction and application for kind polymorphism, but applications are only inferred internally; they may not be written explicitly in source programs.
adamc@655 258
adamc@525 259 Modules of the module system are described by \emph{signatures}.
adamc@525 260 $$\begin{array}{rrcll}
adamc@525 261 \textrm{Signatures} & S &::=& \mt{sig} \; s^* \; \mt{end} & \textrm{constant} \\
adamc@525 262 &&& X & \textrm{variable} \\
adamc@525 263 &&& \mt{functor}(X : S) : S & \textrm{functor} \\
adamc@529 264 &&& S \; \mt{where} \; \mt{con} \; x = c & \textrm{concretizing an abstract constructor} \\
adamc@525 265 &&& M.X & \textrm{projection from a module} \\
adamc@525 266 \\
adamc@525 267 \textrm{Signature items} & s &::=& \mt{con} \; x :: \kappa & \textrm{abstract constructor} \\
adamc@525 268 &&& \mt{con} \; x :: \kappa = c & \textrm{concrete constructor} \\
adamc@528 269 &&& \mt{datatype} \; x \; x^* = dc\mid^+ & \textrm{algebraic datatype definition} \\
adamc@529 270 &&& \mt{datatype} \; x = \mt{datatype} \; M.x & \textrm{algebraic datatype import} \\
adamc@525 271 &&& \mt{val} \; x : \tau & \textrm{value} \\
adamc@525 272 &&& \mt{structure} \; X : S & \textrm{sub-module} \\
adamc@525 273 &&& \mt{signature} \; X = S & \textrm{sub-signature} \\
adamc@525 274 &&& \mt{include} \; S & \textrm{signature inclusion} \\
adamc@525 275 &&& \mt{constraint} \; c \sim c & \textrm{record disjointness constraint} \\
adamc@654 276 &&& \mt{class} \; x :: \kappa & \textrm{abstract constructor class} \\
adamc@654 277 &&& \mt{class} \; x :: \kappa = c & \textrm{concrete constructor class} \\
adamc@525 278 \\
adamc@525 279 \textrm{Datatype constructors} & dc &::=& X & \textrm{nullary constructor} \\
adamc@525 280 &&& X \; \mt{of} \; \tau & \textrm{unary constructor} \\
adamc@524 281 \end{array}$$
adamc@524 282
adamc@526 283 \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 284 $$\begin{array}{rrcll}
adamc@526 285 \textrm{Patterns} & p &::=& \_ & \textrm{wildcard} \\
adamc@526 286 &&& x & \textrm{variable} \\
adamc@526 287 &&& \ell & \textrm{constant} \\
adamc@526 288 &&& \hat{X} & \textrm{nullary constructor} \\
adamc@526 289 &&& \hat{X} \; p & \textrm{unary constructor} \\
adamc@526 290 &&& \{(x = p,)^*\} & \textrm{rigid record pattern} \\
adamc@526 291 &&& \{(x = p,)^+, \ldots\} & \textrm{flexible record pattern} \\
adamc@852 292 &&& p : \tau & \textrm{type annotation} \\
adamc@527 293 &&& (p) & \textrm{explicit precedence} \\
adamc@526 294 \\
adamc@529 295 \textrm{Qualified capitalized variables} & \hat{X} &::=& X & \textrm{not from a module} \\
adamc@526 296 &&& M.X & \textrm{projection from a module} \\
adamc@526 297 \end{array}$$
adamc@526 298
adamc@527 299 \emph{Expressions} are the main run-time entities, corresponding to both ``expressions'' and ``statements'' in mainstream imperative languages.
adamc@527 300 $$\begin{array}{rrcll}
adamc@527 301 \textrm{Expressions} & e &::=& e : \tau & \textrm{type annotation} \\
adamc@529 302 &&& \hat{x} & \textrm{variable} \\
adamc@529 303 &&& \hat{X} & \textrm{datatype constructor} \\
adamc@527 304 &&& \ell & \textrm{constant} \\
adamc@527 305 \\
adamc@527 306 &&& e \; e & \textrm{function application} \\
adamc@527 307 &&& \lambda x : \tau \Rightarrow e & \textrm{function abstraction} \\
adamc@527 308 &&& e [c] & \textrm{polymorphic function application} \\
adamc@852 309 &&& \lambda [x \; ? \; \kappa] \Rightarrow e & \textrm{polymorphic function abstraction} \\
adamc@655 310 &&& e [\kappa] & \textrm{kind-polymorphic function application} \\
adamc@652 311 &&& X \Longrightarrow e & \textrm{kind-polymorphic function abstraction} \\
adamc@527 312 \\
adamc@527 313 &&& \{(c = e,)^*\} & \textrm{known-length record} \\
adamc@527 314 &&& e.c & \textrm{record field projection} \\
adamc@527 315 &&& e \rc e & \textrm{record concatenation} \\
adamc@527 316 &&& e \rcut c & \textrm{removal of a single record field} \\
adamc@527 317 &&& e \rcutM c & \textrm{removal of multiple record fields} \\
adamc@527 318 \\
adamc@527 319 &&& \mt{let} \; ed^* \; \mt{in} \; e \; \mt{end} & \textrm{local definitions} \\
adamc@527 320 \\
adamc@527 321 &&& \mt{case} \; e \; \mt{of} \; (p \Rightarrow e|)^+ & \textrm{pattern matching} \\
adamc@527 322 \\
adamc@654 323 &&& \lambda [c \sim c] \Rightarrow e & \textrm{guarded expression abstraction} \\
adamc@654 324 &&& e \; ! & \textrm{guarded expression application} \\
adamc@527 325 \\
adamc@527 326 &&& \_ & \textrm{wildcard} \\
adamc@527 327 &&& (e) & \textrm{explicit precedence} \\
adamc@527 328 \\
adamc@527 329 \textrm{Local declarations} & ed &::=& \cd{val} \; x : \tau = e & \textrm{non-recursive value} \\
adamc@527 330 &&& \cd{val} \; \cd{rec} \; (x : \tau = e \; \cd{and})^+ & \textrm{mutually-recursive values} \\
adamc@527 331 \end{array}$$
adamc@527 332
adamc@655 333 As with constructors, we include both abstraction and application for kind polymorphism, but applications are only inferred internally.
adamc@655 334
adamc@528 335 \emph{Declarations} primarily bring new symbols into context.
adamc@528 336 $$\begin{array}{rrcll}
adamc@528 337 \textrm{Declarations} & d &::=& \mt{con} \; x :: \kappa = c & \textrm{constructor synonym} \\
adamc@528 338 &&& \mt{datatype} \; x \; x^* = dc\mid^+ & \textrm{algebraic datatype definition} \\
adamc@529 339 &&& \mt{datatype} \; x = \mt{datatype} \; M.x & \textrm{algebraic datatype import} \\
adamc@528 340 &&& \mt{val} \; x : \tau = e & \textrm{value} \\
adamc@528 341 &&& \mt{val} \; \cd{rec} \; (x : \tau = e \; \mt{and})^+ & \textrm{mutually-recursive values} \\
adamc@528 342 &&& \mt{structure} \; X : S = M & \textrm{module definition} \\
adamc@528 343 &&& \mt{signature} \; X = S & \textrm{signature definition} \\
adamc@528 344 &&& \mt{open} \; M & \textrm{module inclusion} \\
adamc@528 345 &&& \mt{constraint} \; c \sim c & \textrm{record disjointness constraint} \\
adamc@528 346 &&& \mt{open} \; \mt{constraints} \; M & \textrm{inclusion of just the constraints from a module} \\
adamc@528 347 &&& \mt{table} \; x : c & \textrm{SQL table} \\
adamc@784 348 &&& \mt{view} \; x : c & \textrm{SQL view} \\
adamc@528 349 &&& \mt{sequence} \; x & \textrm{SQL sequence} \\
adamc@535 350 &&& \mt{cookie} \; x : \tau & \textrm{HTTP cookie} \\
adamc@784 351 &&& \mt{style} \; x : \tau & \textrm{CSS class} \\
adamc@654 352 &&& \mt{class} \; x :: \kappa = c & \textrm{concrete constructor class} \\
adamc@528 353 \\
adamc@529 354 \textrm{Modules} & M &::=& \mt{struct} \; d^* \; \mt{end} & \textrm{constant} \\
adamc@529 355 &&& X & \textrm{variable} \\
adamc@529 356 &&& M.X & \textrm{projection} \\
adamc@529 357 &&& M(M) & \textrm{functor application} \\
adamc@529 358 &&& \mt{functor}(X : S) : S = M & \textrm{functor abstraction} \\
adamc@528 359 \end{array}$$
adamc@528 360
adamc@528 361 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 362
adamc@784 363 We omit some extra possibilities in $\mt{table}$ syntax, deferring them to Section \ref{tables}.
adamc@784 364
adamc@529 365 \subsection{Shorthands}
adamc@529 366
adamc@529 367 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 368
adamc@529 369 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 370
adamc@529 371 A record type may be written $\{(c = c,)^*\}$, which elaborates to $\$[(c = c,)^*]$.
adamc@529 372
adamc@533 373 The notation $[c_1, \ldots, c_n]$ is shorthand for $[c_1 = (), \ldots, c_n = ()]$.
adamc@533 374
adamc@529 375 A tuple type $(\tau_1, \ldots, \tau_n)$ expands to a record type $\{1 = \tau_1, \ldots, n = \tau_n\}$, with natural numbers as field names. A tuple pattern $(p_1, \ldots, p_n)$ expands to a rigid record pattern $\{1 = p_1, \ldots, n = p_n\}$. Positive natural numbers may be used in most places where field names would be allowed.
adamc@529 376
adamc@852 377 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 378
adamc@529 379 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 380
adamc@529 381 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 382
adamc@654 383 A signature item or declaration $\mt{class} \; x = \lambda y \Rightarrow c$ may be abbreviated $\mt{class} \; x \; y = c$.
adamc@529 384
adamc@654 385 Handling of implicit and explicit constructor arguments may be tweaked with some prefixes to variable references. An expression $@x$ is a version of $x$ where all implicit constructor arguments have been made explicit. An expression $@@x$ achieves the same effect, additionally halting automatic resolution of type class instances and automatic proving of disjointness constraints. The default is that any prefix of a variable's type consisting only of implicit polymorphism, type class instances, and disjointness obligations is resolved automatically, with the variable treated as having the type that starts after the last implicit element, with suitable unification variables substituted. The same syntax works for variables projected out of modules and for capitalized variables (datatype constructors).
adamc@529 386
adamc@852 387 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 388
adamc@852 389 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 390
adamc@852 391 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 392
adamc@529 393 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 394
adamc@852 395 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 396
adamc@529 397 A declaration $\mt{table} \; x : \{(c = c,)^*\}$ is elaborated into $\mt{table} \; x : [(c = c,)^*]$
adamc@529 398
adamc@529 399 The syntax $\mt{where} \; \mt{type}$ is an alternate form of $\mt{where} \; \mt{con}$.
adamc@529 400
adamc@529 401 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 402
adamc@529 403 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 404
adamc@784 405 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 406
adamc@530 407
adamc@530 408 \section{Static Semantics}
adamc@530 409
adamc@530 410 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 411
adamc@530 412 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 413 \begin{itemize}
adamc@655 414 \item $\Gamma \vdash \kappa$ expresses kind well-formedness.
adamc@530 415 \item $\Gamma \vdash c :: \kappa$ assigns a kind to a constructor in a context.
adamc@530 416 \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 417 \item $\Gamma \vdash c \hookrightarrow C$ proves that record constructor $c$ decomposes into set $C$ of field names and record constructors.
adamc@530 418 \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 419 \item $\Gamma \vdash e : \tau$ is a standard typing judgment.
adamc@534 420 \item $\Gamma \vdash p \leadsto \Gamma; \tau$ combines typing of patterns with calculation of which new variables they bind.
adamc@537 421 \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 422 \item $\Gamma \vdash S \equiv S$ is the signature equivalence judgment.
adamc@536 423 \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 424 \item $\Gamma \vdash M : S$ is the module signature checking judgment.
adamc@537 425 \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 426 \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 427 \end{itemize}
adamc@530 428
adamc@655 429
adamc@655 430 \subsection{Kind Well-Formedness}
adamc@655 431
adamc@655 432 $$\infer{\Gamma \vdash \mt{Type}}{}
adamc@655 433 \quad \infer{\Gamma \vdash \mt{Unit}}{}
adamc@655 434 \quad \infer{\Gamma \vdash \mt{Name}}{}
adamc@655 435 \quad \infer{\Gamma \vdash \kappa_1 \to \kappa_2}{
adamc@655 436 \Gamma \vdash \kappa_1
adamc@655 437 & \Gamma \vdash \kappa_2
adamc@655 438 }
adamc@655 439 \quad \infer{\Gamma \vdash \{\kappa\}}{
adamc@655 440 \Gamma \vdash \kappa
adamc@655 441 }
adamc@655 442 \quad \infer{\Gamma \vdash (\kappa_1 \times \ldots \times \kappa_n)}{
adamc@655 443 \forall i: \Gamma \vdash \kappa_i
adamc@655 444 }$$
adamc@655 445
adamc@655 446 $$\infer{\Gamma \vdash X}{
adamc@655 447 X \in \Gamma
adamc@655 448 }
adamc@655 449 \quad \infer{\Gamma \vdash X \longrightarrow \kappa}{
adamc@655 450 \Gamma, X \vdash \kappa
adamc@655 451 }$$
adamc@655 452
adamc@530 453 \subsection{Kinding}
adamc@530 454
adamc@655 455 We write $[X \mapsto \kappa_1]\kappa_2$ for capture-avoiding substitution of $\kappa_1$ for $X$ in $\kappa_2$.
adamc@655 456
adamc@530 457 $$\infer{\Gamma \vdash (c) :: \kappa :: \kappa}{
adamc@530 458 \Gamma \vdash c :: \kappa
adamc@530 459 }
adamc@530 460 \quad \infer{\Gamma \vdash x :: \kappa}{
adamc@530 461 x :: \kappa \in \Gamma
adamc@530 462 }
adamc@530 463 \quad \infer{\Gamma \vdash x :: \kappa}{
adamc@530 464 x :: \kappa = c \in \Gamma
adamc@530 465 }$$
adamc@530 466
adamc@530 467 $$\infer{\Gamma \vdash M.x :: \kappa}{
adamc@537 468 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 469 & \mt{proj}(M, \overline{s}, \mt{con} \; x) = \kappa
adamc@530 470 }
adamc@530 471 \quad \infer{\Gamma \vdash M.x :: \kappa}{
adamc@537 472 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 473 & \mt{proj}(M, \overline{s}, \mt{con} \; x) = (\kappa, c)
adamc@530 474 }$$
adamc@530 475
adamc@530 476 $$\infer{\Gamma \vdash \tau_1 \to \tau_2 :: \mt{Type}}{
adamc@530 477 \Gamma \vdash \tau_1 :: \mt{Type}
adamc@530 478 & \Gamma \vdash \tau_2 :: \mt{Type}
adamc@530 479 }
adamc@530 480 \quad \infer{\Gamma \vdash x \; ? \: \kappa \to \tau :: \mt{Type}}{
adamc@530 481 \Gamma, x :: \kappa \vdash \tau :: \mt{Type}
adamc@530 482 }
adamc@655 483 \quad \infer{\Gamma \vdash X \longrightarrow \tau :: \mt{Type}}{
adamc@655 484 \Gamma, X \vdash \tau :: \mt{Type}
adamc@655 485 }
adamc@530 486 \quad \infer{\Gamma \vdash \$c :: \mt{Type}}{
adamc@530 487 \Gamma \vdash c :: \{\mt{Type}\}
adamc@530 488 }$$
adamc@530 489
adamc@530 490 $$\infer{\Gamma \vdash c_1 \; c_2 :: \kappa_2}{
adamc@530 491 \Gamma \vdash c_1 :: \kappa_1 \to \kappa_2
adamc@530 492 & \Gamma \vdash c_2 :: \kappa_1
adamc@530 493 }
adamc@530 494 \quad \infer{\Gamma \vdash \lambda x \; :: \; \kappa_1 \Rightarrow c :: \kappa_1 \to \kappa_2}{
adamc@530 495 \Gamma, x :: \kappa_1 \vdash c :: \kappa_2
adamc@530 496 }$$
adamc@530 497
adamc@655 498 $$\infer{\Gamma \vdash c[\kappa'] :: [X \mapsto \kappa']\kappa}{
adamc@655 499 \Gamma \vdash c :: X \to \kappa
adamc@655 500 & \Gamma \vdash \kappa'
adamc@655 501 }
adamc@655 502 \quad \infer{\Gamma \vdash X \Longrightarrow c :: X \to \kappa}{
adamc@655 503 \Gamma, X \vdash c :: \kappa
adamc@655 504 }$$
adamc@655 505
adamc@530 506 $$\infer{\Gamma \vdash () :: \mt{Unit}}{}
adamc@530 507 \quad \infer{\Gamma \vdash \#X :: \mt{Name}}{}$$
adamc@530 508
adamc@530 509 $$\infer{\Gamma \vdash [\overline{c_i = c'_i}] :: \{\kappa\}}{
adamc@530 510 \forall i: \Gamma \vdash c_i : \mt{Name}
adamc@530 511 & \Gamma \vdash c'_i :: \kappa
adamc@530 512 & \forall i \neq j: \Gamma \vdash c_i \sim c_j
adamc@530 513 }
adamc@530 514 \quad \infer{\Gamma \vdash c_1 \rc c_2 :: \{\kappa\}}{
adamc@530 515 \Gamma \vdash c_1 :: \{\kappa\}
adamc@530 516 & \Gamma \vdash c_2 :: \{\kappa\}
adamc@530 517 & \Gamma \vdash c_1 \sim c_2
adamc@530 518 }$$
adamc@530 519
adamc@655 520 $$\infer{\Gamma \vdash \mt{map} :: (\kappa_1 \to \kappa_2) \to \{\kappa_1\} \to \{\kappa_2\}}{}$$
adamc@530 521
adamc@573 522 $$\infer{\Gamma \vdash (\overline c) :: (\kappa_1 \times \ldots \times \kappa_n)}{
adamc@573 523 \forall i: \Gamma \vdash c_i :: \kappa_i
adamc@530 524 }
adamc@573 525 \quad \infer{\Gamma \vdash c.i :: \kappa_i}{
adamc@573 526 \Gamma \vdash c :: (\kappa_1 \times \ldots \times \kappa_n)
adamc@530 527 }$$
adamc@530 528
adamc@655 529 $$\infer{\Gamma \vdash \lambda [c_1 \sim c_2] \Rightarrow \tau :: \mt{Type}}{
adamc@655 530 \Gamma \vdash c_1 :: \{\kappa\}
adamc@530 531 & \Gamma \vdash c_2 :: \{\kappa'\}
adamc@655 532 & \Gamma, c_1 \sim c_2 \vdash \tau :: \mt{Type}
adamc@530 533 }$$
adamc@530 534
adamc@531 535 \subsection{Record Disjointness}
adamc@531 536
adamc@531 537 $$\infer{\Gamma \vdash c_1 \sim c_2}{
adamc@558 538 \Gamma \vdash c_1 \hookrightarrow C_1
adamc@558 539 & \Gamma \vdash c_2 \hookrightarrow C_2
adamc@558 540 & \forall c'_1 \in C_1, c'_2 \in C_2: \Gamma \vdash c'_1 \sim c'_2
adamc@531 541 }
adamc@531 542 \quad \infer{\Gamma \vdash X \sim X'}{
adamc@531 543 X \neq X'
adamc@531 544 }$$
adamc@531 545
adamc@531 546 $$\infer{\Gamma \vdash c_1 \sim c_2}{
adamc@531 547 c'_1 \sim c'_2 \in \Gamma
adamc@558 548 & \Gamma \vdash c'_1 \hookrightarrow C_1
adamc@558 549 & \Gamma \vdash c'_2 \hookrightarrow C_2
adamc@558 550 & c_1 \in C_1
adamc@558 551 & c_2 \in C_2
adamc@531 552 }$$
adamc@531 553
adamc@531 554 $$\infer{\Gamma \vdash c \hookrightarrow \{c\}}{}
adamc@531 555 \quad \infer{\Gamma \vdash [\overline{c = c'}] \hookrightarrow \{\overline{c}\}}{}
adamc@531 556 \quad \infer{\Gamma \vdash c_1 \rc c_2 \hookrightarrow C_1 \cup C_2}{
adamc@531 557 \Gamma \vdash c_1 \hookrightarrow C_1
adamc@531 558 & \Gamma \vdash c_2 \hookrightarrow C_2
adamc@531 559 }
adamc@531 560 \quad \infer{\Gamma \vdash c \hookrightarrow C}{
adamc@531 561 \Gamma \vdash c \equiv c'
adamc@531 562 & \Gamma \vdash c' \hookrightarrow C
adamc@531 563 }
adamc@531 564 \quad \infer{\Gamma \vdash \mt{map} \; f \; c \hookrightarrow C}{
adamc@531 565 \Gamma \vdash c \hookrightarrow C
adamc@531 566 }$$
adamc@531 567
adamc@541 568 \subsection{\label{definitional}Definitional Equality}
adamc@532 569
adamc@655 570 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 571
adamc@532 572 $$\infer{\Gamma \vdash c \equiv c}{}
adamc@532 573 \quad \infer{\Gamma \vdash c_1 \equiv c_2}{
adamc@532 574 \Gamma \vdash c_2 \equiv c_1
adamc@532 575 }
adamc@532 576 \quad \infer{\Gamma \vdash c_1 \equiv c_3}{
adamc@532 577 \Gamma \vdash c_1 \equiv c_2
adamc@532 578 & \Gamma \vdash c_2 \equiv c_3
adamc@532 579 }
adamc@532 580 \quad \infer{\Gamma \vdash \mathcal C[c_1] \equiv \mathcal C[c_2]}{
adamc@532 581 \Gamma \vdash c_1 \equiv c_2
adamc@532 582 }$$
adamc@532 583
adamc@532 584 $$\infer{\Gamma \vdash x \equiv c}{
adamc@532 585 x :: \kappa = c \in \Gamma
adamc@532 586 }
adamc@532 587 \quad \infer{\Gamma \vdash M.x \equiv c}{
adamc@537 588 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 589 & \mt{proj}(M, \overline{s}, \mt{con} \; x) = (\kappa, c)
adamc@532 590 }
adamc@532 591 \quad \infer{\Gamma \vdash (\overline c).i \equiv c_i}{}$$
adamc@532 592
adamc@532 593 $$\infer{\Gamma \vdash (\lambda x :: \kappa \Rightarrow c) \; c' \equiv [x \mapsto c'] c}{}
adamc@655 594 \quad \infer{\Gamma \vdash (X \Longrightarrow c) [\kappa] \equiv [X \mapsto \kappa] c}{}$$
adamc@655 595
adamc@655 596 $$\infer{\Gamma \vdash c_1 \rc c_2 \equiv c_2 \rc c_1}{}
adamc@532 597 \quad \infer{\Gamma \vdash c_1 \rc (c_2 \rc c_3) \equiv (c_1 \rc c_2) \rc c_3}{}$$
adamc@532 598
adamc@532 599 $$\infer{\Gamma \vdash [] \rc c \equiv c}{}
adamc@532 600 \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 601
adamc@655 602 $$\infer{\Gamma \vdash \mt{map} \; f \; [] \equiv []}{}
adamc@655 603 \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 604
adamc@532 605 $$\infer{\Gamma \vdash \mt{map} \; (\lambda x \Rightarrow x) \; c \equiv c}{}
adamc@655 606 \quad \infer{\Gamma \vdash \mt{map} \; f \; (\mt{map} \; f' \; c)
adamc@655 607 \equiv \mt{map} \; (\lambda x \Rightarrow f \; (f' \; x)) \; c}{}$$
adamc@532 608
adamc@532 609 $$\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 610
adamc@534 611 \subsection{Expression Typing}
adamc@533 612
adamc@533 613 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}$, and string constants to $\mt{Basis}.\mt{string}$.
adamc@533 614
adamc@533 615 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 616
adamc@533 617 $$\infer{\Gamma \vdash e : \tau : \tau}{
adamc@533 618 \Gamma \vdash e : \tau
adamc@533 619 }
adamc@533 620 \quad \infer{\Gamma \vdash e : \tau}{
adamc@533 621 \Gamma \vdash e : \tau'
adamc@533 622 & \Gamma \vdash \tau' \equiv \tau
adamc@533 623 }
adamc@533 624 \quad \infer{\Gamma \vdash \ell : T(\ell)}{}$$
adamc@533 625
adamc@533 626 $$\infer{\Gamma \vdash x : \mathcal I(\tau)}{
adamc@533 627 x : \tau \in \Gamma
adamc@533 628 }
adamc@533 629 \quad \infer{\Gamma \vdash M.x : \mathcal I(\tau)}{
adamc@537 630 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 631 & \mt{proj}(M, \overline{s}, \mt{val} \; x) = \tau
adamc@533 632 }
adamc@533 633 \quad \infer{\Gamma \vdash X : \mathcal I(\tau)}{
adamc@533 634 X : \tau \in \Gamma
adamc@533 635 }
adamc@533 636 \quad \infer{\Gamma \vdash M.X : \mathcal I(\tau)}{
adamc@537 637 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 638 & \mt{proj}(M, \overline{s}, \mt{val} \; X) = \tau
adamc@533 639 }$$
adamc@533 640
adamc@533 641 $$\infer{\Gamma \vdash e_1 \; e_2 : \tau_2}{
adamc@533 642 \Gamma \vdash e_1 : \tau_1 \to \tau_2
adamc@533 643 & \Gamma \vdash e_2 : \tau_1
adamc@533 644 }
adamc@533 645 \quad \infer{\Gamma \vdash \lambda x : \tau_1 \Rightarrow e : \tau_1 \to \tau_2}{
adamc@533 646 \Gamma, x : \tau_1 \vdash e : \tau_2
adamc@533 647 }$$
adamc@533 648
adamc@533 649 $$\infer{\Gamma \vdash e [c] : [x \mapsto c]\tau}{
adamc@533 650 \Gamma \vdash e : x :: \kappa \to \tau
adamc@533 651 & \Gamma \vdash c :: \kappa
adamc@533 652 }
adamc@852 653 \quad \infer{\Gamma \vdash \lambda [x \; ? \; \kappa] \Rightarrow e : x \; ? \; \kappa \to \tau}{
adamc@533 654 \Gamma, x :: \kappa \vdash e : \tau
adamc@533 655 }$$
adamc@533 656
adamc@655 657 $$\infer{\Gamma \vdash e [\kappa] : [X \mapsto \kappa]\tau}{
adamc@655 658 \Gamma \vdash e : X \longrightarrow \tau
adamc@655 659 & \Gamma \vdash \kappa
adamc@655 660 }
adamc@655 661 \quad \infer{\Gamma \vdash X \Longrightarrow e : X \longrightarrow \tau}{
adamc@655 662 \Gamma, X \vdash e : \tau
adamc@655 663 }$$
adamc@655 664
adamc@533 665 $$\infer{\Gamma \vdash \{\overline{c = e}\} : \{\overline{c : \tau}\}}{
adamc@533 666 \forall i: \Gamma \vdash c_i :: \mt{Name}
adamc@533 667 & \Gamma \vdash e_i : \tau_i
adamc@533 668 & \forall i \neq j: \Gamma \vdash c_i \sim c_j
adamc@533 669 }
adamc@533 670 \quad \infer{\Gamma \vdash e.c : \tau}{
adamc@533 671 \Gamma \vdash e : \$([c = \tau] \rc c')
adamc@533 672 }
adamc@533 673 \quad \infer{\Gamma \vdash e_1 \rc e_2 : \$(c_1 \rc c_2)}{
adamc@533 674 \Gamma \vdash e_1 : \$c_1
adamc@533 675 & \Gamma \vdash e_2 : \$c_2
adamc@573 676 & \Gamma \vdash c_1 \sim c_2
adamc@533 677 }$$
adamc@533 678
adamc@533 679 $$\infer{\Gamma \vdash e \rcut c : \$c'}{
adamc@533 680 \Gamma \vdash e : \$([c = \tau] \rc c')
adamc@533 681 }
adamc@533 682 \quad \infer{\Gamma \vdash e \rcutM c : \$c'}{
adamc@533 683 \Gamma \vdash e : \$(c \rc c')
adamc@533 684 }$$
adamc@533 685
adamc@533 686 $$\infer{\Gamma \vdash \mt{let} \; \overline{ed} \; \mt{in} \; e \; \mt{end} : \tau}{
adamc@533 687 \Gamma \vdash \overline{ed} \leadsto \Gamma'
adamc@533 688 & \Gamma' \vdash e : \tau
adamc@533 689 }
adamc@533 690 \quad \infer{\Gamma \vdash \mt{case} \; e \; \mt{of} \; \overline{p \Rightarrow e} : \tau}{
adamc@533 691 \forall i: \Gamma \vdash p_i \leadsto \Gamma_i, \tau'
adamc@533 692 & \Gamma_i \vdash e_i : \tau
adamc@533 693 }$$
adamc@533 694
adamc@573 695 $$\infer{\Gamma \vdash \lambda [c_1 \sim c_2] \Rightarrow e : \lambda [c_1 \sim c_2] \Rightarrow \tau}{
adamc@533 696 \Gamma \vdash c_1 :: \{\kappa\}
adamc@655 697 & \Gamma \vdash c_2 :: \{\kappa'\}
adamc@533 698 & \Gamma, c_1 \sim c_2 \vdash e : \tau
adamc@662 699 }
adamc@662 700 \quad \infer{\Gamma \vdash e \; ! : \tau}{
adamc@662 701 \Gamma \vdash e : [c_1 \sim c_2] \Rightarrow \tau
adamc@662 702 & \Gamma \vdash c_1 \sim c_2
adamc@533 703 }$$
adamc@533 704
adamc@534 705 \subsection{Pattern Typing}
adamc@534 706
adamc@534 707 $$\infer{\Gamma \vdash \_ \leadsto \Gamma; \tau}{}
adamc@534 708 \quad \infer{\Gamma \vdash x \leadsto \Gamma, x : \tau; \tau}{}
adamc@534 709 \quad \infer{\Gamma \vdash \ell \leadsto \Gamma; T(\ell)}{}$$
adamc@534 710
adamc@534 711 $$\infer{\Gamma \vdash X \leadsto \Gamma; \overline{[x_i \mapsto \tau'_i]}\tau}{
adamc@534 712 X : \overline{x ::: \mt{Type}} \to \tau \in \Gamma
adamc@534 713 & \textrm{$\tau$ not a function type}
adamc@534 714 }
adamc@534 715 \quad \infer{\Gamma \vdash X \; p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau}{
adamc@534 716 X : \overline{x ::: \mt{Type}} \to \tau'' \to \tau \in \Gamma
adamc@534 717 & \Gamma \vdash p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau''
adamc@534 718 }$$
adamc@534 719
adamc@534 720 $$\infer{\Gamma \vdash M.X \leadsto \Gamma; \overline{[x_i \mapsto \tau'_i]}\tau}{
adamc@537 721 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 722 & \mt{proj}(M, \overline{s}, \mt{val} \; X) = \overline{x ::: \mt{Type}} \to \tau
adamc@534 723 & \textrm{$\tau$ not a function type}
adamc@534 724 }$$
adamc@534 725
adamc@534 726 $$\infer{\Gamma \vdash M.X \; p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau}{
adamc@537 727 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 728 & \mt{proj}(M, \overline{s}, \mt{val} \; X) = \overline{x ::: \mt{Type}} \to \tau'' \to \tau
adamc@534 729 & \Gamma \vdash p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau''
adamc@534 730 }$$
adamc@534 731
adamc@534 732 $$\infer{\Gamma \vdash \{\overline{x = p}\} \leadsto \Gamma_n; \{\overline{x = \tau}\}}{
adamc@534 733 \Gamma_0 = \Gamma
adamc@534 734 & \forall i: \Gamma_i \vdash p_i \leadsto \Gamma_{i+1}; \tau_i
adamc@534 735 }
adamc@534 736 \quad \infer{\Gamma \vdash \{\overline{x = p}, \ldots\} \leadsto \Gamma_n; \$([\overline{x = \tau}] \rc c)}{
adamc@534 737 \Gamma_0 = \Gamma
adamc@534 738 & \forall i: \Gamma_i \vdash p_i \leadsto \Gamma_{i+1}; \tau_i
adamc@534 739 }$$
adamc@534 740
adamc@852 741 $$\infer{\Gamma \vdash p : \tau \leadsto \Gamma'; \tau}{
adamc@852 742 \Gamma \vdash p \leadsto \Gamma'; \tau'
adamc@852 743 & \Gamma \vdash \tau' \equiv \tau
adamc@852 744 }$$
adamc@852 745
adamc@535 746 \subsection{Declaration Typing}
adamc@535 747
adamc@535 748 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 749
adamc@655 750 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 751
adamc@558 752 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 753 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 754
adamc@535 755 $$\infer{\Gamma \vdash \cdot \leadsto \Gamma}{}
adamc@535 756 \quad \infer{\Gamma \vdash d, \overline{d} \leadsto \Gamma''}{
adamc@535 757 \Gamma \vdash d \leadsto \Gamma'
adamc@535 758 & \Gamma' \vdash \overline{d} \leadsto \Gamma''
adamc@535 759 }$$
adamc@535 760
adamc@535 761 $$\infer{\Gamma \vdash \mt{con} \; x :: \kappa = c \leadsto \Gamma, x :: \kappa = c}{
adamc@535 762 \Gamma \vdash c :: \kappa
adamc@535 763 }
adamc@535 764 \quad \infer{\Gamma \vdash \mt{datatype} \; x \; \overline{y} = \overline{dc} \leadsto \Gamma'}{
adamc@535 765 \overline{y}; x; \Gamma, x :: \mt{Type}^{\mt{len}(\overline y)} \to \mt{Type} \vdash \overline{dc} \leadsto \Gamma'
adamc@535 766 }$$
adamc@535 767
adamc@535 768 $$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leadsto \Gamma'}{
adamc@537 769 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 770 & \mt{proj}(M, \overline{s}, \mt{datatype} \; z) = (\overline{y}, \overline{dc})
adamc@535 771 & \overline{y}; x; \Gamma, x :: \mt{Type}^{\mt{len}(\overline y)} \to \mt{Type} = M.z \vdash \overline{dc} \leadsto \Gamma'
adamc@535 772 }$$
adamc@535 773
adamc@535 774 $$\infer{\Gamma \vdash \mt{val} \; x : \tau = e \leadsto \Gamma, x : \tau}{
adamc@535 775 \Gamma \vdash e : \tau
adamc@535 776 }$$
adamc@535 777
adamc@535 778 $$\infer{\Gamma \vdash \mt{val} \; \mt{rec} \; \overline{x : \tau = e} \leadsto \Gamma, \overline{x : \tau}}{
adamc@535 779 \forall i: \Gamma, \overline{x : \tau} \vdash e_i : \tau_i
adamc@535 780 & \textrm{$e_i$ starts with an expression $\lambda$, optionally preceded by constructor and disjointness $\lambda$s}
adamc@535 781 }$$
adamc@535 782
adamc@535 783 $$\infer{\Gamma \vdash \mt{structure} \; X : S = M \leadsto \Gamma, X : S}{
adamc@535 784 \Gamma \vdash M : S
adamc@558 785 & \textrm{ $M$ not a constant or application}
adamc@535 786 }
adamc@558 787 \quad \infer{\Gamma \vdash \mt{structure} \; X : S = M \leadsto \Gamma, X : \mt{selfify}(X, \overline{s})}{
adamc@558 788 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@539 789 }$$
adamc@539 790
adamc@539 791 $$\infer{\Gamma \vdash \mt{signature} \; X = S \leadsto \Gamma, X = S}{
adamc@535 792 \Gamma \vdash S
adamc@535 793 }$$
adamc@535 794
adamc@537 795 $$\infer{\Gamma \vdash \mt{open} \; M \leadsto \Gamma, \mathcal O(M, \overline{s})}{
adamc@537 796 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@535 797 }$$
adamc@535 798
adamc@535 799 $$\infer{\Gamma \vdash \mt{constraint} \; c_1 \sim c_2 \leadsto \Gamma}{
adamc@535 800 \Gamma \vdash c_1 :: \{\kappa\}
adamc@535 801 & \Gamma \vdash c_2 :: \{\kappa\}
adamc@535 802 & \Gamma \vdash c_1 \sim c_2
adamc@535 803 }
adamc@537 804 \quad \infer{\Gamma \vdash \mt{open} \; \mt{constraints} \; M \leadsto \Gamma, \mathcal O_c(M, \overline{s})}{
adamc@537 805 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@535 806 }$$
adamc@535 807
adamc@784 808 $$\infer{\Gamma \vdash \mt{table} \; x : c \leadsto \Gamma, x : \mt{Basis}.\mt{sql\_table} \; c \; []}{
adamc@535 809 \Gamma \vdash c :: \{\mt{Type}\}
adamc@535 810 }
adamc@784 811 \quad \infer{\Gamma \vdash \mt{view} \; x : c \leadsto \Gamma, x : \mt{Basis}.\mt{sql\_view} \; c}{
adamc@784 812 \Gamma \vdash c :: \{\mt{Type}\}
adamc@784 813 }$$
adamc@784 814
adamc@784 815 $$\infer{\Gamma \vdash \mt{sequence} \; x \leadsto \Gamma, x : \mt{Basis}.\mt{sql\_sequence}}{}$$
adamc@535 816
adamc@535 817 $$\infer{\Gamma \vdash \mt{cookie} \; x : \tau \leadsto \Gamma, x : \mt{Basis}.\mt{http\_cookie} \; \tau}{
adamc@535 818 \Gamma \vdash \tau :: \mt{Type}
adamc@784 819 }
adamc@784 820 \quad \infer{\Gamma \vdash \mt{style} \; x \leadsto \Gamma, x : \mt{Basis}.\mt{css\_class}}{}$$
adamc@535 821
adamc@784 822 $$\infer{\Gamma \vdash \mt{class} \; x :: \kappa = c \leadsto \Gamma, x :: \kappa = c}{
adamc@784 823 \Gamma \vdash c :: \kappa
adamc@535 824 }$$
adamc@535 825
adamc@535 826 $$\infer{\overline{y}; x; \Gamma \vdash \cdot \leadsto \Gamma}{}
adamc@535 827 \quad \infer{\overline{y}; x; \Gamma \vdash X \mid \overline{dc} \leadsto \Gamma', X : \overline{y ::: \mt{Type}} \to x \; \overline{y}}{
adamc@535 828 \overline{y}; x; \Gamma \vdash \overline{dc} \leadsto \Gamma'
adamc@535 829 }
adamc@535 830 \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 831 \overline{y}; x; \Gamma \vdash \overline{dc} \leadsto \Gamma'
adamc@535 832 }$$
adamc@535 833
adamc@537 834 \subsection{Signature Item Typing}
adamc@537 835
adamc@537 836 We appeal to a signature item analogue of the $\mathcal O$ function from the last subsection.
adamc@537 837
adamc@537 838 $$\infer{\Gamma \vdash \cdot \leadsto \Gamma}{}
adamc@537 839 \quad \infer{\Gamma \vdash s, \overline{s} \leadsto \Gamma''}{
adamc@537 840 \Gamma \vdash s \leadsto \Gamma'
adamc@537 841 & \Gamma' \vdash \overline{s} \leadsto \Gamma''
adamc@537 842 }$$
adamc@537 843
adamc@537 844 $$\infer{\Gamma \vdash \mt{con} \; x :: \kappa \leadsto \Gamma, x :: \kappa}{}
adamc@537 845 \quad \infer{\Gamma \vdash \mt{con} \; x :: \kappa = c \leadsto \Gamma, x :: \kappa = c}{
adamc@537 846 \Gamma \vdash c :: \kappa
adamc@537 847 }
adamc@537 848 \quad \infer{\Gamma \vdash \mt{datatype} \; x \; \overline{y} = \overline{dc} \leadsto \Gamma'}{
adamc@537 849 \overline{y}; x; \Gamma, x :: \mt{Type}^{\mt{len}(\overline y)} \to \mt{Type} \vdash \overline{dc} \leadsto \Gamma'
adamc@537 850 }$$
adamc@537 851
adamc@537 852 $$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leadsto \Gamma'}{
adamc@537 853 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 854 & \mt{proj}(M, \overline{s}, \mt{datatype} \; z) = (\overline{y}, \overline{dc})
adamc@537 855 & \overline{y}; x; \Gamma, x :: \mt{Type}^{\mt{len}(\overline y)} \to \mt{Type} = M.z \vdash \overline{dc} \leadsto \Gamma'
adamc@537 856 }$$
adamc@537 857
adamc@537 858 $$\infer{\Gamma \vdash \mt{val} \; x : \tau \leadsto \Gamma, x : \tau}{
adamc@537 859 \Gamma \vdash \tau :: \mt{Type}
adamc@537 860 }$$
adamc@537 861
adamc@537 862 $$\infer{\Gamma \vdash \mt{structure} \; X : S \leadsto \Gamma, X : S}{
adamc@537 863 \Gamma \vdash S
adamc@537 864 }
adamc@537 865 \quad \infer{\Gamma \vdash \mt{signature} \; X = S \leadsto \Gamma, X = S}{
adamc@537 866 \Gamma \vdash S
adamc@537 867 }$$
adamc@537 868
adamc@537 869 $$\infer{\Gamma \vdash \mt{include} \; S \leadsto \Gamma, \mathcal O(\overline{s})}{
adamc@537 870 \Gamma \vdash S
adamc@537 871 & \Gamma \vdash S \equiv \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 872 }$$
adamc@537 873
adamc@537 874 $$\infer{\Gamma \vdash \mt{constraint} \; c_1 \sim c_2 \leadsto \Gamma, c_1 \sim c_2}{
adamc@537 875 \Gamma \vdash c_1 :: \{\kappa\}
adamc@537 876 & \Gamma \vdash c_2 :: \{\kappa\}
adamc@537 877 }$$
adamc@537 878
adamc@784 879 $$\infer{\Gamma \vdash \mt{class} \; x :: \kappa = c \leadsto \Gamma, x :: \kappa = c}{
adamc@784 880 \Gamma \vdash c :: \kappa
adamc@537 881 }
adamc@784 882 \quad \infer{\Gamma \vdash \mt{class} \; x :: \kappa \leadsto \Gamma, x :: \kappa}{}$$
adamc@537 883
adamc@536 884 \subsection{Signature Compatibility}
adamc@536 885
adamc@558 886 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 887
adamc@537 888 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 889
adamc@536 890 $$\infer{\Gamma \vdash S \equiv S}{}
adamc@536 891 \quad \infer{\Gamma \vdash S_1 \equiv S_2}{
adamc@536 892 \Gamma \vdash S_2 \equiv S_1
adamc@536 893 }
adamc@536 894 \quad \infer{\Gamma \vdash X \equiv S}{
adamc@536 895 X = S \in \Gamma
adamc@536 896 }
adamc@536 897 \quad \infer{\Gamma \vdash M.X \equiv S}{
adamc@537 898 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 899 & \mt{proj}(M, \overline{s}, \mt{signature} \; X) = S
adamc@536 900 }$$
adamc@536 901
adamc@536 902 $$\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 903 \Gamma \vdash S \equiv \mt{sig} \; \overline{s^1} \; \mt{con} \; x :: \kappa \; \overline{s_2} \; \mt{end}
adamc@536 904 & \Gamma \vdash c :: \kappa
adamc@537 905 }
adamc@537 906 \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 907 \Gamma \vdash S \equiv \mt{sig} \; \overline{s} \; \mt{end}
adamc@536 908 }$$
adamc@536 909
adamc@536 910 $$\infer{\Gamma \vdash S_1 \leq S_2}{
adamc@536 911 \Gamma \vdash S_1 \equiv S_2
adamc@536 912 }
adamc@536 913 \quad \infer{\Gamma \vdash \mt{sig} \; \overline{s} \; \mt{end} \leq \mt{sig} \; \mt{end}}{}
adamc@537 914 \quad \infer{\Gamma \vdash \mt{sig} \; \overline{s} \; \mt{end} \leq \mt{sig} \; s' \; \overline{s'} \; \mt{end}}{
adamc@537 915 \Gamma \vdash \overline{s} \leq s'
adamc@537 916 & \Gamma \vdash s' \leadsto \Gamma'
adamc@537 917 & \Gamma' \vdash \mt{sig} \; \overline{s} \; \mt{end} \leq \mt{sig} \; \overline{s'} \; \mt{end}
adamc@537 918 }$$
adamc@537 919
adamc@537 920 $$\infer{\Gamma \vdash s \; \overline{s} \leq s'}{
adamc@537 921 \Gamma \vdash s \leq s'
adamc@537 922 }
adamc@537 923 \quad \infer{\Gamma \vdash s \; \overline{s} \leq s'}{
adamc@537 924 \Gamma \vdash s \leadsto \Gamma'
adamc@537 925 & \Gamma' \vdash \overline{s} \leq s'
adamc@536 926 }$$
adamc@536 927
adamc@536 928 $$\infer{\Gamma \vdash \mt{functor} (X : S_1) : S_2 \leq \mt{functor} (X : S'_1) : S'_2}{
adamc@536 929 \Gamma \vdash S'_1 \leq S_1
adamc@536 930 & \Gamma, X : S'_1 \vdash S_2 \leq S'_2
adamc@536 931 }$$
adamc@536 932
adamc@537 933 $$\infer{\Gamma \vdash \mt{con} \; x :: \kappa \leq \mt{con} \; x :: \kappa}{}
adamc@537 934 \quad \infer{\Gamma \vdash \mt{con} \; x :: \kappa = c \leq \mt{con} \; x :: \kappa}{}
adamc@558 935 \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 936
adamc@537 937 $$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leq \mt{con} \; x :: \mt{Type}^{\mt{len}(y)} \to \mt{Type}}{
adamc@537 938 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 939 & \mt{proj}(M, \overline{s}, \mt{datatype} \; z) = (\overline{y}, \overline{dc})
adamc@537 940 }$$
adamc@537 941
adamc@784 942 $$\infer{\Gamma \vdash \mt{class} \; x :: \kappa \leq \mt{con} \; x :: \kappa}{}
adamc@784 943 \quad \infer{\Gamma \vdash \mt{class} \; x :: \kappa = c \leq \mt{con} \; x :: \kappa}{}$$
adamc@537 944
adamc@537 945 $$\infer{\Gamma \vdash \mt{con} \; x :: \kappa = c_1 \leq \mt{con} \; x :: \mt{\kappa} = c_2}{
adamc@537 946 \Gamma \vdash c_1 \equiv c_2
adamc@537 947 }
adamc@784 948 \quad \infer{\Gamma \vdash \mt{class} \; x :: \kappa = c_1 \leq \mt{con} \; x :: \kappa = c_2}{
adamc@537 949 \Gamma \vdash c_1 \equiv c_2
adamc@537 950 }$$
adamc@537 951
adamc@537 952 $$\infer{\Gamma \vdash \mt{datatype} \; x \; \overline{y} = \overline{dc} \leq \mt{datatype} \; x \; \overline{y} = \overline{dc'}}{
adamc@537 953 \Gamma, \overline{y :: \mt{Type}} \vdash \overline{dc} \leq \overline{dc'}
adamc@537 954 }$$
adamc@537 955
adamc@537 956 $$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leq \mt{datatype} \; x \; \overline{y} = \overline{dc'}}{
adamc@537 957 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 958 & \mt{proj}(M, \overline{s}, \mt{datatype} \; z) = (\overline{y}, \overline{dc})
adamc@537 959 & \Gamma, \overline{y :: \mt{Type}} \vdash \overline{dc} \leq \overline{dc'}
adamc@537 960 }$$
adamc@537 961
adamc@537 962 $$\infer{\Gamma \vdash \cdot \leq \cdot}{}
adamc@537 963 \quad \infer{\Gamma \vdash X; \overline{dc} \leq X; \overline{dc'}}{
adamc@537 964 \Gamma \vdash \overline{dc} \leq \overline{dc'}
adamc@537 965 }
adamc@537 966 \quad \infer{\Gamma \vdash X \; \mt{of} \; \tau_1; \overline{dc} \leq X \; \mt{of} \; \tau_2; \overline{dc'}}{
adamc@537 967 \Gamma \vdash \tau_1 \equiv \tau_2
adamc@537 968 & \Gamma \vdash \overline{dc} \leq \overline{dc'}
adamc@537 969 }$$
adamc@537 970
adamc@537 971 $$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leq \mt{datatype} \; x = \mt{datatype} \; M'.z'}{
adamc@537 972 \Gamma \vdash M.z \equiv M'.z'
adamc@537 973 }$$
adamc@537 974
adamc@537 975 $$\infer{\Gamma \vdash \mt{val} \; x : \tau_1 \leq \mt{val} \; x : \tau_2}{
adamc@537 976 \Gamma \vdash \tau_1 \equiv \tau_2
adamc@537 977 }
adamc@537 978 \quad \infer{\Gamma \vdash \mt{structure} \; X : S_1 \leq \mt{structure} \; X : S_2}{
adamc@537 979 \Gamma \vdash S_1 \leq S_2
adamc@537 980 }
adamc@537 981 \quad \infer{\Gamma \vdash \mt{signature} \; X = S_1 \leq \mt{signature} \; X = S_2}{
adamc@537 982 \Gamma \vdash S_1 \leq S_2
adamc@537 983 & \Gamma \vdash S_2 \leq S_1
adamc@537 984 }$$
adamc@537 985
adamc@537 986 $$\infer{\Gamma \vdash \mt{constraint} \; c_1 \sim c_2 \leq \mt{constraint} \; c'_1 \sim c'_2}{
adamc@537 987 \Gamma \vdash c_1 \equiv c'_1
adamc@537 988 & \Gamma \vdash c_2 \equiv c'_2
adamc@537 989 }$$
adamc@537 990
adamc@655 991 $$\infer{\Gamma \vdash \mt{class} \; x :: \kappa \leq \mt{class} \; x :: \kappa}{}
adamc@655 992 \quad \infer{\Gamma \vdash \mt{class} \; x :: \kappa = c \leq \mt{class} \; x :: \kappa}{}
adamc@655 993 \quad \infer{\Gamma \vdash \mt{class} \; x :: \kappa = c_1 \leq \mt{class} \; x :: \kappa = c_2}{
adamc@537 994 \Gamma \vdash c_1 \equiv c_2
adamc@537 995 }$$
adamc@537 996
adamc@538 997 \subsection{Module Typing}
adamc@538 998
adamc@538 999 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 1000
adamc@538 1001 $$\infer{\Gamma \vdash M : S}{
adamc@538 1002 \Gamma \vdash M : S'
adamc@538 1003 & \Gamma \vdash S' \leq S
adamc@538 1004 }
adamc@538 1005 \quad \infer{\Gamma \vdash \mt{struct} \; \overline{d} \; \mt{end} : \mt{sig} \; \mt{sigOf}(\overline{d}) \; \mt{end}}{
adamc@538 1006 \Gamma \vdash \overline{d} \leadsto \Gamma'
adamc@538 1007 }
adamc@538 1008 \quad \infer{\Gamma \vdash X : S}{
adamc@538 1009 X : S \in \Gamma
adamc@538 1010 }$$
adamc@538 1011
adamc@538 1012 $$\infer{\Gamma \vdash M.X : S}{
adamc@538 1013 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@538 1014 & \mt{proj}(M, \overline{s}, \mt{structure} \; X) = S
adamc@538 1015 }$$
adamc@538 1016
adamc@538 1017 $$\infer{\Gamma \vdash M_1(M_2) : [X \mapsto M_2]S_2}{
adamc@538 1018 \Gamma \vdash M_1 : \mt{functor}(X : S_1) : S_2
adamc@538 1019 & \Gamma \vdash M_2 : S_1
adamc@538 1020 }
adamc@538 1021 \quad \infer{\Gamma \vdash \mt{functor} (X : S_1) : S_2 = M : \mt{functor} (X : S_1) : S_2}{
adamc@538 1022 \Gamma \vdash S_1
adamc@538 1023 & \Gamma, X : S_1 \vdash S_2
adamc@538 1024 & \Gamma, X : S_1 \vdash M : S_2
adamc@538 1025 }$$
adamc@538 1026
adamc@538 1027 \begin{eqnarray*}
adamc@538 1028 \mt{sigOf}(\cdot) &=& \cdot \\
adamc@538 1029 \mt{sigOf}(s \; \overline{s'}) &=& \mt{sigOf}(s) \; \mt{sigOf}(\overline{s'}) \\
adamc@538 1030 \\
adamc@538 1031 \mt{sigOf}(\mt{con} \; x :: \kappa = c) &=& \mt{con} \; x :: \kappa = c \\
adamc@538 1032 \mt{sigOf}(\mt{datatype} \; x \; \overline{y} = \overline{dc}) &=& \mt{datatype} \; x \; \overline{y} = \overline{dc} \\
adamc@538 1033 \mt{sigOf}(\mt{datatype} \; x = \mt{datatype} \; M.z) &=& \mt{datatype} \; x = \mt{datatype} \; M.z \\
adamc@538 1034 \mt{sigOf}(\mt{val} \; x : \tau = e) &=& \mt{val} \; x : \tau \\
adamc@538 1035 \mt{sigOf}(\mt{val} \; \mt{rec} \; \overline{x : \tau = e}) &=& \overline{\mt{val} \; x : \tau} \\
adamc@538 1036 \mt{sigOf}(\mt{structure} \; X : S = M) &=& \mt{structure} \; X : S \\
adamc@538 1037 \mt{sigOf}(\mt{signature} \; X = S) &=& \mt{signature} \; X = S \\
adamc@538 1038 \mt{sigOf}(\mt{open} \; M) &=& \mt{include} \; S \textrm{ (where $\Gamma \vdash M : S$)} \\
adamc@538 1039 \mt{sigOf}(\mt{constraint} \; c_1 \sim c_2) &=& \mt{constraint} \; c_1 \sim c_2 \\
adamc@538 1040 \mt{sigOf}(\mt{open} \; \mt{constraints} \; M) &=& \cdot \\
adamc@538 1041 \mt{sigOf}(\mt{table} \; x : c) &=& \mt{table} \; x : c \\
adamc@784 1042 \mt{sigOf}(\mt{view} \; x : c) &=& \mt{view} \; x : c \\
adamc@538 1043 \mt{sigOf}(\mt{sequence} \; x) &=& \mt{sequence} \; x \\
adamc@538 1044 \mt{sigOf}(\mt{cookie} \; x : \tau) &=& \mt{cookie} \; x : \tau \\
adamc@784 1045 \mt{sigOf}(\mt{style} \; x) &=& \mt{style} \; x \\
adamc@655 1046 \mt{sigOf}(\mt{class} \; x :: \kappa = c) &=& \mt{class} \; x :: \kappa = c \\
adamc@538 1047 \end{eqnarray*}
adamc@539 1048 \begin{eqnarray*}
adamc@539 1049 \mt{selfify}(M, \cdot) &=& \cdot \\
adamc@558 1050 \mt{selfify}(M, s \; \overline{s'}) &=& \mt{selfify}(M, s) \; \mt{selfify}(M, \overline{s'}) \\
adamc@539 1051 \\
adamc@539 1052 \mt{selfify}(M, \mt{con} \; x :: \kappa) &=& \mt{con} \; x :: \kappa = M.x \\
adamc@539 1053 \mt{selfify}(M, \mt{con} \; x :: \kappa = c) &=& \mt{con} \; x :: \kappa = c \\
adamc@539 1054 \mt{selfify}(M, \mt{datatype} \; x \; \overline{y} = \overline{dc}) &=& \mt{datatype} \; x \; \overline{y} = \mt{datatype} \; M.x \\
adamc@539 1055 \mt{selfify}(M, \mt{datatype} \; x = \mt{datatype} \; M'.z) &=& \mt{datatype} \; x = \mt{datatype} \; M'.z \\
adamc@539 1056 \mt{selfify}(M, \mt{val} \; x : \tau) &=& \mt{val} \; x : \tau \\
adamc@539 1057 \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 1058 \mt{selfify}(M, \mt{signature} \; X = S) &=& \mt{signature} \; X = S \\
adamc@539 1059 \mt{selfify}(M, \mt{include} \; S) &=& \mt{include} \; S \\
adamc@539 1060 \mt{selfify}(M, \mt{constraint} \; c_1 \sim c_2) &=& \mt{constraint} \; c_1 \sim c_2 \\
adamc@655 1061 \mt{selfify}(M, \mt{class} \; x :: \kappa) &=& \mt{class} \; x :: \kappa = M.x \\
adamc@655 1062 \mt{selfify}(M, \mt{class} \; x :: \kappa = c) &=& \mt{class} \; x :: \kappa = c \\
adamc@539 1063 \end{eqnarray*}
adamc@539 1064
adamc@540 1065 \subsection{Module Projection}
adamc@540 1066
adamc@540 1067 \begin{eqnarray*}
adamc@540 1068 \mt{proj}(M, \mt{con} \; x :: \kappa \; \overline{s}, \mt{con} \; x) &=& \kappa \\
adamc@540 1069 \mt{proj}(M, \mt{con} \; x :: \kappa = c \; \overline{s}, \mt{con} \; x) &=& (\kappa, c) \\
adamc@540 1070 \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 1071 \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 1072 && \textrm{and $\mt{proj}(M', \overline{s'}, \mt{datatype} \; z) = (\overline{y}, \overline{dc})$)} \\
adamc@655 1073 \mt{proj}(M, \mt{class} \; x :: \kappa \; \overline{s}, \mt{con} \; x) &=& \kappa \to \mt{Type} \\
adamc@655 1074 \mt{proj}(M, \mt{class} \; x :: \kappa = c \; \overline{s}, \mt{con} \; x) &=& (\kappa \to \mt{Type}, c) \\
adamc@540 1075 \\
adamc@540 1076 \mt{proj}(M, \mt{datatype} \; x \; \overline{y} = \overline{dc} \; \overline{s}, \mt{datatype} \; x) &=& (\overline{y}, \overline{dc}) \\
adamc@540 1077 \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 1078 \\
adamc@540 1079 \mt{proj}(M, \mt{val} \; x : \tau \; \overline{s}, \mt{val} \; x) &=& \tau \\
adamc@540 1080 \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 1081 \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 1082 \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 1083 && \textrm{and $\mt{proj}(M', \overline{s'}, \mt{datatype} \; z = (\overline{y}, \overline{dc})$ and $X \in \overline{dc}$)} \\
adamc@540 1084 \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 1085 && \textrm{and $\mt{proj}(M', \overline{s'}, \mt{datatype} \; z = (\overline{y}, \overline{dc})$ and $X \; \mt{of} \; \tau \in \overline{dc}$)} \\
adamc@540 1086 \\
adamc@540 1087 \mt{proj}(M, \mt{structure} \; X : S \; \overline{s}, \mt{structure} \; X) &=& S \\
adamc@540 1088 \\
adamc@540 1089 \mt{proj}(M, \mt{signature} \; X = S \; \overline{s}, \mt{signature} \; X) &=& S \\
adamc@540 1090 \\
adamc@540 1091 \mt{proj}(M, \mt{con} \; x :: \kappa \; \overline{s}, V) &=& [x \mapsto M.x]\mt{proj}(M, \overline{s}, V) \\
adamc@540 1092 \mt{proj}(M, \mt{con} \; x :: \kappa = c \; \overline{s}, V) &=& [x \mapsto M.x]\mt{proj}(M, \overline{s}, V) \\
adamc@540 1093 \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 1094 \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 1095 \mt{proj}(M, \mt{val} \; x : \tau \; \overline{s}, V) &=& \mt{proj}(M, \overline{s}, V) \\
adamc@540 1096 \mt{proj}(M, \mt{structure} \; X : S \; \overline{s}, V) &=& [X \mapsto M.X]\mt{proj}(M, \overline{s}, V) \\
adamc@540 1097 \mt{proj}(M, \mt{signature} \; X = S \; \overline{s}, V) &=& [X \mapsto M.X]\mt{proj}(M, \overline{s}, V) \\
adamc@540 1098 \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 1099 \mt{proj}(M, \mt{constraint} \; c_1 \sim c_2 \; \overline{s}, V) &=& \mt{proj}(M, \overline{s}, V) \\
adamc@655 1100 \mt{proj}(M, \mt{class} \; x :: \kappa \; \overline{s}, V) &=& [x \mapsto M.x]\mt{proj}(M, \overline{s}, V) \\
adamc@655 1101 \mt{proj}(M, \mt{class} \; x :: \kappa = c \; \overline{s}, V) &=& [x \mapsto M.x]\mt{proj}(M, \overline{s}, V) \\
adamc@540 1102 \end{eqnarray*}
adamc@540 1103
adamc@541 1104
adamc@541 1105 \section{Type Inference}
adamc@541 1106
adamc@541 1107 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 1108
adamc@541 1109 \subsection{Basic Unification}
adamc@541 1110
adamc@560 1111 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 1112
adamc@656 1113 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 1114
adamc@541 1115 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 1116
adamc@541 1117 \subsection{Unifying Record Types}
adamc@541 1118
adamc@570 1119 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 1120
adamc@656 1121 \subsection{\label{typeclasses}Constructor Classes}
adamc@541 1122
adamc@784 1123 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 1124
adamc@784 1125 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 1126
adamc@656 1127 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 1128
adamc@656 1129 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 1130
adamc@541 1131 \subsection{Reverse-Engineering Record Types}
adamc@541 1132
adamc@656 1133 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 1134
adamc@541 1135 \subsection{Implicit Arguments in Functor Applications}
adamc@541 1136
adamc@656 1137 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 1138
adamc@541 1139
adamc@542 1140 \section{The Ur Standard Library}
adamc@542 1141
adamc@542 1142 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 1143
adamc@542 1144 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 1145
adamc@542 1146 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 1147 $$\begin{array}{l}
adamc@542 1148 \mt{type} \; \mt{int} \\
adamc@542 1149 \mt{type} \; \mt{float} \\
adamc@542 1150 \mt{type} \; \mt{string} \\
adamc@542 1151 \mt{type} \; \mt{time} \\
adamc@785 1152 \mt{type} \; \mt{blob} \\
adamc@542 1153 \\
adamc@542 1154 \mt{type} \; \mt{unit} = \{\} \\
adamc@542 1155 \\
adamc@542 1156 \mt{datatype} \; \mt{bool} = \mt{False} \mid \mt{True} \\
adamc@542 1157 \\
adamc@785 1158 \mt{datatype} \; \mt{option} \; \mt{t} = \mt{None} \mid \mt{Some} \; \mt{of} \; \mt{t} \\
adamc@785 1159 \\
adamc@785 1160 \mt{datatype} \; \mt{list} \; \mt{t} = \mt{Nil} \mid \mt{Cons} \; \mt{of} \; \mt{t} \times \mt{list} \; \mt{t}
adamc@542 1161 \end{array}$$
adamc@542 1162
adamc@785 1163 The only unusual element of this list is the $\mt{blob}$ type, which stands for binary sequences.
adamc@785 1164
adamc@657 1165 Another important generic Ur element comes at the beginning of \texttt{top.urs}.
adamc@657 1166
adamc@657 1167 $$\begin{array}{l}
adamc@657 1168 \mt{con} \; \mt{folder} :: \mt{K} \longrightarrow \{\mt{K}\} \to \mt{Type} \\
adamc@657 1169 \\
adamc@657 1170 \mt{val} \; \mt{fold} : \mt{K} \longrightarrow \mt{tf} :: (\{\mt{K}\} \to \mt{Type}) \\
adamc@657 1171 \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 1172 \hspace{.2in} \mt{tf} \; \mt{r} \to \mt{tf} \; ([\mt{nm} = \mt{v}] \rc \mt{r})) \\
adamc@657 1173 \hspace{.1in} \to \mt{tf} \; [] \\
adamc@657 1174 \hspace{.1in} \to \mt{r} :: \{\mt{K}\} \to \mt{folder} \; \mt{r} \to \mt{tf} \; \mt{r}
adamc@657 1175 \end{array}$$
adamc@657 1176
adamc@657 1177 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 1178
adamc@664 1179 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 1180
adamc@542 1181
adamc@542 1182 \section{The Ur/Web Standard Library}
adamc@542 1183
adamc@658 1184 \subsection{Monads}
adamc@658 1185
adamc@658 1186 The Ur Basis defines the monad constructor class from Haskell.
adamc@658 1187
adamc@658 1188 $$\begin{array}{l}
adamc@658 1189 \mt{class} \; \mt{monad} :: \mt{Type} \to \mt{Type} \\
adamc@658 1190 \mt{val} \; \mt{return} : \mt{m} ::: (\mt{Type} \to \mt{Type}) \to \mt{t} ::: \mt{Type} \\
adamc@658 1191 \hspace{.1in} \to \mt{monad} \; \mt{m} \\
adamc@658 1192 \hspace{.1in} \to \mt{t} \to \mt{m} \; \mt{t} \\
adamc@658 1193 \mt{val} \; \mt{bind} : \mt{m} ::: (\mt{Type} \to \mt{Type}) \to \mt{t1} ::: \mt{Type} \to \mt{t2} ::: \mt{Type} \\
adamc@658 1194 \hspace{.1in} \to \mt{monad} \; \mt{m} \\
adamc@658 1195 \hspace{.1in} \to \mt{m} \; \mt{t1} \to (\mt{t1} \to \mt{m} \; \mt{t2}) \\
adamc@658 1196 \hspace{.1in} \to \mt{m} \; \mt{t2}
adamc@658 1197 \end{array}$$
adamc@658 1198
adamc@542 1199 \subsection{Transactions}
adamc@542 1200
adamc@542 1201 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 1202 $$\begin{array}{l}
adamc@542 1203 \mt{con} \; \mt{transaction} :: \mt{Type} \to \mt{Type} \\
adamc@658 1204 \mt{val} \; \mt{transaction\_monad} : \mt{monad} \; \mt{transaction}
adamc@542 1205 \end{array}$$
adamc@542 1206
adamc@542 1207 \subsection{HTTP}
adamc@542 1208
adamc@542 1209 There are transactions for reading an HTTP header by name and for getting and setting strongly-typed cookies. Cookies may only be created by the $\mt{cookie}$ declaration form, ensuring that they be named consistently based on module structure.
adamc@542 1210 $$\begin{array}{l}
adamc@786 1211 \mt{val} \; \mt{requestHeader} : \mt{string} \to \mt{transaction} \; (\mt{option} \; \mt{string}) \\
adamc@786 1212 \\
adamc@786 1213 \mt{con} \; \mt{http\_cookie} :: \mt{Type} \to \mt{Type} \\
adamc@786 1214 \mt{val} \; \mt{getCookie} : \mt{t} ::: \mt{Type} \to \mt{http\_cookie} \; \mt{t} \to \mt{transaction} \; (\mt{option} \; \mt{t}) \\
adamc@786 1215 \mt{val} \; \mt{setCookie} : \mt{t} ::: \mt{Type} \to \mt{http\_cookie} \; \mt{t} \to \mt{t} \to \mt{transaction} \; \mt{unit}
adamc@786 1216 \end{array}$$
adamc@786 1217
adamc@786 1218 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 1219 $$\begin{array}{l}
adamc@786 1220 \mt{type} \; \mt{url} \\
adamc@786 1221 \mt{val} \; \mt{bless} : \mt{string} \to \mt{url} \\
adamc@786 1222 \mt{val} \; \mt{checkUrl} : \mt{string} \to \mt{option} \; \mt{url}
adamc@786 1223 \end{array}$$
adamc@786 1224 $\mt{bless}$ raises a runtime error if the string passed to it fails the URL policy.
adamc@786 1225
adamc@786 1226 It's possible for pages to return files of arbitrary MIME types. A file can be input from the user using this data type, along with the $\mt{upload}$ form tag.
adamc@786 1227 $$\begin{array}{l}
adamc@786 1228 \mt{type} \; \mt{file} \\
adamc@786 1229 \mt{val} \; \mt{fileName} : \mt{file} \to \mt{option} \; \mt{string} \\
adamc@786 1230 \mt{val} \; \mt{fileMimeType} : \mt{file} \to \mt{string} \\
adamc@786 1231 \mt{val} \; \mt{fileData} : \mt{file} \to \mt{blob}
adamc@786 1232 \end{array}$$
adamc@786 1233
adamc@786 1234 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 1235 $$\begin{array}{l}
adamc@786 1236 \mt{type} \; \mt{mimeType} \\
adamc@786 1237 \mt{val} \; \mt{blessMime} : \mt{string} \to \mt{mimeType} \\
adamc@786 1238 \mt{val} \; \mt{checkMime} : \mt{string} \to \mt{option} \; \mt{mimeType} \\
adamc@786 1239 \mt{val} \; \mt{returnBlob} : \mt{t} ::: \mt{Type} \to \mt{blob} \to \mt{mimeType} \to \mt{transaction} \; \mt{t}
adamc@542 1240 \end{array}$$
adamc@542 1241
adamc@543 1242 \subsection{SQL}
adamc@543 1243
adamc@543 1244 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 1245 $$\begin{array}{l}
adamc@785 1246 \mt{con} \; \mt{sql\_table} :: \{\mt{Type}\} \to \{\{\mt{Unit}\}\} \to \mt{Type}
adamc@785 1247 \end{array}$$
adamc@785 1248 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 1249
adamc@785 1250 We also have the simpler type family of SQL views, which have no keys.
adamc@785 1251 $$\begin{array}{l}
adamc@785 1252 \mt{con} \; \mt{sql\_view} :: \{\mt{Type}\} \to \mt{Type}
adamc@543 1253 \end{array}$$
adamc@543 1254
adamc@785 1255 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 1256 $$\begin{array}{l}
adamc@785 1257 \mt{class} \; \mt{fieldsOf} :: \mt{Type} \to \{\mt{Type}\} \to \mt{Type} \\
adamc@785 1258 \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 1259 \mt{val} \; \mt{fieldsOf\_view} : \mt{fs} ::: \{\mt{Type}\} \to \mt{fieldsOf} \; (\mt{sql\_view} \; \mt{fs}) \; \mt{fs}
adamc@785 1260 \end{array}$$
adamc@785 1261
adamc@785 1262 \subsubsection{Table Constraints}
adamc@785 1263
adamc@785 1264 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 1265
adamc@785 1266 $$\begin{array}{l}
adamc@785 1267 \mt{con} \; \mt{primary\_key} :: \{\mt{Type}\} \to \{\{\mt{Unit}\}\} \to \mt{Type} \\
adamc@785 1268 \mt{val} \; \mt{no\_primary\_key} : \mt{fs} ::: \{\mt{Type}\} \to \mt{primary\_key} \; \mt{fs} \; [] \\
adamc@785 1269 \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 1270 \hspace{.1in} \to [[\mt{key1}] \sim \mt{keys}] \Rightarrow [[\mt{key1} = \mt{t}] \rc \mt{keys} \sim \mt{rest}] \\
adamc@785 1271 \hspace{.1in} \Rightarrow \$([\mt{key1} = \mt{sql\_injectable\_prim} \; \mt{t}] \rc \mt{map} \; \mt{sql\_injectable\_prim} \; \mt{keys}) \\
adamc@785 1272 \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 1273 \end{array}$$
adamc@785 1274 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 1275
adamc@785 1276 A type family stands for sets of named constraints of the remaining varieties.
adamc@785 1277 $$\begin{array}{l}
adamc@785 1278 \mt{con} \; \mt{sql\_constraints} :: \{\mt{Type}\} \to \{\{\mt{Unit}\}\} \to \mt{Type}
adamc@785 1279 \end{array}$$
adamc@785 1280 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 1281
adamc@785 1282 There is a type family of individual, unnamed constraints.
adamc@785 1283 $$\begin{array}{l}
adamc@785 1284 \mt{con} \; \mt{sql\_constraint} :: \{\mt{Type}\} \to \{\mt{Unit}\} \to \mt{Type}
adamc@785 1285 \end{array}$$
adamc@785 1286 The first argument is the same as above, and the second argument gives the key columns for just this constraint.
adamc@785 1287
adamc@785 1288 We have operations for assembling constraints into constraint sets.
adamc@785 1289 $$\begin{array}{l}
adamc@785 1290 \mt{val} \; \mt{no\_constraint} : \mt{fs} ::: \{\mt{Type}\} \to \mt{sql\_constraints} \; \mt{fs} \; [] \\
adamc@785 1291 \mt{val} \; \mt{one\_constraint} : \mt{fs} ::: \{\mt{Type}\} \to \mt{unique} ::: \{\mt{Unit}\} \to \mt{name} :: \mt{Name} \\
adamc@785 1292 \hspace{.1in} \to \mt{sql\_constraint} \; \mt{fs} \; \mt{unique} \to \mt{sql\_constraints} \; \mt{fs} \; [\mt{name} = \mt{unique}] \\
adamc@785 1293 \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 1294 \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 1295 \end{array}$$
adamc@785 1296
adamc@785 1297 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 1298 $$\begin{array}{l}
adamc@785 1299 \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 1300 \hspace{.1in} \to [[\mt{unique1}] \sim \mt{unique}] \Rightarrow [[\mt{unique1} = \mt{t}] \rc \mt{unique} \sim \mt{rest}] \\
adamc@785 1301 \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 1302 \end{array}$$
adamc@785 1303
adamc@785 1304 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 1305 $$\begin{array}{l}
adamc@785 1306 \mt{class} \; \mt{linkable} :: \mt{Type} \to \mt{Type} \to \mt{Type} \\
adamc@785 1307 \mt{val} \; \mt{linkable\_same} : \mt{t} ::: \mt{Type} \to \mt{linkable} \; \mt{t} \; \mt{t} \\
adamc@785 1308 \mt{val} \; \mt{linkable\_from\_nullable} : \mt{t} ::: \mt{Type} \to \mt{linkable} \; (\mt{option} \; \mt{t}) \; \mt{t} \\
adamc@785 1309 \mt{val} \; \mt{linkable\_to\_nullable} : \mt{t} ::: \mt{Type} \to \mt{linkable} \; \mt{t} \; (\mt{option} \; \mt{t})
adamc@785 1310 \end{array}$$
adamc@785 1311
adamc@785 1312 The $\mt{matching}$ type family uses $\mt{linkable}$ to define when two keys match up type-wise.
adamc@785 1313 $$\begin{array}{l}
adamc@785 1314 \mt{con} \; \mt{matching} :: \{\mt{Type}\} \to \{\mt{Type}\} \to \mt{Type} \\
adamc@785 1315 \mt{val} \; \mt{mat\_nil} : \mt{matching} \; [] \; [] \\
adamc@785 1316 \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 1317 \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 1318 \hspace{.1in} \to \mt{matching} \; ([\mt{nm1} = \mt{t1}] \rc \mt{rest1}) \; ([\mt{nm2} = \mt{t2}] \rc \mt{rest2})
adamc@785 1319 \end{array}$$
adamc@785 1320
adamc@785 1321 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 1322 $$\begin{array}{l}
adamc@785 1323 \mt{con} \; \mt{propagation\_mode} :: \{\mt{Type}\} \to \mt{Type} \\
adamc@785 1324 \mt{val} \; \mt{restrict} : \mt{fs} ::: \{\mt{Type}\} \to \mt{propagation\_mode} \; \mt{fs} \\
adamc@785 1325 \mt{val} \; \mt{cascade} : \mt{fs} ::: \{\mt{Type}\} \to \mt{propagation\_mode} \; \mt{fs} \\
adamc@785 1326 \mt{val} \; \mt{no\_action} : \mt{fs} ::: \{\mt{Type}\} \to \mt{propagation\_mode} \; \mt{fs} \\
adamc@785 1327 \mt{val} \; \mt{set\_null} : \mt{fs} ::: \{\mt{Type}\} \to \mt{propagation\_mode} \; (\mt{map} \; \mt{option} \; \mt{fs})
adamc@785 1328 \end{array}$$
adamc@785 1329
adamc@785 1330 Finally, we put these ingredient together to define the \texttt{FOREIGN KEY} constraint function.
adamc@785 1331 $$\begin{array}{l}
adamc@785 1332 \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 1333 \hspace{.1in} \to \mt{funused} ::: \{\mt{Type}\} \to \mt{nm} ::: \mt{Name} \to \mt{uniques} ::: \{\{\mt{Unit}\}\} \\
adamc@785 1334 \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 1335 \hspace{.1in} \Rightarrow \mt{matching} \; ([\mt{mine1} = \mt{t}] \rc \mt{mine}) \; \mt{foreign} \\
adamc@785 1336 \hspace{.1in} \to \mt{sql\_table} \; (\mt{foreign} \rc \mt{funused}) \; ([\mt{nm} = \mt{map} \; (\lambda \_ \Rightarrow ()) \; \mt{foreign}] \rc \mt{uniques}) \\
adamc@785 1337 \hspace{.1in} \to \{\mt{OnDelete} : \mt{propagation\_mode} \; ([\mt{mine1} = \mt{t}] \rc \mt{mine}), \\
adamc@785 1338 \hspace{.2in} \mt{OnUpdate} : \mt{propagation\_mode} \; ([\mt{mine1} = \mt{t}] \rc \mt{mine})\} \\
adamc@785 1339 \hspace{.1in} \to \mt{sql\_constraint} \; ([\mt{mine1} = \mt{t}] \rc \mt{mine} \rc \mt{munused}) \; []
adamc@785 1340 \end{array}$$
adamc@785 1341
adamc@785 1342 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 1343 $$\begin{array}{l}
adamc@785 1344 \mt{val} \; \mt{check} : \mt{fs} ::: \{\mt{Type}\} \to \mt{sql\_exp} \; [] \; [] \; \mt{fs} \; \mt{bool} \to \mt{sql\_constraint} \; \mt{fs} \; []
adamc@785 1345 \end{array}$$
adamc@785 1346
adamc@785 1347 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 1348
adamc@784 1349
adamc@543 1350 \subsubsection{Queries}
adamc@543 1351
adamc@543 1352 A final query is constructed via the $\mt{sql\_query}$ function. Constructor arguments respectively specify the table fields we select (as records mapping tables to the subsets of their fields that we choose) and the (always named) extra expressions that we select.
adamc@543 1353 $$\begin{array}{l}
adamc@543 1354 \mt{con} \; \mt{sql\_query} :: \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \\
adamc@543 1355 \mt{val} \; \mt{sql\_query} : \mt{tables} ::: \{\{\mt{Type}\}\} \\
adamc@543 1356 \hspace{.1in} \to \mt{selectedFields} ::: \{\{\mt{Type}\}\} \\
adamc@543 1357 \hspace{.1in} \to \mt{selectedExps} ::: \{\mt{Type}\} \\
adamc@543 1358 \hspace{.1in} \to \{\mt{Rows} : \mt{sql\_query1} \; \mt{tables} \; \mt{selectedFields} \; \mt{selectedExps}, \\
adamc@543 1359 \hspace{.2in} \mt{OrderBy} : \mt{sql\_order\_by} \; \mt{tables} \; \mt{selectedExps}, \\
adamc@543 1360 \hspace{.2in} \mt{Limit} : \mt{sql\_limit}, \\
adamc@543 1361 \hspace{.2in} \mt{Offset} : \mt{sql\_offset}\} \\
adamc@543 1362 \hspace{.1in} \to \mt{sql\_query} \; \mt{selectedFields} \; \mt{selectedExps}
adamc@543 1363 \end{array}$$
adamc@543 1364
adamc@545 1365 Queries are used by folding over their results inside transactions.
adamc@545 1366 $$\begin{array}{l}
adamc@545 1367 \mt{val} \; \mt{query} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \lambda [\mt{tables} \sim \mt{exps}] \Rightarrow \mt{state} ::: \mt{Type} \to \mt{sql\_query} \; \mt{tables} \; \mt{exps} \\
adamc@658 1368 \hspace{.1in} \to (\$(\mt{exps} \rc \mt{map} \; (\lambda \mt{fields} :: \{\mt{Type}\} \Rightarrow \$\mt{fields}) \; \mt{tables}) \\
adamc@545 1369 \hspace{.2in} \to \mt{state} \to \mt{transaction} \; \mt{state}) \\
adamc@545 1370 \hspace{.1in} \to \mt{state} \to \mt{transaction} \; \mt{state}
adamc@545 1371 \end{array}$$
adamc@545 1372
adamc@543 1373 Most of the complexity of the query encoding is in the type $\mt{sql\_query1}$, which includes simple queries and derived queries based on relational operators. Constructor arguments respectively specify the tables we select from, the subset of fields that we keep from each table for the result rows, and the extra expressions that we select.
adamc@543 1374 $$\begin{array}{l}
adamc@543 1375 \mt{con} \; \mt{sql\_query1} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \\
adamc@543 1376 \\
adamc@543 1377 \mt{type} \; \mt{sql\_relop} \\
adamc@543 1378 \mt{val} \; \mt{sql\_union} : \mt{sql\_relop} \\
adamc@543 1379 \mt{val} \; \mt{sql\_intersect} : \mt{sql\_relop} \\
adamc@543 1380 \mt{val} \; \mt{sql\_except} : \mt{sql\_relop} \\
adamc@543 1381 \mt{val} \; \mt{sql\_relop} : \mt{tables1} ::: \{\{\mt{Type}\}\} \\
adamc@543 1382 \hspace{.1in} \to \mt{tables2} ::: \{\{\mt{Type}\}\} \\
adamc@543 1383 \hspace{.1in} \to \mt{selectedFields} ::: \{\{\mt{Type}\}\} \\
adamc@543 1384 \hspace{.1in} \to \mt{selectedExps} ::: \{\mt{Type}\} \\
adamc@543 1385 \hspace{.1in} \to \mt{sql\_relop} \\
adamc@543 1386 \hspace{.1in} \to \mt{sql\_query1} \; \mt{tables1} \; \mt{selectedFields} \; \mt{selectedExps} \\
adamc@543 1387 \hspace{.1in} \to \mt{sql\_query1} \; \mt{tables2} \; \mt{selectedFields} \; \mt{selectedExps} \\
adamc@543 1388 \hspace{.1in} \to \mt{sql\_query1} \; \mt{selectedFields} \; \mt{selectedFields} \; \mt{selectedExps}
adamc@543 1389 \end{array}$$
adamc@543 1390
adamc@543 1391 $$\begin{array}{l}
adamc@543 1392 \mt{val} \; \mt{sql\_query1} : \mt{tables} ::: \{\{\mt{Type}\}\} \\
adamc@543 1393 \hspace{.1in} \to \mt{grouped} ::: \{\{\mt{Type}\}\} \\
adamc@543 1394 \hspace{.1in} \to \mt{selectedFields} ::: \{\{\mt{Type}\}\} \\
adamc@543 1395 \hspace{.1in} \to \mt{selectedExps} ::: \{\mt{Type}\} \\
adamc@786 1396 \hspace{.1in} \to \{\mt{From} : \mt{sql\_from\_items} \; \mt{tables}, \\
adamc@543 1397 \hspace{.2in} \mt{Where} : \mt{sql\_exp} \; \mt{tables} \; [] \; [] \; \mt{bool}, \\
adamc@543 1398 \hspace{.2in} \mt{GroupBy} : \mt{sql\_subset} \; \mt{tables} \; \mt{grouped}, \\
adamc@543 1399 \hspace{.2in} \mt{Having} : \mt{sql\_exp} \; \mt{grouped} \; \mt{tables} \; [] \; \mt{bool}, \\
adamc@543 1400 \hspace{.2in} \mt{SelectFields} : \mt{sql\_subset} \; \mt{grouped} \; \mt{selectedFields}, \\
adamc@658 1401 \hspace{.2in} \mt {SelectExps} : \$(\mt{map} \; (\mt{sql\_exp} \; \mt{grouped} \; \mt{tables} \; []) \; \mt{selectedExps}) \} \\
adamc@543 1402 \hspace{.1in} \to \mt{sql\_query1} \; \mt{tables} \; \mt{selectedFields} \; \mt{selectedExps}
adamc@543 1403 \end{array}$$
adamc@543 1404
adamc@543 1405 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 1406 $$\begin{array}{l}
adamc@543 1407 \mt{con} \; \mt{sql\_subset} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \mt{Type} \\
adamc@543 1408 \mt{val} \; \mt{sql\_subset} : \mt{keep\_drop} :: \{(\{\mt{Type}\} \times \{\mt{Type}\})\} \\
adamc@543 1409 \hspace{.1in} \to \mt{sql\_subset} \\
adamc@658 1410 \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 1411 \hspace{.2in} (\mt{map} \; (\lambda \mt{fields} :: (\{\mt{Type}\} \times \{\mt{Type}\}) \Rightarrow \mt{fields}.1) \; \mt{keep\_drop}) \\
adamc@543 1412 \mt{val} \; \mt{sql\_subset\_all} : \mt{tables} :: \{\{\mt{Type}\}\} \to \mt{sql\_subset} \; \mt{tables} \; \mt{tables}
adamc@543 1413 \end{array}$$
adamc@543 1414
adamc@560 1415 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 1416 $$\begin{array}{l}
adamc@543 1417 \mt{con} \; \mt{sql\_exp} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \to \mt{Type}
adamc@543 1418 \end{array}$$
adamc@543 1419
adamc@543 1420 Any field in scope may be converted to an expression.
adamc@543 1421 $$\begin{array}{l}
adamc@543 1422 \mt{val} \; \mt{sql\_field} : \mt{otherTabs} ::: \{\{\mt{Type}\}\} \to \mt{otherFields} ::: \{\mt{Type}\} \\
adamc@543 1423 \hspace{.1in} \to \mt{fieldType} ::: \mt{Type} \to \mt{agg} ::: \{\{\mt{Type}\}\} \\
adamc@543 1424 \hspace{.1in} \to \mt{exps} ::: \{\mt{Type}\} \\
adamc@543 1425 \hspace{.1in} \to \mt{tab} :: \mt{Name} \to \mt{field} :: \mt{Name} \\
adamc@543 1426 \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 1427 \end{array}$$
adamc@543 1428
adamc@544 1429 There is an analogous function for referencing named expressions.
adamc@544 1430 $$\begin{array}{l}
adamc@544 1431 \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 1432 \hspace{.1in} \to \mt{sql\_exp} \; \mt{tabs} \; \mt{agg} \; ([\mt{nm} = \mt{t}] \rc \mt{rest}) \; \mt{t}
adamc@544 1433 \end{array}$$
adamc@544 1434
adamc@544 1435 Ur values of appropriate types may be injected into SQL expressions.
adamc@544 1436 $$\begin{array}{l}
adamc@786 1437 \mt{class} \; \mt{sql\_injectable\_prim} \\
adamc@786 1438 \mt{val} \; \mt{sql\_bool} : \mt{sql\_injectable\_prim} \; \mt{bool} \\
adamc@786 1439 \mt{val} \; \mt{sql\_int} : \mt{sql\_injectable\_prim} \; \mt{int} \\
adamc@786 1440 \mt{val} \; \mt{sql\_float} : \mt{sql\_injectable\_prim} \; \mt{float} \\
adamc@786 1441 \mt{val} \; \mt{sql\_string} : \mt{sql\_injectable\_prim} \; \mt{string} \\
adamc@786 1442 \mt{val} \; \mt{sql\_time} : \mt{sql\_injectable\_prim} \; \mt{time} \\
adamc@786 1443 \mt{val} \; \mt{sql\_blob} : \mt{sql\_injectable\_prim} \; \mt{blob} \\
adamc@786 1444 \mt{val} \; \mt{sql\_channel} : \mt{t} ::: \mt{Type} \to \mt{sql\_injectable\_prim} \; (\mt{channel} \; \mt{t}) \\
adamc@786 1445 \mt{val} \; \mt{sql\_client} : \mt{sql\_injectable\_prim} \; \mt{client} \\
adamc@786 1446 \\
adamc@544 1447 \mt{class} \; \mt{sql\_injectable} \\
adamc@786 1448 \mt{val} \; \mt{sql\_prim} : \mt{t} ::: \mt{Type} \to \mt{sql\_injectable\_prim} \; \mt{t} \to \mt{sql\_injectable} \; \mt{t} \\
adamc@786 1449 \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 1450 \\
adamc@544 1451 \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 1452 \hspace{.1in} \to \mt{t} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t}
adamc@544 1453 \end{array}$$
adamc@544 1454
adamc@544 1455 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 1456 $$\begin{array}{l}
adamc@544 1457 \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 1458 \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 1459 \end{array}$$
adamc@544 1460
adamc@559 1461 We have generic nullary, unary, and binary operators.
adamc@544 1462 $$\begin{array}{l}
adamc@544 1463 \mt{con} \; \mt{sql\_nfunc} :: \mt{Type} \to \mt{Type} \\
adamc@544 1464 \mt{val} \; \mt{sql\_current\_timestamp} : \mt{sql\_nfunc} \; \mt{time} \\
adamc@544 1465 \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 1466 \hspace{.1in} \to \mt{sql\_nfunc} \; \mt{t} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} \\\end{array}$$
adamc@544 1467
adamc@544 1468 $$\begin{array}{l}
adamc@544 1469 \mt{con} \; \mt{sql\_unary} :: \mt{Type} \to \mt{Type} \to \mt{Type} \\
adamc@544 1470 \mt{val} \; \mt{sql\_not} : \mt{sql\_unary} \; \mt{bool} \; \mt{bool} \\
adamc@544 1471 \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 1472 \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 1473 \end{array}$$
adamc@544 1474
adamc@544 1475 $$\begin{array}{l}
adamc@544 1476 \mt{con} \; \mt{sql\_binary} :: \mt{Type} \to \mt{Type} \to \mt{Type} \to \mt{Type} \\
adamc@544 1477 \mt{val} \; \mt{sql\_and} : \mt{sql\_binary} \; \mt{bool} \; \mt{bool} \; \mt{bool} \\
adamc@544 1478 \mt{val} \; \mt{sql\_or} : \mt{sql\_binary} \; \mt{bool} \; \mt{bool} \; \mt{bool} \\
adamc@544 1479 \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 1480 \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 1481 \end{array}$$
adamc@544 1482
adamc@544 1483 $$\begin{array}{l}
adamc@559 1484 \mt{class} \; \mt{sql\_arith} \\
adamc@559 1485 \mt{val} \; \mt{sql\_int\_arith} : \mt{sql\_arith} \; \mt{int} \\
adamc@559 1486 \mt{val} \; \mt{sql\_float\_arith} : \mt{sql\_arith} \; \mt{float} \\
adamc@559 1487 \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 1488 \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 1489 \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 1490 \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 1491 \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 1492 \mt{val} \; \mt{sql\_mod} : \mt{sql\_binary} \; \mt{int} \; \mt{int} \; \mt{int}
adamc@559 1493 \end{array}$$
adamc@544 1494
adamc@656 1495 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 1496 $$\begin{array}{l}
adamc@544 1497 \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 1498 \end{array}$$
adamc@544 1499
adamc@544 1500 $$\begin{array}{l}
adamc@544 1501 \mt{con} \; \mt{sql\_aggregate} :: \mt{Type} \to \mt{Type} \\
adamc@544 1502 \mt{val} \; \mt{sql\_aggregate} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{t} ::: \mt{Type} \\
adamc@544 1503 \hspace{.1in} \to \mt{sql\_aggregate} \; \mt{t} \to \mt{sql\_exp} \; \mt{agg} \; \mt{agg} \; \mt{exps} \; \mt{t} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t}
adamc@544 1504 \end{array}$$
adamc@544 1505
adamc@544 1506 $$\begin{array}{l}
adamc@544 1507 \mt{class} \; \mt{sql\_summable} \\
adamc@544 1508 \mt{val} \; \mt{sql\_summable\_int} : \mt{sql\_summable} \; \mt{int} \\
adamc@544 1509 \mt{val} \; \mt{sql\_summable\_float} : \mt{sql\_summable} \; \mt{float} \\
adamc@544 1510 \mt{val} \; \mt{sql\_avg} : \mt{t} ::: \mt{Type} \to \mt{sql\_summable} \; \mt{t} \to \mt{sql\_aggregate} \; \mt{t} \\
adamc@544 1511 \mt{val} \; \mt{sql\_sum} : \mt{t} ::: \mt{Type} \to \mt{sql\_summable} \mt{t} \to \mt{sql\_aggregate} \; \mt{t}
adamc@544 1512 \end{array}$$
adamc@544 1513
adamc@544 1514 $$\begin{array}{l}
adamc@544 1515 \mt{class} \; \mt{sql\_maxable} \\
adamc@544 1516 \mt{val} \; \mt{sql\_maxable\_int} : \mt{sql\_maxable} \; \mt{int} \\
adamc@544 1517 \mt{val} \; \mt{sql\_maxable\_float} : \mt{sql\_maxable} \; \mt{float} \\
adamc@544 1518 \mt{val} \; \mt{sql\_maxable\_string} : \mt{sql\_maxable} \; \mt{string} \\
adamc@544 1519 \mt{val} \; \mt{sql\_maxable\_time} : \mt{sql\_maxable} \; \mt{time} \\
adamc@544 1520 \mt{val} \; \mt{sql\_max} : \mt{t} ::: \mt{Type} \to \mt{sql\_maxable} \; \mt{t} \to \mt{sql\_aggregate} \; \mt{t} \\
adamc@544 1521 \mt{val} \; \mt{sql\_min} : \mt{t} ::: \mt{Type} \to \mt{sql\_maxable} \; \mt{t} \to \mt{sql\_aggregate} \; \mt{t}
adamc@544 1522 \end{array}$$
adamc@544 1523
adamc@786 1524 \texttt{FROM} clauses are specified using a type family.
adamc@786 1525 $$\begin{array}{l}
adamc@786 1526 \mt{con} \; \mt{sql\_from\_items} :: \{\{\mt{Type}\}\} \to \mt{Type} \\
adamc@786 1527 \mt{val} \; \mt{sql\_from\_table} : \mt{t} ::: \mt{Type} \to \mt{fs} ::: \{\mt{Type}\} \to \mt{fieldsOf} \; \mt{t} \; \mt{fs} \to \mt{name} :: \mt{Name} \to \mt{t} \to \mt{sql\_from\_items} \; [\mt{name} = \mt{fs}] \\
adamc@786 1528 \mt{val} \; \mt{sql\_from\_comma} : \mt{tabs1} ::: \{\{\mt{Type}\}\} \to \mt{tabs2} ::: \{\{\mt{Type}\}\} \to [\mt{tabs1} \sim \mt{tabs2}] \\
adamc@786 1529 \hspace{.1in} \Rightarrow \mt{sql\_from\_items} \; \mt{tabs1} \to \mt{sql\_from\_items} \; \mt{tabs2} \\
adamc@786 1530 \hspace{.1in} \to \mt{sql\_from\_items} \; (\mt{tabs1} \rc \mt{tabs2}) \\
adamc@786 1531 \mt{val} \; \mt{sql\_inner\_join} : \mt{tabs1} ::: \{\{\mt{Type}\}\} \to \mt{tabs2} ::: \{\{\mt{Type}\}\} \to [\mt{tabs1} \sim \mt{tabs2}] \\
adamc@786 1532 \hspace{.1in} \Rightarrow \mt{sql\_from\_items} \; \mt{tabs1} \to \mt{sql\_from\_items} \; \mt{tabs2} \\
adamc@786 1533 \hspace{.1in} \to \mt{sql\_exp} \; (\mt{tabs1} \rc \mt{tabs2}) \; [] \; [] \; \mt{bool} \\
adamc@786 1534 \hspace{.1in} \to \mt{sql\_from\_items} \; (\mt{tabs1} \rc \mt{tabs2})
adamc@786 1535 \end{array}$$
adamc@786 1536
adamc@786 1537 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 1538 $$\begin{array}{l}
adamc@786 1539 \mt{class} \; \mt{nullify} :: \mt{Type} \to \mt{Type} \to \mt{Type} \\
adamc@786 1540 \mt{val} \; \mt{nullify\_option} : \mt{t} ::: \mt{Type} \to \mt{nullify} \; (\mt{option} \; \mt{t}) \; (\mt{option} \; \mt{t}) \\
adamc@786 1541 \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 1542 \end{array}$$
adamc@786 1543
adamc@786 1544 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 1545
adamc@786 1546 $$\begin{array}{l}
adamc@786 1547 \mt{val} \; \mt{sql\_left\_join} : \mt{tabs1} ::: \{\{\mt{Type}\}\} \to \mt{tabs2} ::: \{\{(\mt{Type} \times \mt{Type})\}\} \to [\mt{tabs1} \sim \mt{tabs2}] \\
adamc@786 1548 \hspace{.1in} \Rightarrow \$(\mt{map} \; (\lambda \mt{r} \Rightarrow \$(\mt{map} \; (\lambda \mt{p} :: (\mt{Type} \times \mt{Type}) \Rightarrow \mt{nullify} \; \mt{p}.1 \; \mt{p}.2) \; \mt{r})) \; \mt{tabs2}) \\
adamc@786 1549 \hspace{.1in} \to \mt{sql\_from\_items} \; \mt{tabs1} \to \mt{sql\_from\_items} \; (\mt{map} \; (\mt{map} \; (\lambda \mt{p} :: (\mt{Type} \times \mt{Type}) \Rightarrow \mt{p}.1)) \; \mt{tabs2}) \\
adamc@786 1550 \hspace{.1in} \to \mt{sql\_exp} \; (\mt{tabs1} \rc \mt{map} \; (\mt{map} \; (\lambda \mt{p} :: (\mt{Type} \times \mt{Type}) \Rightarrow \mt{p}.1)) \; \mt{tabs2}) \; [] \; [] \; \mt{bool} \\
adamc@786 1551 \hspace{.1in} \to \mt{sql\_from\_items} \; (\mt{tabs1} \rc \mt{map} \; (\mt{map} \; (\lambda \mt{p} :: (\mt{Type} \times \mt{Type}) \Rightarrow \mt{p}.2)) \; \mt{tabs2})
adamc@786 1552 \end{array}$$
adamc@786 1553
adamc@544 1554 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 1555 $$\begin{array}{l}
adamc@544 1556 \mt{type} \; \mt{sql\_direction} \\
adamc@544 1557 \mt{val} \; \mt{sql\_asc} : \mt{sql\_direction} \\
adamc@544 1558 \mt{val} \; \mt{sql\_desc} : \mt{sql\_direction} \\
adamc@544 1559 \\
adamc@544 1560 \mt{con} \; \mt{sql\_order\_by} :: \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \\
adamc@544 1561 \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 1562 \mt{val} \; \mt{sql\_order\_by\_Cons} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{t} ::: \mt{Type} \\
adamc@544 1563 \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 1564 \\
adamc@544 1565 \mt{type} \; \mt{sql\_limit} \\
adamc@544 1566 \mt{val} \; \mt{sql\_no\_limit} : \mt{sql\_limit} \\
adamc@544 1567 \mt{val} \; \mt{sql\_limit} : \mt{int} \to \mt{sql\_limit} \\
adamc@544 1568 \\
adamc@544 1569 \mt{type} \; \mt{sql\_offset} \\
adamc@544 1570 \mt{val} \; \mt{sql\_no\_offset} : \mt{sql\_offset} \\
adamc@544 1571 \mt{val} \; \mt{sql\_offset} : \mt{int} \to \mt{sql\_offset}
adamc@544 1572 \end{array}$$
adamc@544 1573
adamc@545 1574
adamc@545 1575 \subsubsection{DML}
adamc@545 1576
adamc@545 1577 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 1578
adamc@545 1579 $$\begin{array}{l}
adamc@545 1580 \mt{type} \; \mt{dml} \\
adamc@545 1581 \mt{val} \; \mt{dml} : \mt{dml} \to \mt{transaction} \; \mt{unit}
adamc@545 1582 \end{array}$$
adamc@545 1583
adamc@545 1584 Properly-typed records may be used to form $\mt{INSERT}$ commands.
adamc@545 1585 $$\begin{array}{l}
adamc@545 1586 \mt{val} \; \mt{insert} : \mt{fields} ::: \{\mt{Type}\} \to \mt{sql\_table} \; \mt{fields} \\
adamc@658 1587 \hspace{.1in} \to \$(\mt{map} \; (\mt{sql\_exp} \; [] \; [] \; []) \; \mt{fields}) \to \mt{dml}
adamc@545 1588 \end{array}$$
adamc@545 1589
adamc@545 1590 An $\mt{UPDATE}$ command is formed from a choice of which table fields to leave alone and which to change, along with an expression to use to compute the new value of each changed field and a $\mt{WHERE}$ clause.
adamc@545 1591 $$\begin{array}{l}
adamc@545 1592 \mt{val} \; \mt{update} : \mt{unchanged} ::: \{\mt{Type}\} \to \mt{changed} :: \{\mt{Type}\} \to \lambda [\mt{changed} \sim \mt{unchanged}] \\
adamc@658 1593 \hspace{.1in} \Rightarrow \$(\mt{map} \; (\mt{sql\_exp} \; [\mt{T} = \mt{changed} \rc \mt{unchanged}] \; [] \; []) \; \mt{changed}) \\
adamc@545 1594 \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 1595 \end{array}$$
adamc@545 1596
adamc@545 1597 A $\mt{DELETE}$ command is formed from a table and a $\mt{WHERE}$ clause.
adamc@545 1598 $$\begin{array}{l}
adamc@545 1599 \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 1600 \end{array}$$
adamc@545 1601
adamc@546 1602 \subsubsection{Sequences}
adamc@546 1603
adamc@546 1604 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 1605
adamc@546 1606 $$\begin{array}{l}
adamc@546 1607 \mt{type} \; \mt{sql\_sequence} \\
adamc@546 1608 \mt{val} \; \mt{nextval} : \mt{sql\_sequence} \to \mt{transaction} \; \mt{int}
adamc@546 1609 \end{array}$$
adamc@546 1610
adamc@546 1611
adamc@547 1612 \subsection{XML}
adamc@547 1613
adamc@547 1614 Ur/Web's library contains an encoding of XML syntax and semantic constraints. We make no effort to follow the standards governing XML schemas. Rather, XML fragments are viewed more as values of ML datatypes, and we only track which tags are allowed inside which other tags.
adamc@547 1615
adamc@547 1616 The basic XML type family has arguments respectively indicating the \emph{context} of a fragment, the fields that the fragment expects to be bound on entry (and their types), and the fields that the fragment will bind (and their types). Contexts are a record-based ``poor man's subtyping'' encoding, with each possible set of valid tags corresponding to a different context record. The arguments dealing with field binding are only relevant to HTML forms.
adamc@547 1617 $$\begin{array}{l}
adamc@547 1618 \mt{con} \; \mt{xml} :: \{\mt{Unit}\} \to \{\mt{Type}\} \to \{\mt{Type}\} \to \mt{Type}
adamc@547 1619 \end{array}$$
adamc@547 1620
adamc@547 1621 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 1622 $$\begin{array}{l}
adamc@547 1623 \mt{con} \; \mt{tag} :: \{\mt{Type}\} \to \{\mt{Unit}\} \to \{\mt{Unit}\} \to \{\mt{Type}\} \to \{\mt{Type}\} \to \mt{Type}
adamc@547 1624 \end{array}$$
adamc@547 1625
adamc@547 1626 Literal text may be injected into XML as ``CDATA.''
adamc@547 1627 $$\begin{array}{l}
adamc@547 1628 \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 1629 \end{array}$$
adamc@547 1630
adamc@547 1631 There is a function for producing an XML tree with a particular tag at its root.
adamc@547 1632 $$\begin{array}{l}
adamc@547 1633 \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 1634 \hspace{.1in} \to \mt{useOuter} ::: \{\mt{Type}\} \to \mt{useInner} ::: \{\mt{Type}\} \to \mt{bindOuter} ::: \{\mt{Type}\} \to \mt{bindInner} ::: \{\mt{Type}\} \\
adamc@787 1635 \hspace{.1in} \to \lambda [\mt{attrsGiven} \sim \mt{attrsAbsent}] \; [\mt{useOuter} \sim \mt{useInner}] \; [\mt{bindOuter} \sim \mt{bindInner}] \\
adamc@787 1636 \hspace{.1in} \Rightarrow \mt{option} \; \mt{css\_class} \\
adamc@787 1637 \hspace{.1in} \to \$\mt{attrsGiven} \\
adamc@547 1638 \hspace{.1in} \to \mt{tag} \; (\mt{attrsGiven} \rc \mt{attrsAbsent}) \; \mt{ctxOuter} \; \mt{ctxInner} \; \mt{useOuter} \; \mt{bindOuter} \\
adamc@547 1639 \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 1640 \end{array}$$
adamc@787 1641 Note that any tag may be assigned a CSS class. This is the sole way of making use of the values produced by $\mt{style}$ declarations. Ur/Web itself doesn't deal with the syntax or semantics of style sheets; they can be linked via URLs with \texttt{link} tags. However, Ur/Web does make it easy to calculate upper bounds on usage of CSS classes through program analysis.
adamc@547 1642
adamc@547 1643 Two XML fragments may be concatenated.
adamc@547 1644 $$\begin{array}{l}
adamc@547 1645 \mt{val} \; \mt{join} : \mt{ctx} ::: \{\mt{Unit}\} \to \mt{use_1} ::: \{\mt{Type}\} \to \mt{bind_1} ::: \{\mt{Type}\} \to \mt{bind_2} ::: \{\mt{Type}\} \\
adamc@547 1646 \hspace{.1in} \to \lambda [\mt{use_1} \sim \mt{bind_1}] \; [\mt{bind_1} \sim \mt{bind_2}] \\
adamc@547 1647 \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 1648 \end{array}$$
adamc@547 1649
adamc@547 1650 Finally, any XML fragment may be updated to ``claim'' to use more form fields than it does.
adamc@547 1651 $$\begin{array}{l}
adamc@547 1652 \mt{val} \; \mt{useMore} : \mt{ctx} ::: \{\mt{Unit}\} \to \mt{use_1} ::: \{\mt{Type}\} \to \mt{use_2} ::: \{\mt{Type}\} \to \mt{bind} ::: \{\mt{Type}\} \to \lambda [\mt{use_1} \sim \mt{use_2}] \\
adamc@547 1653 \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 1654 \end{array}$$
adamc@547 1655
adamc@547 1656 We will not list here the different HTML tags and related functions from the standard library. They should be easy enough to understand from the code in \texttt{basis.urs}. The set of tags in the library is not yet claimed to be complete for HTML standards.
adamc@547 1657
adamc@547 1658 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 1659 $$\begin{array}{l}
adamc@547 1660 \mt{val} \; \mt{error} : \mt{t} ::: \mt{Type} \to \mt{xml} \; [\mt{Body}] \; [] \; [] \to \mt{t}
adamc@547 1661 \end{array}$$
adamc@547 1662
adamc@549 1663
adamc@701 1664 \subsection{Client-Side Programming}
adamc@659 1665
adamc@701 1666 Ur/Web supports running code on web browsers, via automatic compilation to JavaScript.
adamc@701 1667
adamc@701 1668 \subsubsection{The Basics}
adamc@701 1669
adamc@701 1670 Clients can open alert dialog boxes, in the usual annoying JavaScript way.
adamc@701 1671 $$\begin{array}{l}
adamc@701 1672 \mt{val} \; \mt{alert} : \mt{string} \to \mt{transaction} \; \mt{unit}
adamc@701 1673 \end{array}$$
adamc@701 1674
adamc@701 1675 Any transaction may be run in a new thread with the $\mt{spawn}$ function.
adamc@701 1676 $$\begin{array}{l}
adamc@701 1677 \mt{val} \; \mt{spawn} : \mt{transaction} \; \mt{unit} \to \mt{transaction} \; \mt{unit}
adamc@701 1678 \end{array}$$
adamc@701 1679
adamc@701 1680 The current thread can be paused for at least a specified number of milliseconds.
adamc@701 1681 $$\begin{array}{l}
adamc@701 1682 \mt{val} \; \mt{sleep} : \mt{int} \to \mt{transaction} \; \mt{unit}
adamc@701 1683 \end{array}$$
adamc@701 1684
adamc@787 1685 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 1686 $$\begin{array}{l}
adamc@787 1687 \mt{val} \; \mt{onError} : (\mt{xbody} \to \mt{transaction} \; \mt{unit}) \to \mt{transaction} \; \mt{unit} \\
adamc@787 1688 \mt{val} \; \mt{onFail} : (\mt{string} \to \mt{transaction} \; \mt{unit}) \to \mt{transaction} \; \mt{unit} \\
adamc@787 1689 \mt{val} \; \mt{onConnectFail} : \mt{transaction} \; \mt{unit} \to \mt{transaction} \; \mt{unit} \\
adamc@787 1690 \mt{val} \; \mt{onDisconnect} : \mt{transaction} \; \mt{unit} \to \mt{transaction} \; \mt{unit} \\
adamc@787 1691 \mt{val} \; \mt{onServerError} : (\mt{string} \to \mt{transaction} \; \mt{unit}) \to \mt{transaction} \; \mt{unit}
adamc@787 1692 \end{array}$$
adamc@787 1693
adamc@701 1694 \subsubsection{Functional-Reactive Page Generation}
adamc@701 1695
adamc@701 1696 Most approaches to ``AJAX''-style coding involve imperative manipulation of the DOM tree representing an HTML document's structure. Ur/Web follows the \emph{functional-reactive} approach instead. Programs may allocate mutable \emph{sources} of arbitrary types, and an HTML page is effectively a pure function over the latest values of the sources. The page is not mutated directly, but rather it changes automatically as the sources are mutated.
adamc@659 1697
adamc@659 1698 $$\begin{array}{l}
adamc@659 1699 \mt{con} \; \mt{source} :: \mt{Type} \to \mt{Type} \\
adamc@659 1700 \mt{val} \; \mt{source} : \mt{t} ::: \mt{Type} \to \mt{t} \to \mt{transaction} \; (\mt{source} \; \mt{t}) \\
adamc@659 1701 \mt{val} \; \mt{set} : \mt{t} ::: \mt{Type} \to \mt{source} \; \mt{t} \to \mt{t} \to \mt{transaction} \; \mt{unit} \\
adamc@659 1702 \mt{val} \; \mt{get} : \mt{t} ::: \mt{Type} \to \mt{source} \; \mt{t} \to \mt{transaction} \; \mt{t}
adamc@659 1703 \end{array}$$
adamc@659 1704
adamc@659 1705 Pure functions over sources are represented in a monad of \emph{signals}.
adamc@659 1706
adamc@659 1707 $$\begin{array}{l}
adamc@659 1708 \mt{con} \; \mt{signal} :: \mt{Type} \to \mt{Type} \\
adamc@659 1709 \mt{val} \; \mt{signal\_monad} : \mt{monad} \; \mt{signal} \\
adamc@659 1710 \mt{val} \; \mt{signal} : \mt{t} ::: \mt{Type} \to \mt{source} \; \mt{t} \to \mt{signal} \; \mt{t}
adamc@659 1711 \end{array}$$
adamc@659 1712
adamc@659 1713 A reactive portion of an HTML page is injected with a $\mt{dyn}$ tag, which has a signal-valued attribute $\mt{Signal}$.
adamc@659 1714
adamc@659 1715 $$\begin{array}{l}
adamc@701 1716 \mt{val} \; \mt{dyn} : \mt{use} ::: \{\mt{Type}\} \to \mt{bind} ::: \{\mt{Type}\} \to \mt{unit} \\
adamc@701 1717 \hspace{.1in} \to \mt{tag} \; [\mt{Signal} = \mt{signal} \; (\mt{xml} \; \mt{body} \; \mt{use} \; \mt{bind})] \; \mt{body} \; [] \; \mt{use} \; \mt{bind}
adamc@659 1718 \end{array}$$
adamc@659 1719
adamc@701 1720 Transactions can be run on the client by including them in attributes like the $\mt{Onclick}$ attribute of $\mt{button}$, and GUI widgets like $\mt{ctextbox}$ have $\mt{Source}$ attributes that can be used to connect them to sources, so that their values can be read by code running because of, e.g., an $\mt{Onclick}$ event.
adamc@701 1721
adamc@701 1722 \subsubsection{Asynchronous Message-Passing}
adamc@701 1723
adamc@701 1724 To support asynchronous, ``server push'' delivery of messages to clients, any client that might need to receive an asynchronous message is assigned a unique ID. These IDs may be retrieved both on the client and on the server, during execution of code related to a client.
adamc@701 1725
adamc@701 1726 $$\begin{array}{l}
adamc@701 1727 \mt{type} \; \mt{client} \\
adamc@701 1728 \mt{val} \; \mt{self} : \mt{transaction} \; \mt{client}
adamc@701 1729 \end{array}$$
adamc@701 1730
adamc@701 1731 \emph{Channels} are the means of message-passing. Each channel is created in the context of a client and belongs to that client; no other client may receive the channel's messages. Each channel type includes the type of values that may be sent over the channel. Sending and receiving are asynchronous, in the sense that a client need not be ready to receive a message right away. Rather, sent messages may queue up, waiting to be processed.
adamc@701 1732
adamc@701 1733 $$\begin{array}{l}
adamc@701 1734 \mt{con} \; \mt{channel} :: \mt{Type} \to \mt{Type} \\
adamc@701 1735 \mt{val} \; \mt{channel} : \mt{t} ::: \mt{Type} \to \mt{transaction} \; (\mt{channel} \; \mt{t}) \\
adamc@701 1736 \mt{val} \; \mt{send} : \mt{t} ::: \mt{Type} \to \mt{channel} \; \mt{t} \to \mt{t} \to \mt{transaction} \; \mt{unit} \\
adamc@701 1737 \mt{val} \; \mt{recv} : \mt{t} ::: \mt{Type} \to \mt{channel} \; \mt{t} \to \mt{transaction} \; \mt{t}
adamc@701 1738 \end{array}$$
adamc@701 1739
adamc@701 1740 The $\mt{channel}$ and $\mt{send}$ operations may only be executed on the server, and $\mt{recv}$ may only be executed on a client. Neither clients nor channels may be passed as arguments from clients to server-side functions, so persistent channels can only be maintained by storing them in the database and looking them up using the current client ID or some application-specific value as a key.
adamc@701 1741
adamc@701 1742 Clients and channels live only as long as the web browser page views that they are associated with. When a user surfs away, his client and its channels will be garbage-collected, after that user is not heard from for the timeout period. Garbage collection deletes any database row that contains a client or channel directly. Any reference to one of these types inside an $\mt{option}$ is set to $\mt{None}$ instead. Both kinds of handling have the flavor of weak pointers, and that is a useful way to think about clients and channels in the database.
adamc@701 1743
adamc@659 1744
adamc@549 1745 \section{Ur/Web Syntax Extensions}
adamc@549 1746
adamc@549 1747 Ur/Web features some syntactic shorthands for building values using the functions from the last section. This section sketches the grammar of those extensions. We write spans of syntax inside brackets to indicate that they are optional.
adamc@549 1748
adamc@549 1749 \subsection{SQL}
adamc@549 1750
adamc@786 1751 \subsubsection{\label{tables}Table Declarations}
adamc@786 1752
adamc@788 1753 $\mt{table}$ declarations may include constraints, via these grammar rules.
adamc@788 1754 $$\begin{array}{rrcll}
adamc@788 1755 \textrm{Declarations} & d &::=& \mt{table} \; x : c \; [pk[,]] \; cts \\
adamc@788 1756 \textrm{Primary key constraints} & pk &::=& \mt{PRIMARY} \; \mt{KEY} \; K \\
adamc@788 1757 \textrm{Keys} & K &::=& f \mid (f, (f,)^+) \\
adamc@788 1758 \textrm{Constraint sets} & cts &::=& \mt{CONSTRAINT} f \; ct \mid cts, cts \mid \{\{e\}\} \\
adamc@788 1759 \textrm{Constraints} & ct &::=& \mt{UNIQUE} \; K \mid \mt{CHECK} \; E \\
adamc@788 1760 &&& \mid \mt{FOREIGN} \; \mt{KEY} \; K \; \mt{REFERENCES} \; F \; (K) \; [\mt{ON} \; \mt{DELETE} \; pr] \; [\mt{ON} \; \mt{UPDATE} \; pr] \\
adamc@788 1761 \textrm{Foreign tables} & F &::=& x \mid \{\{e\}\} \\
adamc@788 1762 \textrm{Propagation modes} & pr &::=& \mt{NO} \; \mt{ACTION} \mid \mt{RESTRICT} \mid \mt{CASCADE} \mid \mt{SET} \; \mt{NULL}
adamc@788 1763 \end{array}$$
adamc@788 1764
adamc@788 1765 A signature item $\mt{table} \; \mt{x} : \mt{c}$ is actually elaborated into two signature items: $\mt{con} \; \mt{x\_hidden\_constraints} :: \{\{\mt{Unit}\}\}$ and $\mt{val} \; \mt{x} : \mt{sql\_table} \; \mt{c} \; \mt{x\_hidden\_constraints}$. This is appropriate for common cases where client code doesn't care which keys a table has. It's also possible to include constraints after a $\mt{table}$ signature item, with the same syntax as for $\mt{table}$ declarations. This may look like dependent typing, but it's just a convenience. The constraints are type-checked to determine a constructor $u$ to include in $\mt{val} \; \mt{x} : \mt{sql\_table} \; \mt{c} \; (u \rc \mt{x\_hidden\_constraints})$, and then the expressions are thrown away. Nonetheless, it can be useful for documentation purposes to include table constraint details in signatures. Note that the automatic generation of $\mt{x\_hidden\_constraints}$ leads to a kind of free subtyping with respect to which constraints are defined.
adamc@788 1766
adamc@788 1767
adamc@549 1768 \subsubsection{Queries}
adamc@549 1769
adamc@550 1770 Queries $Q$ are added to the rules for expressions $e$.
adamc@550 1771
adamc@549 1772 $$\begin{array}{rrcll}
adamc@550 1773 \textrm{Queries} & Q &::=& (q \; [\mt{ORDER} \; \mt{BY} \; (E \; [o],)^+] \; [\mt{LIMIT} \; N] \; [\mt{OFFSET} \; N]) \\
adamc@549 1774 \textrm{Pre-queries} & q &::=& \mt{SELECT} \; P \; \mt{FROM} \; T,^+ \; [\mt{WHERE} \; E] \; [\mt{GROUP} \; \mt{BY} \; p,^+] \; [\mt{HAVING} \; E] \\
adamc@549 1775 &&& \mid q \; R \; q \\
adamc@549 1776 \textrm{Relational operators} & R &::=& \mt{UNION} \mid \mt{INTERSECT} \mid \mt{EXCEPT}
adamc@549 1777 \end{array}$$
adamc@549 1778
adamc@549 1779 $$\begin{array}{rrcll}
adamc@549 1780 \textrm{Projections} & P &::=& \ast & \textrm{all columns} \\
adamc@549 1781 &&& p,^+ & \textrm{particular columns} \\
adamc@549 1782 \textrm{Pre-projections} & p &::=& t.f & \textrm{one column from a table} \\
adamc@558 1783 &&& t.\{\{c\}\} & \textrm{a record of columns from a table (of kind $\{\mt{Type}\}$)} \\
adamc@549 1784 \textrm{Table names} & t &::=& x & \textrm{constant table name (automatically capitalized)} \\
adamc@549 1785 &&& X & \textrm{constant table name} \\
adamc@549 1786 &&& \{\{c\}\} & \textrm{computed table name (of kind $\mt{Name}$)} \\
adamc@549 1787 \textrm{Column names} & f &::=& X & \textrm{constant column name} \\
adamc@549 1788 &&& \{c\} & \textrm{computed column name (of kind $\mt{Name}$)} \\
adamc@549 1789 \textrm{Tables} & T &::=& x & \textrm{table variable, named locally by its own capitalization} \\
adamc@549 1790 &&& x \; \mt{AS} \; t & \textrm{table variable, with local name} \\
adamc@549 1791 &&& \{\{e\}\} \; \mt{AS} \; t & \textrm{computed table expression, with local name} \\
adamc@549 1792 \textrm{SQL expressions} & E &::=& p & \textrm{column references} \\
adamc@549 1793 &&& X & \textrm{named expression references} \\
adamc@549 1794 &&& \{\{e\}\} & \textrm{injected native Ur expressions} \\
adamc@549 1795 &&& \{e\} & \textrm{computed expressions, probably using $\mt{sql\_exp}$ directly} \\
adamc@549 1796 &&& \mt{TRUE} \mid \mt{FALSE} & \textrm{boolean constants} \\
adamc@549 1797 &&& \ell & \textrm{primitive type literals} \\
adamc@549 1798 &&& \mt{NULL} & \textrm{null value (injection of $\mt{None}$)} \\
adamc@549 1799 &&& E \; \mt{IS} \; \mt{NULL} & \textrm{nullness test} \\
adamc@549 1800 &&& n & \textrm{nullary operators} \\
adamc@549 1801 &&& u \; E & \textrm{unary operators} \\
adamc@549 1802 &&& E \; b \; E & \textrm{binary operators} \\
adamc@549 1803 &&& \mt{COUNT}(\ast) & \textrm{count number of rows} \\
adamc@549 1804 &&& a(E) & \textrm{other aggregate function} \\
adamc@549 1805 &&& (E) & \textrm{explicit precedence} \\
adamc@549 1806 \textrm{Nullary operators} & n &::=& \mt{CURRENT\_TIMESTAMP} \\
adamc@549 1807 \textrm{Unary operators} & u &::=& \mt{NOT} \\
adamc@549 1808 \textrm{Binary operators} & b &::=& \mt{AND} \mid \mt{OR} \mid \neq \mid < \mid \leq \mid > \mid \geq \\
adamc@549 1809 \textrm{Aggregate functions} & a &::=& \mt{AVG} \mid \mt{SUM} \mid \mt{MIN} \mid \mt{MAX} \\
adamc@550 1810 \textrm{Directions} & o &::=& \mt{ASC} \mid \mt{DESC} \\
adamc@549 1811 \textrm{SQL integer} & N &::=& n \mid \{e\} \\
adamc@549 1812 \end{array}$$
adamc@549 1813
adamc@549 1814 Additionally, an SQL expression may be inserted into normal Ur code with the syntax $(\mt{SQL} \; E)$ or $(\mt{WHERE} \; E)$.
adamc@549 1815
adamc@550 1816 \subsubsection{DML}
adamc@550 1817
adamc@550 1818 DML commands $D$ are added to the rules for expressions $e$.
adamc@550 1819
adamc@550 1820 $$\begin{array}{rrcll}
adamc@550 1821 \textrm{Commands} & D &::=& (\mt{INSERT} \; \mt{INTO} \; T^E \; (f,^+) \; \mt{VALUES} \; (E,^+)) \\
adamc@550 1822 &&& (\mt{UPDATE} \; T^E \; \mt{SET} \; (f = E,)^+ \; \mt{WHERE} \; E) \\
adamc@550 1823 &&& (\mt{DELETE} \; \mt{FROM} \; T^E \; \mt{WHERE} \; E) \\
adamc@550 1824 \textrm{Table expressions} & T^E &::=& x \mid \{\{e\}\}
adamc@550 1825 \end{array}$$
adamc@550 1826
adamc@550 1827 Inside $\mt{UPDATE}$ and $\mt{DELETE}$ commands, lone variables $X$ are interpreted as references to columns of the implicit table $\mt{T}$, rather than to named expressions.
adamc@549 1828
adamc@551 1829 \subsection{XML}
adamc@551 1830
adamc@551 1831 XML fragments $L$ are added to the rules for expressions $e$.
adamc@551 1832
adamc@551 1833 $$\begin{array}{rrcll}
adamc@551 1834 \textrm{XML fragments} & L &::=& \texttt{<xml/>} \mid \texttt{<xml>}l^*\texttt{</xml>} \\
adamc@551 1835 \textrm{XML pieces} & l &::=& \textrm{text} & \textrm{cdata} \\
adamc@551 1836 &&& \texttt{<}g\texttt{/>} & \textrm{tag with no children} \\
adamc@551 1837 &&& \texttt{<}g\texttt{>}l^*\texttt{</}x\texttt{>} & \textrm{tag with children} \\
adamc@559 1838 &&& \{e\} & \textrm{computed XML fragment} \\
adamc@559 1839 &&& \{[e]\} & \textrm{injection of an Ur expression, via the $\mt{Top}.\mt{txt}$ function} \\
adamc@551 1840 \textrm{Tag} & g &::=& h \; (x = v)^* \\
adamc@551 1841 \textrm{Tag head} & h &::=& x & \textrm{tag name} \\
adamc@551 1842 &&& h\{c\} & \textrm{constructor parameter} \\
adamc@551 1843 \textrm{Attribute value} & v &::=& \ell & \textrm{literal value} \\
adamc@551 1844 &&& \{e\} & \textrm{computed value} \\
adamc@551 1845 \end{array}$$
adamc@551 1846
adamc@552 1847
adamc@553 1848 \section{The Structure of Web Applications}
adamc@553 1849
adamc@553 1850 A web application is built from a series of modules, with one module, the last one appearing in the \texttt{.urp} file, designated as the main module. The signature of the main module determines the URL entry points to the application. Such an entry point should have type $\mt{unit} \to \mt{transaction} \; \mt{page}$, where $\mt{page}$ is a type synonym for top-level HTML pages, defined in $\mt{Basis}$. If such a function is at the top level of main module $M$, it will be accessible at URI \texttt{/M/f}, and so on for more deeply-nested functions, as described in Section \ref{tag} below.
adamc@553 1851
adamc@553 1852 When the standalone web server receives a request for a known page, it calls the function for that page, ``running'' the resulting transaction to produce the page to return to the client. Pages link to other pages with the \texttt{link} attribute of the \texttt{a} HTML tag. A link has type $\mt{transaction} \; \mt{page}$, and the semantics of a link are that this transaction should be run to compute the result page, when the link is followed. Link targets are assigned URL names in the same way as top-level entry points.
adamc@553 1853
adamc@553 1854 HTML forms are handled in a similar way. The $\mt{action}$ attribute of a $\mt{submit}$ form tag takes a value of type $\$\mt{use} \to \mt{transaction} \; \mt{page}$, where $\mt{use}$ is a kind-$\{\mt{Type}\}$ record of the form fields used by this action handler. Action handlers are assigned URL patterns in the same way as above.
adamc@553 1855
adamc@558 1856 For both links and actions, direct arguments and local variables mentioned implicitly via closures are automatically included in serialized form in URLs, in the order in which they appear in the source code.
adamc@553 1857
adamc@660 1858 Ur/Web programs generally mix server- and client-side code in a fairly transparent way. The one important restriction is that mixed client-server code must encapsulate all server-side pieces within named functions. This is because execution of such pieces will be implemented by explicit calls to the remote web server, and it is useful to get the programmer's help in designing the interface to be used. For example, this makes it easier to allow a client running an old version of an application to continue interacting with a server that has been upgraded to a new version, if the programmer took care to keep the interfaces of all of the old remote calls the same. The functions implementing these services are assigned names in the same way as normal web entry points, by using module structure.
adamc@660 1859
adamc@789 1860 \medskip
adamc@789 1861
adamc@789 1862 The HTTP standard suggests that GET requests only be used in ways that generate no side effects. Side effecting operations should use POST requests instead. The Ur/Web compiler enforces this rule strictly, via a simple conservative program analysis. Any page that may have a side effect must be accessed through a form, all of which use POST requests. A page is judged to have a side effect if its code depends syntactically on any of the side-effecting, server-side FFI functions. Links, forms, and most client-side event handlers are not followed during this syntactic traversal, but \texttt{<body onload=\{...\}>} handlers \emph{are} examined, since they run right away and could just as well be considered parts of main page handlers.
adamc@789 1863
adamc@789 1864 Ur/Web includes a kind of automatic protection against cross site request forgery attacks. Whenever any page execution can have side effects and can also read at least one cookie value, all cookie values must be signed cryptographically, to ensure that the user has come to the current page by submitting a form on a real page generated by the proper server. Signing and signature checking are inserted automatically by the compiler. This prevents attacks like phishing schemes where users are directed to counterfeit pages with forms that submit to your application, where a user's cookies might be submitted without his knowledge, causing some undesired side effect.
adamc@789 1865
adamc@553 1866
adamc@552 1867 \section{Compiler Phases}
adamc@552 1868
adamc@552 1869 The Ur/Web compiler is unconventional in that it relies on a kind of \emph{heuristic compilation}. Not all valid programs will compile successfully. Informally, programs fail to compile when they are ``too higher order.'' Compiler phases do their best to eliminate different kinds of higher order-ness, but some programs just won't compile. This is a trade-off for producing very efficient executables. Compiled Ur/Web programs use native C representations and require no garbage collection.
adamc@552 1870
adamc@552 1871 In this section, we step through the main phases of compilation, noting what consequences each phase has for effective programming.
adamc@552 1872
adamc@552 1873 \subsection{Parse}
adamc@552 1874
adamc@552 1875 The compiler reads a \texttt{.urp} file, figures out which \texttt{.urs} and \texttt{.ur} files it references, and combines them all into what is conceptually a single sequence of declarations in the core language of Section \ref{core}.
adamc@552 1876
adamc@552 1877 \subsection{Elaborate}
adamc@552 1878
adamc@552 1879 This is where type inference takes place, translating programs into an explicit form with no more wildcards. This phase is the most likely source of compiler error messages.
adamc@552 1880
adamc@552 1881 \subsection{Unnest}
adamc@552 1882
adamc@552 1883 Named local function definitions are moved to the top level, to avoid the need to generate closures.
adamc@552 1884
adamc@552 1885 \subsection{Corify}
adamc@552 1886
adamc@552 1887 Module system features are compiled away, through inlining of functor definitions at application sites. Afterward, most abstraction boundaries are broken, facilitating optimization.
adamc@552 1888
adamc@552 1889 \subsection{Especialize}
adamc@552 1890
adamc@552 1891 Functions are specialized to particular argument patterns. This is an important trick for avoiding the need to maintain any closures at runtime.
adamc@552 1892
adamc@552 1893 \subsection{Untangle}
adamc@552 1894
adamc@552 1895 Remove unnecessary mutual recursion, splitting recursive groups into strongly-connected components.
adamc@552 1896
adamc@552 1897 \subsection{Shake}
adamc@552 1898
adamc@552 1899 Remove all definitions not needed to run the page handlers that are visible in the signature of the last module listed in the \texttt{.urp} file.
adamc@552 1900
adamc@661 1901 \subsection{Rpcify}
adamc@661 1902
adamc@661 1903 Pieces of code are determined to be client-side, server-side, neither, or both, by figuring out which standard library functions might be needed to execute them. Calls to server-side functions (e.g., $\mt{query}$) within mixed client-server code are identified and replaced with explicit remote calls. Some mixed functions may be converted to continuation-passing style to facilitate this transformation.
adamc@661 1904
adamc@661 1905 \subsection{Untangle, Shake}
adamc@661 1906
adamc@661 1907 Repeat these simplifications.
adamc@661 1908
adamc@553 1909 \subsection{\label{tag}Tag}
adamc@552 1910
adamc@552 1911 Assign a URL name to each link and form action. It is important that these links and actions are written as applications of named functions, because such names are used to generate URL patterns. A URL pattern has a name built from the full module path of the named function, followed by the function name, with all pieces separated by slashes. The path of a functor application is based on the name given to the result, rather than the path of the functor itself.
adamc@552 1912
adamc@552 1913 \subsection{Reduce}
adamc@552 1914
adamc@552 1915 Apply definitional equality rules to simplify the program as much as possible. This effectively includes inlining of every non-recursive definition.
adamc@552 1916
adamc@552 1917 \subsection{Unpoly}
adamc@552 1918
adamc@552 1919 This phase specializes polymorphic functions to the specific arguments passed to them in the program. If the program contains real polymorphic recursion, Unpoly will be insufficient to avoid later error messages about too much polymorphism.
adamc@552 1920
adamc@552 1921 \subsection{Specialize}
adamc@552 1922
adamc@558 1923 Replace uses of parameterized datatypes with versions specialized to specific parameters. As for Unpoly, this phase will not be effective enough in the presence of polymorphic recursion or other fancy uses of impredicative polymorphism.
adamc@552 1924
adamc@552 1925 \subsection{Shake}
adamc@552 1926
adamc@558 1927 Here the compiler repeats the earlier Shake phase.
adamc@552 1928
adamc@552 1929 \subsection{Monoize}
adamc@552 1930
adamc@552 1931 Programs are translated to a new intermediate language without polymorphism or non-$\mt{Type}$ constructors. Error messages may pop up here if earlier phases failed to remove such features.
adamc@552 1932
adamc@552 1933 This is the stage at which concrete names are generated for cookies, tables, and sequences. They are named following the same convention as for links and actions, based on module path information saved from earlier stages. Table and sequence names separate path elements with underscores instead of slashes, and they are prefixed by \texttt{uw\_}.
adamc@664 1934
adamc@552 1935 \subsection{MonoOpt}
adamc@552 1936
adamc@552 1937 Simple algebraic laws are applied to simplify the program, focusing especially on efficient imperative generation of HTML pages.
adamc@552 1938
adamc@552 1939 \subsection{MonoUntangle}
adamc@552 1940
adamc@552 1941 Unnecessary mutual recursion is broken up again.
adamc@552 1942
adamc@552 1943 \subsection{MonoReduce}
adamc@552 1944
adamc@552 1945 Equivalents of the definitional equality rules are applied to simplify programs, with inlining again playing a major role.
adamc@552 1946
adamc@552 1947 \subsection{MonoShake, MonoOpt}
adamc@552 1948
adamc@552 1949 Unneeded declarations are removed, and basic optimizations are repeated.
adamc@552 1950
adamc@552 1951 \subsection{Fuse}
adamc@552 1952
adamc@552 1953 The compiler tries to simplify calls to recursive functions whose results are immediately written as page output. The write action is pushed inside the function definitions to avoid allocation of intermediate results.
adamc@552 1954
adamc@552 1955 \subsection{MonoUntangle, MonoShake}
adamc@552 1956
adamc@552 1957 Fuse often creates more opportunities to remove spurious mutual recursion.
adamc@552 1958
adamc@552 1959 \subsection{Pathcheck}
adamc@552 1960
adamc@552 1961 The compiler checks that no link or action name has been used more than once.
adamc@552 1962
adamc@552 1963 \subsection{Cjrize}
adamc@552 1964
adamc@552 1965 The program is translated to what is more or less a subset of C. If any use of functions as data remains at this point, the compiler will complain.
adamc@552 1966
adamc@552 1967 \subsection{C Compilation and Linking}
adamc@552 1968
adamc@552 1969 The output of the last phase is pretty-printed as C source code and passed to GCC.
adamc@552 1970
adamc@552 1971
adamc@524 1972 \end{document}