annotate doc/manual.tex @ 533:419f51b1e68d

Typing
author Adam Chlipala <adamc@hcoop.net>
date Sat, 29 Nov 2008 10:34:56 -0500
parents 23718a4b23d7
children 65c253a9ca92
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@529 18 \section{Ur Syntax}
adamc@529 19
adamc@529 20 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 21
adamc@524 22 \subsection{Lexical Conventions}
adamc@524 23
adamc@524 24 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 25
adamc@524 26 \begin{center}
adamc@524 27 \begin{tabular}{rl}
adamc@524 28 \textbf{\LaTeX} & \textbf{ASCII} \\
adamc@524 29 $\to$ & \cd{->} \\
adamc@524 30 $\times$ & \cd{*} \\
adamc@524 31 $\lambda$ & \cd{fn} \\
adamc@524 32 $\Rightarrow$ & \cd{=>} \\
adamc@529 33 $\neq$ & \cd{<>} \\
adamc@529 34 $\leq$ & \cd{<=} \\
adamc@529 35 $\geq$ & \cd{>=} \\
adamc@524 36 \\
adamc@524 37 $x$ & Normal textual identifier, not beginning with an uppercase letter \\
adamc@525 38 $X$ & Normal textual identifier, beginning with an uppercase letter \\
adamc@524 39 \end{tabular}
adamc@524 40 \end{center}
adamc@524 41
adamc@525 42 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 43
adamc@526 44 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 45
adamc@527 46 This version of the manual doesn't include operator precedences; see \texttt{src/urweb.grm} for that.
adamc@527 47
adamc@524 48 \subsection{Core Syntax}
adamc@524 49
adamc@524 50 \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 51 $$\begin{array}{rrcll}
adamc@524 52 \textrm{Kinds} & \kappa &::=& \mt{Type} & \textrm{proper types} \\
adamc@525 53 &&& \mt{Unit} & \textrm{the trivial constructor} \\
adamc@525 54 &&& \mt{Name} & \textrm{field names} \\
adamc@525 55 &&& \kappa \to \kappa & \textrm{type-level functions} \\
adamc@525 56 &&& \{\kappa\} & \textrm{type-level records} \\
adamc@525 57 &&& (\kappa\times^+) & \textrm{type-level tuples} \\
adamc@529 58 &&& \_\_ & \textrm{wildcard} \\
adamc@525 59 &&& (\kappa) & \textrm{explicit precedence} \\
adamc@524 60 \end{array}$$
adamc@524 61
adamc@524 62 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 63 $$\begin{array}{rrcll}
adamc@524 64 \textrm{Explicitness} & ? &::=& :: & \textrm{explicit} \\
adamc@525 65 &&& \; ::: & \textrm{implicit}
adamc@524 66 \end{array}$$
adamc@524 67
adamc@524 68 \emph{Constructors} are the main class of compile-time-only data. They include proper types and are classified by kinds.
adamc@524 69 $$\begin{array}{rrcll}
adamc@524 70 \textrm{Constructors} & c, \tau &::=& (c) :: \kappa & \textrm{kind annotation} \\
adamc@530 71 &&& \hat{x} & \textrm{constructor variable} \\
adamc@524 72 \\
adamc@525 73 &&& \tau \to \tau & \textrm{function type} \\
adamc@525 74 &&& x \; ? \; \kappa \to \tau & \textrm{polymorphic function type} \\
adamc@525 75 &&& \$ c & \textrm{record type} \\
adamc@524 76 \\
adamc@525 77 &&& c \; c & \textrm{type-level function application} \\
adamc@530 78 &&& \lambda x \; :: \; \kappa \Rightarrow c & \textrm{type-level function abstraction} \\
adamc@524 79 \\
adamc@525 80 &&& () & \textrm{type-level unit} \\
adamc@525 81 &&& \#X & \textrm{field name} \\
adamc@524 82 \\
adamc@525 83 &&& [(c = c)^*] & \textrm{known-length type-level record} \\
adamc@525 84 &&& c \rc c & \textrm{type-level record concatenation} \\
adamc@525 85 &&& \mt{fold} & \textrm{type-level record fold} \\
adamc@524 86 \\
adamc@525 87 &&& (c^+) & \textrm{type-level tuple} \\
adamc@525 88 &&& c.n & \textrm{type-level tuple projection ($n \in \mathbb N^+$)} \\
adamc@524 89 \\
adamc@525 90 &&& \lambda [c \sim c] \Rightarrow c & \textrm{guarded constructor} \\
adamc@524 91 \\
adamc@529 92 &&& \_ :: \kappa & \textrm{wildcard} \\
adamc@525 93 &&& (c) & \textrm{explicit precedence} \\
adamc@530 94 \\
adamc@530 95 \textrm{Qualified uncapitalized variables} & \hat{x} &::=& x & \textrm{not from a module} \\
adamc@530 96 &&& M.x & \textrm{projection from a module} \\
adamc@525 97 \end{array}$$
adamc@525 98
adamc@525 99 Modules of the module system are described by \emph{signatures}.
adamc@525 100 $$\begin{array}{rrcll}
adamc@525 101 \textrm{Signatures} & S &::=& \mt{sig} \; s^* \; \mt{end} & \textrm{constant} \\
adamc@525 102 &&& X & \textrm{variable} \\
adamc@525 103 &&& \mt{functor}(X : S) : S & \textrm{functor} \\
adamc@529 104 &&& S \; \mt{where} \; \mt{con} \; x = c & \textrm{concretizing an abstract constructor} \\
adamc@525 105 &&& M.X & \textrm{projection from a module} \\
adamc@525 106 \\
adamc@525 107 \textrm{Signature items} & s &::=& \mt{con} \; x :: \kappa & \textrm{abstract constructor} \\
adamc@525 108 &&& \mt{con} \; x :: \kappa = c & \textrm{concrete constructor} \\
adamc@528 109 &&& \mt{datatype} \; x \; x^* = dc\mid^+ & \textrm{algebraic datatype definition} \\
adamc@529 110 &&& \mt{datatype} \; x = \mt{datatype} \; M.x & \textrm{algebraic datatype import} \\
adamc@525 111 &&& \mt{val} \; x : \tau & \textrm{value} \\
adamc@525 112 &&& \mt{structure} \; X : S & \textrm{sub-module} \\
adamc@525 113 &&& \mt{signature} \; X = S & \textrm{sub-signature} \\
adamc@525 114 &&& \mt{include} \; S & \textrm{signature inclusion} \\
adamc@525 115 &&& \mt{constraint} \; c \sim c & \textrm{record disjointness constraint} \\
adamc@525 116 &&& \mt{class} \; x & \textrm{abstract type class} \\
adamc@525 117 &&& \mt{class} \; x = c & \textrm{concrete type class} \\
adamc@525 118 \\
adamc@525 119 \textrm{Datatype constructors} & dc &::=& X & \textrm{nullary constructor} \\
adamc@525 120 &&& X \; \mt{of} \; \tau & \textrm{unary constructor} \\
adamc@524 121 \end{array}$$
adamc@524 122
adamc@526 123 \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 124 $$\begin{array}{rrcll}
adamc@526 125 \textrm{Patterns} & p &::=& \_ & \textrm{wildcard} \\
adamc@526 126 &&& x & \textrm{variable} \\
adamc@526 127 &&& \ell & \textrm{constant} \\
adamc@526 128 &&& \hat{X} & \textrm{nullary constructor} \\
adamc@526 129 &&& \hat{X} \; p & \textrm{unary constructor} \\
adamc@526 130 &&& \{(x = p,)^*\} & \textrm{rigid record pattern} \\
adamc@526 131 &&& \{(x = p,)^+, \ldots\} & \textrm{flexible record pattern} \\
adamc@527 132 &&& (p) & \textrm{explicit precedence} \\
adamc@526 133 \\
adamc@529 134 \textrm{Qualified capitalized variables} & \hat{X} &::=& X & \textrm{not from a module} \\
adamc@526 135 &&& M.X & \textrm{projection from a module} \\
adamc@526 136 \end{array}$$
adamc@526 137
adamc@527 138 \emph{Expressions} are the main run-time entities, corresponding to both ``expressions'' and ``statements'' in mainstream imperative languages.
adamc@527 139 $$\begin{array}{rrcll}
adamc@527 140 \textrm{Expressions} & e &::=& e : \tau & \textrm{type annotation} \\
adamc@529 141 &&& \hat{x} & \textrm{variable} \\
adamc@529 142 &&& \hat{X} & \textrm{datatype constructor} \\
adamc@527 143 &&& \ell & \textrm{constant} \\
adamc@527 144 \\
adamc@527 145 &&& e \; e & \textrm{function application} \\
adamc@527 146 &&& \lambda x : \tau \Rightarrow e & \textrm{function abstraction} \\
adamc@527 147 &&& e [c] & \textrm{polymorphic function application} \\
adamc@527 148 &&& \lambda x \; ? \; \kappa \Rightarrow e & \textrm{polymorphic function abstraction} \\
adamc@527 149 \\
adamc@527 150 &&& \{(c = e,)^*\} & \textrm{known-length record} \\
adamc@527 151 &&& e.c & \textrm{record field projection} \\
adamc@527 152 &&& e \rc e & \textrm{record concatenation} \\
adamc@527 153 &&& e \rcut c & \textrm{removal of a single record field} \\
adamc@527 154 &&& e \rcutM c & \textrm{removal of multiple record fields} \\
adamc@527 155 &&& \mt{fold} & \textrm{fold over fields of a type-level record} \\
adamc@527 156 \\
adamc@527 157 &&& \mt{let} \; ed^* \; \mt{in} \; e \; \mt{end} & \textrm{local definitions} \\
adamc@527 158 \\
adamc@527 159 &&& \mt{case} \; e \; \mt{of} \; (p \Rightarrow e|)^+ & \textrm{pattern matching} \\
adamc@527 160 \\
adamc@527 161 &&& \lambda [c \sim c] \Rightarrow e & \textrm{guarded expression} \\
adamc@527 162 \\
adamc@527 163 &&& \_ & \textrm{wildcard} \\
adamc@527 164 &&& (e) & \textrm{explicit precedence} \\
adamc@527 165 \\
adamc@527 166 \textrm{Local declarations} & ed &::=& \cd{val} \; x : \tau = e & \textrm{non-recursive value} \\
adamc@527 167 &&& \cd{val} \; \cd{rec} \; (x : \tau = e \; \cd{and})^+ & \textrm{mutually-recursive values} \\
adamc@527 168 \end{array}$$
adamc@527 169
adamc@528 170 \emph{Declarations} primarily bring new symbols into context.
adamc@528 171 $$\begin{array}{rrcll}
adamc@528 172 \textrm{Declarations} & d &::=& \mt{con} \; x :: \kappa = c & \textrm{constructor synonym} \\
adamc@528 173 &&& \mt{datatype} \; x \; x^* = dc\mid^+ & \textrm{algebraic datatype definition} \\
adamc@529 174 &&& \mt{datatype} \; x = \mt{datatype} \; M.x & \textrm{algebraic datatype import} \\
adamc@528 175 &&& \mt{val} \; x : \tau = e & \textrm{value} \\
adamc@528 176 &&& \mt{val} \; \cd{rec} \; (x : \tau = e \; \mt{and})^+ & \textrm{mutually-recursive values} \\
adamc@528 177 &&& \mt{structure} \; X : S = M & \textrm{module definition} \\
adamc@528 178 &&& \mt{signature} \; X = S & \textrm{signature definition} \\
adamc@528 179 &&& \mt{open} \; M & \textrm{module inclusion} \\
adamc@528 180 &&& \mt{constraint} \; c \sim c & \textrm{record disjointness constraint} \\
adamc@528 181 &&& \mt{open} \; \mt{constraints} \; M & \textrm{inclusion of just the constraints from a module} \\
adamc@528 182 &&& \mt{table} \; x : c & \textrm{SQL table} \\
adamc@528 183 &&& \mt{sequence} \; x & \textrm{SQL sequence} \\
adamc@528 184 &&& \mt{class} \; x = c & \textrm{concrete type class} \\
adamc@529 185 &&& \mt{cookie} \; x : \tau & \textrm{HTTP cookie} \\
adamc@528 186 \\
adamc@529 187 \textrm{Modules} & M &::=& \mt{struct} \; d^* \; \mt{end} & \textrm{constant} \\
adamc@529 188 &&& X & \textrm{variable} \\
adamc@529 189 &&& M.X & \textrm{projection} \\
adamc@529 190 &&& M(M) & \textrm{functor application} \\
adamc@529 191 &&& \mt{functor}(X : S) : S = M & \textrm{functor abstraction} \\
adamc@528 192 \end{array}$$
adamc@528 193
adamc@528 194 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 195
adamc@529 196 \subsection{Shorthands}
adamc@529 197
adamc@529 198 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 199
adamc@529 200 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 201
adamc@529 202 A record type may be written $\{(c = c,)^*\}$, which elaborates to $\$[(c = c,)^*]$.
adamc@529 203
adamc@533 204 The notation $[c_1, \ldots, c_n]$ is shorthand for $[c_1 = (), \ldots, c_n = ()]$.
adamc@533 205
adamc@529 206 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 207
adamc@529 208 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 209
adamc@529 210 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 211
adamc@529 212 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 213
adamc@529 214 A signature item or declaration $\mt{class} \; x = \lambda y :: \mt{Type} \Rightarrow c$ may be abbreviated $\mt{class} \; x \; y = c$.
adamc@529 215
adamc@529 216 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 217
adamc@529 218 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 219
adamc@529 220 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 221
adamc@529 222 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 223
adamc@529 224 A declaration $\mt{table} \; x : \{(c = c,)^*\}$ is elaborated into $\mt{table} \; x : [(c = c,)^*]$
adamc@529 225
adamc@529 226 The syntax $\mt{where} \; \mt{type}$ is an alternate form of $\mt{where} \; \mt{con}$.
adamc@529 227
adamc@529 228 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 229
adamc@529 230 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 231
adamc@529 232 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 233
adamc@530 234
adamc@530 235 \section{Static Semantics}
adamc@530 236
adamc@530 237 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 238
adamc@530 239 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 240 \begin{itemize}
adamc@530 241 \item $\Gamma \vdash c :: \kappa$ assigns a kind to a constructor in a context.
adamc@530 242 \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 243 \item $\Gamma \vdash c \hookrightarrow C$ proves that record constructor $c$ decomposes into set $C$ of field names and record constructors.
adamc@530 244 \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 245 \item $\Gamma \vdash e : \tau$ is a standard typing judgment.
adamc@533 246 \item $\Gamma \vdash p \leadsto \Gamma, \tau$ combines typing of patterns with calculation of which new variables they bind.
adamc@533 247 \item $\Gamma \vdash d \leadsto \Gamma$ expresses how a declaration modifies a context. We overload this judgment to apply to sequences of declarations.
adamc@530 248 \item $\Gamma \vdash M : S$ is the module signature checking judgment.
adamc@530 249 \item $\mt{proj}(M, S, V)$ is a partial function for projecting a signature item from a signature $S$, given the module $M$ that we project from. $V$ may be $\mt{con} \; 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 of $S$.
adamc@530 250 \end{itemize}
adamc@530 251
adamc@530 252 \subsection{Kinding}
adamc@530 253
adamc@530 254 $$\infer{\Gamma \vdash (c) :: \kappa :: \kappa}{
adamc@530 255 \Gamma \vdash c :: \kappa
adamc@530 256 }
adamc@530 257 \quad \infer{\Gamma \vdash x :: \kappa}{
adamc@530 258 x :: \kappa \in \Gamma
adamc@530 259 }
adamc@530 260 \quad \infer{\Gamma \vdash x :: \kappa}{
adamc@530 261 x :: \kappa = c \in \Gamma
adamc@530 262 }$$
adamc@530 263
adamc@530 264 $$\infer{\Gamma \vdash M.x :: \kappa}{
adamc@530 265 \Gamma \vdash M : S
adamc@530 266 & \mt{proj}(M, S, \mt{con} \; x) = \kappa
adamc@530 267 }
adamc@530 268 \quad \infer{\Gamma \vdash M.x :: \kappa}{
adamc@530 269 \Gamma \vdash M : S
adamc@530 270 & \mt{proj}(M, S, \mt{con} \; x) = (\kappa, c)
adamc@530 271 }$$
adamc@530 272
adamc@530 273 $$\infer{\Gamma \vdash \tau_1 \to \tau_2 :: \mt{Type}}{
adamc@530 274 \Gamma \vdash \tau_1 :: \mt{Type}
adamc@530 275 & \Gamma \vdash \tau_2 :: \mt{Type}
adamc@530 276 }
adamc@530 277 \quad \infer{\Gamma \vdash x \; ? \: \kappa \to \tau :: \mt{Type}}{
adamc@530 278 \Gamma, x :: \kappa \vdash \tau :: \mt{Type}
adamc@530 279 }
adamc@530 280 \quad \infer{\Gamma \vdash \$c :: \mt{Type}}{
adamc@530 281 \Gamma \vdash c :: \{\mt{Type}\}
adamc@530 282 }$$
adamc@530 283
adamc@530 284 $$\infer{\Gamma \vdash c_1 \; c_2 :: \kappa_2}{
adamc@530 285 \Gamma \vdash c_1 :: \kappa_1 \to \kappa_2
adamc@530 286 & \Gamma \vdash c_2 :: \kappa_1
adamc@530 287 }
adamc@530 288 \quad \infer{\Gamma \vdash \lambda x \; :: \; \kappa_1 \Rightarrow c :: \kappa_1 \to \kappa_2}{
adamc@530 289 \Gamma, x :: \kappa_1 \vdash c :: \kappa_2
adamc@530 290 }$$
adamc@530 291
adamc@530 292 $$\infer{\Gamma \vdash () :: \mt{Unit}}{}
adamc@530 293 \quad \infer{\Gamma \vdash \#X :: \mt{Name}}{}$$
adamc@530 294
adamc@530 295 $$\infer{\Gamma \vdash [\overline{c_i = c'_i}] :: \{\kappa\}}{
adamc@530 296 \forall i: \Gamma \vdash c_i : \mt{Name}
adamc@530 297 & \Gamma \vdash c'_i :: \kappa
adamc@530 298 & \forall i \neq j: \Gamma \vdash c_i \sim c_j
adamc@530 299 }
adamc@530 300 \quad \infer{\Gamma \vdash c_1 \rc c_2 :: \{\kappa\}}{
adamc@530 301 \Gamma \vdash c_1 :: \{\kappa\}
adamc@530 302 & \Gamma \vdash c_2 :: \{\kappa\}
adamc@530 303 & \Gamma \vdash c_1 \sim c_2
adamc@530 304 }$$
adamc@530 305
adamc@530 306 $$\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 307
adamc@530 308 $$\infer{\Gamma \vdash (\overline c) :: (k_1 \times \ldots \times k_n)}{
adamc@530 309 \forall i: \Gamma \vdash c_i :: k_i
adamc@530 310 }
adamc@530 311 \quad \infer{\Gamma \vdash c.i :: k_i}{
adamc@530 312 \Gamma \vdash c :: (k_1 \times \ldots \times k_n)
adamc@530 313 }$$
adamc@530 314
adamc@530 315 $$\infer{\Gamma \vdash \lambda [c_1 \sim c_2] \Rightarrow c :: \kappa}{
adamc@530 316 \Gamma \vdash c_1 :: \{\kappa'\}
adamc@530 317 & \Gamma \vdash c_2 :: \{\kappa'\}
adamc@530 318 & \Gamma, c_1 \sim c_2 \vdash c :: \kappa
adamc@530 319 }$$
adamc@530 320
adamc@531 321 \subsection{Record Disjointness}
adamc@531 322
adamc@531 323 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 324
adamc@531 325 $$\infer{\Gamma \vdash c_1 \sim c_2}{
adamc@531 326 \Gamma \vdash c_1 \hookrightarrow c'_1
adamc@531 327 & \Gamma \vdash c_2 \hookrightarrow c'_2
adamc@531 328 & \forall c''_1 \in c'_1, c''_2 \in c'_2: \Gamma \vdash c''_1 \sim c''_2
adamc@531 329 }
adamc@531 330 \quad \infer{\Gamma \vdash X \sim X'}{
adamc@531 331 X \neq X'
adamc@531 332 }$$
adamc@531 333
adamc@531 334 $$\infer{\Gamma \vdash c_1 \sim c_2}{
adamc@531 335 c'_1 \sim c'_2 \in \Gamma
adamc@531 336 & \Gamma \vdash c'_1 \hookrightarrow c''_1
adamc@531 337 & \Gamma \vdash c'_2 \hookrightarrow c''_2
adamc@531 338 & c_1 \in c''_1
adamc@531 339 & c_2 \in c''_2
adamc@531 340 }$$
adamc@531 341
adamc@531 342 $$\infer{\Gamma \vdash c \hookrightarrow \{c\}}{}
adamc@531 343 \quad \infer{\Gamma \vdash [\overline{c = c'}] \hookrightarrow \{\overline{c}\}}{}
adamc@531 344 \quad \infer{\Gamma \vdash c_1 \rc c_2 \hookrightarrow C_1 \cup C_2}{
adamc@531 345 \Gamma \vdash c_1 \hookrightarrow C_1
adamc@531 346 & \Gamma \vdash c_2 \hookrightarrow C_2
adamc@531 347 }
adamc@531 348 \quad \infer{\Gamma \vdash c \hookrightarrow C}{
adamc@531 349 \Gamma \vdash c \equiv c'
adamc@531 350 & \Gamma \vdash c' \hookrightarrow C
adamc@531 351 }
adamc@531 352 \quad \infer{\Gamma \vdash \mt{map} \; f \; c \hookrightarrow C}{
adamc@531 353 \Gamma \vdash c \hookrightarrow C
adamc@531 354 }$$
adamc@531 355
adamc@532 356 \subsection{Definitional Equality}
adamc@532 357
adamc@532 358 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 359
adamc@532 360 $$\infer{\Gamma \vdash c \equiv c}{}
adamc@532 361 \quad \infer{\Gamma \vdash c_1 \equiv c_2}{
adamc@532 362 \Gamma \vdash c_2 \equiv c_1
adamc@532 363 }
adamc@532 364 \quad \infer{\Gamma \vdash c_1 \equiv c_3}{
adamc@532 365 \Gamma \vdash c_1 \equiv c_2
adamc@532 366 & \Gamma \vdash c_2 \equiv c_3
adamc@532 367 }
adamc@532 368 \quad \infer{\Gamma \vdash \mathcal C[c_1] \equiv \mathcal C[c_2]}{
adamc@532 369 \Gamma \vdash c_1 \equiv c_2
adamc@532 370 }$$
adamc@532 371
adamc@532 372 $$\infer{\Gamma \vdash x \equiv c}{
adamc@532 373 x :: \kappa = c \in \Gamma
adamc@532 374 }
adamc@532 375 \quad \infer{\Gamma \vdash M.x \equiv c}{
adamc@532 376 \Gamma \vdash M : S
adamc@532 377 & \mt{proj}(M, S, \mt{con} \; x) = (\kappa, c)
adamc@532 378 }
adamc@532 379 \quad \infer{\Gamma \vdash (\overline c).i \equiv c_i}{}$$
adamc@532 380
adamc@532 381 $$\infer{\Gamma \vdash (\lambda x :: \kappa \Rightarrow c) \; c' \equiv [x \mapsto c'] c}{}
adamc@532 382 \quad \infer{\Gamma \vdash c_1 \rc c_2 \equiv c_2 \rc c_1}{}
adamc@532 383 \quad \infer{\Gamma \vdash c_1 \rc (c_2 \rc c_3) \equiv (c_1 \rc c_2) \rc c_3}{}$$
adamc@532 384
adamc@532 385 $$\infer{\Gamma \vdash [] \rc c \equiv c}{}
adamc@532 386 \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 387
adamc@532 388 $$\infer{\Gamma \vdash \lambda [c_1 \sim c_2] \Rightarrow c \equiv c}{
adamc@532 389 \Gamma \vdash c_1 \sim c_2
adamc@532 390 }
adamc@532 391 \quad \infer{\Gamma \vdash \mt{fold} \; f \; i \; [] \equiv i}{}
adamc@532 392 \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 393
adamc@532 394 $$\infer{\Gamma \vdash \mt{map} \; (\lambda x \Rightarrow x) \; c \equiv c}{}
adamc@532 395 \quad \infer{\Gamma \vdash \mt{fold} \; f \; i \; (\mt{map} \; f' \; c)
adamc@532 396 \equiv \mt{fold} \; (\lambda (x_1 :: \mt{Name}) (x_2 :: \kappa) \Rightarrow f \; x_1 \; (f' \; x_2)) \; i \; c}{}$$
adamc@532 397
adamc@532 398 $$\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 399
adamc@533 400 \subsection{Typing}
adamc@533 401
adamc@533 402 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 403
adamc@533 404 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 405
adamc@533 406 $$\infer{\Gamma \vdash e : \tau : \tau}{
adamc@533 407 \Gamma \vdash e : \tau
adamc@533 408 }
adamc@533 409 \quad \infer{\Gamma \vdash e : \tau}{
adamc@533 410 \Gamma \vdash e : \tau'
adamc@533 411 & \Gamma \vdash \tau' \equiv \tau
adamc@533 412 }
adamc@533 413 \quad \infer{\Gamma \vdash \ell : T(\ell)}{}$$
adamc@533 414
adamc@533 415 $$\infer{\Gamma \vdash x : \mathcal I(\tau)}{
adamc@533 416 x : \tau \in \Gamma
adamc@533 417 }
adamc@533 418 \quad \infer{\Gamma \vdash M.x : \mathcal I(\tau)}{
adamc@533 419 \Gamma \vdash M : S
adamc@533 420 & \mt{proj}(M, S, \mt{val} \; x) = \tau
adamc@533 421 }
adamc@533 422 \quad \infer{\Gamma \vdash X : \mathcal I(\tau)}{
adamc@533 423 X : \tau \in \Gamma
adamc@533 424 }
adamc@533 425 \quad \infer{\Gamma \vdash M.X : \mathcal I(\tau)}{
adamc@533 426 \Gamma \vdash M : S
adamc@533 427 & \mt{proj}(M, S, \mt{val} \; X) = \tau
adamc@533 428 }$$
adamc@533 429
adamc@533 430 $$\infer{\Gamma \vdash e_1 \; e_2 : \tau_2}{
adamc@533 431 \Gamma \vdash e_1 : \tau_1 \to \tau_2
adamc@533 432 & \Gamma \vdash e_2 : \tau_1
adamc@533 433 }
adamc@533 434 \quad \infer{\Gamma \vdash \lambda x : \tau_1 \Rightarrow e : \tau_1 \to \tau_2}{
adamc@533 435 \Gamma, x : \tau_1 \vdash e : \tau_2
adamc@533 436 }$$
adamc@533 437
adamc@533 438 $$\infer{\Gamma \vdash e [c] : [x \mapsto c]\tau}{
adamc@533 439 \Gamma \vdash e : x :: \kappa \to \tau
adamc@533 440 & \Gamma \vdash c :: \kappa
adamc@533 441 }
adamc@533 442 \quad \infer{\Gamma \vdash \lambda x \; ? \; \kappa \Rightarrow e : x \; ? \; \kappa \to \tau}{
adamc@533 443 \Gamma, x :: \kappa \vdash e : \tau
adamc@533 444 }$$
adamc@533 445
adamc@533 446 $$\infer{\Gamma \vdash \{\overline{c = e}\} : \{\overline{c : \tau}\}}{
adamc@533 447 \forall i: \Gamma \vdash c_i :: \mt{Name}
adamc@533 448 & \Gamma \vdash e_i : \tau_i
adamc@533 449 & \forall i \neq j: \Gamma \vdash c_i \sim c_j
adamc@533 450 }
adamc@533 451 \quad \infer{\Gamma \vdash e.c : \tau}{
adamc@533 452 \Gamma \vdash e : \$([c = \tau] \rc c')
adamc@533 453 }
adamc@533 454 \quad \infer{\Gamma \vdash e_1 \rc e_2 : \$(c_1 \rc c_2)}{
adamc@533 455 \Gamma \vdash e_1 : \$c_1
adamc@533 456 & \Gamma \vdash e_2 : \$c_2
adamc@533 457 }$$
adamc@533 458
adamc@533 459 $$\infer{\Gamma \vdash e \rcut c : \$c'}{
adamc@533 460 \Gamma \vdash e : \$([c = \tau] \rc c')
adamc@533 461 }
adamc@533 462 \quad \infer{\Gamma \vdash e \rcutM c : \$c'}{
adamc@533 463 \Gamma \vdash e : \$(c \rc c')
adamc@533 464 }$$
adamc@533 465
adamc@533 466 $$\infer{\Gamma \vdash \mt{fold} : \begin{array}{c}
adamc@533 467 x_1 :: (\{\kappa\} \to \tau)
adamc@533 468 \to (x_2 :: \mt{Name} \to x_3 :: \kappa \to x_4 :: \{\kappa\} \to \lambda [[x_2] \sim x_4]
adamc@533 469 \Rightarrow x_1 \; x_4 \to x_1 \; ([x_2 = x_3] \rc x_4)) \\
adamc@533 470 \to x_1 \; [] \to x_5 :: \{\kappa\} \to x_1 \; x_5
adamc@533 471 \end{array}}{}$$
adamc@533 472
adamc@533 473 $$\infer{\Gamma \vdash \mt{let} \; \overline{ed} \; \mt{in} \; e \; \mt{end} : \tau}{
adamc@533 474 \Gamma \vdash \overline{ed} \leadsto \Gamma'
adamc@533 475 & \Gamma' \vdash e : \tau
adamc@533 476 }
adamc@533 477 \quad \infer{\Gamma \vdash \mt{case} \; e \; \mt{of} \; \overline{p \Rightarrow e} : \tau}{
adamc@533 478 \forall i: \Gamma \vdash p_i \leadsto \Gamma_i, \tau'
adamc@533 479 & \Gamma_i \vdash e_i : \tau
adamc@533 480 }$$
adamc@533 481
adamc@533 482 $$\infer{\Gamma \vdash [c_1 \sim c_2] \Rightarrow e : [c_1 \sim c_2] \Rightarrow \tau}{
adamc@533 483 \Gamma \vdash c_1 :: \{\kappa\}
adamc@533 484 & \Gamma \vdash c_2 :: \{\kappa\}
adamc@533 485 & \Gamma, c_1 \sim c_2 \vdash e : \tau
adamc@533 486 }$$
adamc@533 487
adamc@524 488 \end{document}