Ur/Web: doc/manual.tex annotate

annotate doc/manual.tex @ 713:baaae037e7f6

Retry failed record summary unifications at the end, in hopes that more has been learned

author	Adam Chlipala <adamc@hcoop.net>
date	Thu, 09 Apr 2009 14:59:29 -0400
parents	f963356b53fd
children	ec0a0dd0ca12

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@555	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; and MLton, the whole-program optimizing compiler for Standard ML. 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@555	62 apt-get install mlton 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@556	130 A few other named directives are supported. \texttt{prefix PREFIX} sets the prefix included before every URI within the generated application; the default is \texttt{/}. \texttt{exe FILENAME} sets the filename to which to write the output executable; the default for file \texttt{P.urp} is \texttt{P.exe}. \texttt{debug} saves some intermediate C files, which is mostly useful to help in debugging the compiler itself. \texttt{profile} generates an executable that may be used with gprof.
adamc@556	131
adamc@701	132 \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@701	133
adamc@701	134
adamc@557	135 \subsection{Building an Application}
adamc@557	136
adamc@557	137 To compile project \texttt{P.urp}, simply run
adamc@557	138 \begin{verbatim}
adamc@557	139 urweb P
adamc@557	140 \end{verbatim}
adamc@558	141 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	142
adamc@557	143 To time how long the different compiler phases run, without generating an executable, run
adamc@557	144 \begin{verbatim}
adamc@557	145 urweb -timing P
adamc@557	146 \end{verbatim}
adamc@557	147
adamc@556	148
adamc@529	149 \section{Ur Syntax}
adamc@529	150
adamc@529	151 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 tables, sequences, and cookies.
adamc@524	152
adamc@524	153 \subsection{Lexical Conventions}
adamc@524	154
adamc@524	155 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	156
adamc@524	157 \begin{center}
adamc@524	158 \begin{tabular}{rl}
adamc@524	159 \textbf{\LaTeX} & \textbf{ASCII} \\
adamc@524	160 $\to$ & \cd{->} \\
adamc@652	161 $\longrightarrow$ & \cd{-->} \\
adamc@524	162 $\times$ & \cd{*} \\
adamc@524	163 $\lambda$ & \cd{fn} \\
adamc@524	164 $\Rightarrow$ & \cd{=>} \\
adamc@652	165 $\Longrightarrow$ & \cd{==>} \\
adamc@529	166 $\neq$ & \cd{<>} \\
adamc@529	167 $\leq$ & \cd{<=} \\
adamc@529	168 $\geq$ & \cd{>=} \\
adamc@524	169 \\
adamc@524	170 $x$ & Normal textual identifier, not beginning with an uppercase letter \\
adamc@525	171 $X$ & Normal textual identifier, beginning with an uppercase letter \\
adamc@524	172 \end{tabular}
adamc@524	173 \end{center}
adamc@524	174
adamc@525	175 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	176
adamc@526	177 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	178
adamc@527	179 This version of the manual doesn't include operator precedences; see \texttt{src/urweb.grm} for that.
adamc@527	180
adamc@552	181 \subsection{\label{core}Core Syntax}
adamc@524	182
adamc@524	183 \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	184 $$\begin{array}{rrcll}
adamc@524	185 \textrm{Kinds} & \kappa &::=& \mt{Type} & \textrm{proper types} \\
adamc@525	186 &&& \mt{Unit} & \textrm{the trivial constructor} \\
adamc@525	187 &&& \mt{Name} & \textrm{field names} \\
adamc@525	188 &&& \kappa \to \kappa & \textrm{type-level functions} \\
adamc@525	189 &&& \{\kappa\} & \textrm{type-level records} \\
adamc@525	190 &&& (\kappa\times^+) & \textrm{type-level tuples} \\
adamc@652	191 &&& X & \textrm{variable} \\
adamc@652	192 &&& X \longrightarrow k & \textrm{kind-polymorphic type-level function} \\
adamc@529	193 &&& \_\_ & \textrm{wildcard} \\
adamc@525	194 &&& (\kappa) & \textrm{explicit precedence} \\
adamc@524	195 \end{array}$$
adamc@524	196
adamc@524	197 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	198 $$\begin{array}{rrcll}
adamc@524	199 \textrm{Explicitness} & ? &::=& :: & \textrm{explicit} \\
adamc@558	200 &&& ::: & \textrm{implicit}
adamc@524	201 \end{array}$$
adamc@524	202
adamc@524	203 \emph{Constructors} are the main class of compile-time-only data. They include proper types and are classified by kinds.
adamc@524	204 $$\begin{array}{rrcll}
adamc@524	205 \textrm{Constructors} & c, \tau &::=& (c) :: \kappa & \textrm{kind annotation} \\
adamc@530	206 &&& \hat{x} & \textrm{constructor variable} \\
adamc@524	207 \\
adamc@525	208 &&& \tau \to \tau & \textrm{function type} \\
adamc@525	209 &&& x \; ? \; \kappa \to \tau & \textrm{polymorphic function type} \\
adamc@652	210 &&& X \longrightarrow \tau & \textrm{kind-polymorphic function type} \\
adamc@525	211 &&& \$ c & \textrm{record type} \\
adamc@524	212 \\
adamc@525	213 &&& c \; c & \textrm{type-level function application} \\
adamc@530	214 &&& \lambda x \; :: \; \kappa \Rightarrow c & \textrm{type-level function abstraction} \\
adamc@524	215 \\
adamc@652	216 &&& X \Longrightarrow c & \textrm{type-level kind-polymorphic function abstraction} \\
adamc@655	217 &&& c [\kappa] & \textrm{type-level kind-polymorphic function application} \\
adamc@652	218 \\
adamc@525	219 &&& () & \textrm{type-level unit} \\
adamc@525	220 &&& \#X & \textrm{field name} \\
adamc@524	221 \\
adamc@525	222 &&& [(c = c)^*] & \textrm{known-length type-level record} \\
adamc@525	223 &&& c \rc c & \textrm{type-level record concatenation} \\
adamc@652	224 &&& \mt{map} & \textrm{type-level record map} \\
adamc@524	225 \\
adamc@558	226 &&& (c,^+) & \textrm{type-level tuple} \\
adamc@525	227 &&& c.n & \textrm{type-level tuple projection ($n \in \mathbb N^+$)} \\
adamc@524	228 \\
adamc@652	229 &&& [c \sim c] \Rightarrow \tau & \textrm{guarded type} \\
adamc@524	230 \\
adamc@529	231 &&& \_ :: \kappa & \textrm{wildcard} \\
adamc@525	232 &&& (c) & \textrm{explicit precedence} \\
adamc@530	233 \\
adamc@530	234 \textrm{Qualified uncapitalized variables} & \hat{x} &::=& x & \textrm{not from a module} \\
adamc@530	235 &&& M.x & \textrm{projection from a module} \\
adamc@525	236 \end{array}$$
adamc@525	237
adamc@655	238 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	239
adamc@525	240 Modules of the module system are described by \emph{signatures}.
adamc@525	241 $$\begin{array}{rrcll}
adamc@525	242 \textrm{Signatures} & S &::=& \mt{sig} \; s^* \; \mt{end} & \textrm{constant} \\
adamc@525	243 &&& X & \textrm{variable} \\
adamc@525	244 &&& \mt{functor}(X : S) : S & \textrm{functor} \\
adamc@529	245 &&& S \; \mt{where} \; \mt{con} \; x = c & \textrm{concretizing an abstract constructor} \\
adamc@525	246 &&& M.X & \textrm{projection from a module} \\
adamc@525	247 \\
adamc@525	248 \textrm{Signature items} & s &::=& \mt{con} \; x :: \kappa & \textrm{abstract constructor} \\
adamc@525	249 &&& \mt{con} \; x :: \kappa = c & \textrm{concrete constructor} \\
adamc@528	250 &&& \mt{datatype} \; x \; x^* = dc\mid^+ & \textrm{algebraic datatype definition} \\
adamc@529	251 &&& \mt{datatype} \; x = \mt{datatype} \; M.x & \textrm{algebraic datatype import} \\
adamc@525	252 &&& \mt{val} \; x : \tau & \textrm{value} \\
adamc@525	253 &&& \mt{structure} \; X : S & \textrm{sub-module} \\
adamc@525	254 &&& \mt{signature} \; X = S & \textrm{sub-signature} \\
adamc@525	255 &&& \mt{include} \; S & \textrm{signature inclusion} \\
adamc@525	256 &&& \mt{constraint} \; c \sim c & \textrm{record disjointness constraint} \\
adamc@654	257 &&& \mt{class} \; x :: \kappa & \textrm{abstract constructor class} \\
adamc@654	258 &&& \mt{class} \; x :: \kappa = c & \textrm{concrete constructor class} \\
adamc@525	259 \\
adamc@525	260 \textrm{Datatype constructors} & dc &::=& X & \textrm{nullary constructor} \\
adamc@525	261 &&& X \; \mt{of} \; \tau & \textrm{unary constructor} \\
adamc@524	262 \end{array}$$
adamc@524	263
adamc@526	264 \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	265 $$\begin{array}{rrcll}
adamc@526	266 \textrm{Patterns} & p &::=& \_ & \textrm{wildcard} \\
adamc@526	267 &&& x & \textrm{variable} \\
adamc@526	268 &&& \ell & \textrm{constant} \\
adamc@526	269 &&& \hat{X} & \textrm{nullary constructor} \\
adamc@526	270 &&& \hat{X} \; p & \textrm{unary constructor} \\
adamc@526	271 &&& \{(x = p,)^*\} & \textrm{rigid record pattern} \\
adamc@526	272 &&& \{(x = p,)^+, \ldots\} & \textrm{flexible record pattern} \\
adamc@527	273 &&& (p) & \textrm{explicit precedence} \\
adamc@526	274 \\
adamc@529	275 \textrm{Qualified capitalized variables} & \hat{X} &::=& X & \textrm{not from a module} \\
adamc@526	276 &&& M.X & \textrm{projection from a module} \\
adamc@526	277 \end{array}$$
adamc@526	278
adamc@527	279 \emph{Expressions} are the main run-time entities, corresponding to both ``expressions'' and ``statements'' in mainstream imperative languages.
adamc@527	280 $$\begin{array}{rrcll}
adamc@527	281 \textrm{Expressions} & e &::=& e : \tau & \textrm{type annotation} \\
adamc@529	282 &&& \hat{x} & \textrm{variable} \\
adamc@529	283 &&& \hat{X} & \textrm{datatype constructor} \\
adamc@527	284 &&& \ell & \textrm{constant} \\
adamc@527	285 \\
adamc@527	286 &&& e \; e & \textrm{function application} \\
adamc@527	287 &&& \lambda x : \tau \Rightarrow e & \textrm{function abstraction} \\
adamc@527	288 &&& e [c] & \textrm{polymorphic function application} \\
adamc@527	289 &&& \lambda x \; ? \; \kappa \Rightarrow e & \textrm{polymorphic function abstraction} \\
adamc@655	290 &&& e [\kappa] & \textrm{kind-polymorphic function application} \\
adamc@652	291 &&& X \Longrightarrow e & \textrm{kind-polymorphic function abstraction} \\
adamc@527	292 \\
adamc@527	293 &&& \{(c = e,)^*\} & \textrm{known-length record} \\
adamc@527	294 &&& e.c & \textrm{record field projection} \\
adamc@527	295 &&& e \rc e & \textrm{record concatenation} \\
adamc@527	296 &&& e \rcut c & \textrm{removal of a single record field} \\
adamc@527	297 &&& e \rcutM c & \textrm{removal of multiple record fields} \\
adamc@527	298 \\
adamc@527	299 &&& \mt{let} \; ed^* \; \mt{in} \; e \; \mt{end} & \textrm{local definitions} \\
adamc@527	300 \\
adamc@527	301 &&& \mt{case} \; e \; \mt{of} \; (p \Rightarrow e\|)^+ & \textrm{pattern matching} \\
adamc@527	302 \\
adamc@654	303 &&& \lambda [c \sim c] \Rightarrow e & \textrm{guarded expression abstraction} \\
adamc@654	304 &&& e \; ! & \textrm{guarded expression application} \\
adamc@527	305 \\
adamc@527	306 &&& \_ & \textrm{wildcard} \\
adamc@527	307 &&& (e) & \textrm{explicit precedence} \\
adamc@527	308 \\
adamc@527	309 \textrm{Local declarations} & ed &::=& \cd{val} \; x : \tau = e & \textrm{non-recursive value} \\
adamc@527	310 &&& \cd{val} \; \cd{rec} \; (x : \tau = e \; \cd{and})^+ & \textrm{mutually-recursive values} \\
adamc@527	311 \end{array}$$
adamc@527	312
adamc@655	313 As with constructors, we include both abstraction and application for kind polymorphism, but applications are only inferred internally.
adamc@655	314
adamc@528	315 \emph{Declarations} primarily bring new symbols into context.
adamc@528	316 $$\begin{array}{rrcll}
adamc@528	317 \textrm{Declarations} & d &::=& \mt{con} \; x :: \kappa = c & \textrm{constructor synonym} \\
adamc@528	318 &&& \mt{datatype} \; x \; x^* = dc\mid^+ & \textrm{algebraic datatype definition} \\
adamc@529	319 &&& \mt{datatype} \; x = \mt{datatype} \; M.x & \textrm{algebraic datatype import} \\
adamc@528	320 &&& \mt{val} \; x : \tau = e & \textrm{value} \\
adamc@528	321 &&& \mt{val} \; \cd{rec} \; (x : \tau = e \; \mt{and})^+ & \textrm{mutually-recursive values} \\
adamc@528	322 &&& \mt{structure} \; X : S = M & \textrm{module definition} \\
adamc@528	323 &&& \mt{signature} \; X = S & \textrm{signature definition} \\
adamc@528	324 &&& \mt{open} \; M & \textrm{module inclusion} \\
adamc@528	325 &&& \mt{constraint} \; c \sim c & \textrm{record disjointness constraint} \\
adamc@528	326 &&& \mt{open} \; \mt{constraints} \; M & \textrm{inclusion of just the constraints from a module} \\
adamc@528	327 &&& \mt{table} \; x : c & \textrm{SQL table} \\
adamc@528	328 &&& \mt{sequence} \; x & \textrm{SQL sequence} \\
adamc@535	329 &&& \mt{cookie} \; x : \tau & \textrm{HTTP cookie} \\
adamc@654	330 &&& \mt{class} \; x :: \kappa = c & \textrm{concrete constructor class} \\
adamc@528	331 \\
adamc@529	332 \textrm{Modules} & M &::=& \mt{struct} \; d^* \; \mt{end} & \textrm{constant} \\
adamc@529	333 &&& X & \textrm{variable} \\
adamc@529	334 &&& M.X & \textrm{projection} \\
adamc@529	335 &&& M(M) & \textrm{functor application} \\
adamc@529	336 &&& \mt{functor}(X : S) : S = M & \textrm{functor abstraction} \\
adamc@528	337 \end{array}$$
adamc@528	338
adamc@528	339 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	340
adamc@529	341 \subsection{Shorthands}
adamc@529	342
adamc@529	343 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	344
adamc@529	345 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	346
adamc@529	347 A record type may be written $\{(c = c,)^\}$, which elaborates to $\$[(c = c,)^]$.
adamc@529	348
adamc@533	349 The notation $[c_1, \ldots, c_n]$ is shorthand for $[c_1 = (), \ldots, c_n = ()]$.
adamc@533	350
adamc@529	351 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	352
adamc@654	353 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	354
adamc@529	355 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	356
adamc@529	357 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	358
adamc@654	359 A signature item or declaration $\mt{class} \; x = \lambda y \Rightarrow c$ may be abbreviated $\mt{class} \; x \; y = c$.
adamc@529	360
adamc@654	361 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	362
adamc@654	363 At the expression level, an analogue is available of the composite $\lambda$ form for constructors. We define the language of binders as $b ::= x \mid (x : \tau) \mid (x \; ? \; \kappa) \mid X \mid [c \sim c]$. A lone variable $x$ as a binder stands for an expression variable of unspecified type.
adamc@529	364
adamc@529	365 A $\mt{val}$ or $\mt{val} \; \mt{rec}$ declaration may include expression binders before the equal sign, following the binder grammar from the last paragraph. Such declarations are elaborated into versions that add additional $\lambda$s to the fronts of the righthand sides, as appropriate. The keyword $\mt{fun}$ is a synonym for $\mt{val} \; \mt{rec}$.
adamc@529	366
adamc@529	367 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	368
adamc@529	369 A declaration $\mt{table} \; x : \{(c = c,)^\}$ is elaborated into $\mt{table} \; x : [(c = c,)^]$
adamc@529	370
adamc@529	371 The syntax $\mt{where} \; \mt{type}$ is an alternate form of $\mt{where} \; \mt{con}$.
adamc@529	372
adamc@529	373 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	374
adamc@529	375 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	376
adamc@529	377 A signature item $\mt{table} \; x : c$ is shorthand for $\mt{val} \; x : \mt{Basis}.\mt{sql\_table} \; c$. $\mt{sequence} \; x$ is short for $\mt{val} \; x : \mt{Basis}.\mt{sql\_sequence}$, and $\mt{cookie} \; x : \tau$ is shorthand for $\mt{val} \; x : \mt{Basis}.\mt{http\_cookie} \; \tau$.
adamc@529	378
adamc@530	379
adamc@530	380 \section{Static Semantics}
adamc@530	381
adamc@530	382 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	383
adamc@530	384 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	385 \begin{itemize}
adamc@655	386 \item $\Gamma \vdash \kappa$ expresses kind well-formedness.
adamc@530	387 \item $\Gamma \vdash c :: \kappa$ assigns a kind to a constructor in a context.
adamc@530	388 \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	389 \item $\Gamma \vdash c \hookrightarrow C$ proves that record constructor $c$ decomposes into set $C$ of field names and record constructors.
adamc@530	390 \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	391 \item $\Gamma \vdash e : \tau$ is a standard typing judgment.
adamc@534	392 \item $\Gamma \vdash p \leadsto \Gamma; \tau$ combines typing of patterns with calculation of which new variables they bind.
adamc@537	393 \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	394 \item $\Gamma \vdash S \equiv S$ is the signature equivalence judgment.
adamc@536	395 \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	396 \item $\Gamma \vdash M : S$ is the module signature checking judgment.
adamc@537	397 \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	398 \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	399 \end{itemize}
adamc@530	400
adamc@655	401
adamc@655	402 \subsection{Kind Well-Formedness}
adamc@655	403
adamc@655	404 $$\infer{\Gamma \vdash \mt{Type}}{}
adamc@655	405 \quad \infer{\Gamma \vdash \mt{Unit}}{}
adamc@655	406 \quad \infer{\Gamma \vdash \mt{Name}}{}
adamc@655	407 \quad \infer{\Gamma \vdash \kappa_1 \to \kappa_2}{
adamc@655	408 \Gamma \vdash \kappa_1
adamc@655	409 & \Gamma \vdash \kappa_2
adamc@655	410 }
adamc@655	411 \quad \infer{\Gamma \vdash \{\kappa\}}{
adamc@655	412 \Gamma \vdash \kappa
adamc@655	413 }
adamc@655	414 \quad \infer{\Gamma \vdash (\kappa_1 \times \ldots \times \kappa_n)}{
adamc@655	415 \forall i: \Gamma \vdash \kappa_i
adamc@655	416 }$$
adamc@655	417
adamc@655	418 $$\infer{\Gamma \vdash X}{
adamc@655	419 X \in \Gamma
adamc@655	420 }
adamc@655	421 \quad \infer{\Gamma \vdash X \longrightarrow \kappa}{
adamc@655	422 \Gamma, X \vdash \kappa
adamc@655	423 }$$
adamc@655	424
adamc@530	425 \subsection{Kinding}
adamc@530	426
adamc@655	427 We write $[X \mapsto \kappa_1]\kappa_2$ for capture-avoiding substitution of $\kappa_1$ for $X$ in $\kappa_2$.
adamc@655	428
adamc@530	429 $$\infer{\Gamma \vdash (c) :: \kappa :: \kappa}{
adamc@530	430 \Gamma \vdash c :: \kappa
adamc@530	431 }
adamc@530	432 \quad \infer{\Gamma \vdash x :: \kappa}{
adamc@530	433 x :: \kappa \in \Gamma
adamc@530	434 }
adamc@530	435 \quad \infer{\Gamma \vdash x :: \kappa}{
adamc@530	436 x :: \kappa = c \in \Gamma
adamc@530	437 }$$
adamc@530	438
adamc@530	439 $$\infer{\Gamma \vdash M.x :: \kappa}{
adamc@537	440 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537	441 & \mt{proj}(M, \overline{s}, \mt{con} \; x) = \kappa
adamc@530	442 }
adamc@530	443 \quad \infer{\Gamma \vdash M.x :: \kappa}{
adamc@537	444 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537	445 & \mt{proj}(M, \overline{s}, \mt{con} \; x) = (\kappa, c)
adamc@530	446 }$$
adamc@530	447
adamc@530	448 $$\infer{\Gamma \vdash \tau_1 \to \tau_2 :: \mt{Type}}{
adamc@530	449 \Gamma \vdash \tau_1 :: \mt{Type}
adamc@530	450 & \Gamma \vdash \tau_2 :: \mt{Type}
adamc@530	451 }
adamc@530	452 \quad \infer{\Gamma \vdash x \; ? \: \kappa \to \tau :: \mt{Type}}{
adamc@530	453 \Gamma, x :: \kappa \vdash \tau :: \mt{Type}
adamc@530	454 }
adamc@655	455 \quad \infer{\Gamma \vdash X \longrightarrow \tau :: \mt{Type}}{
adamc@655	456 \Gamma, X \vdash \tau :: \mt{Type}
adamc@655	457 }
adamc@530	458 \quad \infer{\Gamma \vdash \$c :: \mt{Type}}{
adamc@530	459 \Gamma \vdash c :: \{\mt{Type}\}
adamc@530	460 }$$
adamc@530	461
adamc@530	462 $$\infer{\Gamma \vdash c_1 \; c_2 :: \kappa_2}{
adamc@530	463 \Gamma \vdash c_1 :: \kappa_1 \to \kappa_2
adamc@530	464 & \Gamma \vdash c_2 :: \kappa_1
adamc@530	465 }
adamc@530	466 \quad \infer{\Gamma \vdash \lambda x \; :: \; \kappa_1 \Rightarrow c :: \kappa_1 \to \kappa_2}{
adamc@530	467 \Gamma, x :: \kappa_1 \vdash c :: \kappa_2
adamc@530	468 }$$
adamc@530	469
adamc@655	470 $$\infer{\Gamma \vdash c[\kappa'] :: [X \mapsto \kappa']\kappa}{
adamc@655	471 \Gamma \vdash c :: X \to \kappa
adamc@655	472 & \Gamma \vdash \kappa'
adamc@655	473 }
adamc@655	474 \quad \infer{\Gamma \vdash X \Longrightarrow c :: X \to \kappa}{
adamc@655	475 \Gamma, X \vdash c :: \kappa
adamc@655	476 }$$
adamc@655	477
adamc@530	478 $$\infer{\Gamma \vdash () :: \mt{Unit}}{}
adamc@530	479 \quad \infer{\Gamma \vdash \#X :: \mt{Name}}{}$$
adamc@530	480
adamc@530	481 $$\infer{\Gamma \vdash [\overline{c_i = c'_i}] :: \{\kappa\}}{
adamc@530	482 \forall i: \Gamma \vdash c_i : \mt{Name}
adamc@530	483 & \Gamma \vdash c'_i :: \kappa
adamc@530	484 & \forall i \neq j: \Gamma \vdash c_i \sim c_j
adamc@530	485 }
adamc@530	486 \quad \infer{\Gamma \vdash c_1 \rc c_2 :: \{\kappa\}}{
adamc@530	487 \Gamma \vdash c_1 :: \{\kappa\}
adamc@530	488 & \Gamma \vdash c_2 :: \{\kappa\}
adamc@530	489 & \Gamma \vdash c_1 \sim c_2
adamc@530	490 }$$
adamc@530	491
adamc@655	492 $$\infer{\Gamma \vdash \mt{map} :: (\kappa_1 \to \kappa_2) \to \{\kappa_1\} \to \{\kappa_2\}}{}$$
adamc@530	493
adamc@573	494 $$\infer{\Gamma \vdash (\overline c) :: (\kappa_1 \times \ldots \times \kappa_n)}{
adamc@573	495 \forall i: \Gamma \vdash c_i :: \kappa_i
adamc@530	496 }
adamc@573	497 \quad \infer{\Gamma \vdash c.i :: \kappa_i}{
adamc@573	498 \Gamma \vdash c :: (\kappa_1 \times \ldots \times \kappa_n)
adamc@530	499 }$$
adamc@530	500
adamc@655	501 $$\infer{\Gamma \vdash \lambda [c_1 \sim c_2] \Rightarrow \tau :: \mt{Type}}{
adamc@655	502 \Gamma \vdash c_1 :: \{\kappa\}
adamc@530	503 & \Gamma \vdash c_2 :: \{\kappa'\}
adamc@655	504 & \Gamma, c_1 \sim c_2 \vdash \tau :: \mt{Type}
adamc@530	505 }$$
adamc@530	506
adamc@531	507 \subsection{Record Disjointness}
adamc@531	508
adamc@531	509 $$\infer{\Gamma \vdash c_1 \sim c_2}{
adamc@558	510 \Gamma \vdash c_1 \hookrightarrow C_1
adamc@558	511 & \Gamma \vdash c_2 \hookrightarrow C_2
adamc@558	512 & \forall c'_1 \in C_1, c'_2 \in C_2: \Gamma \vdash c'_1 \sim c'_2
adamc@531	513 }
adamc@531	514 \quad \infer{\Gamma \vdash X \sim X'}{
adamc@531	515 X \neq X'
adamc@531	516 }$$
adamc@531	517
adamc@531	518 $$\infer{\Gamma \vdash c_1 \sim c_2}{
adamc@531	519 c'_1 \sim c'_2 \in \Gamma
adamc@558	520 & \Gamma \vdash c'_1 \hookrightarrow C_1
adamc@558	521 & \Gamma \vdash c'_2 \hookrightarrow C_2
adamc@558	522 & c_1 \in C_1
adamc@558	523 & c_2 \in C_2
adamc@531	524 }$$
adamc@531	525
adamc@531	526 $$\infer{\Gamma \vdash c \hookrightarrow \{c\}}{}
adamc@531	527 \quad \infer{\Gamma \vdash [\overline{c = c'}] \hookrightarrow \{\overline{c}\}}{}
adamc@531	528 \quad \infer{\Gamma \vdash c_1 \rc c_2 \hookrightarrow C_1 \cup C_2}{
adamc@531	529 \Gamma \vdash c_1 \hookrightarrow C_1
adamc@531	530 & \Gamma \vdash c_2 \hookrightarrow C_2
adamc@531	531 }
adamc@531	532 \quad \infer{\Gamma \vdash c \hookrightarrow C}{
adamc@531	533 \Gamma \vdash c \equiv c'
adamc@531	534 & \Gamma \vdash c' \hookrightarrow C
adamc@531	535 }
adamc@531	536 \quad \infer{\Gamma \vdash \mt{map} \; f \; c \hookrightarrow C}{
adamc@531	537 \Gamma \vdash c \hookrightarrow C
adamc@531	538 }$$
adamc@531	539
adamc@541	540 \subsection{\label{definitional}Definitional Equality}
adamc@532	541
adamc@655	542 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	543
adamc@532	544 $$\infer{\Gamma \vdash c \equiv c}{}
adamc@532	545 \quad \infer{\Gamma \vdash c_1 \equiv c_2}{
adamc@532	546 \Gamma \vdash c_2 \equiv c_1
adamc@532	547 }
adamc@532	548 \quad \infer{\Gamma \vdash c_1 \equiv c_3}{
adamc@532	549 \Gamma \vdash c_1 \equiv c_2
adamc@532	550 & \Gamma \vdash c_2 \equiv c_3
adamc@532	551 }
adamc@532	552 \quad \infer{\Gamma \vdash \mathcal C[c_1] \equiv \mathcal C[c_2]}{
adamc@532	553 \Gamma \vdash c_1 \equiv c_2
adamc@532	554 }$$
adamc@532	555
adamc@532	556 $$\infer{\Gamma \vdash x \equiv c}{
adamc@532	557 x :: \kappa = c \in \Gamma
adamc@532	558 }
adamc@532	559 \quad \infer{\Gamma \vdash M.x \equiv c}{
adamc@537	560 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537	561 & \mt{proj}(M, \overline{s}, \mt{con} \; x) = (\kappa, c)
adamc@532	562 }
adamc@532	563 \quad \infer{\Gamma \vdash (\overline c).i \equiv c_i}{}$$
adamc@532	564
adamc@532	565 $$\infer{\Gamma \vdash (\lambda x :: \kappa \Rightarrow c) \; c' \equiv [x \mapsto c'] c}{}
adamc@655	566 \quad \infer{\Gamma \vdash (X \Longrightarrow c) [\kappa] \equiv [X \mapsto \kappa] c}{}$$
adamc@655	567
adamc@655	568 $$\infer{\Gamma \vdash c_1 \rc c_2 \equiv c_2 \rc c_1}{}
adamc@532	569 \quad \infer{\Gamma \vdash c_1 \rc (c_2 \rc c_3) \equiv (c_1 \rc c_2) \rc c_3}{}$$
adamc@532	570
adamc@532	571 $$\infer{\Gamma \vdash [] \rc c \equiv c}{}
adamc@532	572 \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	573
adamc@655	574 $$\infer{\Gamma \vdash \mt{map} \; f \; [] \equiv []}{}
adamc@655	575 \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	576
adamc@532	577 $$\infer{\Gamma \vdash \mt{map} \; (\lambda x \Rightarrow x) \; c \equiv c}{}
adamc@655	578 \quad \infer{\Gamma \vdash \mt{map} \; f \; (\mt{map} \; f' \; c)
adamc@655	579 \equiv \mt{map} \; (\lambda x \Rightarrow f \; (f' \; x)) \; c}{}$$
adamc@532	580
adamc@532	581 $$\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	582
adamc@534	583 \subsection{Expression Typing}
adamc@533	584
adamc@533	585 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	586
adamc@533	587 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	588
adamc@533	589 $$\infer{\Gamma \vdash e : \tau : \tau}{
adamc@533	590 \Gamma \vdash e : \tau
adamc@533	591 }
adamc@533	592 \quad \infer{\Gamma \vdash e : \tau}{
adamc@533	593 \Gamma \vdash e : \tau'
adamc@533	594 & \Gamma \vdash \tau' \equiv \tau
adamc@533	595 }
adamc@533	596 \quad \infer{\Gamma \vdash \ell : T(\ell)}{}$$
adamc@533	597
adamc@533	598 $$\infer{\Gamma \vdash x : \mathcal I(\tau)}{
adamc@533	599 x : \tau \in \Gamma
adamc@533	600 }
adamc@533	601 \quad \infer{\Gamma \vdash M.x : \mathcal I(\tau)}{
adamc@537	602 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537	603 & \mt{proj}(M, \overline{s}, \mt{val} \; x) = \tau
adamc@533	604 }
adamc@533	605 \quad \infer{\Gamma \vdash X : \mathcal I(\tau)}{
adamc@533	606 X : \tau \in \Gamma
adamc@533	607 }
adamc@533	608 \quad \infer{\Gamma \vdash M.X : \mathcal I(\tau)}{
adamc@537	609 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537	610 & \mt{proj}(M, \overline{s}, \mt{val} \; X) = \tau
adamc@533	611 }$$
adamc@533	612
adamc@533	613 $$\infer{\Gamma \vdash e_1 \; e_2 : \tau_2}{
adamc@533	614 \Gamma \vdash e_1 : \tau_1 \to \tau_2
adamc@533	615 & \Gamma \vdash e_2 : \tau_1
adamc@533	616 }
adamc@533	617 \quad \infer{\Gamma \vdash \lambda x : \tau_1 \Rightarrow e : \tau_1 \to \tau_2}{
adamc@533	618 \Gamma, x : \tau_1 \vdash e : \tau_2
adamc@533	619 }$$
adamc@533	620
adamc@533	621 $$\infer{\Gamma \vdash e [c] : [x \mapsto c]\tau}{
adamc@533	622 \Gamma \vdash e : x :: \kappa \to \tau
adamc@533	623 & \Gamma \vdash c :: \kappa
adamc@533	624 }
adamc@533	625 \quad \infer{\Gamma \vdash \lambda x \; ? \; \kappa \Rightarrow e : x \; ? \; \kappa \to \tau}{
adamc@533	626 \Gamma, x :: \kappa \vdash e : \tau
adamc@533	627 }$$
adamc@533	628
adamc@655	629 $$\infer{\Gamma \vdash e [\kappa] : [X \mapsto \kappa]\tau}{
adamc@655	630 \Gamma \vdash e : X \longrightarrow \tau
adamc@655	631 & \Gamma \vdash \kappa
adamc@655	632 }
adamc@655	633 \quad \infer{\Gamma \vdash X \Longrightarrow e : X \longrightarrow \tau}{
adamc@655	634 \Gamma, X \vdash e : \tau
adamc@655	635 }$$
adamc@655	636
adamc@533	637 $$\infer{\Gamma \vdash \{\overline{c = e}\} : \{\overline{c : \tau}\}}{
adamc@533	638 \forall i: \Gamma \vdash c_i :: \mt{Name}
adamc@533	639 & \Gamma \vdash e_i : \tau_i
adamc@533	640 & \forall i \neq j: \Gamma \vdash c_i \sim c_j
adamc@533	641 }
adamc@533	642 \quad \infer{\Gamma \vdash e.c : \tau}{
adamc@533	643 \Gamma \vdash e : \$([c = \tau] \rc c')
adamc@533	644 }
adamc@533	645 \quad \infer{\Gamma \vdash e_1 \rc e_2 : \$(c_1 \rc c_2)}{
adamc@533	646 \Gamma \vdash e_1 : \$c_1
adamc@533	647 & \Gamma \vdash e_2 : \$c_2
adamc@573	648 & \Gamma \vdash c_1 \sim c_2
adamc@533	649 }$$
adamc@533	650
adamc@533	651 $$\infer{\Gamma \vdash e \rcut c : \$c'}{
adamc@533	652 \Gamma \vdash e : \$([c = \tau] \rc c')
adamc@533	653 }
adamc@533	654 \quad \infer{\Gamma \vdash e \rcutM c : \$c'}{
adamc@533	655 \Gamma \vdash e : \$(c \rc c')
adamc@533	656 }$$
adamc@533	657
adamc@533	658 $$\infer{\Gamma \vdash \mt{let} \; \overline{ed} \; \mt{in} \; e \; \mt{end} : \tau}{
adamc@533	659 \Gamma \vdash \overline{ed} \leadsto \Gamma'
adamc@533	660 & \Gamma' \vdash e : \tau
adamc@533	661 }
adamc@533	662 \quad \infer{\Gamma \vdash \mt{case} \; e \; \mt{of} \; \overline{p \Rightarrow e} : \tau}{
adamc@533	663 \forall i: \Gamma \vdash p_i \leadsto \Gamma_i, \tau'
adamc@533	664 & \Gamma_i \vdash e_i : \tau
adamc@533	665 }$$
adamc@533	666
adamc@573	667 $$\infer{\Gamma \vdash \lambda [c_1 \sim c_2] \Rightarrow e : \lambda [c_1 \sim c_2] \Rightarrow \tau}{
adamc@533	668 \Gamma \vdash c_1 :: \{\kappa\}
adamc@655	669 & \Gamma \vdash c_2 :: \{\kappa'\}
adamc@533	670 & \Gamma, c_1 \sim c_2 \vdash e : \tau
adamc@662	671 }
adamc@662	672 \quad \infer{\Gamma \vdash e \; ! : \tau}{
adamc@662	673 \Gamma \vdash e : [c_1 \sim c_2] \Rightarrow \tau
adamc@662	674 & \Gamma \vdash c_1 \sim c_2
adamc@533	675 }$$
adamc@533	676
adamc@534	677 \subsection{Pattern Typing}
adamc@534	678
adamc@534	679 $$\infer{\Gamma \vdash \_ \leadsto \Gamma; \tau}{}
adamc@534	680 \quad \infer{\Gamma \vdash x \leadsto \Gamma, x : \tau; \tau}{}
adamc@534	681 \quad \infer{\Gamma \vdash \ell \leadsto \Gamma; T(\ell)}{}$$
adamc@534	682
adamc@534	683 $$\infer{\Gamma \vdash X \leadsto \Gamma; \overline{[x_i \mapsto \tau'_i]}\tau}{
adamc@534	684 X : \overline{x ::: \mt{Type}} \to \tau \in \Gamma
adamc@534	685 & \textrm{$\tau$ not a function type}
adamc@534	686 }
adamc@534	687 \quad \infer{\Gamma \vdash X \; p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau}{
adamc@534	688 X : \overline{x ::: \mt{Type}} \to \tau'' \to \tau \in \Gamma
adamc@534	689 & \Gamma \vdash p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau''
adamc@534	690 }$$
adamc@534	691
adamc@534	692 $$\infer{\Gamma \vdash M.X \leadsto \Gamma; \overline{[x_i \mapsto \tau'_i]}\tau}{
adamc@537	693 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537	694 & \mt{proj}(M, \overline{s}, \mt{val} \; X) = \overline{x ::: \mt{Type}} \to \tau
adamc@534	695 & \textrm{$\tau$ not a function type}
adamc@534	696 }$$
adamc@534	697
adamc@534	698 $$\infer{\Gamma \vdash M.X \; p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau}{
adamc@537	699 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537	700 & \mt{proj}(M, \overline{s}, \mt{val} \; X) = \overline{x ::: \mt{Type}} \to \tau'' \to \tau
adamc@534	701 & \Gamma \vdash p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau''
adamc@534	702 }$$
adamc@534	703
adamc@534	704 $$\infer{\Gamma \vdash \{\overline{x = p}\} \leadsto \Gamma_n; \{\overline{x = \tau}\}}{
adamc@534	705 \Gamma_0 = \Gamma
adamc@534	706 & \forall i: \Gamma_i \vdash p_i \leadsto \Gamma_{i+1}; \tau_i
adamc@534	707 }
adamc@534	708 \quad \infer{\Gamma \vdash \{\overline{x = p}, \ldots\} \leadsto \Gamma_n; \$([\overline{x = \tau}] \rc c)}{
adamc@534	709 \Gamma_0 = \Gamma
adamc@534	710 & \forall i: \Gamma_i \vdash p_i \leadsto \Gamma_{i+1}; \tau_i
adamc@534	711 }$$
adamc@534	712
adamc@535	713 \subsection{Declaration Typing}
adamc@535	714
adamc@535	715 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	716
adamc@655	717 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	718
adamc@558	719 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	720 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	721
adamc@535	722 $$\infer{\Gamma \vdash \cdot \leadsto \Gamma}{}
adamc@535	723 \quad \infer{\Gamma \vdash d, \overline{d} \leadsto \Gamma''}{
adamc@535	724 \Gamma \vdash d \leadsto \Gamma'
adamc@535	725 & \Gamma' \vdash \overline{d} \leadsto \Gamma''
adamc@535	726 }$$
adamc@535	727
adamc@535	728 $$\infer{\Gamma \vdash \mt{con} \; x :: \kappa = c \leadsto \Gamma, x :: \kappa = c}{
adamc@535	729 \Gamma \vdash c :: \kappa
adamc@535	730 }
adamc@535	731 \quad \infer{\Gamma \vdash \mt{datatype} \; x \; \overline{y} = \overline{dc} \leadsto \Gamma'}{
adamc@535	732 \overline{y}; x; \Gamma, x :: \mt{Type}^{\mt{len}(\overline y)} \to \mt{Type} \vdash \overline{dc} \leadsto \Gamma'
adamc@535	733 }$$
adamc@535	734
adamc@535	735 $$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leadsto \Gamma'}{
adamc@537	736 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537	737 & \mt{proj}(M, \overline{s}, \mt{datatype} \; z) = (\overline{y}, \overline{dc})
adamc@535	738 & \overline{y}; x; \Gamma, x :: \mt{Type}^{\mt{len}(\overline y)} \to \mt{Type} = M.z \vdash \overline{dc} \leadsto \Gamma'
adamc@535	739 }$$
adamc@535	740
adamc@535	741 $$\infer{\Gamma \vdash \mt{val} \; x : \tau = e \leadsto \Gamma, x : \tau}{
adamc@535	742 \Gamma \vdash e : \tau
adamc@535	743 }$$
adamc@535	744
adamc@535	745 $$\infer{\Gamma \vdash \mt{val} \; \mt{rec} \; \overline{x : \tau = e} \leadsto \Gamma, \overline{x : \tau}}{
adamc@535	746 \forall i: \Gamma, \overline{x : \tau} \vdash e_i : \tau_i
adamc@535	747 & \textrm{$e_i$ starts with an expression $\lambda$, optionally preceded by constructor and disjointness $\lambda$s}
adamc@535	748 }$$
adamc@535	749
adamc@535	750 $$\infer{\Gamma \vdash \mt{structure} \; X : S = M \leadsto \Gamma, X : S}{
adamc@535	751 \Gamma \vdash M : S
adamc@558	752 & \textrm{ $M$ not a constant or application}
adamc@535	753 }
adamc@558	754 \quad \infer{\Gamma \vdash \mt{structure} \; X : S = M \leadsto \Gamma, X : \mt{selfify}(X, \overline{s})}{
adamc@558	755 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@539	756 }$$
adamc@539	757
adamc@539	758 $$\infer{\Gamma \vdash \mt{signature} \; X = S \leadsto \Gamma, X = S}{
adamc@535	759 \Gamma \vdash S
adamc@535	760 }$$
adamc@535	761
adamc@537	762 $$\infer{\Gamma \vdash \mt{open} \; M \leadsto \Gamma, \mathcal O(M, \overline{s})}{
adamc@537	763 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@535	764 }$$
adamc@535	765
adamc@535	766 $$\infer{\Gamma \vdash \mt{constraint} \; c_1 \sim c_2 \leadsto \Gamma}{
adamc@535	767 \Gamma \vdash c_1 :: \{\kappa\}
adamc@535	768 & \Gamma \vdash c_2 :: \{\kappa\}
adamc@535	769 & \Gamma \vdash c_1 \sim c_2
adamc@535	770 }
adamc@537	771 \quad \infer{\Gamma \vdash \mt{open} \; \mt{constraints} \; M \leadsto \Gamma, \mathcal O_c(M, \overline{s})}{
adamc@537	772 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@535	773 }$$
adamc@535	774
adamc@535	775 $$\infer{\Gamma \vdash \mt{table} \; x : c \leadsto \Gamma, x : \mt{Basis}.\mt{sql\_table} \; c}{
adamc@535	776 \Gamma \vdash c :: \{\mt{Type}\}
adamc@535	777 }
adamc@535	778 \quad \infer{\Gamma \vdash \mt{sequence} \; x \leadsto \Gamma, x : \mt{Basis}.\mt{sql\_sequence}}{}$$
adamc@535	779
adamc@535	780 $$\infer{\Gamma \vdash \mt{cookie} \; x : \tau \leadsto \Gamma, x : \mt{Basis}.\mt{http\_cookie} \; \tau}{
adamc@535	781 \Gamma \vdash \tau :: \mt{Type}
adamc@535	782 }$$
adamc@535	783
adamc@655	784 $$\infer{\Gamma \vdash \mt{class} \; x :: \kappa = c \leadsto \Gamma, x :: \kappa \to \mt{Type} = c}{
adamc@655	785 \Gamma \vdash c :: \kappa \to \mt{Type}
adamc@535	786 }$$
adamc@535	787
adamc@535	788 $$\infer{\overline{y}; x; \Gamma \vdash \cdot \leadsto \Gamma}{}
adamc@535	789 \quad \infer{\overline{y}; x; \Gamma \vdash X \mid \overline{dc} \leadsto \Gamma', X : \overline{y ::: \mt{Type}} \to x \; \overline{y}}{
adamc@535	790 \overline{y}; x; \Gamma \vdash \overline{dc} \leadsto \Gamma'
adamc@535	791 }
adamc@535	792 \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	793 \overline{y}; x; \Gamma \vdash \overline{dc} \leadsto \Gamma'
adamc@535	794 }$$
adamc@535	795
adamc@537	796 \subsection{Signature Item Typing}
adamc@537	797
adamc@537	798 We appeal to a signature item analogue of the $\mathcal O$ function from the last subsection.
adamc@537	799
adamc@537	800 $$\infer{\Gamma \vdash \cdot \leadsto \Gamma}{}
adamc@537	801 \quad \infer{\Gamma \vdash s, \overline{s} \leadsto \Gamma''}{
adamc@537	802 \Gamma \vdash s \leadsto \Gamma'
adamc@537	803 & \Gamma' \vdash \overline{s} \leadsto \Gamma''
adamc@537	804 }$$
adamc@537	805
adamc@537	806 $$\infer{\Gamma \vdash \mt{con} \; x :: \kappa \leadsto \Gamma, x :: \kappa}{}
adamc@537	807 \quad \infer{\Gamma \vdash \mt{con} \; x :: \kappa = c \leadsto \Gamma, x :: \kappa = c}{
adamc@537	808 \Gamma \vdash c :: \kappa
adamc@537	809 }
adamc@537	810 \quad \infer{\Gamma \vdash \mt{datatype} \; x \; \overline{y} = \overline{dc} \leadsto \Gamma'}{
adamc@537	811 \overline{y}; x; \Gamma, x :: \mt{Type}^{\mt{len}(\overline y)} \to \mt{Type} \vdash \overline{dc} \leadsto \Gamma'
adamc@537	812 }$$
adamc@537	813
adamc@537	814 $$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leadsto \Gamma'}{
adamc@537	815 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537	816 & \mt{proj}(M, \overline{s}, \mt{datatype} \; z) = (\overline{y}, \overline{dc})
adamc@537	817 & \overline{y}; x; \Gamma, x :: \mt{Type}^{\mt{len}(\overline y)} \to \mt{Type} = M.z \vdash \overline{dc} \leadsto \Gamma'
adamc@537	818 }$$
adamc@537	819
adamc@537	820 $$\infer{\Gamma \vdash \mt{val} \; x : \tau \leadsto \Gamma, x : \tau}{
adamc@537	821 \Gamma \vdash \tau :: \mt{Type}
adamc@537	822 }$$
adamc@537	823
adamc@537	824 $$\infer{\Gamma \vdash \mt{structure} \; X : S \leadsto \Gamma, X : S}{
adamc@537	825 \Gamma \vdash S
adamc@537	826 }
adamc@537	827 \quad \infer{\Gamma \vdash \mt{signature} \; X = S \leadsto \Gamma, X = S}{
adamc@537	828 \Gamma \vdash S
adamc@537	829 }$$
adamc@537	830
adamc@537	831 $$\infer{\Gamma \vdash \mt{include} \; S \leadsto \Gamma, \mathcal O(\overline{s})}{
adamc@537	832 \Gamma \vdash S
adamc@537	833 & \Gamma \vdash S \equiv \mt{sig} \; \overline{s} \; \mt{end}
adamc@537	834 }$$
adamc@537	835
adamc@537	836 $$\infer{\Gamma \vdash \mt{constraint} \; c_1 \sim c_2 \leadsto \Gamma, c_1 \sim c_2}{
adamc@537	837 \Gamma \vdash c_1 :: \{\kappa\}
adamc@537	838 & \Gamma \vdash c_2 :: \{\kappa\}
adamc@537	839 }$$
adamc@537	840
adamc@655	841 $$\infer{\Gamma \vdash \mt{class} \; x :: \kappa = c \leadsto \Gamma, x :: \kappa \to \mt{Type} = c}{
adamc@655	842 \Gamma \vdash c :: \kappa \to \mt{Type}
adamc@537	843 }
adamc@655	844 \quad \infer{\Gamma \vdash \mt{class} \; x :: \kappa \leadsto \Gamma, x :: \kappa \to \mt{Type}}{}$$
adamc@537	845
adamc@536	846 \subsection{Signature Compatibility}
adamc@536	847
adamc@558	848 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	849
adamc@537	850 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	851
adamc@536	852 $$\infer{\Gamma \vdash S \equiv S}{}
adamc@536	853 \quad \infer{\Gamma \vdash S_1 \equiv S_2}{
adamc@536	854 \Gamma \vdash S_2 \equiv S_1
adamc@536	855 }
adamc@536	856 \quad \infer{\Gamma \vdash X \equiv S}{
adamc@536	857 X = S \in \Gamma
adamc@536	858 }
adamc@536	859 \quad \infer{\Gamma \vdash M.X \equiv S}{
adamc@537	860 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537	861 & \mt{proj}(M, \overline{s}, \mt{signature} \; X) = S
adamc@536	862 }$$
adamc@536	863
adamc@536	864 $$\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	865 \Gamma \vdash S \equiv \mt{sig} \; \overline{s^1} \; \mt{con} \; x :: \kappa \; \overline{s_2} \; \mt{end}
adamc@536	866 & \Gamma \vdash c :: \kappa
adamc@537	867 }
adamc@537	868 \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	869 \Gamma \vdash S \equiv \mt{sig} \; \overline{s} \; \mt{end}
adamc@536	870 }$$
adamc@536	871
adamc@536	872 $$\infer{\Gamma \vdash S_1 \leq S_2}{
adamc@536	873 \Gamma \vdash S_1 \equiv S_2
adamc@536	874 }
adamc@536	875 \quad \infer{\Gamma \vdash \mt{sig} \; \overline{s} \; \mt{end} \leq \mt{sig} \; \mt{end}}{}
adamc@537	876 \quad \infer{\Gamma \vdash \mt{sig} \; \overline{s} \; \mt{end} \leq \mt{sig} \; s' \; \overline{s'} \; \mt{end}}{
adamc@537	877 \Gamma \vdash \overline{s} \leq s'
adamc@537	878 & \Gamma \vdash s' \leadsto \Gamma'
adamc@537	879 & \Gamma' \vdash \mt{sig} \; \overline{s} \; \mt{end} \leq \mt{sig} \; \overline{s'} \; \mt{end}
adamc@537	880 }$$
adamc@537	881
adamc@537	882 $$\infer{\Gamma \vdash s \; \overline{s} \leq s'}{
adamc@537	883 \Gamma \vdash s \leq s'
adamc@537	884 }
adamc@537	885 \quad \infer{\Gamma \vdash s \; \overline{s} \leq s'}{
adamc@537	886 \Gamma \vdash s \leadsto \Gamma'
adamc@537	887 & \Gamma' \vdash \overline{s} \leq s'
adamc@536	888 }$$
adamc@536	889
adamc@536	890 $$\infer{\Gamma \vdash \mt{functor} (X : S_1) : S_2 \leq \mt{functor} (X : S'_1) : S'_2}{
adamc@536	891 \Gamma \vdash S'_1 \leq S_1
adamc@536	892 & \Gamma, X : S'_1 \vdash S_2 \leq S'_2
adamc@536	893 }$$
adamc@536	894
adamc@537	895 $$\infer{\Gamma \vdash \mt{con} \; x :: \kappa \leq \mt{con} \; x :: \kappa}{}
adamc@537	896 \quad \infer{\Gamma \vdash \mt{con} \; x :: \kappa = c \leq \mt{con} \; x :: \kappa}{}
adamc@558	897 \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	898
adamc@537	899 $$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leq \mt{con} \; x :: \mt{Type}^{\mt{len}(y)} \to \mt{Type}}{
adamc@537	900 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537	901 & \mt{proj}(M, \overline{s}, \mt{datatype} \; z) = (\overline{y}, \overline{dc})
adamc@537	902 }$$
adamc@537	903
adamc@655	904 $$\infer{\Gamma \vdash \mt{class} \; x :: \kappa \leq \mt{con} \; x :: \kappa \to \mt{Type}}{}
adamc@655	905 \quad \infer{\Gamma \vdash \mt{class} \; x :: \kappa = c \leq \mt{con} \; x :: \kappa \to \mt{Type}}{}$$
adamc@537	906
adamc@537	907 $$\infer{\Gamma \vdash \mt{con} \; x :: \kappa = c_1 \leq \mt{con} \; x :: \mt{\kappa} = c_2}{
adamc@537	908 \Gamma \vdash c_1 \equiv c_2
adamc@537	909 }
adamc@655	910 \quad \infer{\Gamma \vdash \mt{class} \; x :: \kappa = c_1 \leq \mt{con} \; x :: \kappa \to \mt{Type} = c_2}{
adamc@537	911 \Gamma \vdash c_1 \equiv c_2
adamc@537	912 }$$
adamc@537	913
adamc@537	914 $$\infer{\Gamma \vdash \mt{datatype} \; x \; \overline{y} = \overline{dc} \leq \mt{datatype} \; x \; \overline{y} = \overline{dc'}}{
adamc@537	915 \Gamma, \overline{y :: \mt{Type}} \vdash \overline{dc} \leq \overline{dc'}
adamc@537	916 }$$
adamc@537	917
adamc@537	918 $$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leq \mt{datatype} \; x \; \overline{y} = \overline{dc'}}{
adamc@537	919 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537	920 & \mt{proj}(M, \overline{s}, \mt{datatype} \; z) = (\overline{y}, \overline{dc})
adamc@537	921 & \Gamma, \overline{y :: \mt{Type}} \vdash \overline{dc} \leq \overline{dc'}
adamc@537	922 }$$
adamc@537	923
adamc@537	924 $$\infer{\Gamma \vdash \cdot \leq \cdot}{}
adamc@537	925 \quad \infer{\Gamma \vdash X; \overline{dc} \leq X; \overline{dc'}}{
adamc@537	926 \Gamma \vdash \overline{dc} \leq \overline{dc'}
adamc@537	927 }
adamc@537	928 \quad \infer{\Gamma \vdash X \; \mt{of} \; \tau_1; \overline{dc} \leq X \; \mt{of} \; \tau_2; \overline{dc'}}{
adamc@537	929 \Gamma \vdash \tau_1 \equiv \tau_2
adamc@537	930 & \Gamma \vdash \overline{dc} \leq \overline{dc'}
adamc@537	931 }$$
adamc@537	932
adamc@537	933 $$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leq \mt{datatype} \; x = \mt{datatype} \; M'.z'}{
adamc@537	934 \Gamma \vdash M.z \equiv M'.z'
adamc@537	935 }$$
adamc@537	936
adamc@537	937 $$\infer{\Gamma \vdash \mt{val} \; x : \tau_1 \leq \mt{val} \; x : \tau_2}{
adamc@537	938 \Gamma \vdash \tau_1 \equiv \tau_2
adamc@537	939 }
adamc@537	940 \quad \infer{\Gamma \vdash \mt{structure} \; X : S_1 \leq \mt{structure} \; X : S_2}{
adamc@537	941 \Gamma \vdash S_1 \leq S_2
adamc@537	942 }
adamc@537	943 \quad \infer{\Gamma \vdash \mt{signature} \; X = S_1 \leq \mt{signature} \; X = S_2}{
adamc@537	944 \Gamma \vdash S_1 \leq S_2
adamc@537	945 & \Gamma \vdash S_2 \leq S_1
adamc@537	946 }$$
adamc@537	947
adamc@537	948 $$\infer{\Gamma \vdash \mt{constraint} \; c_1 \sim c_2 \leq \mt{constraint} \; c'_1 \sim c'_2}{
adamc@537	949 \Gamma \vdash c_1 \equiv c'_1
adamc@537	950 & \Gamma \vdash c_2 \equiv c'_2
adamc@537	951 }$$
adamc@537	952
adamc@655	953 $$\infer{\Gamma \vdash \mt{class} \; x :: \kappa \leq \mt{class} \; x :: \kappa}{}
adamc@655	954 \quad \infer{\Gamma \vdash \mt{class} \; x :: \kappa = c \leq \mt{class} \; x :: \kappa}{}
adamc@655	955 \quad \infer{\Gamma \vdash \mt{class} \; x :: \kappa = c_1 \leq \mt{class} \; x :: \kappa = c_2}{
adamc@537	956 \Gamma \vdash c_1 \equiv c_2
adamc@537	957 }$$
adamc@537	958
adamc@538	959 \subsection{Module Typing}
adamc@538	960
adamc@538	961 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	962
adamc@538	963 $$\infer{\Gamma \vdash M : S}{
adamc@538	964 \Gamma \vdash M : S'
adamc@538	965 & \Gamma \vdash S' \leq S
adamc@538	966 }
adamc@538	967 \quad \infer{\Gamma \vdash \mt{struct} \; \overline{d} \; \mt{end} : \mt{sig} \; \mt{sigOf}(\overline{d}) \; \mt{end}}{
adamc@538	968 \Gamma \vdash \overline{d} \leadsto \Gamma'
adamc@538	969 }
adamc@538	970 \quad \infer{\Gamma \vdash X : S}{
adamc@538	971 X : S \in \Gamma
adamc@538	972 }$$
adamc@538	973
adamc@538	974 $$\infer{\Gamma \vdash M.X : S}{
adamc@538	975 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@538	976 & \mt{proj}(M, \overline{s}, \mt{structure} \; X) = S
adamc@538	977 }$$
adamc@538	978
adamc@538	979 $$\infer{\Gamma \vdash M_1(M_2) : [X \mapsto M_2]S_2}{
adamc@538	980 \Gamma \vdash M_1 : \mt{functor}(X : S_1) : S_2
adamc@538	981 & \Gamma \vdash M_2 : S_1
adamc@538	982 }
adamc@538	983 \quad \infer{\Gamma \vdash \mt{functor} (X : S_1) : S_2 = M : \mt{functor} (X : S_1) : S_2}{
adamc@538	984 \Gamma \vdash S_1
adamc@538	985 & \Gamma, X : S_1 \vdash S_2
adamc@538	986 & \Gamma, X : S_1 \vdash M : S_2
adamc@538	987 }$$
adamc@538	988
adamc@538	989 \begin{eqnarray*}
adamc@538	990 \mt{sigOf}(\cdot) &=& \cdot \\
adamc@538	991 \mt{sigOf}(s \; \overline{s'}) &=& \mt{sigOf}(s) \; \mt{sigOf}(\overline{s'}) \\
adamc@538	992 \\
adamc@538	993 \mt{sigOf}(\mt{con} \; x :: \kappa = c) &=& \mt{con} \; x :: \kappa = c \\
adamc@538	994 \mt{sigOf}(\mt{datatype} \; x \; \overline{y} = \overline{dc}) &=& \mt{datatype} \; x \; \overline{y} = \overline{dc} \\
adamc@538	995 \mt{sigOf}(\mt{datatype} \; x = \mt{datatype} \; M.z) &=& \mt{datatype} \; x = \mt{datatype} \; M.z \\
adamc@538	996 \mt{sigOf}(\mt{val} \; x : \tau = e) &=& \mt{val} \; x : \tau \\
adamc@538	997 \mt{sigOf}(\mt{val} \; \mt{rec} \; \overline{x : \tau = e}) &=& \overline{\mt{val} \; x : \tau} \\
adamc@538	998 \mt{sigOf}(\mt{structure} \; X : S = M) &=& \mt{structure} \; X : S \\
adamc@538	999 \mt{sigOf}(\mt{signature} \; X = S) &=& \mt{signature} \; X = S \\
adamc@538	1000 \mt{sigOf}(\mt{open} \; M) &=& \mt{include} \; S \textrm{ (where $\Gamma \vdash M : S$)} \\
adamc@538	1001 \mt{sigOf}(\mt{constraint} \; c_1 \sim c_2) &=& \mt{constraint} \; c_1 \sim c_2 \\
adamc@538	1002 \mt{sigOf}(\mt{open} \; \mt{constraints} \; M) &=& \cdot \\
adamc@538	1003 \mt{sigOf}(\mt{table} \; x : c) &=& \mt{table} \; x : c \\
adamc@538	1004 \mt{sigOf}(\mt{sequence} \; x) &=& \mt{sequence} \; x \\
adamc@538	1005 \mt{sigOf}(\mt{cookie} \; x : \tau) &=& \mt{cookie} \; x : \tau \\
adamc@655	1006 \mt{sigOf}(\mt{class} \; x :: \kappa = c) &=& \mt{class} \; x :: \kappa = c \\
adamc@538	1007 \end{eqnarray*}
adamc@539	1008 \begin{eqnarray*}
adamc@539	1009 \mt{selfify}(M, \cdot) &=& \cdot \\
adamc@558	1010 \mt{selfify}(M, s \; \overline{s'}) &=& \mt{selfify}(M, s) \; \mt{selfify}(M, \overline{s'}) \\
adamc@539	1011 \\
adamc@539	1012 \mt{selfify}(M, \mt{con} \; x :: \kappa) &=& \mt{con} \; x :: \kappa = M.x \\
adamc@539	1013 \mt{selfify}(M, \mt{con} \; x :: \kappa = c) &=& \mt{con} \; x :: \kappa = c \\
adamc@539	1014 \mt{selfify}(M, \mt{datatype} \; x \; \overline{y} = \overline{dc}) &=& \mt{datatype} \; x \; \overline{y} = \mt{datatype} \; M.x \\
adamc@539	1015 \mt{selfify}(M, \mt{datatype} \; x = \mt{datatype} \; M'.z) &=& \mt{datatype} \; x = \mt{datatype} \; M'.z \\
adamc@539	1016 \mt{selfify}(M, \mt{val} \; x : \tau) &=& \mt{val} \; x : \tau \\
adamc@539	1017 \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	1018 \mt{selfify}(M, \mt{signature} \; X = S) &=& \mt{signature} \; X = S \\
adamc@539	1019 \mt{selfify}(M, \mt{include} \; S) &=& \mt{include} \; S \\
adamc@539	1020 \mt{selfify}(M, \mt{constraint} \; c_1 \sim c_2) &=& \mt{constraint} \; c_1 \sim c_2 \\
adamc@655	1021 \mt{selfify}(M, \mt{class} \; x :: \kappa) &=& \mt{class} \; x :: \kappa = M.x \\
adamc@655	1022 \mt{selfify}(M, \mt{class} \; x :: \kappa = c) &=& \mt{class} \; x :: \kappa = c \\
adamc@539	1023 \end{eqnarray*}
adamc@539	1024
adamc@540	1025 \subsection{Module Projection}
adamc@540	1026
adamc@540	1027 \begin{eqnarray*}
adamc@540	1028 \mt{proj}(M, \mt{con} \; x :: \kappa \; \overline{s}, \mt{con} \; x) &=& \kappa \\
adamc@540	1029 \mt{proj}(M, \mt{con} \; x :: \kappa = c \; \overline{s}, \mt{con} \; x) &=& (\kappa, c) \\
adamc@540	1030 \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	1031 \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	1032 && \textrm{and $\mt{proj}(M', \overline{s'}, \mt{datatype} \; z) = (\overline{y}, \overline{dc})$)} \\
adamc@655	1033 \mt{proj}(M, \mt{class} \; x :: \kappa \; \overline{s}, \mt{con} \; x) &=& \kappa \to \mt{Type} \\
adamc@655	1034 \mt{proj}(M, \mt{class} \; x :: \kappa = c \; \overline{s}, \mt{con} \; x) &=& (\kappa \to \mt{Type}, c) \\
adamc@540	1035 \\
adamc@540	1036 \mt{proj}(M, \mt{datatype} \; x \; \overline{y} = \overline{dc} \; \overline{s}, \mt{datatype} \; x) &=& (\overline{y}, \overline{dc}) \\
adamc@540	1037 \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	1038 \\
adamc@540	1039 \mt{proj}(M, \mt{val} \; x : \tau \; \overline{s}, \mt{val} \; x) &=& \tau \\
adamc@540	1040 \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	1041 \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	1042 \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	1043 && \textrm{and $\mt{proj}(M', \overline{s'}, \mt{datatype} \; z = (\overline{y}, \overline{dc})$ and $X \in \overline{dc}$)} \\
adamc@540	1044 \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	1045 && \textrm{and $\mt{proj}(M', \overline{s'}, \mt{datatype} \; z = (\overline{y}, \overline{dc})$ and $X \; \mt{of} \; \tau \in \overline{dc}$)} \\
adamc@540	1046 \\
adamc@540	1047 \mt{proj}(M, \mt{structure} \; X : S \; \overline{s}, \mt{structure} \; X) &=& S \\
adamc@540	1048 \\
adamc@540	1049 \mt{proj}(M, \mt{signature} \; X = S \; \overline{s}, \mt{signature} \; X) &=& S \\
adamc@540	1050 \\
adamc@540	1051 \mt{proj}(M, \mt{con} \; x :: \kappa \; \overline{s}, V) &=& [x \mapsto M.x]\mt{proj}(M, \overline{s}, V) \\
adamc@540	1052 \mt{proj}(M, \mt{con} \; x :: \kappa = c \; \overline{s}, V) &=& [x \mapsto M.x]\mt{proj}(M, \overline{s}, V) \\
adamc@540	1053 \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	1054 \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	1055 \mt{proj}(M, \mt{val} \; x : \tau \; \overline{s}, V) &=& \mt{proj}(M, \overline{s}, V) \\
adamc@540	1056 \mt{proj}(M, \mt{structure} \; X : S \; \overline{s}, V) &=& [X \mapsto M.X]\mt{proj}(M, \overline{s}, V) \\
adamc@540	1057 \mt{proj}(M, \mt{signature} \; X = S \; \overline{s}, V) &=& [X \mapsto M.X]\mt{proj}(M, \overline{s}, V) \\
adamc@540	1058 \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	1059 \mt{proj}(M, \mt{constraint} \; c_1 \sim c_2 \; \overline{s}, V) &=& \mt{proj}(M, \overline{s}, V) \\
adamc@655	1060 \mt{proj}(M, \mt{class} \; x :: \kappa \; \overline{s}, V) &=& [x \mapsto M.x]\mt{proj}(M, \overline{s}, V) \\
adamc@655	1061 \mt{proj}(M, \mt{class} \; x :: \kappa = c \; \overline{s}, V) &=& [x \mapsto M.x]\mt{proj}(M, \overline{s}, V) \\
adamc@540	1062 \end{eqnarray*}
adamc@540	1063
adamc@541	1064
adamc@541	1065 \section{Type Inference}
adamc@541	1066
adamc@541	1067 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	1068
adamc@541	1069 \subsection{Basic Unification}
adamc@541	1070
adamc@560	1071 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	1072
adamc@656	1073 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	1074
adamc@541	1075 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	1076
adamc@541	1077 \subsection{Unifying Record Types}
adamc@541	1078
adamc@570	1079 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	1080
adamc@656	1081 \subsection{\label{typeclasses}Constructor Classes}
adamc@541	1082
adamc@656	1083 Ur includes a constructor class facility inspired by Haskell's. The current version is very rudimentary, only supporting instances for particular constructors built up from abstract constructors and datatypes and type-level application.
adamc@541	1084
adamc@656	1085 Constructor classes are integrated with the module system. A constructor class of kind $\kappa$ is just a constructor of kind $\kappa \to \mt{Type}$. 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'$ 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	1086
adamc@656	1087 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	1088
adamc@656	1089 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	1090
adamc@541	1091 \subsection{Reverse-Engineering Record Types}
adamc@541	1092
adamc@656	1093 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	1094
adamc@541	1095 \subsection{Implicit Arguments in Functor Applications}
adamc@541	1096
adamc@656	1097 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	1098
adamc@541	1099
adamc@542	1100 \section{The Ur Standard Library}
adamc@542	1101
adamc@542	1102 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	1103
adamc@542	1104 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	1105
adamc@542	1106 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	1107 $$\begin{array}{l}
adamc@542	1108 \mt{type} \; \mt{int} \\
adamc@542	1109 \mt{type} \; \mt{float} \\
adamc@542	1110 \mt{type} \; \mt{string} \\
adamc@542	1111 \mt{type} \; \mt{time} \\
adamc@542	1112 \\
adamc@542	1113 \mt{type} \; \mt{unit} = \{\} \\
adamc@542	1114 \\
adamc@542	1115 \mt{datatype} \; \mt{bool} = \mt{False} \mid \mt{True} \\
adamc@542	1116 \\
adamc@542	1117 \mt{datatype} \; \mt{option} \; \mt{t} = \mt{None} \mid \mt{Some} \; \mt{of} \; \mt{t}
adamc@542	1118 \end{array}$$
adamc@542	1119
adamc@657	1120 Another important generic Ur element comes at the beginning of \texttt{top.urs}.
adamc@657	1121
adamc@657	1122 $$\begin{array}{l}
adamc@657	1123 \mt{con} \; \mt{folder} :: \mt{K} \longrightarrow \{\mt{K}\} \to \mt{Type} \\
adamc@657	1124 \\
adamc@657	1125 \mt{val} \; \mt{fold} : \mt{K} \longrightarrow \mt{tf} :: (\{\mt{K}\} \to \mt{Type}) \\
adamc@657	1126 \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	1127 \hspace{.2in} \mt{tf} \; \mt{r} \to \mt{tf} \; ([\mt{nm} = \mt{v}] \rc \mt{r})) \\
adamc@657	1128 \hspace{.1in} \to \mt{tf} \; [] \\
adamc@657	1129 \hspace{.1in} \to \mt{r} :: \{\mt{K}\} \to \mt{folder} \; \mt{r} \to \mt{tf} \; \mt{r}
adamc@657	1130 \end{array}$$
adamc@657	1131
adamc@657	1132 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	1133
adamc@664	1134 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	1135
adamc@542	1136
adamc@542	1137 \section{The Ur/Web Standard Library}
adamc@542	1138
adamc@658	1139 \subsection{Monads}
adamc@658	1140
adamc@658	1141 The Ur Basis defines the monad constructor class from Haskell.
adamc@658	1142
adamc@658	1143 $$\begin{array}{l}
adamc@658	1144 \mt{class} \; \mt{monad} :: \mt{Type} \to \mt{Type} \\
adamc@658	1145 \mt{val} \; \mt{return} : \mt{m} ::: (\mt{Type} \to \mt{Type}) \to \mt{t} ::: \mt{Type} \\
adamc@658	1146 \hspace{.1in} \to \mt{monad} \; \mt{m} \\
adamc@658	1147 \hspace{.1in} \to \mt{t} \to \mt{m} \; \mt{t} \\
adamc@658	1148 \mt{val} \; \mt{bind} : \mt{m} ::: (\mt{Type} \to \mt{Type}) \to \mt{t1} ::: \mt{Type} \to \mt{t2} ::: \mt{Type} \\
adamc@658	1149 \hspace{.1in} \to \mt{monad} \; \mt{m} \\
adamc@658	1150 \hspace{.1in} \to \mt{m} \; \mt{t1} \to (\mt{t1} \to \mt{m} \; \mt{t2}) \\
adamc@658	1151 \hspace{.1in} \to \mt{m} \; \mt{t2}
adamc@658	1152 \end{array}$$
adamc@658	1153
adamc@542	1154 \subsection{Transactions}
adamc@542	1155
adamc@542	1156 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	1157 $$\begin{array}{l}
adamc@542	1158 \mt{con} \; \mt{transaction} :: \mt{Type} \to \mt{Type} \\
adamc@658	1159 \mt{val} \; \mt{transaction\_monad} : \mt{monad} \; \mt{transaction}
adamc@542	1160 \end{array}$$
adamc@542	1161
adamc@542	1162 \subsection{HTTP}
adamc@542	1163
adamc@542	1164 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	1165 $$\begin{array}{l}
adamc@542	1166 \mt{val} \; \mt{requestHeader} : \mt{string} \to \mt{transaction} \; (\mt{option} \; \mt{string}) \\
adamc@542	1167 \\
adamc@542	1168 \mt{con} \; \mt{http\_cookie} :: \mt{Type} \to \mt{Type} \\
adamc@542	1169 \mt{val} \; \mt{getCookie} : \mt{t} ::: \mt{Type} \to \mt{http\_cookie} \; \mt{t} \to \mt{transaction} \; (\mt{option} \; \mt{t}) \\
adamc@542	1170 \mt{val} \; \mt{setCookie} : \mt{t} ::: \mt{Type} \to \mt{http\_cookie} \; \mt{t} \to \mt{t} \to \mt{transaction} \; \mt{unit}
adamc@542	1171 \end{array}$$
adamc@542	1172
adamc@543	1173 \subsection{SQL}
adamc@543	1174
adamc@543	1175 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	1176 $$\begin{array}{l}
adamc@543	1177 \mt{con} \; \mt{sql\_table} :: \{\mt{Type}\} \to \mt{Type}
adamc@543	1178 \end{array}$$
adamc@543	1179
adamc@543	1180 \subsubsection{Queries}
adamc@543	1181
adamc@543	1182 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	1183 $$\begin{array}{l}
adamc@543	1184 \mt{con} \; \mt{sql\_query} :: \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \\
adamc@543	1185 \mt{val} \; \mt{sql\_query} : \mt{tables} ::: \{\{\mt{Type}\}\} \\
adamc@543	1186 \hspace{.1in} \to \mt{selectedFields} ::: \{\{\mt{Type}\}\} \\
adamc@543	1187 \hspace{.1in} \to \mt{selectedExps} ::: \{\mt{Type}\} \\
adamc@543	1188 \hspace{.1in} \to \{\mt{Rows} : \mt{sql\_query1} \; \mt{tables} \; \mt{selectedFields} \; \mt{selectedExps}, \\
adamc@543	1189 \hspace{.2in} \mt{OrderBy} : \mt{sql\_order\_by} \; \mt{tables} \; \mt{selectedExps}, \\
adamc@543	1190 \hspace{.2in} \mt{Limit} : \mt{sql\_limit}, \\
adamc@543	1191 \hspace{.2in} \mt{Offset} : \mt{sql\_offset}\} \\
adamc@543	1192 \hspace{.1in} \to \mt{sql\_query} \; \mt{selectedFields} \; \mt{selectedExps}
adamc@543	1193 \end{array}$$
adamc@543	1194
adamc@545	1195 Queries are used by folding over their results inside transactions.
adamc@545	1196 $$\begin{array}{l}
adamc@545	1197 \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	1198 \hspace{.1in} \to (\$(\mt{exps} \rc \mt{map} \; (\lambda \mt{fields} :: \{\mt{Type}\} \Rightarrow \$\mt{fields}) \; \mt{tables}) \\
adamc@545	1199 \hspace{.2in} \to \mt{state} \to \mt{transaction} \; \mt{state}) \\
adamc@545	1200 \hspace{.1in} \to \mt{state} \to \mt{transaction} \; \mt{state}
adamc@545	1201 \end{array}$$
adamc@545	1202
adamc@543	1203 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	1204 $$\begin{array}{l}
adamc@543	1205 \mt{con} \; \mt{sql\_query1} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \\
adamc@543	1206 \\
adamc@543	1207 \mt{type} \; \mt{sql\_relop} \\
adamc@543	1208 \mt{val} \; \mt{sql\_union} : \mt{sql\_relop} \\
adamc@543	1209 \mt{val} \; \mt{sql\_intersect} : \mt{sql\_relop} \\
adamc@543	1210 \mt{val} \; \mt{sql\_except} : \mt{sql\_relop} \\
adamc@543	1211 \mt{val} \; \mt{sql\_relop} : \mt{tables1} ::: \{\{\mt{Type}\}\} \\
adamc@543	1212 \hspace{.1in} \to \mt{tables2} ::: \{\{\mt{Type}\}\} \\
adamc@543	1213 \hspace{.1in} \to \mt{selectedFields} ::: \{\{\mt{Type}\}\} \\
adamc@543	1214 \hspace{.1in} \to \mt{selectedExps} ::: \{\mt{Type}\} \\
adamc@543	1215 \hspace{.1in} \to \mt{sql\_relop} \\
adamc@543	1216 \hspace{.1in} \to \mt{sql\_query1} \; \mt{tables1} \; \mt{selectedFields} \; \mt{selectedExps} \\
adamc@543	1217 \hspace{.1in} \to \mt{sql\_query1} \; \mt{tables2} \; \mt{selectedFields} \; \mt{selectedExps} \\
adamc@543	1218 \hspace{.1in} \to \mt{sql\_query1} \; \mt{selectedFields} \; \mt{selectedFields} \; \mt{selectedExps}
adamc@543	1219 \end{array}$$
adamc@543	1220
adamc@543	1221 $$\begin{array}{l}
adamc@543	1222 \mt{val} \; \mt{sql\_query1} : \mt{tables} ::: \{\{\mt{Type}\}\} \\
adamc@543	1223 \hspace{.1in} \to \mt{grouped} ::: \{\{\mt{Type}\}\} \\
adamc@543	1224 \hspace{.1in} \to \mt{selectedFields} ::: \{\{\mt{Type}\}\} \\
adamc@543	1225 \hspace{.1in} \to \mt{selectedExps} ::: \{\mt{Type}\} \\
adamc@658	1226 \hspace{.1in} \to \{\mt{From} : \$(\mt{map} \; \mt{sql\_table} \; \mt{tables}), \\
adamc@543	1227 \hspace{.2in} \mt{Where} : \mt{sql\_exp} \; \mt{tables} \; [] \; [] \; \mt{bool}, \\
adamc@543	1228 \hspace{.2in} \mt{GroupBy} : \mt{sql\_subset} \; \mt{tables} \; \mt{grouped}, \\
adamc@543	1229 \hspace{.2in} \mt{Having} : \mt{sql\_exp} \; \mt{grouped} \; \mt{tables} \; [] \; \mt{bool}, \\
adamc@543	1230 \hspace{.2in} \mt{SelectFields} : \mt{sql\_subset} \; \mt{grouped} \; \mt{selectedFields}, \\
adamc@658	1231 \hspace{.2in} \mt {SelectExps} : \$(\mt{map} \; (\mt{sql\_exp} \; \mt{grouped} \; \mt{tables} \; []) \; \mt{selectedExps}) \} \\
adamc@543	1232 \hspace{.1in} \to \mt{sql\_query1} \; \mt{tables} \; \mt{selectedFields} \; \mt{selectedExps}
adamc@543	1233 \end{array}$$
adamc@543	1234
adamc@543	1235 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	1236 $$\begin{array}{l}
adamc@543	1237 \mt{con} \; \mt{sql\_subset} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \mt{Type} \\
adamc@543	1238 \mt{val} \; \mt{sql\_subset} : \mt{keep\_drop} :: \{(\{\mt{Type}\} \times \{\mt{Type}\})\} \\
adamc@543	1239 \hspace{.1in} \to \mt{sql\_subset} \\
adamc@658	1240 \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	1241 \hspace{.2in} (\mt{map} \; (\lambda \mt{fields} :: (\{\mt{Type}\} \times \{\mt{Type}\}) \Rightarrow \mt{fields}.1) \; \mt{keep\_drop}) \\
adamc@543	1242 \mt{val} \; \mt{sql\_subset\_all} : \mt{tables} :: \{\{\mt{Type}\}\} \to \mt{sql\_subset} \; \mt{tables} \; \mt{tables}
adamc@543	1243 \end{array}$$
adamc@543	1244
adamc@560	1245 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	1246 $$\begin{array}{l}
adamc@543	1247 \mt{con} \; \mt{sql\_exp} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \to \mt{Type}
adamc@543	1248 \end{array}$$
adamc@543	1249
adamc@543	1250 Any field in scope may be converted to an expression.
adamc@543	1251 $$\begin{array}{l}
adamc@543	1252 \mt{val} \; \mt{sql\_field} : \mt{otherTabs} ::: \{\{\mt{Type}\}\} \to \mt{otherFields} ::: \{\mt{Type}\} \\
adamc@543	1253 \hspace{.1in} \to \mt{fieldType} ::: \mt{Type} \to \mt{agg} ::: \{\{\mt{Type}\}\} \\
adamc@543	1254 \hspace{.1in} \to \mt{exps} ::: \{\mt{Type}\} \\
adamc@543	1255 \hspace{.1in} \to \mt{tab} :: \mt{Name} \to \mt{field} :: \mt{Name} \\
adamc@543	1256 \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	1257 \end{array}$$
adamc@543	1258
adamc@544	1259 There is an analogous function for referencing named expressions.
adamc@544	1260 $$\begin{array}{l}
adamc@544	1261 \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	1262 \hspace{.1in} \to \mt{sql\_exp} \; \mt{tabs} \; \mt{agg} \; ([\mt{nm} = \mt{t}] \rc \mt{rest}) \; \mt{t}
adamc@544	1263 \end{array}$$
adamc@544	1264
adamc@544	1265 Ur values of appropriate types may be injected into SQL expressions.
adamc@544	1266 $$\begin{array}{l}
adamc@544	1267 \mt{class} \; \mt{sql\_injectable} \\
adamc@544	1268 \mt{val} \; \mt{sql\_bool} : \mt{sql\_injectable} \; \mt{bool} \\
adamc@544	1269 \mt{val} \; \mt{sql\_int} : \mt{sql\_injectable} \; \mt{int} \\
adamc@544	1270 \mt{val} \; \mt{sql\_float} : \mt{sql\_injectable} \; \mt{float} \\
adamc@544	1271 \mt{val} \; \mt{sql\_string} : \mt{sql\_injectable} \; \mt{string} \\
adamc@544	1272 \mt{val} \; \mt{sql\_time} : \mt{sql\_injectable} \; \mt{time} \\
adamc@544	1273 \mt{val} \; \mt{sql\_option\_bool} : \mt{sql\_injectable} \; (\mt{option} \; \mt{bool}) \\
adamc@544	1274 \mt{val} \; \mt{sql\_option\_int} : \mt{sql\_injectable} \; (\mt{option} \; \mt{int}) \\
adamc@544	1275 \mt{val} \; \mt{sql\_option\_float} : \mt{sql\_injectable} \; (\mt{option} \; \mt{float}) \\
adamc@544	1276 \mt{val} \; \mt{sql\_option\_string} : \mt{sql\_injectable} \; (\mt{option} \; \mt{string}) \\
adamc@544	1277 \mt{val} \; \mt{sql\_option\_time} : \mt{sql\_injectable} \; (\mt{option} \; \mt{time}) \\
adamc@544	1278 \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	1279 \hspace{.1in} \to \mt{t} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t}
adamc@544	1280 \end{array}$$
adamc@544	1281
adamc@544	1282 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	1283 $$\begin{array}{l}
adamc@544	1284 \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	1285 \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	1286 \end{array}$$
adamc@544	1287
adamc@559	1288 We have generic nullary, unary, and binary operators.
adamc@544	1289 $$\begin{array}{l}
adamc@544	1290 \mt{con} \; \mt{sql\_nfunc} :: \mt{Type} \to \mt{Type} \\
adamc@544	1291 \mt{val} \; \mt{sql\_current\_timestamp} : \mt{sql\_nfunc} \; \mt{time} \\
adamc@544	1292 \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	1293 \hspace{.1in} \to \mt{sql\_nfunc} \; \mt{t} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} \\\end{array}$$
adamc@544	1294
adamc@544	1295 $$\begin{array}{l}
adamc@544	1296 \mt{con} \; \mt{sql\_unary} :: \mt{Type} \to \mt{Type} \to \mt{Type} \\
adamc@544	1297 \mt{val} \; \mt{sql\_not} : \mt{sql\_unary} \; \mt{bool} \; \mt{bool} \\
adamc@544	1298 \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	1299 \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	1300 \end{array}$$
adamc@544	1301
adamc@544	1302 $$\begin{array}{l}
adamc@544	1303 \mt{con} \; \mt{sql\_binary} :: \mt{Type} \to \mt{Type} \to \mt{Type} \to \mt{Type} \\
adamc@544	1304 \mt{val} \; \mt{sql\_and} : \mt{sql\_binary} \; \mt{bool} \; \mt{bool} \; \mt{bool} \\
adamc@544	1305 \mt{val} \; \mt{sql\_or} : \mt{sql\_binary} \; \mt{bool} \; \mt{bool} \; \mt{bool} \\
adamc@544	1306 \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	1307 \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	1308 \end{array}$$
adamc@544	1309
adamc@544	1310 $$\begin{array}{l}
adamc@559	1311 \mt{class} \; \mt{sql\_arith} \\
adamc@559	1312 \mt{val} \; \mt{sql\_int\_arith} : \mt{sql\_arith} \; \mt{int} \\
adamc@559	1313 \mt{val} \; \mt{sql\_float\_arith} : \mt{sql\_arith} \; \mt{float} \\
adamc@559	1314 \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	1315 \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	1316 \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	1317 \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	1318 \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	1319 \mt{val} \; \mt{sql\_mod} : \mt{sql\_binary} \; \mt{int} \; \mt{int} \; \mt{int}
adamc@559	1320 \end{array}$$
adamc@544	1321
adamc@656	1322 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	1323
adamc@544	1324 $$\begin{array}{l}
adamc@544	1325 \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	1326 \end{array}$$
adamc@544	1327
adamc@544	1328 $$\begin{array}{l}
adamc@544	1329 \mt{con} \; \mt{sql\_aggregate} :: \mt{Type} \to \mt{Type} \\
adamc@544	1330 \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	1331 \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	1332 \end{array}$$
adamc@544	1333
adamc@544	1334 $$\begin{array}{l}
adamc@544	1335 \mt{class} \; \mt{sql\_summable} \\
adamc@544	1336 \mt{val} \; \mt{sql\_summable\_int} : \mt{sql\_summable} \; \mt{int} \\
adamc@544	1337 \mt{val} \; \mt{sql\_summable\_float} : \mt{sql\_summable} \; \mt{float} \\
adamc@544	1338 \mt{val} \; \mt{sql\_avg} : \mt{t} ::: \mt{Type} \to \mt{sql\_summable} \; \mt{t} \to \mt{sql\_aggregate} \; \mt{t} \\
adamc@544	1339 \mt{val} \; \mt{sql\_sum} : \mt{t} ::: \mt{Type} \to \mt{sql\_summable} \mt{t} \to \mt{sql\_aggregate} \; \mt{t}
adamc@544	1340 \end{array}$$
adamc@544	1341
adamc@544	1342 $$\begin{array}{l}
adamc@544	1343 \mt{class} \; \mt{sql\_maxable} \\
adamc@544	1344 \mt{val} \; \mt{sql\_maxable\_int} : \mt{sql\_maxable} \; \mt{int} \\
adamc@544	1345 \mt{val} \; \mt{sql\_maxable\_float} : \mt{sql\_maxable} \; \mt{float} \\
adamc@544	1346 \mt{val} \; \mt{sql\_maxable\_string} : \mt{sql\_maxable} \; \mt{string} \\
adamc@544	1347 \mt{val} \; \mt{sql\_maxable\_time} : \mt{sql\_maxable} \; \mt{time} \\
adamc@544	1348 \mt{val} \; \mt{sql\_max} : \mt{t} ::: \mt{Type} \to \mt{sql\_maxable} \; \mt{t} \to \mt{sql\_aggregate} \; \mt{t} \\
adamc@544	1349 \mt{val} \; \mt{sql\_min} : \mt{t} ::: \mt{Type} \to \mt{sql\_maxable} \; \mt{t} \to \mt{sql\_aggregate} \; \mt{t}
adamc@544	1350 \end{array}$$
adamc@544	1351
adamc@544	1352 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	1353 $$\begin{array}{l}
adamc@544	1354 \mt{type} \; \mt{sql\_direction} \\
adamc@544	1355 \mt{val} \; \mt{sql\_asc} : \mt{sql\_direction} \\
adamc@544	1356 \mt{val} \; \mt{sql\_desc} : \mt{sql\_direction} \\
adamc@544	1357 \\
adamc@544	1358 \mt{con} \; \mt{sql\_order\_by} :: \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \\
adamc@544	1359 \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	1360 \mt{val} \; \mt{sql\_order\_by\_Cons} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{t} ::: \mt{Type} \\
adamc@544	1361 \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	1362 \\
adamc@544	1363 \mt{type} \; \mt{sql\_limit} \\
adamc@544	1364 \mt{val} \; \mt{sql\_no\_limit} : \mt{sql\_limit} \\
adamc@544	1365 \mt{val} \; \mt{sql\_limit} : \mt{int} \to \mt{sql\_limit} \\
adamc@544	1366 \\
adamc@544	1367 \mt{type} \; \mt{sql\_offset} \\
adamc@544	1368 \mt{val} \; \mt{sql\_no\_offset} : \mt{sql\_offset} \\
adamc@544	1369 \mt{val} \; \mt{sql\_offset} : \mt{int} \to \mt{sql\_offset}
adamc@544	1370 \end{array}$$
adamc@544	1371
adamc@545	1372
adamc@545	1373 \subsubsection{DML}
adamc@545	1374
adamc@545	1375 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	1376
adamc@545	1377 $$\begin{array}{l}
adamc@545	1378 \mt{type} \; \mt{dml} \\
adamc@545	1379 \mt{val} \; \mt{dml} : \mt{dml} \to \mt{transaction} \; \mt{unit}
adamc@545	1380 \end{array}$$
adamc@545	1381
adamc@545	1382 Properly-typed records may be used to form $\mt{INSERT}$ commands.
adamc@545	1383 $$\begin{array}{l}
adamc@545	1384 \mt{val} \; \mt{insert} : \mt{fields} ::: \{\mt{Type}\} \to \mt{sql\_table} \; \mt{fields} \\
adamc@658	1385 \hspace{.1in} \to \$(\mt{map} \; (\mt{sql\_exp} \; [] \; [] \; []) \; \mt{fields}) \to \mt{dml}
adamc@545	1386 \end{array}$$
adamc@545	1387
adamc@545	1388 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	1389 $$\begin{array}{l}
adamc@545	1390 \mt{val} \; \mt{update} : \mt{unchanged} ::: \{\mt{Type}\} \to \mt{changed} :: \{\mt{Type}\} \to \lambda [\mt{changed} \sim \mt{unchanged}] \\
adamc@658	1391 \hspace{.1in} \Rightarrow \$(\mt{map} \; (\mt{sql\_exp} \; [\mt{T} = \mt{changed} \rc \mt{unchanged}] \; [] \; []) \; \mt{changed}) \\
adamc@545	1392 \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	1393 \end{array}$$
adamc@545	1394
adamc@545	1395 A $\mt{DELETE}$ command is formed from a table and a $\mt{WHERE}$ clause.
adamc@545	1396 $$\begin{array}{l}
adamc@545	1397 \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	1398 \end{array}$$
adamc@545	1399
adamc@546	1400 \subsubsection{Sequences}
adamc@546	1401
adamc@546	1402 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	1403
adamc@546	1404 $$\begin{array}{l}
adamc@546	1405 \mt{type} \; \mt{sql\_sequence} \\
adamc@546	1406 \mt{val} \; \mt{nextval} : \mt{sql\_sequence} \to \mt{transaction} \; \mt{int}
adamc@546	1407 \end{array}$$
adamc@546	1408
adamc@546	1409
adamc@547	1410 \subsection{XML}
adamc@547	1411
adamc@547	1412 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	1413
adamc@547	1414 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	1415 $$\begin{array}{l}
adamc@547	1416 \mt{con} \; \mt{xml} :: \{\mt{Unit}\} \to \{\mt{Type}\} \to \{\mt{Type}\} \to \mt{Type}
adamc@547	1417 \end{array}$$
adamc@547	1418
adamc@547	1419 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	1420 $$\begin{array}{l}
adamc@547	1421 \mt{con} \; \mt{tag} :: \{\mt{Type}\} \to \{\mt{Unit}\} \to \{\mt{Unit}\} \to \{\mt{Type}\} \to \{\mt{Type}\} \to \mt{Type}
adamc@547	1422 \end{array}$$
adamc@547	1423
adamc@547	1424 Literal text may be injected into XML as ``CDATA.''
adamc@547	1425 $$\begin{array}{l}
adamc@547	1426 \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	1427 \end{array}$$
adamc@547	1428
adamc@547	1429 There is a function for producing an XML tree with a particular tag at its root.
adamc@547	1430 $$\begin{array}{l}
adamc@547	1431 \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	1432 \hspace{.1in} \to \mt{useOuter} ::: \{\mt{Type}\} \to \mt{useInner} ::: \{\mt{Type}\} \to \mt{bindOuter} ::: \{\mt{Type}\} \to \mt{bindInner} ::: \{\mt{Type}\} \\
adamc@547	1433 \hspace{.1in} \to \lambda [\mt{attrsGiven} \sim \mt{attrsAbsent}] \; [\mt{useOuter} \sim \mt{useInner}] \; [\mt{bindOuter} \sim \mt{bindInner}] \Rightarrow \$\mt{attrsGiven} \\
adamc@547	1434 \hspace{.1in} \to \mt{tag} \; (\mt{attrsGiven} \rc \mt{attrsAbsent}) \; \mt{ctxOuter} \; \mt{ctxInner} \; \mt{useOuter} \; \mt{bindOuter} \\
adamc@547	1435 \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	1436 \end{array}$$
adamc@547	1437
adamc@547	1438 Two XML fragments may be concatenated.
adamc@547	1439 $$\begin{array}{l}
adamc@547	1440 \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	1441 \hspace{.1in} \to \lambda [\mt{use_1} \sim \mt{bind_1}] \; [\mt{bind_1} \sim \mt{bind_2}] \\
adamc@547	1442 \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	1443 \end{array}$$
adamc@547	1444
adamc@547	1445 Finally, any XML fragment may be updated to ``claim'' to use more form fields than it does.
adamc@547	1446 $$\begin{array}{l}
adamc@547	1447 \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	1448 \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	1449 \end{array}$$
adamc@547	1450
adamc@547	1451 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	1452
adamc@547	1453 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	1454 $$\begin{array}{l}
adamc@547	1455 \mt{val} \; \mt{error} : \mt{t} ::: \mt{Type} \to \mt{xml} \; [\mt{Body}] \; [] \; [] \to \mt{t}
adamc@547	1456 \end{array}$$
adamc@547	1457
adamc@549	1458
adamc@701	1459 \subsection{Client-Side Programming}
adamc@659	1460
adamc@701	1461 Ur/Web supports running code on web browsers, via automatic compilation to JavaScript.
adamc@701	1462
adamc@701	1463 \subsubsection{The Basics}
adamc@701	1464
adamc@701	1465 Clients can open alert dialog boxes, in the usual annoying JavaScript way.
adamc@701	1466 $$\begin{array}{l}
adamc@701	1467 \mt{val} \; \mt{alert} : \mt{string} \to \mt{transaction} \; \mt{unit}
adamc@701	1468 \end{array}$$
adamc@701	1469
adamc@701	1470 Any transaction may be run in a new thread with the $\mt{spawn}$ function.
adamc@701	1471 $$\begin{array}{l}
adamc@701	1472 \mt{val} \; \mt{spawn} : \mt{transaction} \; \mt{unit} \to \mt{transaction} \; \mt{unit}
adamc@701	1473 \end{array}$$
adamc@701	1474
adamc@701	1475 The current thread can be paused for at least a specified number of milliseconds.
adamc@701	1476 $$\begin{array}{l}
adamc@701	1477 \mt{val} \; \mt{sleep} : \mt{int} \to \mt{transaction} \; \mt{unit}
adamc@701	1478 \end{array}$$
adamc@701	1479
adamc@701	1480 \subsubsection{Functional-Reactive Page Generation}
adamc@701	1481
adamc@701	1482 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	1483
adamc@659	1484 $$\begin{array}{l}
adamc@659	1485 \mt{con} \; \mt{source} :: \mt{Type} \to \mt{Type} \\
adamc@659	1486 \mt{val} \; \mt{source} : \mt{t} ::: \mt{Type} \to \mt{t} \to \mt{transaction} \; (\mt{source} \; \mt{t}) \\
adamc@659	1487 \mt{val} \; \mt{set} : \mt{t} ::: \mt{Type} \to \mt{source} \; \mt{t} \to \mt{t} \to \mt{transaction} \; \mt{unit} \\
adamc@659	1488 \mt{val} \; \mt{get} : \mt{t} ::: \mt{Type} \to \mt{source} \; \mt{t} \to \mt{transaction} \; \mt{t}
adamc@659	1489 \end{array}$$
adamc@659	1490
adamc@659	1491 Pure functions over sources are represented in a monad of \emph{signals}.
adamc@659	1492
adamc@659	1493 $$\begin{array}{l}
adamc@659	1494 \mt{con} \; \mt{signal} :: \mt{Type} \to \mt{Type} \\
adamc@659	1495 \mt{val} \; \mt{signal\_monad} : \mt{monad} \; \mt{signal} \\
adamc@659	1496 \mt{val} \; \mt{signal} : \mt{t} ::: \mt{Type} \to \mt{source} \; \mt{t} \to \mt{signal} \; \mt{t}
adamc@659	1497 \end{array}$$
adamc@659	1498
adamc@659	1499 A reactive portion of an HTML page is injected with a $\mt{dyn}$ tag, which has a signal-valued attribute $\mt{Signal}$.
adamc@659	1500
adamc@659	1501 $$\begin{array}{l}
adamc@701	1502 \mt{val} \; \mt{dyn} : \mt{use} ::: \{\mt{Type}\} \to \mt{bind} ::: \{\mt{Type}\} \to \mt{unit} \\
adamc@701	1503 \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	1504 \end{array}$$
adamc@659	1505
adamc@701	1506 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	1507
adamc@701	1508 \subsubsection{Asynchronous Message-Passing}
adamc@701	1509
adamc@701	1510 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	1511
adamc@701	1512 $$\begin{array}{l}
adamc@701	1513 \mt{type} \; \mt{client} \\
adamc@701	1514 \mt{val} \; \mt{self} : \mt{transaction} \; \mt{client}
adamc@701	1515 \end{array}$$
adamc@701	1516
adamc@701	1517 \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	1518
adamc@701	1519 $$\begin{array}{l}
adamc@701	1520 \mt{con} \; \mt{channel} :: \mt{Type} \to \mt{Type} \\
adamc@701	1521 \mt{val} \; \mt{channel} : \mt{t} ::: \mt{Type} \to \mt{transaction} \; (\mt{channel} \; \mt{t}) \\
adamc@701	1522 \mt{val} \; \mt{send} : \mt{t} ::: \mt{Type} \to \mt{channel} \; \mt{t} \to \mt{t} \to \mt{transaction} \; \mt{unit} \\
adamc@701	1523 \mt{val} \; \mt{recv} : \mt{t} ::: \mt{Type} \to \mt{channel} \; \mt{t} \to \mt{transaction} \; \mt{t}
adamc@701	1524 \end{array}$$
adamc@701	1525
adamc@701	1526 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	1527
adamc@701	1528 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	1529
adamc@659	1530
adamc@549	1531 \section{Ur/Web Syntax Extensions}
adamc@549	1532
adamc@549	1533 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	1534
adamc@549	1535 \subsection{SQL}
adamc@549	1536
adamc@549	1537 \subsubsection{Queries}
adamc@549	1538
adamc@550	1539 Queries $Q$ are added to the rules for expressions $e$.
adamc@550	1540
adamc@549	1541 $$\begin{array}{rrcll}
adamc@550	1542 \textrm{Queries} & Q &::=& (q \; [\mt{ORDER} \; \mt{BY} \; (E \; [o],)^+] \; [\mt{LIMIT} \; N] \; [\mt{OFFSET} \; N]) \\
adamc@549	1543 \textrm{Pre-queries} & q &::=& \mt{SELECT} \; P \; \mt{FROM} \; T,^+ \; [\mt{WHERE} \; E] \; [\mt{GROUP} \; \mt{BY} \; p,^+] \; [\mt{HAVING} \; E] \\
adamc@549	1544 &&& \mid q \; R \; q \\
adamc@549	1545 \textrm{Relational operators} & R &::=& \mt{UNION} \mid \mt{INTERSECT} \mid \mt{EXCEPT}
adamc@549	1546 \end{array}$$
adamc@549	1547
adamc@549	1548 $$\begin{array}{rrcll}
adamc@549	1549 \textrm{Projections} & P &::=& \ast & \textrm{all columns} \\
adamc@549	1550 &&& p,^+ & \textrm{particular columns} \\
adamc@549	1551 \textrm{Pre-projections} & p &::=& t.f & \textrm{one column from a table} \\
adamc@558	1552 &&& t.\{\{c\}\} & \textrm{a record of columns from a table (of kind $\{\mt{Type}\}$)} \\
adamc@549	1553 \textrm{Table names} & t &::=& x & \textrm{constant table name (automatically capitalized)} \\
adamc@549	1554 &&& X & \textrm{constant table name} \\
adamc@549	1555 &&& \{\{c\}\} & \textrm{computed table name (of kind $\mt{Name}$)} \\
adamc@549	1556 \textrm{Column names} & f &::=& X & \textrm{constant column name} \\
adamc@549	1557 &&& \{c\} & \textrm{computed column name (of kind $\mt{Name}$)} \\
adamc@549	1558 \textrm{Tables} & T &::=& x & \textrm{table variable, named locally by its own capitalization} \\
adamc@549	1559 &&& x \; \mt{AS} \; t & \textrm{table variable, with local name} \\
adamc@549	1560 &&& \{\{e\}\} \; \mt{AS} \; t & \textrm{computed table expression, with local name} \\
adamc@549	1561 \textrm{SQL expressions} & E &::=& p & \textrm{column references} \\
adamc@549	1562 &&& X & \textrm{named expression references} \\
adamc@549	1563 &&& \{\{e\}\} & \textrm{injected native Ur expressions} \\
adamc@549	1564 &&& \{e\} & \textrm{computed expressions, probably using $\mt{sql\_exp}$ directly} \\
adamc@549	1565 &&& \mt{TRUE} \mid \mt{FALSE} & \textrm{boolean constants} \\
adamc@549	1566 &&& \ell & \textrm{primitive type literals} \\
adamc@549	1567 &&& \mt{NULL} & \textrm{null value (injection of $\mt{None}$)} \\
adamc@549	1568 &&& E \; \mt{IS} \; \mt{NULL} & \textrm{nullness test} \\
adamc@549	1569 &&& n & \textrm{nullary operators} \\
adamc@549	1570 &&& u \; E & \textrm{unary operators} \\
adamc@549	1571 &&& E \; b \; E & \textrm{binary operators} \\
adamc@549	1572 &&& \mt{COUNT}(\ast) & \textrm{count number of rows} \\
adamc@549	1573 &&& a(E) & \textrm{other aggregate function} \\
adamc@549	1574 &&& (E) & \textrm{explicit precedence} \\
adamc@549	1575 \textrm{Nullary operators} & n &::=& \mt{CURRENT\_TIMESTAMP} \\
adamc@549	1576 \textrm{Unary operators} & u &::=& \mt{NOT} \\
adamc@549	1577 \textrm{Binary operators} & b &::=& \mt{AND} \mid \mt{OR} \mid \neq \mid < \mid \leq \mid > \mid \geq \\
adamc@549	1578 \textrm{Aggregate functions} & a &::=& \mt{AVG} \mid \mt{SUM} \mid \mt{MIN} \mid \mt{MAX} \\
adamc@550	1579 \textrm{Directions} & o &::=& \mt{ASC} \mid \mt{DESC} \\
adamc@549	1580 \textrm{SQL integer} & N &::=& n \mid \{e\} \\
adamc@549	1581 \end{array}$$
adamc@549	1582
adamc@549	1583 Additionally, an SQL expression may be inserted into normal Ur code with the syntax $(\mt{SQL} \; E)$ or $(\mt{WHERE} \; E)$.
adamc@549	1584
adamc@550	1585 \subsubsection{DML}
adamc@550	1586
adamc@550	1587 DML commands $D$ are added to the rules for expressions $e$.
adamc@550	1588
adamc@550	1589 $$\begin{array}{rrcll}
adamc@550	1590 \textrm{Commands} & D &::=& (\mt{INSERT} \; \mt{INTO} \; T^E \; (f,^+) \; \mt{VALUES} \; (E,^+)) \\
adamc@550	1591 &&& (\mt{UPDATE} \; T^E \; \mt{SET} \; (f = E,)^+ \; \mt{WHERE} \; E) \\
adamc@550	1592 &&& (\mt{DELETE} \; \mt{FROM} \; T^E \; \mt{WHERE} \; E) \\
adamc@550	1593 \textrm{Table expressions} & T^E &::=& x \mid \{\{e\}\}
adamc@550	1594 \end{array}$$
adamc@550	1595
adamc@550	1596 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	1597
adamc@551	1598 \subsection{XML}
adamc@551	1599
adamc@551	1600 XML fragments $L$ are added to the rules for expressions $e$.
adamc@551	1601
adamc@551	1602 $$\begin{array}{rrcll}
adamc@551	1603 \textrm{XML fragments} & L &::=& \texttt{<xml/>} \mid \texttt{<xml>}l^*\texttt{</xml>} \\
adamc@551	1604 \textrm{XML pieces} & l &::=& \textrm{text} & \textrm{cdata} \\
adamc@551	1605 &&& \texttt{<}g\texttt{/>} & \textrm{tag with no children} \\
adamc@551	1606 &&& \texttt{<}g\texttt{>}l^*\texttt{</}x\texttt{>} & \textrm{tag with children} \\
adamc@559	1607 &&& \{e\} & \textrm{computed XML fragment} \\
adamc@559	1608 &&& \{[e]\} & \textrm{injection of an Ur expression, via the $\mt{Top}.\mt{txt}$ function} \\
adamc@551	1609 \textrm{Tag} & g &::=& h \; (x = v)^* \\
adamc@551	1610 \textrm{Tag head} & h &::=& x & \textrm{tag name} \\
adamc@551	1611 &&& h\{c\} & \textrm{constructor parameter} \\
adamc@551	1612 \textrm{Attribute value} & v &::=& \ell & \textrm{literal value} \\
adamc@551	1613 &&& \{e\} & \textrm{computed value} \\
adamc@551	1614 \end{array}$$
adamc@551	1615
adamc@552	1616
adamc@553	1617 \section{The Structure of Web Applications}
adamc@553	1618
adamc@553	1619 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	1620
adamc@553	1621 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	1622
adamc@553	1623 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	1624
adamc@558	1625 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	1626
adamc@660	1627 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	1628
adamc@553	1629
adamc@552	1630 \section{Compiler Phases}
adamc@552	1631
adamc@552	1632 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	1633
adamc@552	1634 In this section, we step through the main phases of compilation, noting what consequences each phase has for effective programming.
adamc@552	1635
adamc@552	1636 \subsection{Parse}
adamc@552	1637
adamc@552	1638 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	1639
adamc@552	1640 \subsection{Elaborate}
adamc@552	1641
adamc@552	1642 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	1643
adamc@552	1644 \subsection{Unnest}
adamc@552	1645
adamc@552	1646 Named local function definitions are moved to the top level, to avoid the need to generate closures.
adamc@552	1647
adamc@552	1648 \subsection{Corify}
adamc@552	1649
adamc@552	1650 Module system features are compiled away, through inlining of functor definitions at application sites. Afterward, most abstraction boundaries are broken, facilitating optimization.
adamc@552	1651
adamc@552	1652 \subsection{Especialize}
adamc@552	1653
adamc@552	1654 Functions are specialized to particular argument patterns. This is an important trick for avoiding the need to maintain any closures at runtime.
adamc@552	1655
adamc@552	1656 \subsection{Untangle}
adamc@552	1657
adamc@552	1658 Remove unnecessary mutual recursion, splitting recursive groups into strongly-connected components.
adamc@552	1659
adamc@552	1660 \subsection{Shake}
adamc@552	1661
adamc@552	1662 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	1663
adamc@661	1664 \subsection{Rpcify}
adamc@661	1665
adamc@661	1666 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	1667
adamc@661	1668 \subsection{Untangle, Shake}
adamc@661	1669
adamc@661	1670 Repeat these simplifications.
adamc@661	1671
adamc@553	1672 \subsection{\label{tag}Tag}
adamc@552	1673
adamc@552	1674 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	1675
adamc@552	1676 \subsection{Reduce}
adamc@552	1677
adamc@552	1678 Apply definitional equality rules to simplify the program as much as possible. This effectively includes inlining of every non-recursive definition.
adamc@552	1679
adamc@552	1680 \subsection{Unpoly}
adamc@552	1681
adamc@552	1682 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	1683
adamc@552	1684 \subsection{Specialize}
adamc@552	1685
adamc@558	1686 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	1687
adamc@552	1688 \subsection{Shake}
adamc@552	1689
adamc@558	1690 Here the compiler repeats the earlier Shake phase.
adamc@552	1691
adamc@552	1692 \subsection{Monoize}
adamc@552	1693
adamc@552	1694 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	1695
adamc@552	1696 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	1697
adamc@552	1698 \subsection{MonoOpt}
adamc@552	1699
adamc@552	1700 Simple algebraic laws are applied to simplify the program, focusing especially on efficient imperative generation of HTML pages.
adamc@552	1701
adamc@552	1702 \subsection{MonoUntangle}
adamc@552	1703
adamc@552	1704 Unnecessary mutual recursion is broken up again.
adamc@552	1705
adamc@552	1706 \subsection{MonoReduce}
adamc@552	1707
adamc@552	1708 Equivalents of the definitional equality rules are applied to simplify programs, with inlining again playing a major role.
adamc@552	1709
adamc@552	1710 \subsection{MonoShake, MonoOpt}
adamc@552	1711
adamc@552	1712 Unneeded declarations are removed, and basic optimizations are repeated.
adamc@552	1713
adamc@552	1714 \subsection{Fuse}
adamc@552	1715
adamc@552	1716 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	1717
adamc@552	1718 \subsection{MonoUntangle, MonoShake}
adamc@552	1719
adamc@552	1720 Fuse often creates more opportunities to remove spurious mutual recursion.
adamc@552	1721
adamc@552	1722 \subsection{Pathcheck}
adamc@552	1723
adamc@552	1724 The compiler checks that no link or action name has been used more than once.
adamc@552	1725
adamc@552	1726 \subsection{Cjrize}
adamc@552	1727
adamc@552	1728 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	1729
adamc@552	1730 \subsection{C Compilation and Linking}
adamc@552	1731
adamc@552	1732 The output of the last phase is pretty-printed as C source code and passed to GCC.
adamc@552	1733
adamc@552	1734
adamc@524	1735 \end{document}

Mercurial > urweb

annotate doc/manual.tex @ 713:baaae037e7f6