Mercurial > urweb

annotate doc/manual.tex @ 531:e47eff8c9037

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Disjointness
author Adam Chlipala <adamc@hcoop.net>
date Sat, 29 Nov 2008 09:48:10 -0500
parents c2f9f94ea709
children 23718a4b23d7
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@529 204 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 205
adamc@529 206 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 207
adamc@529 208 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 209
adamc@529 210 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 211
adamc@529 212 A signature item or declaration $\mt{class} \; x = \lambda y :: \mt{Type} \Rightarrow c$ may be abbreviated $\mt{class} \; x \; y = c$.
adamc@529 213
adamc@529 214 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 215
adamc@529 216 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 217
adamc@529 218 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 219
adamc@529 220 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 221
adamc@529 222 A declaration $\mt{table} \; x : \{(c = c,)^*\}$ is elaborated into $\mt{table} \; x : [(c = c,)^*]$
adamc@529 223
adamc@529 224 The syntax $\mt{where} \; \mt{type}$ is an alternate form of $\mt{where} \; \mt{con}$.
adamc@529 225
adamc@529 226 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 227
adamc@529 228 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 229
adamc@529 230 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 231
adamc@530 232
adamc@530 233 \section{Static Semantics}
adamc@530 234
adamc@530 235 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 236
adamc@530 237 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 238 \begin{itemize}
adamc@530 239 \item $\Gamma \vdash c :: \kappa$ assigns a kind to a constructor in a context.
adamc@530 240 \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 241 \item $\Gamma \vdash c \hookrightarrow C$ proves that record constructor $c$ decomposes into set $C$ of field names and record constructors.
adamc@530 242 \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 243 \item $\Gamma \vdash e : \tau$ is a standard typing judgment.
adamc@530 244 \item $\Gamma \vdash M : S$ is the module signature checking judgment.
adamc@530 245 \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 246 \end{itemize}
adamc@530 247
adamc@530 248 \subsection{Kinding}
adamc@530 249
adamc@530 250 $$\infer{\Gamma \vdash (c) :: \kappa :: \kappa}{
adamc@530 251 \Gamma \vdash c :: \kappa
adamc@530 252 }
adamc@530 253 \quad \infer{\Gamma \vdash x :: \kappa}{
adamc@530 254 x :: \kappa \in \Gamma
adamc@530 255 }
adamc@530 256 \quad \infer{\Gamma \vdash x :: \kappa}{
adamc@530 257 x :: \kappa = c \in \Gamma
adamc@530 258 }$$
adamc@530 259
adamc@530 260 $$\infer{\Gamma \vdash M.x :: \kappa}{
adamc@530 261 \Gamma \vdash M : S
adamc@530 262 & \mt{proj}(M, S, \mt{con} \; x) = \kappa
adamc@530 263 }
adamc@530 264 \quad \infer{\Gamma \vdash M.x :: \kappa}{
adamc@530 265 \Gamma \vdash M : S
adamc@530 266 & \mt{proj}(M, S, \mt{con} \; x) = (\kappa, c)
adamc@530 267 }$$
adamc@530 268
adamc@530 269 $$\infer{\Gamma \vdash \tau_1 \to \tau_2 :: \mt{Type}}{
adamc@530 270 \Gamma \vdash \tau_1 :: \mt{Type}
adamc@530 271 & \Gamma \vdash \tau_2 :: \mt{Type}
adamc@530 272 }
adamc@530 273 \quad \infer{\Gamma \vdash x \; ? \: \kappa \to \tau :: \mt{Type}}{
adamc@530 274 \Gamma, x :: \kappa \vdash \tau :: \mt{Type}
adamc@530 275 }
adamc@530 276 \quad \infer{\Gamma \vdash \$c :: \mt{Type}}{
adamc@530 277 \Gamma \vdash c :: \{\mt{Type}\}
adamc@530 278 }$$
adamc@530 279
adamc@530 280 $$\infer{\Gamma \vdash c_1 \; c_2 :: \kappa_2}{
adamc@530 281 \Gamma \vdash c_1 :: \kappa_1 \to \kappa_2
adamc@530 282 & \Gamma \vdash c_2 :: \kappa_1
adamc@530 283 }
adamc@530 284 \quad \infer{\Gamma \vdash \lambda x \; :: \; \kappa_1 \Rightarrow c :: \kappa_1 \to \kappa_2}{
adamc@530 285 \Gamma, x :: \kappa_1 \vdash c :: \kappa_2
adamc@530 286 }$$
adamc@530 287
adamc@530 288 $$\infer{\Gamma \vdash () :: \mt{Unit}}{}
adamc@530 289 \quad \infer{\Gamma \vdash \#X :: \mt{Name}}{}$$
adamc@530 290
adamc@530 291 $$\infer{\Gamma \vdash [\overline{c_i = c'_i}] :: \{\kappa\}}{
adamc@530 292 \forall i: \Gamma \vdash c_i : \mt{Name}
adamc@530 293 & \Gamma \vdash c'_i :: \kappa
adamc@530 294 & \forall i \neq j: \Gamma \vdash c_i \sim c_j
adamc@530 295 }
adamc@530 296 \quad \infer{\Gamma \vdash c_1 \rc c_2 :: \{\kappa\}}{
adamc@530 297 \Gamma \vdash c_1 :: \{\kappa\}
adamc@530 298 & \Gamma \vdash c_2 :: \{\kappa\}
adamc@530 299 & \Gamma \vdash c_1 \sim c_2
adamc@530 300 }$$
adamc@530 301
adamc@530 302 $$\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 303
adamc@530 304 $$\infer{\Gamma \vdash (\overline c) :: (k_1 \times \ldots \times k_n)}{
adamc@530 305 \forall i: \Gamma \vdash c_i :: k_i
adamc@530 306 }
adamc@530 307 \quad \infer{\Gamma \vdash c.i :: k_i}{
adamc@530 308 \Gamma \vdash c :: (k_1 \times \ldots \times k_n)
adamc@530 309 }$$
adamc@530 310
adamc@530 311 $$\infer{\Gamma \vdash \lambda [c_1 \sim c_2] \Rightarrow c :: \kappa}{
adamc@530 312 \Gamma \vdash c_1 :: \{\kappa'\}
adamc@530 313 & \Gamma \vdash c_2 :: \{\kappa'\}
adamc@530 314 & \Gamma, c_1 \sim c_2 \vdash c :: \kappa
adamc@530 315 }$$
adamc@530 316
adamc@531 317 \subsection{Record Disjointness}
adamc@531 318
adamc@531 319 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 320
adamc@531 321 $$\infer{\Gamma \vdash c_1 \sim c_2}{
adamc@531 322 \Gamma \vdash c_1 \hookrightarrow c'_1
adamc@531 323 & \Gamma \vdash c_2 \hookrightarrow c'_2
adamc@531 324 & \forall c''_1 \in c'_1, c''_2 \in c'_2: \Gamma \vdash c''_1 \sim c''_2
adamc@531 325 }
adamc@531 326 \quad \infer{\Gamma \vdash X \sim X'}{
adamc@531 327 X \neq X'
adamc@531 328 }$$
adamc@531 329
adamc@531 330 $$\infer{\Gamma \vdash c_1 \sim c_2}{
adamc@531 331 c'_1 \sim c'_2 \in \Gamma
adamc@531 332 & \Gamma \vdash c'_1 \hookrightarrow c''_1
adamc@531 333 & \Gamma \vdash c'_2 \hookrightarrow c''_2
adamc@531 334 & c_1 \in c''_1
adamc@531 335 & c_2 \in c''_2
adamc@531 336 }$$
adamc@531 337
adamc@531 338 $$\infer{\Gamma \vdash c \hookrightarrow \{c\}}{}
adamc@531 339 \quad \infer{\Gamma \vdash [\overline{c = c'}] \hookrightarrow \{\overline{c}\}}{}
adamc@531 340 \quad \infer{\Gamma \vdash c_1 \rc c_2 \hookrightarrow C_1 \cup C_2}{
adamc@531 341 \Gamma \vdash c_1 \hookrightarrow C_1
adamc@531 342 & \Gamma \vdash c_2 \hookrightarrow C_2
adamc@531 343 }
adamc@531 344 \quad \infer{\Gamma \vdash c \hookrightarrow C}{
adamc@531 345 \Gamma \vdash c \equiv c'
adamc@531 346 & \Gamma \vdash c' \hookrightarrow C
adamc@531 347 }
adamc@531 348 \quad \infer{\Gamma \vdash \mt{map} \; f \; c \hookrightarrow C}{
adamc@531 349 \Gamma \vdash c \hookrightarrow C
adamc@531 350 }$$
adamc@531 351
adamc@531 352
adamc@524 353 \end{document}