annotate doc/manual.tex @ 671:729e65db2e2f

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