annotate doc/manual.tex @ 657:74140535291d

Describe folders
author Adam Chlipala <adamc@hcoop.net>
date Thu, 12 Mar 2009 11:36:27 -0400
parents 3be5e6f01c32
children 81c5c2674215
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@533 668 }$$
adamc@533 669
adamc@534 670 \subsection{Pattern Typing}
adamc@534 671
adamc@534 672 $$\infer{\Gamma \vdash \_ \leadsto \Gamma; \tau}{}
adamc@534 673 \quad \infer{\Gamma \vdash x \leadsto \Gamma, x : \tau; \tau}{}
adamc@534 674 \quad \infer{\Gamma \vdash \ell \leadsto \Gamma; T(\ell)}{}$$
adamc@534 675
adamc@534 676 $$\infer{\Gamma \vdash X \leadsto \Gamma; \overline{[x_i \mapsto \tau'_i]}\tau}{
adamc@534 677 X : \overline{x ::: \mt{Type}} \to \tau \in \Gamma
adamc@534 678 & \textrm{$\tau$ not a function type}
adamc@534 679 }
adamc@534 680 \quad \infer{\Gamma \vdash X \; p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau}{
adamc@534 681 X : \overline{x ::: \mt{Type}} \to \tau'' \to \tau \in \Gamma
adamc@534 682 & \Gamma \vdash p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau''
adamc@534 683 }$$
adamc@534 684
adamc@534 685 $$\infer{\Gamma \vdash M.X \leadsto \Gamma; \overline{[x_i \mapsto \tau'_i]}\tau}{
adamc@537 686 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 687 & \mt{proj}(M, \overline{s}, \mt{val} \; X) = \overline{x ::: \mt{Type}} \to \tau
adamc@534 688 & \textrm{$\tau$ not a function type}
adamc@534 689 }$$
adamc@534 690
adamc@534 691 $$\infer{\Gamma \vdash M.X \; p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau}{
adamc@537 692 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 693 & \mt{proj}(M, \overline{s}, \mt{val} \; X) = \overline{x ::: \mt{Type}} \to \tau'' \to \tau
adamc@534 694 & \Gamma \vdash p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau''
adamc@534 695 }$$
adamc@534 696
adamc@534 697 $$\infer{\Gamma \vdash \{\overline{x = p}\} \leadsto \Gamma_n; \{\overline{x = \tau}\}}{
adamc@534 698 \Gamma_0 = \Gamma
adamc@534 699 & \forall i: \Gamma_i \vdash p_i \leadsto \Gamma_{i+1}; \tau_i
adamc@534 700 }
adamc@534 701 \quad \infer{\Gamma \vdash \{\overline{x = p}, \ldots\} \leadsto \Gamma_n; \$([\overline{x = \tau}] \rc c)}{
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
adamc@535 706 \subsection{Declaration Typing}
adamc@535 707
adamc@535 708 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 709
adamc@655 710 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 711
adamc@558 712 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 713 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 714
adamc@535 715 $$\infer{\Gamma \vdash \cdot \leadsto \Gamma}{}
adamc@535 716 \quad \infer{\Gamma \vdash d, \overline{d} \leadsto \Gamma''}{
adamc@535 717 \Gamma \vdash d \leadsto \Gamma'
adamc@535 718 & \Gamma' \vdash \overline{d} \leadsto \Gamma''
adamc@535 719 }$$
adamc@535 720
adamc@535 721 $$\infer{\Gamma \vdash \mt{con} \; x :: \kappa = c \leadsto \Gamma, x :: \kappa = c}{
adamc@535 722 \Gamma \vdash c :: \kappa
adamc@535 723 }
adamc@535 724 \quad \infer{\Gamma \vdash \mt{datatype} \; x \; \overline{y} = \overline{dc} \leadsto \Gamma'}{
adamc@535 725 \overline{y}; x; \Gamma, x :: \mt{Type}^{\mt{len}(\overline y)} \to \mt{Type} \vdash \overline{dc} \leadsto \Gamma'
adamc@535 726 }$$
adamc@535 727
adamc@535 728 $$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leadsto \Gamma'}{
adamc@537 729 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 730 & \mt{proj}(M, \overline{s}, \mt{datatype} \; z) = (\overline{y}, \overline{dc})
adamc@535 731 & \overline{y}; x; \Gamma, x :: \mt{Type}^{\mt{len}(\overline y)} \to \mt{Type} = M.z \vdash \overline{dc} \leadsto \Gamma'
adamc@535 732 }$$
adamc@535 733
adamc@535 734 $$\infer{\Gamma \vdash \mt{val} \; x : \tau = e \leadsto \Gamma, x : \tau}{
adamc@535 735 \Gamma \vdash e : \tau
adamc@535 736 }$$
adamc@535 737
adamc@535 738 $$\infer{\Gamma \vdash \mt{val} \; \mt{rec} \; \overline{x : \tau = e} \leadsto \Gamma, \overline{x : \tau}}{
adamc@535 739 \forall i: \Gamma, \overline{x : \tau} \vdash e_i : \tau_i
adamc@535 740 & \textrm{$e_i$ starts with an expression $\lambda$, optionally preceded by constructor and disjointness $\lambda$s}
adamc@535 741 }$$
adamc@535 742
adamc@535 743 $$\infer{\Gamma \vdash \mt{structure} \; X : S = M \leadsto \Gamma, X : S}{
adamc@535 744 \Gamma \vdash M : S
adamc@558 745 & \textrm{ $M$ not a constant or application}
adamc@535 746 }
adamc@558 747 \quad \infer{\Gamma \vdash \mt{structure} \; X : S = M \leadsto \Gamma, X : \mt{selfify}(X, \overline{s})}{
adamc@558 748 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@539 749 }$$
adamc@539 750
adamc@539 751 $$\infer{\Gamma \vdash \mt{signature} \; X = S \leadsto \Gamma, X = S}{
adamc@535 752 \Gamma \vdash S
adamc@535 753 }$$
adamc@535 754
adamc@537 755 $$\infer{\Gamma \vdash \mt{open} \; M \leadsto \Gamma, \mathcal O(M, \overline{s})}{
adamc@537 756 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@535 757 }$$
adamc@535 758
adamc@535 759 $$\infer{\Gamma \vdash \mt{constraint} \; c_1 \sim c_2 \leadsto \Gamma}{
adamc@535 760 \Gamma \vdash c_1 :: \{\kappa\}
adamc@535 761 & \Gamma \vdash c_2 :: \{\kappa\}
adamc@535 762 & \Gamma \vdash c_1 \sim c_2
adamc@535 763 }
adamc@537 764 \quad \infer{\Gamma \vdash \mt{open} \; \mt{constraints} \; M \leadsto \Gamma, \mathcal O_c(M, \overline{s})}{
adamc@537 765 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@535 766 }$$
adamc@535 767
adamc@535 768 $$\infer{\Gamma \vdash \mt{table} \; x : c \leadsto \Gamma, x : \mt{Basis}.\mt{sql\_table} \; c}{
adamc@535 769 \Gamma \vdash c :: \{\mt{Type}\}
adamc@535 770 }
adamc@535 771 \quad \infer{\Gamma \vdash \mt{sequence} \; x \leadsto \Gamma, x : \mt{Basis}.\mt{sql\_sequence}}{}$$
adamc@535 772
adamc@535 773 $$\infer{\Gamma \vdash \mt{cookie} \; x : \tau \leadsto \Gamma, x : \mt{Basis}.\mt{http\_cookie} \; \tau}{
adamc@535 774 \Gamma \vdash \tau :: \mt{Type}
adamc@535 775 }$$
adamc@535 776
adamc@655 777 $$\infer{\Gamma \vdash \mt{class} \; x :: \kappa = c \leadsto \Gamma, x :: \kappa \to \mt{Type} = c}{
adamc@655 778 \Gamma \vdash c :: \kappa \to \mt{Type}
adamc@535 779 }$$
adamc@535 780
adamc@535 781 $$\infer{\overline{y}; x; \Gamma \vdash \cdot \leadsto \Gamma}{}
adamc@535 782 \quad \infer{\overline{y}; x; \Gamma \vdash X \mid \overline{dc} \leadsto \Gamma', X : \overline{y ::: \mt{Type}} \to x \; \overline{y}}{
adamc@535 783 \overline{y}; x; \Gamma \vdash \overline{dc} \leadsto \Gamma'
adamc@535 784 }
adamc@535 785 \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 786 \overline{y}; x; \Gamma \vdash \overline{dc} \leadsto \Gamma'
adamc@535 787 }$$
adamc@535 788
adamc@537 789 \subsection{Signature Item Typing}
adamc@537 790
adamc@537 791 We appeal to a signature item analogue of the $\mathcal O$ function from the last subsection.
adamc@537 792
adamc@537 793 $$\infer{\Gamma \vdash \cdot \leadsto \Gamma}{}
adamc@537 794 \quad \infer{\Gamma \vdash s, \overline{s} \leadsto \Gamma''}{
adamc@537 795 \Gamma \vdash s \leadsto \Gamma'
adamc@537 796 & \Gamma' \vdash \overline{s} \leadsto \Gamma''
adamc@537 797 }$$
adamc@537 798
adamc@537 799 $$\infer{\Gamma \vdash \mt{con} \; x :: \kappa \leadsto \Gamma, x :: \kappa}{}
adamc@537 800 \quad \infer{\Gamma \vdash \mt{con} \; x :: \kappa = c \leadsto \Gamma, x :: \kappa = c}{
adamc@537 801 \Gamma \vdash c :: \kappa
adamc@537 802 }
adamc@537 803 \quad \infer{\Gamma \vdash \mt{datatype} \; x \; \overline{y} = \overline{dc} \leadsto \Gamma'}{
adamc@537 804 \overline{y}; x; \Gamma, x :: \mt{Type}^{\mt{len}(\overline y)} \to \mt{Type} \vdash \overline{dc} \leadsto \Gamma'
adamc@537 805 }$$
adamc@537 806
adamc@537 807 $$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leadsto \Gamma'}{
adamc@537 808 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 809 & \mt{proj}(M, \overline{s}, \mt{datatype} \; z) = (\overline{y}, \overline{dc})
adamc@537 810 & \overline{y}; x; \Gamma, x :: \mt{Type}^{\mt{len}(\overline y)} \to \mt{Type} = M.z \vdash \overline{dc} \leadsto \Gamma'
adamc@537 811 }$$
adamc@537 812
adamc@537 813 $$\infer{\Gamma \vdash \mt{val} \; x : \tau \leadsto \Gamma, x : \tau}{
adamc@537 814 \Gamma \vdash \tau :: \mt{Type}
adamc@537 815 }$$
adamc@537 816
adamc@537 817 $$\infer{\Gamma \vdash \mt{structure} \; X : S \leadsto \Gamma, X : S}{
adamc@537 818 \Gamma \vdash S
adamc@537 819 }
adamc@537 820 \quad \infer{\Gamma \vdash \mt{signature} \; X = S \leadsto \Gamma, X = S}{
adamc@537 821 \Gamma \vdash S
adamc@537 822 }$$
adamc@537 823
adamc@537 824 $$\infer{\Gamma \vdash \mt{include} \; S \leadsto \Gamma, \mathcal O(\overline{s})}{
adamc@537 825 \Gamma \vdash S
adamc@537 826 & \Gamma \vdash S \equiv \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 827 }$$
adamc@537 828
adamc@537 829 $$\infer{\Gamma \vdash \mt{constraint} \; c_1 \sim c_2 \leadsto \Gamma, c_1 \sim c_2}{
adamc@537 830 \Gamma \vdash c_1 :: \{\kappa\}
adamc@537 831 & \Gamma \vdash c_2 :: \{\kappa\}
adamc@537 832 }$$
adamc@537 833
adamc@655 834 $$\infer{\Gamma \vdash \mt{class} \; x :: \kappa = c \leadsto \Gamma, x :: \kappa \to \mt{Type} = c}{
adamc@655 835 \Gamma \vdash c :: \kappa \to \mt{Type}
adamc@537 836 }
adamc@655 837 \quad \infer{\Gamma \vdash \mt{class} \; x :: \kappa \leadsto \Gamma, x :: \kappa \to \mt{Type}}{}$$
adamc@537 838
adamc@536 839 \subsection{Signature Compatibility}
adamc@536 840
adamc@558 841 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 842
adamc@537 843 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 844
adamc@536 845 $$\infer{\Gamma \vdash S \equiv S}{}
adamc@536 846 \quad \infer{\Gamma \vdash S_1 \equiv S_2}{
adamc@536 847 \Gamma \vdash S_2 \equiv S_1
adamc@536 848 }
adamc@536 849 \quad \infer{\Gamma \vdash X \equiv S}{
adamc@536 850 X = S \in \Gamma
adamc@536 851 }
adamc@536 852 \quad \infer{\Gamma \vdash M.X \equiv S}{
adamc@537 853 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 854 & \mt{proj}(M, \overline{s}, \mt{signature} \; X) = S
adamc@536 855 }$$
adamc@536 856
adamc@536 857 $$\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 858 \Gamma \vdash S \equiv \mt{sig} \; \overline{s^1} \; \mt{con} \; x :: \kappa \; \overline{s_2} \; \mt{end}
adamc@536 859 & \Gamma \vdash c :: \kappa
adamc@537 860 }
adamc@537 861 \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 862 \Gamma \vdash S \equiv \mt{sig} \; \overline{s} \; \mt{end}
adamc@536 863 }$$
adamc@536 864
adamc@536 865 $$\infer{\Gamma \vdash S_1 \leq S_2}{
adamc@536 866 \Gamma \vdash S_1 \equiv S_2
adamc@536 867 }
adamc@536 868 \quad \infer{\Gamma \vdash \mt{sig} \; \overline{s} \; \mt{end} \leq \mt{sig} \; \mt{end}}{}
adamc@537 869 \quad \infer{\Gamma \vdash \mt{sig} \; \overline{s} \; \mt{end} \leq \mt{sig} \; s' \; \overline{s'} \; \mt{end}}{
adamc@537 870 \Gamma \vdash \overline{s} \leq s'
adamc@537 871 & \Gamma \vdash s' \leadsto \Gamma'
adamc@537 872 & \Gamma' \vdash \mt{sig} \; \overline{s} \; \mt{end} \leq \mt{sig} \; \overline{s'} \; \mt{end}
adamc@537 873 }$$
adamc@537 874
adamc@537 875 $$\infer{\Gamma \vdash s \; \overline{s} \leq s'}{
adamc@537 876 \Gamma \vdash s \leq s'
adamc@537 877 }
adamc@537 878 \quad \infer{\Gamma \vdash s \; \overline{s} \leq s'}{
adamc@537 879 \Gamma \vdash s \leadsto \Gamma'
adamc@537 880 & \Gamma' \vdash \overline{s} \leq s'
adamc@536 881 }$$
adamc@536 882
adamc@536 883 $$\infer{\Gamma \vdash \mt{functor} (X : S_1) : S_2 \leq \mt{functor} (X : S'_1) : S'_2}{
adamc@536 884 \Gamma \vdash S'_1 \leq S_1
adamc@536 885 & \Gamma, X : S'_1 \vdash S_2 \leq S'_2
adamc@536 886 }$$
adamc@536 887
adamc@537 888 $$\infer{\Gamma \vdash \mt{con} \; x :: \kappa \leq \mt{con} \; x :: \kappa}{}
adamc@537 889 \quad \infer{\Gamma \vdash \mt{con} \; x :: \kappa = c \leq \mt{con} \; x :: \kappa}{}
adamc@558 890 \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 891
adamc@537 892 $$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leq \mt{con} \; x :: \mt{Type}^{\mt{len}(y)} \to \mt{Type}}{
adamc@537 893 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 894 & \mt{proj}(M, \overline{s}, \mt{datatype} \; z) = (\overline{y}, \overline{dc})
adamc@537 895 }$$
adamc@537 896
adamc@655 897 $$\infer{\Gamma \vdash \mt{class} \; x :: \kappa \leq \mt{con} \; x :: \kappa \to \mt{Type}}{}
adamc@655 898 \quad \infer{\Gamma \vdash \mt{class} \; x :: \kappa = c \leq \mt{con} \; x :: \kappa \to \mt{Type}}{}$$
adamc@537 899
adamc@537 900 $$\infer{\Gamma \vdash \mt{con} \; x :: \kappa = c_1 \leq \mt{con} \; x :: \mt{\kappa} = c_2}{
adamc@537 901 \Gamma \vdash c_1 \equiv c_2
adamc@537 902 }
adamc@655 903 \quad \infer{\Gamma \vdash \mt{class} \; x :: \kappa = c_1 \leq \mt{con} \; x :: \kappa \to \mt{Type} = c_2}{
adamc@537 904 \Gamma \vdash c_1 \equiv c_2
adamc@537 905 }$$
adamc@537 906
adamc@537 907 $$\infer{\Gamma \vdash \mt{datatype} \; x \; \overline{y} = \overline{dc} \leq \mt{datatype} \; x \; \overline{y} = \overline{dc'}}{
adamc@537 908 \Gamma, \overline{y :: \mt{Type}} \vdash \overline{dc} \leq \overline{dc'}
adamc@537 909 }$$
adamc@537 910
adamc@537 911 $$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leq \mt{datatype} \; x \; \overline{y} = \overline{dc'}}{
adamc@537 912 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 913 & \mt{proj}(M, \overline{s}, \mt{datatype} \; z) = (\overline{y}, \overline{dc})
adamc@537 914 & \Gamma, \overline{y :: \mt{Type}} \vdash \overline{dc} \leq \overline{dc'}
adamc@537 915 }$$
adamc@537 916
adamc@537 917 $$\infer{\Gamma \vdash \cdot \leq \cdot}{}
adamc@537 918 \quad \infer{\Gamma \vdash X; \overline{dc} \leq X; \overline{dc'}}{
adamc@537 919 \Gamma \vdash \overline{dc} \leq \overline{dc'}
adamc@537 920 }
adamc@537 921 \quad \infer{\Gamma \vdash X \; \mt{of} \; \tau_1; \overline{dc} \leq X \; \mt{of} \; \tau_2; \overline{dc'}}{
adamc@537 922 \Gamma \vdash \tau_1 \equiv \tau_2
adamc@537 923 & \Gamma \vdash \overline{dc} \leq \overline{dc'}
adamc@537 924 }$$
adamc@537 925
adamc@537 926 $$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leq \mt{datatype} \; x = \mt{datatype} \; M'.z'}{
adamc@537 927 \Gamma \vdash M.z \equiv M'.z'
adamc@537 928 }$$
adamc@537 929
adamc@537 930 $$\infer{\Gamma \vdash \mt{val} \; x : \tau_1 \leq \mt{val} \; x : \tau_2}{
adamc@537 931 \Gamma \vdash \tau_1 \equiv \tau_2
adamc@537 932 }
adamc@537 933 \quad \infer{\Gamma \vdash \mt{structure} \; X : S_1 \leq \mt{structure} \; X : S_2}{
adamc@537 934 \Gamma \vdash S_1 \leq S_2
adamc@537 935 }
adamc@537 936 \quad \infer{\Gamma \vdash \mt{signature} \; X = S_1 \leq \mt{signature} \; X = S_2}{
adamc@537 937 \Gamma \vdash S_1 \leq S_2
adamc@537 938 & \Gamma \vdash S_2 \leq S_1
adamc@537 939 }$$
adamc@537 940
adamc@537 941 $$\infer{\Gamma \vdash \mt{constraint} \; c_1 \sim c_2 \leq \mt{constraint} \; c'_1 \sim c'_2}{
adamc@537 942 \Gamma \vdash c_1 \equiv c'_1
adamc@537 943 & \Gamma \vdash c_2 \equiv c'_2
adamc@537 944 }$$
adamc@537 945
adamc@655 946 $$\infer{\Gamma \vdash \mt{class} \; x :: \kappa \leq \mt{class} \; x :: \kappa}{}
adamc@655 947 \quad \infer{\Gamma \vdash \mt{class} \; x :: \kappa = c \leq \mt{class} \; x :: \kappa}{}
adamc@655 948 \quad \infer{\Gamma \vdash \mt{class} \; x :: \kappa = c_1 \leq \mt{class} \; x :: \kappa = c_2}{
adamc@537 949 \Gamma \vdash c_1 \equiv c_2
adamc@537 950 }$$
adamc@537 951
adamc@538 952 \subsection{Module Typing}
adamc@538 953
adamc@538 954 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 955
adamc@538 956 $$\infer{\Gamma \vdash M : S}{
adamc@538 957 \Gamma \vdash M : S'
adamc@538 958 & \Gamma \vdash S' \leq S
adamc@538 959 }
adamc@538 960 \quad \infer{\Gamma \vdash \mt{struct} \; \overline{d} \; \mt{end} : \mt{sig} \; \mt{sigOf}(\overline{d}) \; \mt{end}}{
adamc@538 961 \Gamma \vdash \overline{d} \leadsto \Gamma'
adamc@538 962 }
adamc@538 963 \quad \infer{\Gamma \vdash X : S}{
adamc@538 964 X : S \in \Gamma
adamc@538 965 }$$
adamc@538 966
adamc@538 967 $$\infer{\Gamma \vdash M.X : S}{
adamc@538 968 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@538 969 & \mt{proj}(M, \overline{s}, \mt{structure} \; X) = S
adamc@538 970 }$$
adamc@538 971
adamc@538 972 $$\infer{\Gamma \vdash M_1(M_2) : [X \mapsto M_2]S_2}{
adamc@538 973 \Gamma \vdash M_1 : \mt{functor}(X : S_1) : S_2
adamc@538 974 & \Gamma \vdash M_2 : S_1
adamc@538 975 }
adamc@538 976 \quad \infer{\Gamma \vdash \mt{functor} (X : S_1) : S_2 = M : \mt{functor} (X : S_1) : S_2}{
adamc@538 977 \Gamma \vdash S_1
adamc@538 978 & \Gamma, X : S_1 \vdash S_2
adamc@538 979 & \Gamma, X : S_1 \vdash M : S_2
adamc@538 980 }$$
adamc@538 981
adamc@538 982 \begin{eqnarray*}
adamc@538 983 \mt{sigOf}(\cdot) &=& \cdot \\
adamc@538 984 \mt{sigOf}(s \; \overline{s'}) &=& \mt{sigOf}(s) \; \mt{sigOf}(\overline{s'}) \\
adamc@538 985 \\
adamc@538 986 \mt{sigOf}(\mt{con} \; x :: \kappa = c) &=& \mt{con} \; x :: \kappa = c \\
adamc@538 987 \mt{sigOf}(\mt{datatype} \; x \; \overline{y} = \overline{dc}) &=& \mt{datatype} \; x \; \overline{y} = \overline{dc} \\
adamc@538 988 \mt{sigOf}(\mt{datatype} \; x = \mt{datatype} \; M.z) &=& \mt{datatype} \; x = \mt{datatype} \; M.z \\
adamc@538 989 \mt{sigOf}(\mt{val} \; x : \tau = e) &=& \mt{val} \; x : \tau \\
adamc@538 990 \mt{sigOf}(\mt{val} \; \mt{rec} \; \overline{x : \tau = e}) &=& \overline{\mt{val} \; x : \tau} \\
adamc@538 991 \mt{sigOf}(\mt{structure} \; X : S = M) &=& \mt{structure} \; X : S \\
adamc@538 992 \mt{sigOf}(\mt{signature} \; X = S) &=& \mt{signature} \; X = S \\
adamc@538 993 \mt{sigOf}(\mt{open} \; M) &=& \mt{include} \; S \textrm{ (where $\Gamma \vdash M : S$)} \\
adamc@538 994 \mt{sigOf}(\mt{constraint} \; c_1 \sim c_2) &=& \mt{constraint} \; c_1 \sim c_2 \\
adamc@538 995 \mt{sigOf}(\mt{open} \; \mt{constraints} \; M) &=& \cdot \\
adamc@538 996 \mt{sigOf}(\mt{table} \; x : c) &=& \mt{table} \; x : c \\
adamc@538 997 \mt{sigOf}(\mt{sequence} \; x) &=& \mt{sequence} \; x \\
adamc@538 998 \mt{sigOf}(\mt{cookie} \; x : \tau) &=& \mt{cookie} \; x : \tau \\
adamc@655 999 \mt{sigOf}(\mt{class} \; x :: \kappa = c) &=& \mt{class} \; x :: \kappa = c \\
adamc@538 1000 \end{eqnarray*}
adamc@539 1001 \begin{eqnarray*}
adamc@539 1002 \mt{selfify}(M, \cdot) &=& \cdot \\
adamc@558 1003 \mt{selfify}(M, s \; \overline{s'}) &=& \mt{selfify}(M, s) \; \mt{selfify}(M, \overline{s'}) \\
adamc@539 1004 \\
adamc@539 1005 \mt{selfify}(M, \mt{con} \; x :: \kappa) &=& \mt{con} \; x :: \kappa = M.x \\
adamc@539 1006 \mt{selfify}(M, \mt{con} \; x :: \kappa = c) &=& \mt{con} \; x :: \kappa = c \\
adamc@539 1007 \mt{selfify}(M, \mt{datatype} \; x \; \overline{y} = \overline{dc}) &=& \mt{datatype} \; x \; \overline{y} = \mt{datatype} \; M.x \\
adamc@539 1008 \mt{selfify}(M, \mt{datatype} \; x = \mt{datatype} \; M'.z) &=& \mt{datatype} \; x = \mt{datatype} \; M'.z \\
adamc@539 1009 \mt{selfify}(M, \mt{val} \; x : \tau) &=& \mt{val} \; x : \tau \\
adamc@539 1010 \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 1011 \mt{selfify}(M, \mt{signature} \; X = S) &=& \mt{signature} \; X = S \\
adamc@539 1012 \mt{selfify}(M, \mt{include} \; S) &=& \mt{include} \; S \\
adamc@539 1013 \mt{selfify}(M, \mt{constraint} \; c_1 \sim c_2) &=& \mt{constraint} \; c_1 \sim c_2 \\
adamc@655 1014 \mt{selfify}(M, \mt{class} \; x :: \kappa) &=& \mt{class} \; x :: \kappa = M.x \\
adamc@655 1015 \mt{selfify}(M, \mt{class} \; x :: \kappa = c) &=& \mt{class} \; x :: \kappa = c \\
adamc@539 1016 \end{eqnarray*}
adamc@539 1017
adamc@540 1018 \subsection{Module Projection}
adamc@540 1019
adamc@540 1020 \begin{eqnarray*}
adamc@540 1021 \mt{proj}(M, \mt{con} \; x :: \kappa \; \overline{s}, \mt{con} \; x) &=& \kappa \\
adamc@540 1022 \mt{proj}(M, \mt{con} \; x :: \kappa = c \; \overline{s}, \mt{con} \; x) &=& (\kappa, c) \\
adamc@540 1023 \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 1024 \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 1025 && \textrm{and $\mt{proj}(M', \overline{s'}, \mt{datatype} \; z) = (\overline{y}, \overline{dc})$)} \\
adamc@655 1026 \mt{proj}(M, \mt{class} \; x :: \kappa \; \overline{s}, \mt{con} \; x) &=& \kappa \to \mt{Type} \\
adamc@655 1027 \mt{proj}(M, \mt{class} \; x :: \kappa = c \; \overline{s}, \mt{con} \; x) &=& (\kappa \to \mt{Type}, c) \\
adamc@540 1028 \\
adamc@540 1029 \mt{proj}(M, \mt{datatype} \; x \; \overline{y} = \overline{dc} \; \overline{s}, \mt{datatype} \; x) &=& (\overline{y}, \overline{dc}) \\
adamc@540 1030 \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 1031 \\
adamc@540 1032 \mt{proj}(M, \mt{val} \; x : \tau \; \overline{s}, \mt{val} \; x) &=& \tau \\
adamc@540 1033 \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 1034 \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 1035 \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 1036 && \textrm{and $\mt{proj}(M', \overline{s'}, \mt{datatype} \; z = (\overline{y}, \overline{dc})$ and $X \in \overline{dc}$)} \\
adamc@540 1037 \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 1038 && \textrm{and $\mt{proj}(M', \overline{s'}, \mt{datatype} \; z = (\overline{y}, \overline{dc})$ and $X \; \mt{of} \; \tau \in \overline{dc}$)} \\
adamc@540 1039 \\
adamc@540 1040 \mt{proj}(M, \mt{structure} \; X : S \; \overline{s}, \mt{structure} \; X) &=& S \\
adamc@540 1041 \\
adamc@540 1042 \mt{proj}(M, \mt{signature} \; X = S \; \overline{s}, \mt{signature} \; X) &=& S \\
adamc@540 1043 \\
adamc@540 1044 \mt{proj}(M, \mt{con} \; x :: \kappa \; \overline{s}, V) &=& [x \mapsto M.x]\mt{proj}(M, \overline{s}, V) \\
adamc@540 1045 \mt{proj}(M, \mt{con} \; x :: \kappa = c \; \overline{s}, V) &=& [x \mapsto M.x]\mt{proj}(M, \overline{s}, V) \\
adamc@540 1046 \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 1047 \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 1048 \mt{proj}(M, \mt{val} \; x : \tau \; \overline{s}, V) &=& \mt{proj}(M, \overline{s}, V) \\
adamc@540 1049 \mt{proj}(M, \mt{structure} \; X : S \; \overline{s}, V) &=& [X \mapsto M.X]\mt{proj}(M, \overline{s}, V) \\
adamc@540 1050 \mt{proj}(M, \mt{signature} \; X = S \; \overline{s}, V) &=& [X \mapsto M.X]\mt{proj}(M, \overline{s}, V) \\
adamc@540 1051 \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 1052 \mt{proj}(M, \mt{constraint} \; c_1 \sim c_2 \; \overline{s}, V) &=& \mt{proj}(M, \overline{s}, V) \\
adamc@655 1053 \mt{proj}(M, \mt{class} \; x :: \kappa \; \overline{s}, V) &=& [x \mapsto M.x]\mt{proj}(M, \overline{s}, V) \\
adamc@655 1054 \mt{proj}(M, \mt{class} \; x :: \kappa = c \; \overline{s}, V) &=& [x \mapsto M.x]\mt{proj}(M, \overline{s}, V) \\
adamc@540 1055 \end{eqnarray*}
adamc@540 1056
adamc@541 1057
adamc@541 1058 \section{Type Inference}
adamc@541 1059
adamc@541 1060 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 1061
adamc@541 1062 \subsection{Basic Unification}
adamc@541 1063
adamc@560 1064 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 1065
adamc@656 1066 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 1067
adamc@541 1068 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 1069
adamc@541 1070 \subsection{Unifying Record Types}
adamc@541 1071
adamc@570 1072 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 1073
adamc@656 1074 \subsection{\label{typeclasses}Constructor Classes}
adamc@541 1075
adamc@656 1076 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 1077
adamc@656 1078 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 1079
adamc@656 1080 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 1081
adamc@656 1082 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 1083
adamc@541 1084 \subsection{Reverse-Engineering Record Types}
adamc@541 1085
adamc@656 1086 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 1087
adamc@541 1088 \subsection{Implicit Arguments in Functor Applications}
adamc@541 1089
adamc@656 1090 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 1091
adamc@541 1092
adamc@542 1093 \section{The Ur Standard Library}
adamc@542 1094
adamc@542 1095 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 1096
adamc@542 1097 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 1098
adamc@542 1099 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 1100 $$\begin{array}{l}
adamc@542 1101 \mt{type} \; \mt{int} \\
adamc@542 1102 \mt{type} \; \mt{float} \\
adamc@542 1103 \mt{type} \; \mt{string} \\
adamc@542 1104 \mt{type} \; \mt{time} \\
adamc@542 1105 \\
adamc@542 1106 \mt{type} \; \mt{unit} = \{\} \\
adamc@542 1107 \\
adamc@542 1108 \mt{datatype} \; \mt{bool} = \mt{False} \mid \mt{True} \\
adamc@542 1109 \\
adamc@542 1110 \mt{datatype} \; \mt{option} \; \mt{t} = \mt{None} \mid \mt{Some} \; \mt{of} \; \mt{t}
adamc@542 1111 \end{array}$$
adamc@542 1112
adamc@657 1113 Another important generic Ur element comes at the beginning of \texttt{top.urs}.
adamc@657 1114
adamc@657 1115 $$\begin{array}{l}
adamc@657 1116 \mt{con} \; \mt{folder} :: \mt{K} \longrightarrow \{\mt{K}\} \to \mt{Type} \\
adamc@657 1117 \\
adamc@657 1118 \mt{val} \; \mt{fold} : \mt{K} \longrightarrow \mt{tf} :: (\{\mt{K}\} \to \mt{Type}) \\
adamc@657 1119 \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 1120 \hspace{.2in} \mt{tf} \; \mt{r} \to \mt{tf} \; ([\mt{nm} = \mt{v}] \rc \mt{r})) \\
adamc@657 1121 \hspace{.1in} \to \mt{tf} \; [] \\
adamc@657 1122 \hspace{.1in} \to \mt{r} :: \{\mt{K}\} \to \mt{folder} \; \mt{r} \to \mt{tf} \; \mt{r}
adamc@657 1123 \end{array}$$
adamc@657 1124
adamc@657 1125 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 1126
adamc@657 1127 The Ur compiler treates $\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 1128
adamc@542 1129
adamc@542 1130 \section{The Ur/Web Standard Library}
adamc@542 1131
adamc@542 1132 \subsection{Transactions}
adamc@542 1133
adamc@542 1134 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 1135 $$\begin{array}{l}
adamc@542 1136 \mt{con} \; \mt{transaction} :: \mt{Type} \to \mt{Type} \\
adamc@542 1137 \\
adamc@542 1138 \mt{val} \; \mt{return} : \mt{t} ::: \mt{Type} \to \mt{t} \to \mt{transaction} \; \mt{t} \\
adamc@542 1139 \mt{val} \; \mt{bind} : \mt{t_1} ::: \mt{Type} \to \mt{t_2} ::: \mt{Type} \to \mt{transaction} \; \mt{t_1} \to (\mt{t_1} \to \mt{transaction} \; \mt{t_2}) \to \mt{transaction} \; \mt{t_2}
adamc@542 1140 \end{array}$$
adamc@542 1141
adamc@542 1142 \subsection{HTTP}
adamc@542 1143
adamc@542 1144 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 1145 $$\begin{array}{l}
adamc@542 1146 \mt{val} \; \mt{requestHeader} : \mt{string} \to \mt{transaction} \; (\mt{option} \; \mt{string}) \\
adamc@542 1147 \\
adamc@542 1148 \mt{con} \; \mt{http\_cookie} :: \mt{Type} \to \mt{Type} \\
adamc@542 1149 \mt{val} \; \mt{getCookie} : \mt{t} ::: \mt{Type} \to \mt{http\_cookie} \; \mt{t} \to \mt{transaction} \; (\mt{option} \; \mt{t}) \\
adamc@542 1150 \mt{val} \; \mt{setCookie} : \mt{t} ::: \mt{Type} \to \mt{http\_cookie} \; \mt{t} \to \mt{t} \to \mt{transaction} \; \mt{unit}
adamc@542 1151 \end{array}$$
adamc@542 1152
adamc@543 1153 \subsection{SQL}
adamc@543 1154
adamc@543 1155 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 1156 $$\begin{array}{l}
adamc@543 1157 \mt{con} \; \mt{sql\_table} :: \{\mt{Type}\} \to \mt{Type}
adamc@543 1158 \end{array}$$
adamc@543 1159
adamc@543 1160 \subsubsection{Queries}
adamc@543 1161
adamc@543 1162 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 1163 $$\begin{array}{l}
adamc@543 1164 \mt{con} \; \mt{sql\_query} :: \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \\
adamc@543 1165 \mt{val} \; \mt{sql\_query} : \mt{tables} ::: \{\{\mt{Type}\}\} \\
adamc@543 1166 \hspace{.1in} \to \mt{selectedFields} ::: \{\{\mt{Type}\}\} \\
adamc@543 1167 \hspace{.1in} \to \mt{selectedExps} ::: \{\mt{Type}\} \\
adamc@543 1168 \hspace{.1in} \to \{\mt{Rows} : \mt{sql\_query1} \; \mt{tables} \; \mt{selectedFields} \; \mt{selectedExps}, \\
adamc@543 1169 \hspace{.2in} \mt{OrderBy} : \mt{sql\_order\_by} \; \mt{tables} \; \mt{selectedExps}, \\
adamc@543 1170 \hspace{.2in} \mt{Limit} : \mt{sql\_limit}, \\
adamc@543 1171 \hspace{.2in} \mt{Offset} : \mt{sql\_offset}\} \\
adamc@543 1172 \hspace{.1in} \to \mt{sql\_query} \; \mt{selectedFields} \; \mt{selectedExps}
adamc@543 1173 \end{array}$$
adamc@543 1174
adamc@545 1175 Queries are used by folding over their results inside transactions.
adamc@545 1176 $$\begin{array}{l}
adamc@545 1177 \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@545 1178 \hspace{.1in} \to (\$(\mt{exps} \rc \mt{fold} \; (\lambda \mt{nm} \; (\mt{fields} :: \{\mt{Type}\}) \; \mt{acc} \; [[\mt{nm}] \sim \mt{acc}] \Rightarrow [\mt{nm} = \$\mt{fields}] \rc \mt{acc}) \; [] \; \mt{tables}) \\
adamc@545 1179 \hspace{.2in} \to \mt{state} \to \mt{transaction} \; \mt{state}) \\
adamc@545 1180 \hspace{.1in} \to \mt{state} \to \mt{transaction} \; \mt{state}
adamc@545 1181 \end{array}$$
adamc@545 1182
adamc@543 1183 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 1184 $$\begin{array}{l}
adamc@543 1185 \mt{con} \; \mt{sql\_query1} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \\
adamc@543 1186 \\
adamc@543 1187 \mt{type} \; \mt{sql\_relop} \\
adamc@543 1188 \mt{val} \; \mt{sql\_union} : \mt{sql\_relop} \\
adamc@543 1189 \mt{val} \; \mt{sql\_intersect} : \mt{sql\_relop} \\
adamc@543 1190 \mt{val} \; \mt{sql\_except} : \mt{sql\_relop} \\
adamc@543 1191 \mt{val} \; \mt{sql\_relop} : \mt{tables1} ::: \{\{\mt{Type}\}\} \\
adamc@543 1192 \hspace{.1in} \to \mt{tables2} ::: \{\{\mt{Type}\}\} \\
adamc@543 1193 \hspace{.1in} \to \mt{selectedFields} ::: \{\{\mt{Type}\}\} \\
adamc@543 1194 \hspace{.1in} \to \mt{selectedExps} ::: \{\mt{Type}\} \\
adamc@543 1195 \hspace{.1in} \to \mt{sql\_relop} \\
adamc@543 1196 \hspace{.1in} \to \mt{sql\_query1} \; \mt{tables1} \; \mt{selectedFields} \; \mt{selectedExps} \\
adamc@543 1197 \hspace{.1in} \to \mt{sql\_query1} \; \mt{tables2} \; \mt{selectedFields} \; \mt{selectedExps} \\
adamc@543 1198 \hspace{.1in} \to \mt{sql\_query1} \; \mt{selectedFields} \; \mt{selectedFields} \; \mt{selectedExps}
adamc@543 1199 \end{array}$$
adamc@543 1200
adamc@543 1201 $$\begin{array}{l}
adamc@543 1202 \mt{val} \; \mt{sql\_query1} : \mt{tables} ::: \{\{\mt{Type}\}\} \\
adamc@543 1203 \hspace{.1in} \to \mt{grouped} ::: \{\{\mt{Type}\}\} \\
adamc@543 1204 \hspace{.1in} \to \mt{selectedFields} ::: \{\{\mt{Type}\}\} \\
adamc@543 1205 \hspace{.1in} \to \mt{selectedExps} ::: \{\mt{Type}\} \\
adamc@543 1206 \hspace{.1in} \to \{\mt{From} : \$(\mt{fold} \; (\lambda \mt{nm} \; (\mt{fields} :: \{\mt{Type}\}) \; \mt{acc} \; [[\mt{nm}] \sim \mt{acc}] \Rightarrow [\mt{nm} = \mt{sql\_table} \; \mt{fields}] \rc \mt{acc}) \; [] \; \mt{tables}), \\
adamc@543 1207 \hspace{.2in} \mt{Where} : \mt{sql\_exp} \; \mt{tables} \; [] \; [] \; \mt{bool}, \\
adamc@543 1208 \hspace{.2in} \mt{GroupBy} : \mt{sql\_subset} \; \mt{tables} \; \mt{grouped}, \\
adamc@543 1209 \hspace{.2in} \mt{Having} : \mt{sql\_exp} \; \mt{grouped} \; \mt{tables} \; [] \; \mt{bool}, \\
adamc@543 1210 \hspace{.2in} \mt{SelectFields} : \mt{sql\_subset} \; \mt{grouped} \; \mt{selectedFields}, \\
adamc@543 1211 \hspace{.2in} \mt {SelectExps} : \$(\mt{fold} \; (\lambda \mt{nm} \; (\mt{t} :: \mt{Type}) \; \mt{acc} \; [[\mt{nm}] \sim \mt{acc}] \Rightarrow [\mt{nm} = \mt{sql\_exp} \; \mt{grouped} \; \mt{tables} \; [] \; \mt{t}] \rc \mt{acc}) \; [] \; \mt{selectedExps}) \} \\
adamc@543 1212 \hspace{.1in} \to \mt{sql\_query1} \; \mt{tables} \; \mt{selectedFields} \; \mt{selectedExps}
adamc@543 1213 \end{array}$$
adamc@543 1214
adamc@543 1215 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 1216 $$\begin{array}{l}
adamc@543 1217 \mt{con} \; \mt{sql\_subset} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \mt{Type} \\
adamc@543 1218 \mt{val} \; \mt{sql\_subset} : \mt{keep\_drop} :: \{(\{\mt{Type}\} \times \{\mt{Type}\})\} \\
adamc@543 1219 \hspace{.1in} \to \mt{sql\_subset} \\
adamc@543 1220 \hspace{.2in} (\mt{fold} \; (\lambda \mt{nm} \; (\mt{fields} :: (\{\mt{Type}\} \times \{\mt{Type}\})) \; \mt{acc} \; [[\mt{nm}] \sim \mt{acc}] \; [\mt{fields}.1 \sim \mt{fields}.2] \Rightarrow \\
adamc@543 1221 \hspace{.3in} [\mt{nm} = \mt{fields}.1 \rc \mt{fields}.2] \rc \mt{acc}) \; [] \; \mt{keep\_drop}) \\
adamc@543 1222 \hspace{.2in} (\mt{fold} \; (\lambda \mt{nm} \; (\mt{fields} :: (\{\mt{Type}\} \times \{\mt{Type}\})) \; \mt{acc} \; [[\mt{nm}] \sim \mt{acc}] \Rightarrow [\mt{nm} = \mt{fields}.1] \rc \mt{acc}) \; [] \; \mt{keep\_drop}) \\
adamc@543 1223 \mt{val} \; \mt{sql\_subset\_all} : \mt{tables} :: \{\{\mt{Type}\}\} \to \mt{sql\_subset} \; \mt{tables} \; \mt{tables}
adamc@543 1224 \end{array}$$
adamc@543 1225
adamc@560 1226 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 1227 $$\begin{array}{l}
adamc@543 1228 \mt{con} \; \mt{sql\_exp} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \to \mt{Type}
adamc@543 1229 \end{array}$$
adamc@543 1230
adamc@543 1231 Any field in scope may be converted to an expression.
adamc@543 1232 $$\begin{array}{l}
adamc@543 1233 \mt{val} \; \mt{sql\_field} : \mt{otherTabs} ::: \{\{\mt{Type}\}\} \to \mt{otherFields} ::: \{\mt{Type}\} \\
adamc@543 1234 \hspace{.1in} \to \mt{fieldType} ::: \mt{Type} \to \mt{agg} ::: \{\{\mt{Type}\}\} \\
adamc@543 1235 \hspace{.1in} \to \mt{exps} ::: \{\mt{Type}\} \\
adamc@543 1236 \hspace{.1in} \to \mt{tab} :: \mt{Name} \to \mt{field} :: \mt{Name} \\
adamc@543 1237 \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 1238 \end{array}$$
adamc@543 1239
adamc@544 1240 There is an analogous function for referencing named expressions.
adamc@544 1241 $$\begin{array}{l}
adamc@544 1242 \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 1243 \hspace{.1in} \to \mt{sql\_exp} \; \mt{tabs} \; \mt{agg} \; ([\mt{nm} = \mt{t}] \rc \mt{rest}) \; \mt{t}
adamc@544 1244 \end{array}$$
adamc@544 1245
adamc@544 1246 Ur values of appropriate types may be injected into SQL expressions.
adamc@544 1247 $$\begin{array}{l}
adamc@544 1248 \mt{class} \; \mt{sql\_injectable} \\
adamc@544 1249 \mt{val} \; \mt{sql\_bool} : \mt{sql\_injectable} \; \mt{bool} \\
adamc@544 1250 \mt{val} \; \mt{sql\_int} : \mt{sql\_injectable} \; \mt{int} \\
adamc@544 1251 \mt{val} \; \mt{sql\_float} : \mt{sql\_injectable} \; \mt{float} \\
adamc@544 1252 \mt{val} \; \mt{sql\_string} : \mt{sql\_injectable} \; \mt{string} \\
adamc@544 1253 \mt{val} \; \mt{sql\_time} : \mt{sql\_injectable} \; \mt{time} \\
adamc@544 1254 \mt{val} \; \mt{sql\_option\_bool} : \mt{sql\_injectable} \; (\mt{option} \; \mt{bool}) \\
adamc@544 1255 \mt{val} \; \mt{sql\_option\_int} : \mt{sql\_injectable} \; (\mt{option} \; \mt{int}) \\
adamc@544 1256 \mt{val} \; \mt{sql\_option\_float} : \mt{sql\_injectable} \; (\mt{option} \; \mt{float}) \\
adamc@544 1257 \mt{val} \; \mt{sql\_option\_string} : \mt{sql\_injectable} \; (\mt{option} \; \mt{string}) \\
adamc@544 1258 \mt{val} \; \mt{sql\_option\_time} : \mt{sql\_injectable} \; (\mt{option} \; \mt{time}) \\
adamc@544 1259 \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 1260 \hspace{.1in} \to \mt{t} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t}
adamc@544 1261 \end{array}$$
adamc@544 1262
adamc@544 1263 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 1264 $$\begin{array}{l}
adamc@544 1265 \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 1266 \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 1267 \end{array}$$
adamc@544 1268
adamc@559 1269 We have generic nullary, unary, and binary operators.
adamc@544 1270 $$\begin{array}{l}
adamc@544 1271 \mt{con} \; \mt{sql\_nfunc} :: \mt{Type} \to \mt{Type} \\
adamc@544 1272 \mt{val} \; \mt{sql\_current\_timestamp} : \mt{sql\_nfunc} \; \mt{time} \\
adamc@544 1273 \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 1274 \hspace{.1in} \to \mt{sql\_nfunc} \; \mt{t} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} \\\end{array}$$
adamc@544 1275
adamc@544 1276 $$\begin{array}{l}
adamc@544 1277 \mt{con} \; \mt{sql\_unary} :: \mt{Type} \to \mt{Type} \to \mt{Type} \\
adamc@544 1278 \mt{val} \; \mt{sql\_not} : \mt{sql\_unary} \; \mt{bool} \; \mt{bool} \\
adamc@544 1279 \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 1280 \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 1281 \end{array}$$
adamc@544 1282
adamc@544 1283 $$\begin{array}{l}
adamc@544 1284 \mt{con} \; \mt{sql\_binary} :: \mt{Type} \to \mt{Type} \to \mt{Type} \to \mt{Type} \\
adamc@544 1285 \mt{val} \; \mt{sql\_and} : \mt{sql\_binary} \; \mt{bool} \; \mt{bool} \; \mt{bool} \\
adamc@544 1286 \mt{val} \; \mt{sql\_or} : \mt{sql\_binary} \; \mt{bool} \; \mt{bool} \; \mt{bool} \\
adamc@544 1287 \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 1288 \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 1289 \end{array}$$
adamc@544 1290
adamc@544 1291 $$\begin{array}{l}
adamc@559 1292 \mt{class} \; \mt{sql\_arith} \\
adamc@559 1293 \mt{val} \; \mt{sql\_int\_arith} : \mt{sql\_arith} \; \mt{int} \\
adamc@559 1294 \mt{val} \; \mt{sql\_float\_arith} : \mt{sql\_arith} \; \mt{float} \\
adamc@559 1295 \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 1296 \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 1297 \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 1298 \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 1299 \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 1300 \mt{val} \; \mt{sql\_mod} : \mt{sql\_binary} \; \mt{int} \; \mt{int} \; \mt{int}
adamc@559 1301 \end{array}$$
adamc@544 1302
adamc@656 1303 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 1304
adamc@544 1305 $$\begin{array}{l}
adamc@544 1306 \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 1307 \end{array}$$
adamc@544 1308
adamc@544 1309 $$\begin{array}{l}
adamc@544 1310 \mt{con} \; \mt{sql\_aggregate} :: \mt{Type} \to \mt{Type} \\
adamc@544 1311 \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 1312 \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 1313 \end{array}$$
adamc@544 1314
adamc@544 1315 $$\begin{array}{l}
adamc@544 1316 \mt{class} \; \mt{sql\_summable} \\
adamc@544 1317 \mt{val} \; \mt{sql\_summable\_int} : \mt{sql\_summable} \; \mt{int} \\
adamc@544 1318 \mt{val} \; \mt{sql\_summable\_float} : \mt{sql\_summable} \; \mt{float} \\
adamc@544 1319 \mt{val} \; \mt{sql\_avg} : \mt{t} ::: \mt{Type} \to \mt{sql\_summable} \; \mt{t} \to \mt{sql\_aggregate} \; \mt{t} \\
adamc@544 1320 \mt{val} \; \mt{sql\_sum} : \mt{t} ::: \mt{Type} \to \mt{sql\_summable} \mt{t} \to \mt{sql\_aggregate} \; \mt{t}
adamc@544 1321 \end{array}$$
adamc@544 1322
adamc@544 1323 $$\begin{array}{l}
adamc@544 1324 \mt{class} \; \mt{sql\_maxable} \\
adamc@544 1325 \mt{val} \; \mt{sql\_maxable\_int} : \mt{sql\_maxable} \; \mt{int} \\
adamc@544 1326 \mt{val} \; \mt{sql\_maxable\_float} : \mt{sql\_maxable} \; \mt{float} \\
adamc@544 1327 \mt{val} \; \mt{sql\_maxable\_string} : \mt{sql\_maxable} \; \mt{string} \\
adamc@544 1328 \mt{val} \; \mt{sql\_maxable\_time} : \mt{sql\_maxable} \; \mt{time} \\
adamc@544 1329 \mt{val} \; \mt{sql\_max} : \mt{t} ::: \mt{Type} \to \mt{sql\_maxable} \; \mt{t} \to \mt{sql\_aggregate} \; \mt{t} \\
adamc@544 1330 \mt{val} \; \mt{sql\_min} : \mt{t} ::: \mt{Type} \to \mt{sql\_maxable} \; \mt{t} \to \mt{sql\_aggregate} \; \mt{t}
adamc@544 1331 \end{array}$$
adamc@544 1332
adamc@544 1333 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 1334 $$\begin{array}{l}
adamc@544 1335 \mt{type} \; \mt{sql\_direction} \\
adamc@544 1336 \mt{val} \; \mt{sql\_asc} : \mt{sql\_direction} \\
adamc@544 1337 \mt{val} \; \mt{sql\_desc} : \mt{sql\_direction} \\
adamc@544 1338 \\
adamc@544 1339 \mt{con} \; \mt{sql\_order\_by} :: \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \\
adamc@544 1340 \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 1341 \mt{val} \; \mt{sql\_order\_by\_Cons} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{t} ::: \mt{Type} \\
adamc@544 1342 \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 1343 \\
adamc@544 1344 \mt{type} \; \mt{sql\_limit} \\
adamc@544 1345 \mt{val} \; \mt{sql\_no\_limit} : \mt{sql\_limit} \\
adamc@544 1346 \mt{val} \; \mt{sql\_limit} : \mt{int} \to \mt{sql\_limit} \\
adamc@544 1347 \\
adamc@544 1348 \mt{type} \; \mt{sql\_offset} \\
adamc@544 1349 \mt{val} \; \mt{sql\_no\_offset} : \mt{sql\_offset} \\
adamc@544 1350 \mt{val} \; \mt{sql\_offset} : \mt{int} \to \mt{sql\_offset}
adamc@544 1351 \end{array}$$
adamc@544 1352
adamc@545 1353
adamc@545 1354 \subsubsection{DML}
adamc@545 1355
adamc@545 1356 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 1357
adamc@545 1358 $$\begin{array}{l}
adamc@545 1359 \mt{type} \; \mt{dml} \\
adamc@545 1360 \mt{val} \; \mt{dml} : \mt{dml} \to \mt{transaction} \; \mt{unit}
adamc@545 1361 \end{array}$$
adamc@545 1362
adamc@545 1363 Properly-typed records may be used to form $\mt{INSERT}$ commands.
adamc@545 1364 $$\begin{array}{l}
adamc@545 1365 \mt{val} \; \mt{insert} : \mt{fields} ::: \{\mt{Type}\} \to \mt{sql\_table} \; \mt{fields} \\
adamc@545 1366 \hspace{.1in} \to \$(\mt{fold} \; (\lambda \mt{nm} \; (\mt{t} :: \mt{Type}) \; \mt{acc} \; [[\mt{nm}] \sim \mt{acc}] \Rightarrow [\mt{nm} = \mt{sql\_exp} \; [] \; [] \; [] \; \mt{t}] \rc \mt{acc}) \; [] \; \mt{fields}) \to \mt{dml}
adamc@545 1367 \end{array}$$
adamc@545 1368
adamc@545 1369 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 1370 $$\begin{array}{l}
adamc@545 1371 \mt{val} \; \mt{update} : \mt{unchanged} ::: \{\mt{Type}\} \to \mt{changed} :: \{\mt{Type}\} \to \lambda [\mt{changed} \sim \mt{unchanged}] \\
adamc@545 1372 \hspace{.1in} \Rightarrow \$(\mt{fold} \; (\lambda \mt{nm} \; (\mt{t} :: \mt{Type}) \; \mt{acc} \; [[\mt{nm}] \sim \mt{acc}] \Rightarrow [\mt{nm} = \mt{sql\_exp} \; [\mt{T} = \mt{changed} \rc \mt{unchanged}] \; [] \; [] \; \mt{t}] \rc \mt{acc}) \; [] \; \mt{changed}) \\
adamc@545 1373 \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 1374 \end{array}$$
adamc@545 1375
adamc@545 1376 A $\mt{DELETE}$ command is formed from a table and a $\mt{WHERE}$ clause.
adamc@545 1377 $$\begin{array}{l}
adamc@545 1378 \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 1379 \end{array}$$
adamc@545 1380
adamc@546 1381 \subsubsection{Sequences}
adamc@546 1382
adamc@546 1383 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 1384
adamc@546 1385 $$\begin{array}{l}
adamc@546 1386 \mt{type} \; \mt{sql\_sequence} \\
adamc@546 1387 \mt{val} \; \mt{nextval} : \mt{sql\_sequence} \to \mt{transaction} \; \mt{int}
adamc@546 1388 \end{array}$$
adamc@546 1389
adamc@546 1390
adamc@547 1391 \subsection{XML}
adamc@547 1392
adamc@547 1393 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 1394
adamc@547 1395 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 1396 $$\begin{array}{l}
adamc@547 1397 \mt{con} \; \mt{xml} :: \{\mt{Unit}\} \to \{\mt{Type}\} \to \{\mt{Type}\} \to \mt{Type}
adamc@547 1398 \end{array}$$
adamc@547 1399
adamc@547 1400 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 1401 $$\begin{array}{l}
adamc@547 1402 \mt{con} \; \mt{tag} :: \{\mt{Type}\} \to \{\mt{Unit}\} \to \{\mt{Unit}\} \to \{\mt{Type}\} \to \{\mt{Type}\} \to \mt{Type}
adamc@547 1403 \end{array}$$
adamc@547 1404
adamc@547 1405 Literal text may be injected into XML as ``CDATA.''
adamc@547 1406 $$\begin{array}{l}
adamc@547 1407 \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 1408 \end{array}$$
adamc@547 1409
adamc@547 1410 There is a function for producing an XML tree with a particular tag at its root.
adamc@547 1411 $$\begin{array}{l}
adamc@547 1412 \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 1413 \hspace{.1in} \to \mt{useOuter} ::: \{\mt{Type}\} \to \mt{useInner} ::: \{\mt{Type}\} \to \mt{bindOuter} ::: \{\mt{Type}\} \to \mt{bindInner} ::: \{\mt{Type}\} \\
adamc@547 1414 \hspace{.1in} \to \lambda [\mt{attrsGiven} \sim \mt{attrsAbsent}] \; [\mt{useOuter} \sim \mt{useInner}] \; [\mt{bindOuter} \sim \mt{bindInner}] \Rightarrow \$\mt{attrsGiven} \\
adamc@547 1415 \hspace{.1in} \to \mt{tag} \; (\mt{attrsGiven} \rc \mt{attrsAbsent}) \; \mt{ctxOuter} \; \mt{ctxInner} \; \mt{useOuter} \; \mt{bindOuter} \\
adamc@547 1416 \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 1417 \end{array}$$
adamc@547 1418
adamc@547 1419 Two XML fragments may be concatenated.
adamc@547 1420 $$\begin{array}{l}
adamc@547 1421 \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 1422 \hspace{.1in} \to \lambda [\mt{use_1} \sim \mt{bind_1}] \; [\mt{bind_1} \sim \mt{bind_2}] \\
adamc@547 1423 \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 1424 \end{array}$$
adamc@547 1425
adamc@547 1426 Finally, any XML fragment may be updated to ``claim'' to use more form fields than it does.
adamc@547 1427 $$\begin{array}{l}
adamc@547 1428 \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 1429 \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 1430 \end{array}$$
adamc@547 1431
adamc@547 1432 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 1433
adamc@547 1434 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 1435 $$\begin{array}{l}
adamc@547 1436 \mt{val} \; \mt{error} : \mt{t} ::: \mt{Type} \to \mt{xml} \; [\mt{Body}] \; [] \; [] \to \mt{t}
adamc@547 1437 \end{array}$$
adamc@547 1438
adamc@549 1439
adamc@549 1440 \section{Ur/Web Syntax Extensions}
adamc@549 1441
adamc@549 1442 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 1443
adamc@549 1444 \subsection{SQL}
adamc@549 1445
adamc@549 1446 \subsubsection{Queries}
adamc@549 1447
adamc@550 1448 Queries $Q$ are added to the rules for expressions $e$.
adamc@550 1449
adamc@549 1450 $$\begin{array}{rrcll}
adamc@550 1451 \textrm{Queries} & Q &::=& (q \; [\mt{ORDER} \; \mt{BY} \; (E \; [o],)^+] \; [\mt{LIMIT} \; N] \; [\mt{OFFSET} \; N]) \\
adamc@549 1452 \textrm{Pre-queries} & q &::=& \mt{SELECT} \; P \; \mt{FROM} \; T,^+ \; [\mt{WHERE} \; E] \; [\mt{GROUP} \; \mt{BY} \; p,^+] \; [\mt{HAVING} \; E] \\
adamc@549 1453 &&& \mid q \; R \; q \\
adamc@549 1454 \textrm{Relational operators} & R &::=& \mt{UNION} \mid \mt{INTERSECT} \mid \mt{EXCEPT}
adamc@549 1455 \end{array}$$
adamc@549 1456
adamc@549 1457 $$\begin{array}{rrcll}
adamc@549 1458 \textrm{Projections} & P &::=& \ast & \textrm{all columns} \\
adamc@549 1459 &&& p,^+ & \textrm{particular columns} \\
adamc@549 1460 \textrm{Pre-projections} & p &::=& t.f & \textrm{one column from a table} \\
adamc@558 1461 &&& t.\{\{c\}\} & \textrm{a record of columns from a table (of kind $\{\mt{Type}\}$)} \\
adamc@549 1462 \textrm{Table names} & t &::=& x & \textrm{constant table name (automatically capitalized)} \\
adamc@549 1463 &&& X & \textrm{constant table name} \\
adamc@549 1464 &&& \{\{c\}\} & \textrm{computed table name (of kind $\mt{Name}$)} \\
adamc@549 1465 \textrm{Column names} & f &::=& X & \textrm{constant column name} \\
adamc@549 1466 &&& \{c\} & \textrm{computed column name (of kind $\mt{Name}$)} \\
adamc@549 1467 \textrm{Tables} & T &::=& x & \textrm{table variable, named locally by its own capitalization} \\
adamc@549 1468 &&& x \; \mt{AS} \; t & \textrm{table variable, with local name} \\
adamc@549 1469 &&& \{\{e\}\} \; \mt{AS} \; t & \textrm{computed table expression, with local name} \\
adamc@549 1470 \textrm{SQL expressions} & E &::=& p & \textrm{column references} \\
adamc@549 1471 &&& X & \textrm{named expression references} \\
adamc@549 1472 &&& \{\{e\}\} & \textrm{injected native Ur expressions} \\
adamc@549 1473 &&& \{e\} & \textrm{computed expressions, probably using $\mt{sql\_exp}$ directly} \\
adamc@549 1474 &&& \mt{TRUE} \mid \mt{FALSE} & \textrm{boolean constants} \\
adamc@549 1475 &&& \ell & \textrm{primitive type literals} \\
adamc@549 1476 &&& \mt{NULL} & \textrm{null value (injection of $\mt{None}$)} \\
adamc@549 1477 &&& E \; \mt{IS} \; \mt{NULL} & \textrm{nullness test} \\
adamc@549 1478 &&& n & \textrm{nullary operators} \\
adamc@549 1479 &&& u \; E & \textrm{unary operators} \\
adamc@549 1480 &&& E \; b \; E & \textrm{binary operators} \\
adamc@549 1481 &&& \mt{COUNT}(\ast) & \textrm{count number of rows} \\
adamc@549 1482 &&& a(E) & \textrm{other aggregate function} \\
adamc@549 1483 &&& (E) & \textrm{explicit precedence} \\
adamc@549 1484 \textrm{Nullary operators} & n &::=& \mt{CURRENT\_TIMESTAMP} \\
adamc@549 1485 \textrm{Unary operators} & u &::=& \mt{NOT} \\
adamc@549 1486 \textrm{Binary operators} & b &::=& \mt{AND} \mid \mt{OR} \mid \neq \mid < \mid \leq \mid > \mid \geq \\
adamc@549 1487 \textrm{Aggregate functions} & a &::=& \mt{AVG} \mid \mt{SUM} \mid \mt{MIN} \mid \mt{MAX} \\
adamc@550 1488 \textrm{Directions} & o &::=& \mt{ASC} \mid \mt{DESC} \\
adamc@549 1489 \textrm{SQL integer} & N &::=& n \mid \{e\} \\
adamc@549 1490 \end{array}$$
adamc@549 1491
adamc@549 1492 Additionally, an SQL expression may be inserted into normal Ur code with the syntax $(\mt{SQL} \; E)$ or $(\mt{WHERE} \; E)$.
adamc@549 1493
adamc@550 1494 \subsubsection{DML}
adamc@550 1495
adamc@550 1496 DML commands $D$ are added to the rules for expressions $e$.
adamc@550 1497
adamc@550 1498 $$\begin{array}{rrcll}
adamc@550 1499 \textrm{Commands} & D &::=& (\mt{INSERT} \; \mt{INTO} \; T^E \; (f,^+) \; \mt{VALUES} \; (E,^+)) \\
adamc@550 1500 &&& (\mt{UPDATE} \; T^E \; \mt{SET} \; (f = E,)^+ \; \mt{WHERE} \; E) \\
adamc@550 1501 &&& (\mt{DELETE} \; \mt{FROM} \; T^E \; \mt{WHERE} \; E) \\
adamc@550 1502 \textrm{Table expressions} & T^E &::=& x \mid \{\{e\}\}
adamc@550 1503 \end{array}$$
adamc@550 1504
adamc@550 1505 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 1506
adamc@551 1507 \subsection{XML}
adamc@551 1508
adamc@551 1509 XML fragments $L$ are added to the rules for expressions $e$.
adamc@551 1510
adamc@551 1511 $$\begin{array}{rrcll}
adamc@551 1512 \textrm{XML fragments} & L &::=& \texttt{<xml/>} \mid \texttt{<xml>}l^*\texttt{</xml>} \\
adamc@551 1513 \textrm{XML pieces} & l &::=& \textrm{text} & \textrm{cdata} \\
adamc@551 1514 &&& \texttt{<}g\texttt{/>} & \textrm{tag with no children} \\
adamc@551 1515 &&& \texttt{<}g\texttt{>}l^*\texttt{</}x\texttt{>} & \textrm{tag with children} \\
adamc@559 1516 &&& \{e\} & \textrm{computed XML fragment} \\
adamc@559 1517 &&& \{[e]\} & \textrm{injection of an Ur expression, via the $\mt{Top}.\mt{txt}$ function} \\
adamc@551 1518 \textrm{Tag} & g &::=& h \; (x = v)^* \\
adamc@551 1519 \textrm{Tag head} & h &::=& x & \textrm{tag name} \\
adamc@551 1520 &&& h\{c\} & \textrm{constructor parameter} \\
adamc@551 1521 \textrm{Attribute value} & v &::=& \ell & \textrm{literal value} \\
adamc@551 1522 &&& \{e\} & \textrm{computed value} \\
adamc@551 1523 \end{array}$$
adamc@551 1524
adamc@552 1525
adamc@553 1526 \section{The Structure of Web Applications}
adamc@553 1527
adamc@553 1528 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 1529
adamc@553 1530 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 1531
adamc@553 1532 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 1533
adamc@558 1534 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 1535
adamc@553 1536
adamc@552 1537 \section{Compiler Phases}
adamc@552 1538
adamc@552 1539 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 1540
adamc@552 1541 In this section, we step through the main phases of compilation, noting what consequences each phase has for effective programming.
adamc@552 1542
adamc@552 1543 \subsection{Parse}
adamc@552 1544
adamc@552 1545 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 1546
adamc@552 1547 \subsection{Elaborate}
adamc@552 1548
adamc@552 1549 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 1550
adamc@552 1551 \subsection{Unnest}
adamc@552 1552
adamc@552 1553 Named local function definitions are moved to the top level, to avoid the need to generate closures.
adamc@552 1554
adamc@552 1555 \subsection{Corify}
adamc@552 1556
adamc@552 1557 Module system features are compiled away, through inlining of functor definitions at application sites. Afterward, most abstraction boundaries are broken, facilitating optimization.
adamc@552 1558
adamc@552 1559 \subsection{Especialize}
adamc@552 1560
adamc@552 1561 Functions are specialized to particular argument patterns. This is an important trick for avoiding the need to maintain any closures at runtime.
adamc@552 1562
adamc@552 1563 \subsection{Untangle}
adamc@552 1564
adamc@552 1565 Remove unnecessary mutual recursion, splitting recursive groups into strongly-connected components.
adamc@552 1566
adamc@552 1567 \subsection{Shake}
adamc@552 1568
adamc@552 1569 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 1570
adamc@553 1571 \subsection{\label{tag}Tag}
adamc@552 1572
adamc@552 1573 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 1574
adamc@552 1575 \subsection{Reduce}
adamc@552 1576
adamc@552 1577 Apply definitional equality rules to simplify the program as much as possible. This effectively includes inlining of every non-recursive definition.
adamc@552 1578
adamc@552 1579 \subsection{Unpoly}
adamc@552 1580
adamc@552 1581 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 1582
adamc@552 1583 \subsection{Specialize}
adamc@552 1584
adamc@558 1585 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 1586
adamc@552 1587 \subsection{Shake}
adamc@552 1588
adamc@558 1589 Here the compiler repeats the earlier Shake phase.
adamc@552 1590
adamc@552 1591 \subsection{Monoize}
adamc@552 1592
adamc@552 1593 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 1594
adamc@552 1595 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@552 1596 \subsection{MonoOpt}
adamc@552 1597
adamc@552 1598 Simple algebraic laws are applied to simplify the program, focusing especially on efficient imperative generation of HTML pages.
adamc@552 1599
adamc@552 1600 \subsection{MonoUntangle}
adamc@552 1601
adamc@552 1602 Unnecessary mutual recursion is broken up again.
adamc@552 1603
adamc@552 1604 \subsection{MonoReduce}
adamc@552 1605
adamc@552 1606 Equivalents of the definitional equality rules are applied to simplify programs, with inlining again playing a major role.
adamc@552 1607
adamc@552 1608 \subsection{MonoShake, MonoOpt}
adamc@552 1609
adamc@552 1610 Unneeded declarations are removed, and basic optimizations are repeated.
adamc@552 1611
adamc@552 1612 \subsection{Fuse}
adamc@552 1613
adamc@552 1614 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 1615
adamc@552 1616 \subsection{MonoUntangle, MonoShake}
adamc@552 1617
adamc@552 1618 Fuse often creates more opportunities to remove spurious mutual recursion.
adamc@552 1619
adamc@552 1620 \subsection{Pathcheck}
adamc@552 1621
adamc@552 1622 The compiler checks that no link or action name has been used more than once.
adamc@552 1623
adamc@552 1624 \subsection{Cjrize}
adamc@552 1625
adamc@552 1626 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 1627
adamc@552 1628 \subsection{C Compilation and Linking}
adamc@552 1629
adamc@552 1630 The output of the last phase is pretty-printed as C source code and passed to GCC.
adamc@552 1631
adamc@552 1632
adamc@524 1633 \end{document}