annotate doc/manual.tex @ 546:7417c4b57aeb

Sequences
author Adam Chlipala <adamc@hcoop.net>
date Sun, 07 Dec 2008 10:25:55 -0500
parents f31aa2a3a72d
children 8e615bb605c9
rev   line source
adamc@524 1 \documentclass{article}
adamc@524 2 \usepackage{fullpage,amsmath,amssymb,proof}
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@529 20 \section{Ur Syntax}
adamc@529 21
adamc@529 22 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 23
adamc@524 24 \subsection{Lexical Conventions}
adamc@524 25
adamc@524 26 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 27
adamc@524 28 \begin{center}
adamc@524 29 \begin{tabular}{rl}
adamc@524 30 \textbf{\LaTeX} & \textbf{ASCII} \\
adamc@524 31 $\to$ & \cd{->} \\
adamc@524 32 $\times$ & \cd{*} \\
adamc@524 33 $\lambda$ & \cd{fn} \\
adamc@524 34 $\Rightarrow$ & \cd{=>} \\
adamc@529 35 $\neq$ & \cd{<>} \\
adamc@529 36 $\leq$ & \cd{<=} \\
adamc@529 37 $\geq$ & \cd{>=} \\
adamc@524 38 \\
adamc@524 39 $x$ & Normal textual identifier, not beginning with an uppercase letter \\
adamc@525 40 $X$ & Normal textual identifier, beginning with an uppercase letter \\
adamc@524 41 \end{tabular}
adamc@524 42 \end{center}
adamc@524 43
adamc@525 44 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 45
adamc@526 46 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 47
adamc@527 48 This version of the manual doesn't include operator precedences; see \texttt{src/urweb.grm} for that.
adamc@527 49
adamc@524 50 \subsection{Core Syntax}
adamc@524 51
adamc@524 52 \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 53 $$\begin{array}{rrcll}
adamc@524 54 \textrm{Kinds} & \kappa &::=& \mt{Type} & \textrm{proper types} \\
adamc@525 55 &&& \mt{Unit} & \textrm{the trivial constructor} \\
adamc@525 56 &&& \mt{Name} & \textrm{field names} \\
adamc@525 57 &&& \kappa \to \kappa & \textrm{type-level functions} \\
adamc@525 58 &&& \{\kappa\} & \textrm{type-level records} \\
adamc@525 59 &&& (\kappa\times^+) & \textrm{type-level tuples} \\
adamc@529 60 &&& \_\_ & \textrm{wildcard} \\
adamc@525 61 &&& (\kappa) & \textrm{explicit precedence} \\
adamc@524 62 \end{array}$$
adamc@524 63
adamc@524 64 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 65 $$\begin{array}{rrcll}
adamc@524 66 \textrm{Explicitness} & ? &::=& :: & \textrm{explicit} \\
adamc@525 67 &&& \; ::: & \textrm{implicit}
adamc@524 68 \end{array}$$
adamc@524 69
adamc@524 70 \emph{Constructors} are the main class of compile-time-only data. They include proper types and are classified by kinds.
adamc@524 71 $$\begin{array}{rrcll}
adamc@524 72 \textrm{Constructors} & c, \tau &::=& (c) :: \kappa & \textrm{kind annotation} \\
adamc@530 73 &&& \hat{x} & \textrm{constructor variable} \\
adamc@524 74 \\
adamc@525 75 &&& \tau \to \tau & \textrm{function type} \\
adamc@525 76 &&& x \; ? \; \kappa \to \tau & \textrm{polymorphic function type} \\
adamc@525 77 &&& \$ c & \textrm{record type} \\
adamc@524 78 \\
adamc@525 79 &&& c \; c & \textrm{type-level function application} \\
adamc@530 80 &&& \lambda x \; :: \; \kappa \Rightarrow c & \textrm{type-level function abstraction} \\
adamc@524 81 \\
adamc@525 82 &&& () & \textrm{type-level unit} \\
adamc@525 83 &&& \#X & \textrm{field name} \\
adamc@524 84 \\
adamc@525 85 &&& [(c = c)^*] & \textrm{known-length type-level record} \\
adamc@525 86 &&& c \rc c & \textrm{type-level record concatenation} \\
adamc@525 87 &&& \mt{fold} & \textrm{type-level record fold} \\
adamc@524 88 \\
adamc@525 89 &&& (c^+) & \textrm{type-level tuple} \\
adamc@525 90 &&& c.n & \textrm{type-level tuple projection ($n \in \mathbb N^+$)} \\
adamc@524 91 \\
adamc@525 92 &&& \lambda [c \sim c] \Rightarrow c & \textrm{guarded constructor} \\
adamc@524 93 \\
adamc@529 94 &&& \_ :: \kappa & \textrm{wildcard} \\
adamc@525 95 &&& (c) & \textrm{explicit precedence} \\
adamc@530 96 \\
adamc@530 97 \textrm{Qualified uncapitalized variables} & \hat{x} &::=& x & \textrm{not from a module} \\
adamc@530 98 &&& M.x & \textrm{projection from a module} \\
adamc@525 99 \end{array}$$
adamc@525 100
adamc@525 101 Modules of the module system are described by \emph{signatures}.
adamc@525 102 $$\begin{array}{rrcll}
adamc@525 103 \textrm{Signatures} & S &::=& \mt{sig} \; s^* \; \mt{end} & \textrm{constant} \\
adamc@525 104 &&& X & \textrm{variable} \\
adamc@525 105 &&& \mt{functor}(X : S) : S & \textrm{functor} \\
adamc@529 106 &&& S \; \mt{where} \; \mt{con} \; x = c & \textrm{concretizing an abstract constructor} \\
adamc@525 107 &&& M.X & \textrm{projection from a module} \\
adamc@525 108 \\
adamc@525 109 \textrm{Signature items} & s &::=& \mt{con} \; x :: \kappa & \textrm{abstract constructor} \\
adamc@525 110 &&& \mt{con} \; x :: \kappa = c & \textrm{concrete constructor} \\
adamc@528 111 &&& \mt{datatype} \; x \; x^* = dc\mid^+ & \textrm{algebraic datatype definition} \\
adamc@529 112 &&& \mt{datatype} \; x = \mt{datatype} \; M.x & \textrm{algebraic datatype import} \\
adamc@525 113 &&& \mt{val} \; x : \tau & \textrm{value} \\
adamc@525 114 &&& \mt{structure} \; X : S & \textrm{sub-module} \\
adamc@525 115 &&& \mt{signature} \; X = S & \textrm{sub-signature} \\
adamc@525 116 &&& \mt{include} \; S & \textrm{signature inclusion} \\
adamc@525 117 &&& \mt{constraint} \; c \sim c & \textrm{record disjointness constraint} \\
adamc@525 118 &&& \mt{class} \; x & \textrm{abstract type class} \\
adamc@525 119 &&& \mt{class} \; x = c & \textrm{concrete type class} \\
adamc@525 120 \\
adamc@525 121 \textrm{Datatype constructors} & dc &::=& X & \textrm{nullary constructor} \\
adamc@525 122 &&& X \; \mt{of} \; \tau & \textrm{unary constructor} \\
adamc@524 123 \end{array}$$
adamc@524 124
adamc@526 125 \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 126 $$\begin{array}{rrcll}
adamc@526 127 \textrm{Patterns} & p &::=& \_ & \textrm{wildcard} \\
adamc@526 128 &&& x & \textrm{variable} \\
adamc@526 129 &&& \ell & \textrm{constant} \\
adamc@526 130 &&& \hat{X} & \textrm{nullary constructor} \\
adamc@526 131 &&& \hat{X} \; p & \textrm{unary constructor} \\
adamc@526 132 &&& \{(x = p,)^*\} & \textrm{rigid record pattern} \\
adamc@526 133 &&& \{(x = p,)^+, \ldots\} & \textrm{flexible record pattern} \\
adamc@527 134 &&& (p) & \textrm{explicit precedence} \\
adamc@526 135 \\
adamc@529 136 \textrm{Qualified capitalized variables} & \hat{X} &::=& X & \textrm{not from a module} \\
adamc@526 137 &&& M.X & \textrm{projection from a module} \\
adamc@526 138 \end{array}$$
adamc@526 139
adamc@527 140 \emph{Expressions} are the main run-time entities, corresponding to both ``expressions'' and ``statements'' in mainstream imperative languages.
adamc@527 141 $$\begin{array}{rrcll}
adamc@527 142 \textrm{Expressions} & e &::=& e : \tau & \textrm{type annotation} \\
adamc@529 143 &&& \hat{x} & \textrm{variable} \\
adamc@529 144 &&& \hat{X} & \textrm{datatype constructor} \\
adamc@527 145 &&& \ell & \textrm{constant} \\
adamc@527 146 \\
adamc@527 147 &&& e \; e & \textrm{function application} \\
adamc@527 148 &&& \lambda x : \tau \Rightarrow e & \textrm{function abstraction} \\
adamc@527 149 &&& e [c] & \textrm{polymorphic function application} \\
adamc@527 150 &&& \lambda x \; ? \; \kappa \Rightarrow e & \textrm{polymorphic function abstraction} \\
adamc@527 151 \\
adamc@527 152 &&& \{(c = e,)^*\} & \textrm{known-length record} \\
adamc@527 153 &&& e.c & \textrm{record field projection} \\
adamc@527 154 &&& e \rc e & \textrm{record concatenation} \\
adamc@527 155 &&& e \rcut c & \textrm{removal of a single record field} \\
adamc@527 156 &&& e \rcutM c & \textrm{removal of multiple record fields} \\
adamc@527 157 &&& \mt{fold} & \textrm{fold over fields of a type-level record} \\
adamc@527 158 \\
adamc@527 159 &&& \mt{let} \; ed^* \; \mt{in} \; e \; \mt{end} & \textrm{local definitions} \\
adamc@527 160 \\
adamc@527 161 &&& \mt{case} \; e \; \mt{of} \; (p \Rightarrow e|)^+ & \textrm{pattern matching} \\
adamc@527 162 \\
adamc@527 163 &&& \lambda [c \sim c] \Rightarrow e & \textrm{guarded expression} \\
adamc@527 164 \\
adamc@527 165 &&& \_ & \textrm{wildcard} \\
adamc@527 166 &&& (e) & \textrm{explicit precedence} \\
adamc@527 167 \\
adamc@527 168 \textrm{Local declarations} & ed &::=& \cd{val} \; x : \tau = e & \textrm{non-recursive value} \\
adamc@527 169 &&& \cd{val} \; \cd{rec} \; (x : \tau = e \; \cd{and})^+ & \textrm{mutually-recursive values} \\
adamc@527 170 \end{array}$$
adamc@527 171
adamc@528 172 \emph{Declarations} primarily bring new symbols into context.
adamc@528 173 $$\begin{array}{rrcll}
adamc@528 174 \textrm{Declarations} & d &::=& \mt{con} \; x :: \kappa = c & \textrm{constructor synonym} \\
adamc@528 175 &&& \mt{datatype} \; x \; x^* = dc\mid^+ & \textrm{algebraic datatype definition} \\
adamc@529 176 &&& \mt{datatype} \; x = \mt{datatype} \; M.x & \textrm{algebraic datatype import} \\
adamc@528 177 &&& \mt{val} \; x : \tau = e & \textrm{value} \\
adamc@528 178 &&& \mt{val} \; \cd{rec} \; (x : \tau = e \; \mt{and})^+ & \textrm{mutually-recursive values} \\
adamc@528 179 &&& \mt{structure} \; X : S = M & \textrm{module definition} \\
adamc@528 180 &&& \mt{signature} \; X = S & \textrm{signature definition} \\
adamc@528 181 &&& \mt{open} \; M & \textrm{module inclusion} \\
adamc@528 182 &&& \mt{constraint} \; c \sim c & \textrm{record disjointness constraint} \\
adamc@528 183 &&& \mt{open} \; \mt{constraints} \; M & \textrm{inclusion of just the constraints from a module} \\
adamc@528 184 &&& \mt{table} \; x : c & \textrm{SQL table} \\
adamc@528 185 &&& \mt{sequence} \; x & \textrm{SQL sequence} \\
adamc@535 186 &&& \mt{cookie} \; x : \tau & \textrm{HTTP cookie} \\
adamc@528 187 &&& \mt{class} \; x = c & \textrm{concrete type class} \\
adamc@528 188 \\
adamc@529 189 \textrm{Modules} & M &::=& \mt{struct} \; d^* \; \mt{end} & \textrm{constant} \\
adamc@529 190 &&& X & \textrm{variable} \\
adamc@529 191 &&& M.X & \textrm{projection} \\
adamc@529 192 &&& M(M) & \textrm{functor application} \\
adamc@529 193 &&& \mt{functor}(X : S) : S = M & \textrm{functor abstraction} \\
adamc@528 194 \end{array}$$
adamc@528 195
adamc@528 196 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 197
adamc@529 198 \subsection{Shorthands}
adamc@529 199
adamc@529 200 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 201
adamc@529 202 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 203
adamc@529 204 A record type may be written $\{(c = c,)^*\}$, which elaborates to $\$[(c = c,)^*]$.
adamc@529 205
adamc@533 206 The notation $[c_1, \ldots, c_n]$ is shorthand for $[c_1 = (), \ldots, c_n = ()]$.
adamc@533 207
adamc@529 208 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 209
adamc@529 210 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 [c \sim c]$ 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 211
adamc@529 212 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 213
adamc@529 214 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 215
adamc@529 216 A signature item or declaration $\mt{class} \; x = \lambda y :: \mt{Type} \Rightarrow c$ may be abbreviated $\mt{class} \; x \; y = c$.
adamc@529 217
adamc@529 218 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. The same syntax works for variables projected out of modules and for capitalized variables (datatype constructors).
adamc@529 219
adamc@529 220 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 [c \sim c]$. A lone variable $x$ as a binder stands for an expression variable of unspecified type.
adamc@529 221
adamc@529 222 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 223
adamc@529 224 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 225
adamc@529 226 A declaration $\mt{table} \; x : \{(c = c,)^*\}$ is elaborated into $\mt{table} \; x : [(c = c,)^*]$
adamc@529 227
adamc@529 228 The syntax $\mt{where} \; \mt{type}$ is an alternate form of $\mt{where} \; \mt{con}$.
adamc@529 229
adamc@529 230 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 231
adamc@529 232 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 233
adamc@529 234 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 235
adamc@530 236
adamc@530 237 \section{Static Semantics}
adamc@530 238
adamc@530 239 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 240
adamc@530 241 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 242 \begin{itemize}
adamc@530 243 \item $\Gamma \vdash c :: \kappa$ assigns a kind to a constructor in a context.
adamc@530 244 \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 245 \item $\Gamma \vdash c \hookrightarrow C$ proves that record constructor $c$ decomposes into set $C$ of field names and record constructors.
adamc@530 246 \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 247 \item $\Gamma \vdash e : \tau$ is a standard typing judgment.
adamc@534 248 \item $\Gamma \vdash p \leadsto \Gamma; \tau$ combines typing of patterns with calculation of which new variables they bind.
adamc@537 249 \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 250 \item $\Gamma \vdash S \equiv S$ is the signature equivalence judgment.
adamc@536 251 \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 252 \item $\Gamma \vdash M : S$ is the module signature checking judgment.
adamc@537 253 \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 254 \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 255 \end{itemize}
adamc@530 256
adamc@530 257 \subsection{Kinding}
adamc@530 258
adamc@530 259 $$\infer{\Gamma \vdash (c) :: \kappa :: \kappa}{
adamc@530 260 \Gamma \vdash c :: \kappa
adamc@530 261 }
adamc@530 262 \quad \infer{\Gamma \vdash x :: \kappa}{
adamc@530 263 x :: \kappa \in \Gamma
adamc@530 264 }
adamc@530 265 \quad \infer{\Gamma \vdash x :: \kappa}{
adamc@530 266 x :: \kappa = c \in \Gamma
adamc@530 267 }$$
adamc@530 268
adamc@530 269 $$\infer{\Gamma \vdash M.x :: \kappa}{
adamc@537 270 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 271 & \mt{proj}(M, \overline{s}, \mt{con} \; x) = \kappa
adamc@530 272 }
adamc@530 273 \quad \infer{\Gamma \vdash M.x :: \kappa}{
adamc@537 274 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 275 & \mt{proj}(M, \overline{s}, \mt{con} \; x) = (\kappa, c)
adamc@530 276 }$$
adamc@530 277
adamc@530 278 $$\infer{\Gamma \vdash \tau_1 \to \tau_2 :: \mt{Type}}{
adamc@530 279 \Gamma \vdash \tau_1 :: \mt{Type}
adamc@530 280 & \Gamma \vdash \tau_2 :: \mt{Type}
adamc@530 281 }
adamc@530 282 \quad \infer{\Gamma \vdash x \; ? \: \kappa \to \tau :: \mt{Type}}{
adamc@530 283 \Gamma, x :: \kappa \vdash \tau :: \mt{Type}
adamc@530 284 }
adamc@530 285 \quad \infer{\Gamma \vdash \$c :: \mt{Type}}{
adamc@530 286 \Gamma \vdash c :: \{\mt{Type}\}
adamc@530 287 }$$
adamc@530 288
adamc@530 289 $$\infer{\Gamma \vdash c_1 \; c_2 :: \kappa_2}{
adamc@530 290 \Gamma \vdash c_1 :: \kappa_1 \to \kappa_2
adamc@530 291 & \Gamma \vdash c_2 :: \kappa_1
adamc@530 292 }
adamc@530 293 \quad \infer{\Gamma \vdash \lambda x \; :: \; \kappa_1 \Rightarrow c :: \kappa_1 \to \kappa_2}{
adamc@530 294 \Gamma, x :: \kappa_1 \vdash c :: \kappa_2
adamc@530 295 }$$
adamc@530 296
adamc@530 297 $$\infer{\Gamma \vdash () :: \mt{Unit}}{}
adamc@530 298 \quad \infer{\Gamma \vdash \#X :: \mt{Name}}{}$$
adamc@530 299
adamc@530 300 $$\infer{\Gamma \vdash [\overline{c_i = c'_i}] :: \{\kappa\}}{
adamc@530 301 \forall i: \Gamma \vdash c_i : \mt{Name}
adamc@530 302 & \Gamma \vdash c'_i :: \kappa
adamc@530 303 & \forall i \neq j: \Gamma \vdash c_i \sim c_j
adamc@530 304 }
adamc@530 305 \quad \infer{\Gamma \vdash c_1 \rc c_2 :: \{\kappa\}}{
adamc@530 306 \Gamma \vdash c_1 :: \{\kappa\}
adamc@530 307 & \Gamma \vdash c_2 :: \{\kappa\}
adamc@530 308 & \Gamma \vdash c_1 \sim c_2
adamc@530 309 }$$
adamc@530 310
adamc@530 311 $$\infer{\Gamma \vdash \mt{fold} :: ((\mt{Name} \to \kappa_1 \to \kappa_2 \to \kappa_2) \to \kappa_2 \to \{\kappa_1\} \to \kappa_2}{}$$
adamc@530 312
adamc@530 313 $$\infer{\Gamma \vdash (\overline c) :: (k_1 \times \ldots \times k_n)}{
adamc@530 314 \forall i: \Gamma \vdash c_i :: k_i
adamc@530 315 }
adamc@530 316 \quad \infer{\Gamma \vdash c.i :: k_i}{
adamc@530 317 \Gamma \vdash c :: (k_1 \times \ldots \times k_n)
adamc@530 318 }$$
adamc@530 319
adamc@530 320 $$\infer{\Gamma \vdash \lambda [c_1 \sim c_2] \Rightarrow c :: \kappa}{
adamc@530 321 \Gamma \vdash c_1 :: \{\kappa'\}
adamc@530 322 & \Gamma \vdash c_2 :: \{\kappa'\}
adamc@530 323 & \Gamma, c_1 \sim c_2 \vdash c :: \kappa
adamc@530 324 }$$
adamc@530 325
adamc@531 326 \subsection{Record Disjointness}
adamc@531 327
adamc@531 328 We will use a keyword $\mt{map}$ as a shorthand, such that, for $f$ of kind $\kappa \to \kappa'$, $\mt{map} \; f$ stands for $\mt{fold} \; (\lambda (x_1 :: \mt{Name}) (x_2 :: \kappa) (x_3 :: \{\kappa'\}) \Rightarrow [x_1 = f \; x_2] \rc x_3) \; []$.
adamc@531 329
adamc@531 330 $$\infer{\Gamma \vdash c_1 \sim c_2}{
adamc@531 331 \Gamma \vdash c_1 \hookrightarrow c'_1
adamc@531 332 & \Gamma \vdash c_2 \hookrightarrow c'_2
adamc@531 333 & \forall c''_1 \in c'_1, c''_2 \in c'_2: \Gamma \vdash c''_1 \sim c''_2
adamc@531 334 }
adamc@531 335 \quad \infer{\Gamma \vdash X \sim X'}{
adamc@531 336 X \neq X'
adamc@531 337 }$$
adamc@531 338
adamc@531 339 $$\infer{\Gamma \vdash c_1 \sim c_2}{
adamc@531 340 c'_1 \sim c'_2 \in \Gamma
adamc@531 341 & \Gamma \vdash c'_1 \hookrightarrow c''_1
adamc@531 342 & \Gamma \vdash c'_2 \hookrightarrow c''_2
adamc@531 343 & c_1 \in c''_1
adamc@531 344 & c_2 \in c''_2
adamc@531 345 }$$
adamc@531 346
adamc@531 347 $$\infer{\Gamma \vdash c \hookrightarrow \{c\}}{}
adamc@531 348 \quad \infer{\Gamma \vdash [\overline{c = c'}] \hookrightarrow \{\overline{c}\}}{}
adamc@531 349 \quad \infer{\Gamma \vdash c_1 \rc c_2 \hookrightarrow C_1 \cup C_2}{
adamc@531 350 \Gamma \vdash c_1 \hookrightarrow C_1
adamc@531 351 & \Gamma \vdash c_2 \hookrightarrow C_2
adamc@531 352 }
adamc@531 353 \quad \infer{\Gamma \vdash c \hookrightarrow C}{
adamc@531 354 \Gamma \vdash c \equiv c'
adamc@531 355 & \Gamma \vdash c' \hookrightarrow C
adamc@531 356 }
adamc@531 357 \quad \infer{\Gamma \vdash \mt{map} \; f \; c \hookrightarrow C}{
adamc@531 358 \Gamma \vdash c \hookrightarrow C
adamc@531 359 }$$
adamc@531 360
adamc@541 361 \subsection{\label{definitional}Definitional Equality}
adamc@532 362
adamc@532 363 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$.
adamc@532 364
adamc@532 365 $$\infer{\Gamma \vdash c \equiv c}{}
adamc@532 366 \quad \infer{\Gamma \vdash c_1 \equiv c_2}{
adamc@532 367 \Gamma \vdash c_2 \equiv c_1
adamc@532 368 }
adamc@532 369 \quad \infer{\Gamma \vdash c_1 \equiv c_3}{
adamc@532 370 \Gamma \vdash c_1 \equiv c_2
adamc@532 371 & \Gamma \vdash c_2 \equiv c_3
adamc@532 372 }
adamc@532 373 \quad \infer{\Gamma \vdash \mathcal C[c_1] \equiv \mathcal C[c_2]}{
adamc@532 374 \Gamma \vdash c_1 \equiv c_2
adamc@532 375 }$$
adamc@532 376
adamc@532 377 $$\infer{\Gamma \vdash x \equiv c}{
adamc@532 378 x :: \kappa = c \in \Gamma
adamc@532 379 }
adamc@532 380 \quad \infer{\Gamma \vdash M.x \equiv c}{
adamc@537 381 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 382 & \mt{proj}(M, \overline{s}, \mt{con} \; x) = (\kappa, c)
adamc@532 383 }
adamc@532 384 \quad \infer{\Gamma \vdash (\overline c).i \equiv c_i}{}$$
adamc@532 385
adamc@532 386 $$\infer{\Gamma \vdash (\lambda x :: \kappa \Rightarrow c) \; c' \equiv [x \mapsto c'] c}{}
adamc@532 387 \quad \infer{\Gamma \vdash c_1 \rc c_2 \equiv c_2 \rc c_1}{}
adamc@532 388 \quad \infer{\Gamma \vdash c_1 \rc (c_2 \rc c_3) \equiv (c_1 \rc c_2) \rc c_3}{}$$
adamc@532 389
adamc@532 390 $$\infer{\Gamma \vdash [] \rc c \equiv c}{}
adamc@532 391 \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 392
adamc@532 393 $$\infer{\Gamma \vdash \lambda [c_1 \sim c_2] \Rightarrow c \equiv c}{
adamc@532 394 \Gamma \vdash c_1 \sim c_2
adamc@532 395 }
adamc@532 396 \quad \infer{\Gamma \vdash \mt{fold} \; f \; i \; [] \equiv i}{}
adamc@532 397 \quad \infer{\Gamma \vdash \mt{fold} \; f \; i \; ([c_1 = c_2] \rc c) \equiv f \; c_1 \; c_2 \; (\mt{fold} \; f \; i \; c)}{}$$
adamc@532 398
adamc@532 399 $$\infer{\Gamma \vdash \mt{map} \; (\lambda x \Rightarrow x) \; c \equiv c}{}
adamc@532 400 \quad \infer{\Gamma \vdash \mt{fold} \; f \; i \; (\mt{map} \; f' \; c)
adamc@532 401 \equiv \mt{fold} \; (\lambda (x_1 :: \mt{Name}) (x_2 :: \kappa) \Rightarrow f \; x_1 \; (f' \; x_2)) \; i \; c}{}$$
adamc@532 402
adamc@532 403 $$\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 404
adamc@534 405 \subsection{Expression Typing}
adamc@533 406
adamc@533 407 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 408
adamc@533 409 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 410
adamc@533 411 $$\infer{\Gamma \vdash e : \tau : \tau}{
adamc@533 412 \Gamma \vdash e : \tau
adamc@533 413 }
adamc@533 414 \quad \infer{\Gamma \vdash e : \tau}{
adamc@533 415 \Gamma \vdash e : \tau'
adamc@533 416 & \Gamma \vdash \tau' \equiv \tau
adamc@533 417 }
adamc@533 418 \quad \infer{\Gamma \vdash \ell : T(\ell)}{}$$
adamc@533 419
adamc@533 420 $$\infer{\Gamma \vdash x : \mathcal I(\tau)}{
adamc@533 421 x : \tau \in \Gamma
adamc@533 422 }
adamc@533 423 \quad \infer{\Gamma \vdash M.x : \mathcal I(\tau)}{
adamc@537 424 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 425 & \mt{proj}(M, \overline{s}, \mt{val} \; x) = \tau
adamc@533 426 }
adamc@533 427 \quad \infer{\Gamma \vdash X : \mathcal I(\tau)}{
adamc@533 428 X : \tau \in \Gamma
adamc@533 429 }
adamc@533 430 \quad \infer{\Gamma \vdash M.X : \mathcal I(\tau)}{
adamc@537 431 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 432 & \mt{proj}(M, \overline{s}, \mt{val} \; X) = \tau
adamc@533 433 }$$
adamc@533 434
adamc@533 435 $$\infer{\Gamma \vdash e_1 \; e_2 : \tau_2}{
adamc@533 436 \Gamma \vdash e_1 : \tau_1 \to \tau_2
adamc@533 437 & \Gamma \vdash e_2 : \tau_1
adamc@533 438 }
adamc@533 439 \quad \infer{\Gamma \vdash \lambda x : \tau_1 \Rightarrow e : \tau_1 \to \tau_2}{
adamc@533 440 \Gamma, x : \tau_1 \vdash e : \tau_2
adamc@533 441 }$$
adamc@533 442
adamc@533 443 $$\infer{\Gamma \vdash e [c] : [x \mapsto c]\tau}{
adamc@533 444 \Gamma \vdash e : x :: \kappa \to \tau
adamc@533 445 & \Gamma \vdash c :: \kappa
adamc@533 446 }
adamc@533 447 \quad \infer{\Gamma \vdash \lambda x \; ? \; \kappa \Rightarrow e : x \; ? \; \kappa \to \tau}{
adamc@533 448 \Gamma, x :: \kappa \vdash e : \tau
adamc@533 449 }$$
adamc@533 450
adamc@533 451 $$\infer{\Gamma \vdash \{\overline{c = e}\} : \{\overline{c : \tau}\}}{
adamc@533 452 \forall i: \Gamma \vdash c_i :: \mt{Name}
adamc@533 453 & \Gamma \vdash e_i : \tau_i
adamc@533 454 & \forall i \neq j: \Gamma \vdash c_i \sim c_j
adamc@533 455 }
adamc@533 456 \quad \infer{\Gamma \vdash e.c : \tau}{
adamc@533 457 \Gamma \vdash e : \$([c = \tau] \rc c')
adamc@533 458 }
adamc@533 459 \quad \infer{\Gamma \vdash e_1 \rc e_2 : \$(c_1 \rc c_2)}{
adamc@533 460 \Gamma \vdash e_1 : \$c_1
adamc@533 461 & \Gamma \vdash e_2 : \$c_2
adamc@533 462 }$$
adamc@533 463
adamc@533 464 $$\infer{\Gamma \vdash e \rcut c : \$c'}{
adamc@533 465 \Gamma \vdash e : \$([c = \tau] \rc c')
adamc@533 466 }
adamc@533 467 \quad \infer{\Gamma \vdash e \rcutM c : \$c'}{
adamc@533 468 \Gamma \vdash e : \$(c \rc c')
adamc@533 469 }$$
adamc@533 470
adamc@533 471 $$\infer{\Gamma \vdash \mt{fold} : \begin{array}{c}
adamc@533 472 x_1 :: (\{\kappa\} \to \tau)
adamc@533 473 \to (x_2 :: \mt{Name} \to x_3 :: \kappa \to x_4 :: \{\kappa\} \to \lambda [[x_2] \sim x_4]
adamc@533 474 \Rightarrow x_1 \; x_4 \to x_1 \; ([x_2 = x_3] \rc x_4)) \\
adamc@533 475 \to x_1 \; [] \to x_5 :: \{\kappa\} \to x_1 \; x_5
adamc@533 476 \end{array}}{}$$
adamc@533 477
adamc@533 478 $$\infer{\Gamma \vdash \mt{let} \; \overline{ed} \; \mt{in} \; e \; \mt{end} : \tau}{
adamc@533 479 \Gamma \vdash \overline{ed} \leadsto \Gamma'
adamc@533 480 & \Gamma' \vdash e : \tau
adamc@533 481 }
adamc@533 482 \quad \infer{\Gamma \vdash \mt{case} \; e \; \mt{of} \; \overline{p \Rightarrow e} : \tau}{
adamc@533 483 \forall i: \Gamma \vdash p_i \leadsto \Gamma_i, \tau'
adamc@533 484 & \Gamma_i \vdash e_i : \tau
adamc@533 485 }$$
adamc@533 486
adamc@533 487 $$\infer{\Gamma \vdash [c_1 \sim c_2] \Rightarrow e : [c_1 \sim c_2] \Rightarrow \tau}{
adamc@533 488 \Gamma \vdash c_1 :: \{\kappa\}
adamc@533 489 & \Gamma \vdash c_2 :: \{\kappa\}
adamc@533 490 & \Gamma, c_1 \sim c_2 \vdash e : \tau
adamc@533 491 }$$
adamc@533 492
adamc@534 493 \subsection{Pattern Typing}
adamc@534 494
adamc@534 495 $$\infer{\Gamma \vdash \_ \leadsto \Gamma; \tau}{}
adamc@534 496 \quad \infer{\Gamma \vdash x \leadsto \Gamma, x : \tau; \tau}{}
adamc@534 497 \quad \infer{\Gamma \vdash \ell \leadsto \Gamma; T(\ell)}{}$$
adamc@534 498
adamc@534 499 $$\infer{\Gamma \vdash X \leadsto \Gamma; \overline{[x_i \mapsto \tau'_i]}\tau}{
adamc@534 500 X : \overline{x ::: \mt{Type}} \to \tau \in \Gamma
adamc@534 501 & \textrm{$\tau$ not a function type}
adamc@534 502 }
adamc@534 503 \quad \infer{\Gamma \vdash X \; p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau}{
adamc@534 504 X : \overline{x ::: \mt{Type}} \to \tau'' \to \tau \in \Gamma
adamc@534 505 & \Gamma \vdash p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau''
adamc@534 506 }$$
adamc@534 507
adamc@534 508 $$\infer{\Gamma \vdash M.X \leadsto \Gamma; \overline{[x_i \mapsto \tau'_i]}\tau}{
adamc@537 509 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 510 & \mt{proj}(M, \overline{s}, \mt{val} \; X) = \overline{x ::: \mt{Type}} \to \tau
adamc@534 511 & \textrm{$\tau$ not a function type}
adamc@534 512 }$$
adamc@534 513
adamc@534 514 $$\infer{\Gamma \vdash M.X \; p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau}{
adamc@537 515 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 516 & \mt{proj}(M, \overline{s}, \mt{val} \; X) = \overline{x ::: \mt{Type}} \to \tau'' \to \tau
adamc@534 517 & \Gamma \vdash p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau''
adamc@534 518 }$$
adamc@534 519
adamc@534 520 $$\infer{\Gamma \vdash \{\overline{x = p}\} \leadsto \Gamma_n; \{\overline{x = \tau}\}}{
adamc@534 521 \Gamma_0 = \Gamma
adamc@534 522 & \forall i: \Gamma_i \vdash p_i \leadsto \Gamma_{i+1}; \tau_i
adamc@534 523 }
adamc@534 524 \quad \infer{\Gamma \vdash \{\overline{x = p}, \ldots\} \leadsto \Gamma_n; \$([\overline{x = \tau}] \rc c)}{
adamc@534 525 \Gamma_0 = \Gamma
adamc@534 526 & \forall i: \Gamma_i \vdash p_i \leadsto \Gamma_{i+1}; \tau_i
adamc@534 527 }$$
adamc@534 528
adamc@535 529 \subsection{Declaration Typing}
adamc@535 530
adamc@535 531 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 532
adamc@541 533 This is the first judgment where we deal with type 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 type classes influence type inference.
adamc@535 534
adamc@537 535 We presuppose the existence of a function $\mathcal O$, where $\mathcal(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 $S$.
adamc@537 536
adamc@537 537 We write $\kappa_1^n \to \kappa$ as a shorthand, where $\kappa_1^0 \to \kappa = \kappa$ and $\kappa_1^{n+1} \to \kappa_2 = \kappa_1 \to (\kappa_1^n \to \kappa_2)$. We write $\mt{len}(\overline{y})$ for the length of vector $\overline{y}$ of variables.
adamc@535 538
adamc@535 539 $$\infer{\Gamma \vdash \cdot \leadsto \Gamma}{}
adamc@535 540 \quad \infer{\Gamma \vdash d, \overline{d} \leadsto \Gamma''}{
adamc@535 541 \Gamma \vdash d \leadsto \Gamma'
adamc@535 542 & \Gamma' \vdash \overline{d} \leadsto \Gamma''
adamc@535 543 }$$
adamc@535 544
adamc@535 545 $$\infer{\Gamma \vdash \mt{con} \; x :: \kappa = c \leadsto \Gamma, x :: \kappa = c}{
adamc@535 546 \Gamma \vdash c :: \kappa
adamc@535 547 }
adamc@535 548 \quad \infer{\Gamma \vdash \mt{datatype} \; x \; \overline{y} = \overline{dc} \leadsto \Gamma'}{
adamc@535 549 \overline{y}; x; \Gamma, x :: \mt{Type}^{\mt{len}(\overline y)} \to \mt{Type} \vdash \overline{dc} \leadsto \Gamma'
adamc@535 550 }$$
adamc@535 551
adamc@535 552 $$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leadsto \Gamma'}{
adamc@537 553 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 554 & \mt{proj}(M, \overline{s}, \mt{datatype} \; z) = (\overline{y}, \overline{dc})
adamc@535 555 & \overline{y}; x; \Gamma, x :: \mt{Type}^{\mt{len}(\overline y)} \to \mt{Type} = M.z \vdash \overline{dc} \leadsto \Gamma'
adamc@535 556 }$$
adamc@535 557
adamc@535 558 $$\infer{\Gamma \vdash \mt{val} \; x : \tau = e \leadsto \Gamma, x : \tau}{
adamc@535 559 \Gamma \vdash e : \tau
adamc@535 560 }$$
adamc@535 561
adamc@535 562 $$\infer{\Gamma \vdash \mt{val} \; \mt{rec} \; \overline{x : \tau = e} \leadsto \Gamma, \overline{x : \tau}}{
adamc@535 563 \forall i: \Gamma, \overline{x : \tau} \vdash e_i : \tau_i
adamc@535 564 & \textrm{$e_i$ starts with an expression $\lambda$, optionally preceded by constructor and disjointness $\lambda$s}
adamc@535 565 }$$
adamc@535 566
adamc@535 567 $$\infer{\Gamma \vdash \mt{structure} \; X : S = M \leadsto \Gamma, X : S}{
adamc@535 568 \Gamma \vdash M : S
adamc@539 569 & \textrm{ ($M$ not a $\mt{struct} \; \ldots \; \mt{end}$)}
adamc@535 570 }
adamc@539 571 \quad \infer{\Gamma \vdash \mt{structure} \; X : S = \mt{struct} \; \overline{d} \; \mt{end} \leadsto \Gamma, X : \mt{selfify}(X, \overline{s})}{
adamc@539 572 \Gamma \vdash \mt{struct} \; \overline{d} \; \mt{end} : \mt{sig} \; \overline{s} \; \mt{end}
adamc@539 573 }$$
adamc@539 574
adamc@539 575 $$\infer{\Gamma \vdash \mt{signature} \; X = S \leadsto \Gamma, X = S}{
adamc@535 576 \Gamma \vdash S
adamc@535 577 }$$
adamc@535 578
adamc@537 579 $$\infer{\Gamma \vdash \mt{open} \; M \leadsto \Gamma, \mathcal O(M, \overline{s})}{
adamc@537 580 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@535 581 }$$
adamc@535 582
adamc@535 583 $$\infer{\Gamma \vdash \mt{constraint} \; c_1 \sim c_2 \leadsto \Gamma}{
adamc@535 584 \Gamma \vdash c_1 :: \{\kappa\}
adamc@535 585 & \Gamma \vdash c_2 :: \{\kappa\}
adamc@535 586 & \Gamma \vdash c_1 \sim c_2
adamc@535 587 }
adamc@537 588 \quad \infer{\Gamma \vdash \mt{open} \; \mt{constraints} \; M \leadsto \Gamma, \mathcal O_c(M, \overline{s})}{
adamc@537 589 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@535 590 }$$
adamc@535 591
adamc@535 592 $$\infer{\Gamma \vdash \mt{table} \; x : c \leadsto \Gamma, x : \mt{Basis}.\mt{sql\_table} \; c}{
adamc@535 593 \Gamma \vdash c :: \{\mt{Type}\}
adamc@535 594 }
adamc@535 595 \quad \infer{\Gamma \vdash \mt{sequence} \; x \leadsto \Gamma, x : \mt{Basis}.\mt{sql\_sequence}}{}$$
adamc@535 596
adamc@535 597 $$\infer{\Gamma \vdash \mt{cookie} \; x : \tau \leadsto \Gamma, x : \mt{Basis}.\mt{http\_cookie} \; \tau}{
adamc@535 598 \Gamma \vdash \tau :: \mt{Type}
adamc@535 599 }$$
adamc@535 600
adamc@535 601 $$\infer{\Gamma \vdash \mt{class} \; x = c \leadsto \Gamma, x :: \mt{Type} \to \mt{Type} = c}{
adamc@535 602 \Gamma \vdash c :: \mt{Type} \to \mt{Type}
adamc@535 603 }$$
adamc@535 604
adamc@535 605 $$\infer{\overline{y}; x; \Gamma \vdash \cdot \leadsto \Gamma}{}
adamc@535 606 \quad \infer{\overline{y}; x; \Gamma \vdash X \mid \overline{dc} \leadsto \Gamma', X : \overline{y ::: \mt{Type}} \to x \; \overline{y}}{
adamc@535 607 \overline{y}; x; \Gamma \vdash \overline{dc} \leadsto \Gamma'
adamc@535 608 }
adamc@535 609 \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 610 \overline{y}; x; \Gamma \vdash \overline{dc} \leadsto \Gamma'
adamc@535 611 }$$
adamc@535 612
adamc@537 613 \subsection{Signature Item Typing}
adamc@537 614
adamc@537 615 We appeal to a signature item analogue of the $\mathcal O$ function from the last subsection.
adamc@537 616
adamc@537 617 $$\infer{\Gamma \vdash \cdot \leadsto \Gamma}{}
adamc@537 618 \quad \infer{\Gamma \vdash s, \overline{s} \leadsto \Gamma''}{
adamc@537 619 \Gamma \vdash s \leadsto \Gamma'
adamc@537 620 & \Gamma' \vdash \overline{s} \leadsto \Gamma''
adamc@537 621 }$$
adamc@537 622
adamc@537 623 $$\infer{\Gamma \vdash \mt{con} \; x :: \kappa \leadsto \Gamma, x :: \kappa}{}
adamc@537 624 \quad \infer{\Gamma \vdash \mt{con} \; x :: \kappa = c \leadsto \Gamma, x :: \kappa = c}{
adamc@537 625 \Gamma \vdash c :: \kappa
adamc@537 626 }
adamc@537 627 \quad \infer{\Gamma \vdash \mt{datatype} \; x \; \overline{y} = \overline{dc} \leadsto \Gamma'}{
adamc@537 628 \overline{y}; x; \Gamma, x :: \mt{Type}^{\mt{len}(\overline y)} \to \mt{Type} \vdash \overline{dc} \leadsto \Gamma'
adamc@537 629 }$$
adamc@537 630
adamc@537 631 $$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leadsto \Gamma'}{
adamc@537 632 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 633 & \mt{proj}(M, \overline{s}, \mt{datatype} \; z) = (\overline{y}, \overline{dc})
adamc@537 634 & \overline{y}; x; \Gamma, x :: \mt{Type}^{\mt{len}(\overline y)} \to \mt{Type} = M.z \vdash \overline{dc} \leadsto \Gamma'
adamc@537 635 }$$
adamc@537 636
adamc@537 637 $$\infer{\Gamma \vdash \mt{val} \; x : \tau \leadsto \Gamma, x : \tau}{
adamc@537 638 \Gamma \vdash \tau :: \mt{Type}
adamc@537 639 }$$
adamc@537 640
adamc@537 641 $$\infer{\Gamma \vdash \mt{structure} \; X : S \leadsto \Gamma, X : S}{
adamc@537 642 \Gamma \vdash S
adamc@537 643 }
adamc@537 644 \quad \infer{\Gamma \vdash \mt{signature} \; X = S \leadsto \Gamma, X = S}{
adamc@537 645 \Gamma \vdash S
adamc@537 646 }$$
adamc@537 647
adamc@537 648 $$\infer{\Gamma \vdash \mt{include} \; S \leadsto \Gamma, \mathcal O(\overline{s})}{
adamc@537 649 \Gamma \vdash S
adamc@537 650 & \Gamma \vdash S \equiv \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 651 }$$
adamc@537 652
adamc@537 653 $$\infer{\Gamma \vdash \mt{constraint} \; c_1 \sim c_2 \leadsto \Gamma, c_1 \sim c_2}{
adamc@537 654 \Gamma \vdash c_1 :: \{\kappa\}
adamc@537 655 & \Gamma \vdash c_2 :: \{\kappa\}
adamc@537 656 }$$
adamc@537 657
adamc@537 658 $$\infer{\Gamma \vdash \mt{class} \; x = c \leadsto \Gamma, x :: \mt{Type} \to \mt{Type} = c}{
adamc@537 659 \Gamma \vdash c :: \mt{Type} \to \mt{Type}
adamc@537 660 }
adamc@537 661 \quad \infer{\Gamma \vdash \mt{class} \; x \leadsto \Gamma, x :: \mt{Type} \to \mt{Type}}{}$$
adamc@537 662
adamc@536 663 \subsection{Signature Compatibility}
adamc@536 664
adamc@537 665 To simplify the judgments in this section, we assume that all signatures are alpha-varied as necessary to avoid including mmultiple bindings for the same identifier. This is in addition to the usual alpha-variation of locally-bound variables.
adamc@537 666
adamc@537 667 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 668
adamc@536 669 $$\infer{\Gamma \vdash S \equiv S}{}
adamc@536 670 \quad \infer{\Gamma \vdash S_1 \equiv S_2}{
adamc@536 671 \Gamma \vdash S_2 \equiv S_1
adamc@536 672 }
adamc@536 673 \quad \infer{\Gamma \vdash X \equiv S}{
adamc@536 674 X = S \in \Gamma
adamc@536 675 }
adamc@536 676 \quad \infer{\Gamma \vdash M.X \equiv S}{
adamc@537 677 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 678 & \mt{proj}(M, \overline{s}, \mt{signature} \; X) = S
adamc@536 679 }$$
adamc@536 680
adamc@536 681 $$\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 682 \Gamma \vdash S \equiv \mt{sig} \; \overline{s^1} \; \mt{con} \; x :: \kappa \; \overline{s_2} \; \mt{end}
adamc@536 683 & \Gamma \vdash c :: \kappa
adamc@537 684 }
adamc@537 685 \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 686 \Gamma \vdash S \equiv \mt{sig} \; \overline{s} \; \mt{end}
adamc@536 687 }$$
adamc@536 688
adamc@536 689 $$\infer{\Gamma \vdash S_1 \leq S_2}{
adamc@536 690 \Gamma \vdash S_1 \equiv S_2
adamc@536 691 }
adamc@536 692 \quad \infer{\Gamma \vdash \mt{sig} \; \overline{s} \; \mt{end} \leq \mt{sig} \; \mt{end}}{}
adamc@537 693 \quad \infer{\Gamma \vdash \mt{sig} \; \overline{s} \; \mt{end} \leq \mt{sig} \; s' \; \overline{s'} \; \mt{end}}{
adamc@537 694 \Gamma \vdash \overline{s} \leq s'
adamc@537 695 & \Gamma \vdash s' \leadsto \Gamma'
adamc@537 696 & \Gamma' \vdash \mt{sig} \; \overline{s} \; \mt{end} \leq \mt{sig} \; \overline{s'} \; \mt{end}
adamc@537 697 }$$
adamc@537 698
adamc@537 699 $$\infer{\Gamma \vdash s \; \overline{s} \leq s'}{
adamc@537 700 \Gamma \vdash s \leq s'
adamc@537 701 }
adamc@537 702 \quad \infer{\Gamma \vdash s \; \overline{s} \leq s'}{
adamc@537 703 \Gamma \vdash s \leadsto \Gamma'
adamc@537 704 & \Gamma' \vdash \overline{s} \leq s'
adamc@536 705 }$$
adamc@536 706
adamc@536 707 $$\infer{\Gamma \vdash \mt{functor} (X : S_1) : S_2 \leq \mt{functor} (X : S'_1) : S'_2}{
adamc@536 708 \Gamma \vdash S'_1 \leq S_1
adamc@536 709 & \Gamma, X : S'_1 \vdash S_2 \leq S'_2
adamc@536 710 }$$
adamc@536 711
adamc@537 712 $$\infer{\Gamma \vdash \mt{con} \; x :: \kappa \leq \mt{con} \; x :: \kappa}{}
adamc@537 713 \quad \infer{\Gamma \vdash \mt{con} \; x :: \kappa = c \leq \mt{con} \; x :: \kappa}{}
adamc@537 714 \quad \infer{\Gamma \vdash \mt{datatype} \; x \; \overline{y} = \overline{dc} \leq \mt{con} \; x :: \mt{Type}}{}$$
adamc@537 715
adamc@537 716 $$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leq \mt{con} \; x :: \mt{Type}^{\mt{len}(y)} \to \mt{Type}}{
adamc@537 717 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 718 & \mt{proj}(M, \overline{s}, \mt{datatype} \; z) = (\overline{y}, \overline{dc})
adamc@537 719 }$$
adamc@537 720
adamc@537 721 $$\infer{\Gamma \vdash \mt{class} \; x \leq \mt{con} \; x :: \mt{Type} \to \mt{Type}}{}
adamc@537 722 \quad \infer{\Gamma \vdash \mt{class} \; x = c \leq \mt{con} \; x :: \mt{Type} \to \mt{Type}}{}$$
adamc@537 723
adamc@537 724 $$\infer{\Gamma \vdash \mt{con} \; x :: \kappa = c_1 \leq \mt{con} \; x :: \mt{\kappa} = c_2}{
adamc@537 725 \Gamma \vdash c_1 \equiv c_2
adamc@537 726 }
adamc@537 727 \quad \infer{\Gamma \vdash \mt{class} \; x = c_1 \leq \mt{con} \; x :: \mt{Type} \to \mt{Type} = c_2}{
adamc@537 728 \Gamma \vdash c_1 \equiv c_2
adamc@537 729 }$$
adamc@537 730
adamc@537 731 $$\infer{\Gamma \vdash \mt{datatype} \; x \; \overline{y} = \overline{dc} \leq \mt{datatype} \; x \; \overline{y} = \overline{dc'}}{
adamc@537 732 \Gamma, \overline{y :: \mt{Type}} \vdash \overline{dc} \leq \overline{dc'}
adamc@537 733 }$$
adamc@537 734
adamc@537 735 $$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leq \mt{datatype} \; x \; \overline{y} = \overline{dc'}}{
adamc@537 736 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 737 & \mt{proj}(M, \overline{s}, \mt{datatype} \; z) = (\overline{y}, \overline{dc})
adamc@537 738 & \Gamma, \overline{y :: \mt{Type}} \vdash \overline{dc} \leq \overline{dc'}
adamc@537 739 }$$
adamc@537 740
adamc@537 741 $$\infer{\Gamma \vdash \cdot \leq \cdot}{}
adamc@537 742 \quad \infer{\Gamma \vdash X; \overline{dc} \leq X; \overline{dc'}}{
adamc@537 743 \Gamma \vdash \overline{dc} \leq \overline{dc'}
adamc@537 744 }
adamc@537 745 \quad \infer{\Gamma \vdash X \; \mt{of} \; \tau_1; \overline{dc} \leq X \; \mt{of} \; \tau_2; \overline{dc'}}{
adamc@537 746 \Gamma \vdash \tau_1 \equiv \tau_2
adamc@537 747 & \Gamma \vdash \overline{dc} \leq \overline{dc'}
adamc@537 748 }$$
adamc@537 749
adamc@537 750 $$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leq \mt{datatype} \; x = \mt{datatype} \; M'.z'}{
adamc@537 751 \Gamma \vdash M.z \equiv M'.z'
adamc@537 752 }$$
adamc@537 753
adamc@537 754 $$\infer{\Gamma \vdash \mt{val} \; x : \tau_1 \leq \mt{val} \; x : \tau_2}{
adamc@537 755 \Gamma \vdash \tau_1 \equiv \tau_2
adamc@537 756 }
adamc@537 757 \quad \infer{\Gamma \vdash \mt{structure} \; X : S_1 \leq \mt{structure} \; X : S_2}{
adamc@537 758 \Gamma \vdash S_1 \leq S_2
adamc@537 759 }
adamc@537 760 \quad \infer{\Gamma \vdash \mt{signature} \; X = S_1 \leq \mt{signature} \; X = S_2}{
adamc@537 761 \Gamma \vdash S_1 \leq S_2
adamc@537 762 & \Gamma \vdash S_2 \leq S_1
adamc@537 763 }$$
adamc@537 764
adamc@537 765 $$\infer{\Gamma \vdash \mt{constraint} \; c_1 \sim c_2 \leq \mt{constraint} \; c'_1 \sim c'_2}{
adamc@537 766 \Gamma \vdash c_1 \equiv c'_1
adamc@537 767 & \Gamma \vdash c_2 \equiv c'_2
adamc@537 768 }$$
adamc@537 769
adamc@537 770 $$\infer{\Gamma \vdash \mt{class} \; x \leq \mt{class} \; x}{}
adamc@537 771 \quad \infer{\Gamma \vdash \mt{class} \; x = c \leq \mt{class} \; x}{}
adamc@537 772 \quad \infer{\Gamma \vdash \mt{class} \; x = c_1 \leq \mt{class} \; x = c_2}{
adamc@537 773 \Gamma \vdash c_1 \equiv c_2
adamc@537 774 }$$
adamc@537 775
adamc@538 776 \subsection{Module Typing}
adamc@538 777
adamc@538 778 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 779
adamc@538 780 $$\infer{\Gamma \vdash M : S}{
adamc@538 781 \Gamma \vdash M : S'
adamc@538 782 & \Gamma \vdash S' \leq S
adamc@538 783 }
adamc@538 784 \quad \infer{\Gamma \vdash \mt{struct} \; \overline{d} \; \mt{end} : \mt{sig} \; \mt{sigOf}(\overline{d}) \; \mt{end}}{
adamc@538 785 \Gamma \vdash \overline{d} \leadsto \Gamma'
adamc@538 786 }
adamc@538 787 \quad \infer{\Gamma \vdash X : S}{
adamc@538 788 X : S \in \Gamma
adamc@538 789 }$$
adamc@538 790
adamc@538 791 $$\infer{\Gamma \vdash M.X : S}{
adamc@538 792 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@538 793 & \mt{proj}(M, \overline{s}, \mt{structure} \; X) = S
adamc@538 794 }$$
adamc@538 795
adamc@538 796 $$\infer{\Gamma \vdash M_1(M_2) : [X \mapsto M_2]S_2}{
adamc@538 797 \Gamma \vdash M_1 : \mt{functor}(X : S_1) : S_2
adamc@538 798 & \Gamma \vdash M_2 : S_1
adamc@538 799 }
adamc@538 800 \quad \infer{\Gamma \vdash \mt{functor} (X : S_1) : S_2 = M : \mt{functor} (X : S_1) : S_2}{
adamc@538 801 \Gamma \vdash S_1
adamc@538 802 & \Gamma, X : S_1 \vdash S_2
adamc@538 803 & \Gamma, X : S_1 \vdash M : S_2
adamc@538 804 }$$
adamc@538 805
adamc@538 806 \begin{eqnarray*}
adamc@538 807 \mt{sigOf}(\cdot) &=& \cdot \\
adamc@538 808 \mt{sigOf}(s \; \overline{s'}) &=& \mt{sigOf}(s) \; \mt{sigOf}(\overline{s'}) \\
adamc@538 809 \\
adamc@538 810 \mt{sigOf}(\mt{con} \; x :: \kappa = c) &=& \mt{con} \; x :: \kappa = c \\
adamc@538 811 \mt{sigOf}(\mt{datatype} \; x \; \overline{y} = \overline{dc}) &=& \mt{datatype} \; x \; \overline{y} = \overline{dc} \\
adamc@538 812 \mt{sigOf}(\mt{datatype} \; x = \mt{datatype} \; M.z) &=& \mt{datatype} \; x = \mt{datatype} \; M.z \\
adamc@538 813 \mt{sigOf}(\mt{val} \; x : \tau = e) &=& \mt{val} \; x : \tau \\
adamc@538 814 \mt{sigOf}(\mt{val} \; \mt{rec} \; \overline{x : \tau = e}) &=& \overline{\mt{val} \; x : \tau} \\
adamc@538 815 \mt{sigOf}(\mt{structure} \; X : S = M) &=& \mt{structure} \; X : S \\
adamc@538 816 \mt{sigOf}(\mt{signature} \; X = S) &=& \mt{signature} \; X = S \\
adamc@538 817 \mt{sigOf}(\mt{open} \; M) &=& \mt{include} \; S \textrm{ (where $\Gamma \vdash M : S$)} \\
adamc@538 818 \mt{sigOf}(\mt{constraint} \; c_1 \sim c_2) &=& \mt{constraint} \; c_1 \sim c_2 \\
adamc@538 819 \mt{sigOf}(\mt{open} \; \mt{constraints} \; M) &=& \cdot \\
adamc@538 820 \mt{sigOf}(\mt{table} \; x : c) &=& \mt{table} \; x : c \\
adamc@538 821 \mt{sigOf}(\mt{sequence} \; x) &=& \mt{sequence} \; x \\
adamc@538 822 \mt{sigOf}(\mt{cookie} \; x : \tau) &=& \mt{cookie} \; x : \tau \\
adamc@538 823 \mt{sigOf}(\mt{class} \; x = c) &=& \mt{class} \; x = c \\
adamc@538 824 \end{eqnarray*}
adamc@538 825
adamc@539 826 \begin{eqnarray*}
adamc@539 827 \mt{selfify}(M, \cdot) &=& \cdot \\
adamc@539 828 \mt{selfify}(M, s \; \overline{s'}) &=& \mt{selfify}(M, \sigma, s) \; \mt{selfify}(M, \overline{s'}) \\
adamc@539 829 \\
adamc@539 830 \mt{selfify}(M, \mt{con} \; x :: \kappa) &=& \mt{con} \; x :: \kappa = M.x \\
adamc@539 831 \mt{selfify}(M, \mt{con} \; x :: \kappa = c) &=& \mt{con} \; x :: \kappa = c \\
adamc@539 832 \mt{selfify}(M, \mt{datatype} \; x \; \overline{y} = \overline{dc}) &=& \mt{datatype} \; x \; \overline{y} = \mt{datatype} \; M.x \\
adamc@539 833 \mt{selfify}(M, \mt{datatype} \; x = \mt{datatype} \; M'.z) &=& \mt{datatype} \; x = \mt{datatype} \; M'.z \\
adamc@539 834 \mt{selfify}(M, \mt{val} \; x : \tau) &=& \mt{val} \; x : \tau \\
adamc@539 835 \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 836 \mt{selfify}(M, \mt{signature} \; X = S) &=& \mt{signature} \; X = S \\
adamc@539 837 \mt{selfify}(M, \mt{include} \; S) &=& \mt{include} \; S \\
adamc@539 838 \mt{selfify}(M, \mt{constraint} \; c_1 \sim c_2) &=& \mt{constraint} \; c_1 \sim c_2 \\
adamc@539 839 \mt{selfify}(M, \mt{class} \; x) &=& \mt{class} \; x = M.x \\
adamc@539 840 \mt{selfify}(M, \mt{class} \; x = c) &=& \mt{class} \; x = c \\
adamc@539 841 \end{eqnarray*}
adamc@539 842
adamc@540 843 \subsection{Module Projection}
adamc@540 844
adamc@540 845 \begin{eqnarray*}
adamc@540 846 \mt{proj}(M, \mt{con} \; x :: \kappa \; \overline{s}, \mt{con} \; x) &=& \kappa \\
adamc@540 847 \mt{proj}(M, \mt{con} \; x :: \kappa = c \; \overline{s}, \mt{con} \; x) &=& (\kappa, c) \\
adamc@540 848 \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 849 \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 850 && \textrm{and $\mt{proj}(M', \overline{s'}, \mt{datatype} \; z) = (\overline{y}, \overline{dc})$)} \\
adamc@540 851 \mt{proj}(M, \mt{class} \; x \; \overline{s}, \mt{con} \; x) &=& \mt{Type} \to \mt{Type} \\
adamc@540 852 \mt{proj}(M, \mt{class} \; x = c \; \overline{s}, \mt{con} \; x) &=& (\mt{Type} \to \mt{Type}, c) \\
adamc@540 853 \\
adamc@540 854 \mt{proj}(M, \mt{datatype} \; x \; \overline{y} = \overline{dc} \; \overline{s}, \mt{datatype} \; x) &=& (\overline{y}, \overline{dc}) \\
adamc@540 855 \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 856 \\
adamc@540 857 \mt{proj}(M, \mt{val} \; x : \tau \; \overline{s}, \mt{val} \; x) &=& \tau \\
adamc@540 858 \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 859 \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 860 \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 861 && \textrm{and $\mt{proj}(M', \overline{s'}, \mt{datatype} \; z = (\overline{y}, \overline{dc})$ and $X \in \overline{dc}$)} \\
adamc@540 862 \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@540 863 && \textrm{and $\mt{proj}(M', \overline{s'}, \mt{datatype} \; z = (\overline{y}, \overline{dc})$ and $X : \tau \in \overline{dc}$)} \\
adamc@540 864 \\
adamc@540 865 \mt{proj}(M, \mt{structure} \; X : S \; \overline{s}, \mt{structure} \; X) &=& S \\
adamc@540 866 \\
adamc@540 867 \mt{proj}(M, \mt{signature} \; X = S \; \overline{s}, \mt{signature} \; X) &=& S \\
adamc@540 868 \\
adamc@540 869 \mt{proj}(M, \mt{con} \; x :: \kappa \; \overline{s}, V) &=& [x \mapsto M.x]\mt{proj}(M, \overline{s}, V) \\
adamc@540 870 \mt{proj}(M, \mt{con} \; x :: \kappa = c \; \overline{s}, V) &=& [x \mapsto M.x]\mt{proj}(M, \overline{s}, V) \\
adamc@540 871 \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 872 \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 873 \mt{proj}(M, \mt{val} \; x : \tau \; \overline{s}, V) &=& \mt{proj}(M, \overline{s}, V) \\
adamc@540 874 \mt{proj}(M, \mt{structure} \; X : S \; \overline{s}, V) &=& [X \mapsto M.X]\mt{proj}(M, \overline{s}, V) \\
adamc@540 875 \mt{proj}(M, \mt{signature} \; X = S \; \overline{s}, V) &=& [X \mapsto M.X]\mt{proj}(M, \overline{s}, V) \\
adamc@540 876 \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 877 \mt{proj}(M, \mt{constraint} \; c_1 \sim c_2 \; \overline{s}, V) &=& \mt{proj}(M, \overline{s}, V) \\
adamc@540 878 \mt{proj}(M, \mt{class} \; x \; \overline{s}, V) &=& [x \mapsto M.x]\mt{proj}(M, \overline{s}, V) \\
adamc@540 879 \mt{proj}(M, \mt{class} \; x = c \; \overline{s}, V) &=& [x \mapsto M.x]\mt{proj}(M, \overline{s}, V) \\
adamc@540 880 \end{eqnarray*}
adamc@540 881
adamc@541 882
adamc@541 883 \section{Type Inference}
adamc@541 884
adamc@541 885 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 886
adamc@541 887 \subsection{Basic Unification}
adamc@541 888
adamc@541 889 Type-checkers for languages based on the Hindly-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 890
adamc@541 891 Type-checking can require evaluating recursive functional programs, thanks to the type-level $\mt{fold}$ 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 incompletness.
adamc@541 892
adamc@541 893 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 894
adamc@541 895 \subsection{Unifying Record Types}
adamc@541 896
adamc@541 897 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 reduce 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 898
adamc@541 899 \subsection{\label{typeclasses}Type Classes}
adamc@541 900
adamc@541 901 Ur includes a type class facility inspired by Haskell's. The current version is very rudimentary, only supporting instances for particular types built up from abstract types and datatypes and type-level application.
adamc@541 902
adamc@541 903 Type classes are integrated with the module system. A type class is just a constructor of kind $\mt{Type} \to \mt{Type}$. By marking such a constructor $c$ as a type class, the programmer instructs the type inference engine to, in each scope, record all values of types $c \; \tau$ 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 904
adamc@541 905 The ``dictionary encoding'' often used in Haskell implementations is made explicit in Ur. Type 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 906
adamc@541 907 Just as for types, type classes may be exported from modules, and they may be exported as concrete or abstract. Concrete type classes have their ``real'' definitions exposed, so that client code may add new instances freely. Abstract type 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 908
adamc@541 909 \subsection{Reverse-Engineering Record Types}
adamc@541 910
adamc@541 911 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 folded over, yielding known results. Often, as in the case of $\mt{map}$-like folds, the base and recursive cases of a fold produce constructors with different top-level structure. Thus, if the result of the fold is known, examining its top-level structure reveals whether the record being folded over is empty or not. If it's 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 912
adamc@541 913 \subsection{Implicit Arguments in Functor Applications}
adamc@541 914
adamc@541 915 Constructor, constraint, and type 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 916
adamc@541 917
adamc@542 918 \section{The Ur Standard Library}
adamc@542 919
adamc@542 920 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 921
adamc@542 922 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 923
adamc@542 924 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 925 $$\begin{array}{l}
adamc@542 926 \mt{type} \; \mt{int} \\
adamc@542 927 \mt{type} \; \mt{float} \\
adamc@542 928 \mt{type} \; \mt{string} \\
adamc@542 929 \mt{type} \; \mt{time} \\
adamc@542 930 \\
adamc@542 931 \mt{type} \; \mt{unit} = \{\} \\
adamc@542 932 \\
adamc@542 933 \mt{datatype} \; \mt{bool} = \mt{False} \mid \mt{True} \\
adamc@542 934 \\
adamc@542 935 \mt{datatype} \; \mt{option} \; \mt{t} = \mt{None} \mid \mt{Some} \; \mt{of} \; \mt{t}
adamc@542 936 \end{array}$$
adamc@542 937
adamc@542 938
adamc@542 939 \section{The Ur/Web Standard Library}
adamc@542 940
adamc@542 941 \subsection{Transactions}
adamc@542 942
adamc@542 943 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 944 $$\begin{array}{l}
adamc@542 945 \mt{con} \; \mt{transaction} :: \mt{Type} \to \mt{Type} \\
adamc@542 946 \\
adamc@542 947 \mt{val} \; \mt{return} : \mt{t} ::: \mt{Type} \to \mt{t} \to \mt{transaction} \; \mt{t} \\
adamc@542 948 \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 949 \end{array}$$
adamc@542 950
adamc@542 951 \subsection{HTTP}
adamc@542 952
adamc@542 953 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 954 $$\begin{array}{l}
adamc@542 955 \mt{val} \; \mt{requestHeader} : \mt{string} \to \mt{transaction} \; (\mt{option} \; \mt{string}) \\
adamc@542 956 \\
adamc@542 957 \mt{con} \; \mt{http\_cookie} :: \mt{Type} \to \mt{Type} \\
adamc@542 958 \mt{val} \; \mt{getCookie} : \mt{t} ::: \mt{Type} \to \mt{http\_cookie} \; \mt{t} \to \mt{transaction} \; (\mt{option} \; \mt{t}) \\
adamc@542 959 \mt{val} \; \mt{setCookie} : \mt{t} ::: \mt{Type} \to \mt{http\_cookie} \; \mt{t} \to \mt{t} \to \mt{transaction} \; \mt{unit}
adamc@542 960 \end{array}$$
adamc@542 961
adamc@543 962 \subsection{SQL}
adamc@543 963
adamc@543 964 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 965 $$\begin{array}{l}
adamc@543 966 \mt{con} \; \mt{sql\_table} :: \{\mt{Type}\} \to \mt{Type}
adamc@543 967 \end{array}$$
adamc@543 968
adamc@543 969 \subsubsection{Queries}
adamc@543 970
adamc@543 971 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 972 $$\begin{array}{l}
adamc@543 973 \mt{con} \; \mt{sql\_query} :: \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \\
adamc@543 974 \mt{val} \; \mt{sql\_query} : \mt{tables} ::: \{\{\mt{Type}\}\} \\
adamc@543 975 \hspace{.1in} \to \mt{selectedFields} ::: \{\{\mt{Type}\}\} \\
adamc@543 976 \hspace{.1in} \to \mt{selectedExps} ::: \{\mt{Type}\} \\
adamc@543 977 \hspace{.1in} \to \{\mt{Rows} : \mt{sql\_query1} \; \mt{tables} \; \mt{selectedFields} \; \mt{selectedExps}, \\
adamc@543 978 \hspace{.2in} \mt{OrderBy} : \mt{sql\_order\_by} \; \mt{tables} \; \mt{selectedExps}, \\
adamc@543 979 \hspace{.2in} \mt{Limit} : \mt{sql\_limit}, \\
adamc@543 980 \hspace{.2in} \mt{Offset} : \mt{sql\_offset}\} \\
adamc@543 981 \hspace{.1in} \to \mt{sql\_query} \; \mt{selectedFields} \; \mt{selectedExps}
adamc@543 982 \end{array}$$
adamc@543 983
adamc@545 984 Queries are used by folding over their results inside transactions.
adamc@545 985 $$\begin{array}{l}
adamc@545 986 \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 987 \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 988 \hspace{.2in} \to \mt{state} \to \mt{transaction} \; \mt{state}) \\
adamc@545 989 \hspace{.1in} \to \mt{state} \to \mt{transaction} \; \mt{state}
adamc@545 990 \end{array}$$
adamc@545 991
adamc@543 992 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 993 $$\begin{array}{l}
adamc@543 994 \mt{con} \; \mt{sql\_query1} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \\
adamc@543 995 \\
adamc@543 996 \mt{type} \; \mt{sql\_relop} \\
adamc@543 997 \mt{val} \; \mt{sql\_union} : \mt{sql\_relop} \\
adamc@543 998 \mt{val} \; \mt{sql\_intersect} : \mt{sql\_relop} \\
adamc@543 999 \mt{val} \; \mt{sql\_except} : \mt{sql\_relop} \\
adamc@543 1000 \mt{val} \; \mt{sql\_relop} : \mt{tables1} ::: \{\{\mt{Type}\}\} \\
adamc@543 1001 \hspace{.1in} \to \mt{tables2} ::: \{\{\mt{Type}\}\} \\
adamc@543 1002 \hspace{.1in} \to \mt{selectedFields} ::: \{\{\mt{Type}\}\} \\
adamc@543 1003 \hspace{.1in} \to \mt{selectedExps} ::: \{\mt{Type}\} \\
adamc@543 1004 \hspace{.1in} \to \mt{sql\_relop} \\
adamc@543 1005 \hspace{.1in} \to \mt{sql\_query1} \; \mt{tables1} \; \mt{selectedFields} \; \mt{selectedExps} \\
adamc@543 1006 \hspace{.1in} \to \mt{sql\_query1} \; \mt{tables2} \; \mt{selectedFields} \; \mt{selectedExps} \\
adamc@543 1007 \hspace{.1in} \to \mt{sql\_query1} \; \mt{selectedFields} \; \mt{selectedFields} \; \mt{selectedExps}
adamc@543 1008 \end{array}$$
adamc@543 1009
adamc@543 1010 $$\begin{array}{l}
adamc@543 1011 \mt{val} \; \mt{sql\_query1} : \mt{tables} ::: \{\{\mt{Type}\}\} \\
adamc@543 1012 \hspace{.1in} \to \mt{grouped} ::: \{\{\mt{Type}\}\} \\
adamc@543 1013 \hspace{.1in} \to \mt{selectedFields} ::: \{\{\mt{Type}\}\} \\
adamc@543 1014 \hspace{.1in} \to \mt{selectedExps} ::: \{\mt{Type}\} \\
adamc@543 1015 \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 1016 \hspace{.2in} \mt{Where} : \mt{sql\_exp} \; \mt{tables} \; [] \; [] \; \mt{bool}, \\
adamc@543 1017 \hspace{.2in} \mt{GroupBy} : \mt{sql\_subset} \; \mt{tables} \; \mt{grouped}, \\
adamc@543 1018 \hspace{.2in} \mt{Having} : \mt{sql\_exp} \; \mt{grouped} \; \mt{tables} \; [] \; \mt{bool}, \\
adamc@543 1019 \hspace{.2in} \mt{SelectFields} : \mt{sql\_subset} \; \mt{grouped} \; \mt{selectedFields}, \\
adamc@543 1020 \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 1021 \hspace{.1in} \to \mt{sql\_query1} \; \mt{tables} \; \mt{selectedFields} \; \mt{selectedExps}
adamc@543 1022 \end{array}$$
adamc@543 1023
adamc@543 1024 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 1025 $$\begin{array}{l}
adamc@543 1026 \mt{con} \; \mt{sql\_subset} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \mt{Type} \\
adamc@543 1027 \mt{val} \; \mt{sql\_subset} : \mt{keep\_drop} :: \{(\{\mt{Type}\} \times \{\mt{Type}\})\} \\
adamc@543 1028 \hspace{.1in} \to \mt{sql\_subset} \\
adamc@543 1029 \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 1030 \hspace{.3in} [\mt{nm} = \mt{fields}.1 \rc \mt{fields}.2] \rc \mt{acc}) \; [] \; \mt{keep\_drop}) \\
adamc@543 1031 \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 1032 \mt{val} \; \mt{sql\_subset\_all} : \mt{tables} :: \{\{\mt{Type}\}\} \to \mt{sql\_subset} \; \mt{tables} \; \mt{tables}
adamc@543 1033 \end{array}$$
adamc@543 1034
adamc@543 1035 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-availablity 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 1036 $$\begin{array}{l}
adamc@543 1037 \mt{con} \; \mt{sql\_exp} :: \{\{\mt{Type}\}\} \to \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \to \mt{Type}
adamc@543 1038 \end{array}$$
adamc@543 1039
adamc@543 1040 Any field in scope may be converted to an expression.
adamc@543 1041 $$\begin{array}{l}
adamc@543 1042 \mt{val} \; \mt{sql\_field} : \mt{otherTabs} ::: \{\{\mt{Type}\}\} \to \mt{otherFields} ::: \{\mt{Type}\} \\
adamc@543 1043 \hspace{.1in} \to \mt{fieldType} ::: \mt{Type} \to \mt{agg} ::: \{\{\mt{Type}\}\} \\
adamc@543 1044 \hspace{.1in} \to \mt{exps} ::: \{\mt{Type}\} \\
adamc@543 1045 \hspace{.1in} \to \mt{tab} :: \mt{Name} \to \mt{field} :: \mt{Name} \\
adamc@543 1046 \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 1047 \end{array}$$
adamc@543 1048
adamc@544 1049 There is an analogous function for referencing named expressions.
adamc@544 1050 $$\begin{array}{l}
adamc@544 1051 \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 1052 \hspace{.1in} \to \mt{sql\_exp} \; \mt{tabs} \; \mt{agg} \; ([\mt{nm} = \mt{t}] \rc \mt{rest}) \; \mt{t}
adamc@544 1053 \end{array}$$
adamc@544 1054
adamc@544 1055 Ur values of appropriate types may be injected into SQL expressions.
adamc@544 1056 $$\begin{array}{l}
adamc@544 1057 \mt{class} \; \mt{sql\_injectable} \\
adamc@544 1058 \mt{val} \; \mt{sql\_bool} : \mt{sql\_injectable} \; \mt{bool} \\
adamc@544 1059 \mt{val} \; \mt{sql\_int} : \mt{sql\_injectable} \; \mt{int} \\
adamc@544 1060 \mt{val} \; \mt{sql\_float} : \mt{sql\_injectable} \; \mt{float} \\
adamc@544 1061 \mt{val} \; \mt{sql\_string} : \mt{sql\_injectable} \; \mt{string} \\
adamc@544 1062 \mt{val} \; \mt{sql\_time} : \mt{sql\_injectable} \; \mt{time} \\
adamc@544 1063 \mt{val} \; \mt{sql\_option\_bool} : \mt{sql\_injectable} \; (\mt{option} \; \mt{bool}) \\
adamc@544 1064 \mt{val} \; \mt{sql\_option\_int} : \mt{sql\_injectable} \; (\mt{option} \; \mt{int}) \\
adamc@544 1065 \mt{val} \; \mt{sql\_option\_float} : \mt{sql\_injectable} \; (\mt{option} \; \mt{float}) \\
adamc@544 1066 \mt{val} \; \mt{sql\_option\_string} : \mt{sql\_injectable} \; (\mt{option} \; \mt{string}) \\
adamc@544 1067 \mt{val} \; \mt{sql\_option\_time} : \mt{sql\_injectable} \; (\mt{option} \; \mt{time}) \\
adamc@544 1068 \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 1069 \hspace{.1in} \to \mt{t} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t}
adamc@544 1070 \end{array}$$
adamc@544 1071
adamc@544 1072 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 1073 $$\begin{array}{l}
adamc@544 1074 \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 1075 \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 1076 \end{array}$$
adamc@544 1077
adamc@544 1078 We have generic nullary, unary, and binary operators, as well as comparison operators.
adamc@544 1079 $$\begin{array}{l}
adamc@544 1080 \mt{con} \; \mt{sql\_nfunc} :: \mt{Type} \to \mt{Type} \\
adamc@544 1081 \mt{val} \; \mt{sql\_current\_timestamp} : \mt{sql\_nfunc} \; \mt{time} \\
adamc@544 1082 \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 1083 \hspace{.1in} \to \mt{sql\_nfunc} \; \mt{t} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} \\\end{array}$$
adamc@544 1084
adamc@544 1085 $$\begin{array}{l}
adamc@544 1086 \mt{con} \; \mt{sql\_unary} :: \mt{Type} \to \mt{Type} \to \mt{Type} \\
adamc@544 1087 \mt{val} \; \mt{sql\_not} : \mt{sql\_unary} \; \mt{bool} \; \mt{bool} \\
adamc@544 1088 \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 1089 \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 1090 \end{array}$$
adamc@544 1091
adamc@544 1092 $$\begin{array}{l}
adamc@544 1093 \mt{con} \; \mt{sql\_binary} :: \mt{Type} \to \mt{Type} \to \mt{Type} \to \mt{Type} \\
adamc@544 1094 \mt{val} \; \mt{sql\_and} : \mt{sql\_binary} \; \mt{bool} \; \mt{bool} \; \mt{bool} \\
adamc@544 1095 \mt{val} \; \mt{sql\_or} : \mt{sql\_binary} \; \mt{bool} \; \mt{bool} \; \mt{bool} \\
adamc@544 1096 \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 1097 \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 1098 \end{array}$$
adamc@544 1099
adamc@544 1100 $$\begin{array}{l}
adamc@544 1101 \mt{type} \; \mt{sql\_comparison} \\
adamc@544 1102 \mt{val} \; \mt{sql\_eq} : \mt{sql\_comparison} \\
adamc@544 1103 \mt{val} \; \mt{sql\_ne} : \mt{sql\_comparison} \\
adamc@544 1104 \mt{val} \; \mt{sql\_lt} : \mt{sql\_comparison} \\
adamc@544 1105 \mt{val} \; \mt{sql\_le} : \mt{sql\_comparison} \\
adamc@544 1106 \mt{val} \; \mt{sql\_gt} : \mt{sql\_comparison} \\
adamc@544 1107 \mt{val} \; \mt{sql\_ge} : \mt{sql\_comparison} \\
adamc@544 1108 \mt{val} \; \mt{sql\_comparison} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{agg} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{t} ::: \mt{Type} \\
adamc@544 1109 \hspace{.1in} \to \mt{sql\_comparison} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{t} \to \mt{sql\_exp} \; \mt{tables} \; \mt{agg} \; \mt{exps} \; \mt{bool}
adamc@544 1110 \end{array}$$
adamc@544 1111
adamc@544 1112 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 type 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 1113
adamc@544 1114 $$\begin{array}{l}
adamc@544 1115 \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 1116 \end{array}$$
adamc@544 1117
adamc@544 1118 $$\begin{array}{l}
adamc@544 1119 \mt{con} \; \mt{sql\_aggregate} :: \mt{Type} \to \mt{Type} \\
adamc@544 1120 \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 1121 \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 1122 \end{array}$$
adamc@544 1123
adamc@544 1124 $$\begin{array}{l}
adamc@544 1125 \mt{class} \; \mt{sql\_summable} \\
adamc@544 1126 \mt{val} \; \mt{sql\_summable\_int} : \mt{sql\_summable} \; \mt{int} \\
adamc@544 1127 \mt{val} \; \mt{sql\_summable\_float} : \mt{sql\_summable} \; \mt{float} \\
adamc@544 1128 \mt{val} \; \mt{sql\_avg} : \mt{t} ::: \mt{Type} \to \mt{sql\_summable} \; \mt{t} \to \mt{sql\_aggregate} \; \mt{t} \\
adamc@544 1129 \mt{val} \; \mt{sql\_sum} : \mt{t} ::: \mt{Type} \to \mt{sql\_summable} \mt{t} \to \mt{sql\_aggregate} \; \mt{t}
adamc@544 1130 \end{array}$$
adamc@544 1131
adamc@544 1132 $$\begin{array}{l}
adamc@544 1133 \mt{class} \; \mt{sql\_maxable} \\
adamc@544 1134 \mt{val} \; \mt{sql\_maxable\_int} : \mt{sql\_maxable} \; \mt{int} \\
adamc@544 1135 \mt{val} \; \mt{sql\_maxable\_float} : \mt{sql\_maxable} \; \mt{float} \\
adamc@544 1136 \mt{val} \; \mt{sql\_maxable\_string} : \mt{sql\_maxable} \; \mt{string} \\
adamc@544 1137 \mt{val} \; \mt{sql\_maxable\_time} : \mt{sql\_maxable} \; \mt{time} \\
adamc@544 1138 \mt{val} \; \mt{sql\_max} : \mt{t} ::: \mt{Type} \to \mt{sql\_maxable} \; \mt{t} \to \mt{sql\_aggregate} \; \mt{t} \\
adamc@544 1139 \mt{val} \; \mt{sql\_min} : \mt{t} ::: \mt{Type} \to \mt{sql\_maxable} \; \mt{t} \to \mt{sql\_aggregate} \; \mt{t}
adamc@544 1140 \end{array}$$
adamc@544 1141
adamc@544 1142 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 1143 $$\begin{array}{l}
adamc@544 1144 \mt{type} \; \mt{sql\_direction} \\
adamc@544 1145 \mt{val} \; \mt{sql\_asc} : \mt{sql\_direction} \\
adamc@544 1146 \mt{val} \; \mt{sql\_desc} : \mt{sql\_direction} \\
adamc@544 1147 \\
adamc@544 1148 \mt{con} \; \mt{sql\_order\_by} :: \{\{\mt{Type}\}\} \to \{\mt{Type}\} \to \mt{Type} \\
adamc@544 1149 \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 1150 \mt{val} \; \mt{sql\_order\_by\_Cons} : \mt{tables} ::: \{\{\mt{Type}\}\} \to \mt{exps} ::: \{\mt{Type}\} \to \mt{t} ::: \mt{Type} \\
adamc@544 1151 \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 1152 \\
adamc@544 1153 \mt{type} \; \mt{sql\_limit} \\
adamc@544 1154 \mt{val} \; \mt{sql\_no\_limit} : \mt{sql\_limit} \\
adamc@544 1155 \mt{val} \; \mt{sql\_limit} : \mt{int} \to \mt{sql\_limit} \\
adamc@544 1156 \\
adamc@544 1157 \mt{type} \; \mt{sql\_offset} \\
adamc@544 1158 \mt{val} \; \mt{sql\_no\_offset} : \mt{sql\_offset} \\
adamc@544 1159 \mt{val} \; \mt{sql\_offset} : \mt{int} \to \mt{sql\_offset}
adamc@544 1160 \end{array}$$
adamc@544 1161
adamc@545 1162
adamc@545 1163 \subsubsection{DML}
adamc@545 1164
adamc@545 1165 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 1166
adamc@545 1167 $$\begin{array}{l}
adamc@545 1168 \mt{type} \; \mt{dml} \\
adamc@545 1169 \mt{val} \; \mt{dml} : \mt{dml} \to \mt{transaction} \; \mt{unit}
adamc@545 1170 \end{array}$$
adamc@545 1171
adamc@545 1172 Properly-typed records may be used to form $\mt{INSERT}$ commands.
adamc@545 1173 $$\begin{array}{l}
adamc@545 1174 \mt{val} \; \mt{insert} : \mt{fields} ::: \{\mt{Type}\} \to \mt{sql\_table} \; \mt{fields} \\
adamc@545 1175 \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 1176 \end{array}$$
adamc@545 1177
adamc@545 1178 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 1179 $$\begin{array}{l}
adamc@545 1180 \mt{val} \; \mt{update} : \mt{unchanged} ::: \{\mt{Type}\} \to \mt{changed} :: \{\mt{Type}\} \to \lambda [\mt{changed} \sim \mt{unchanged}] \\
adamc@545 1181 \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 1182 \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 1183 \end{array}$$
adamc@545 1184
adamc@545 1185 A $\mt{DELETE}$ command is formed from a table and a $\mt{WHERE}$ clause.
adamc@545 1186 $$\begin{array}{l}
adamc@545 1187 \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 1188 \end{array}$$
adamc@545 1189
adamc@546 1190 \subsubsection{Sequences}
adamc@546 1191
adamc@546 1192 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 1193
adamc@546 1194 $$\begin{array}{l}
adamc@546 1195 \mt{type} \; \mt{sql\_sequence} \\
adamc@546 1196 \mt{val} \; \mt{nextval} : \mt{sql\_sequence} \to \mt{transaction} \; \mt{int}
adamc@546 1197 \end{array}$$
adamc@546 1198
adamc@546 1199
adamc@524 1200 \end{document}