annotate doc/manual.tex @ 538:a9fba52dfce4

Module typing
author Adam Chlipala <adamc@hcoop.net>
date Sat, 29 Nov 2008 14:09:43 -0500
parents a4a7cd341a1b
children e6b464e48c00
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@535 184 &&& \mt{cookie} \; x : \tau & \textrm{HTTP cookie} \\
adamc@528 185 &&& \mt{class} \; x = c & \textrm{concrete type class} \\
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@534 246 \item $\Gamma \vdash p \leadsto \Gamma; \tau$ combines typing of patterns with calculation of which new variables they bind.
adamc@537 247 \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 248 \item $\Gamma \vdash S \equiv S$ is the signature equivalence judgment.
adamc@536 249 \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 250 \item $\Gamma \vdash M : S$ is the module signature checking judgment.
adamc@537 251 \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@530 252 \end{itemize}
adamc@530 253
adamc@530 254 \subsection{Kinding}
adamc@530 255
adamc@530 256 $$\infer{\Gamma \vdash (c) :: \kappa :: \kappa}{
adamc@530 257 \Gamma \vdash c :: \kappa
adamc@530 258 }
adamc@530 259 \quad \infer{\Gamma \vdash x :: \kappa}{
adamc@530 260 x :: \kappa \in \Gamma
adamc@530 261 }
adamc@530 262 \quad \infer{\Gamma \vdash x :: \kappa}{
adamc@530 263 x :: \kappa = c \in \Gamma
adamc@530 264 }$$
adamc@530 265
adamc@530 266 $$\infer{\Gamma \vdash M.x :: \kappa}{
adamc@537 267 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 268 & \mt{proj}(M, \overline{s}, \mt{con} \; x) = \kappa
adamc@530 269 }
adamc@530 270 \quad \infer{\Gamma \vdash M.x :: \kappa}{
adamc@537 271 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 272 & \mt{proj}(M, \overline{s}, \mt{con} \; x) = (\kappa, c)
adamc@530 273 }$$
adamc@530 274
adamc@530 275 $$\infer{\Gamma \vdash \tau_1 \to \tau_2 :: \mt{Type}}{
adamc@530 276 \Gamma \vdash \tau_1 :: \mt{Type}
adamc@530 277 & \Gamma \vdash \tau_2 :: \mt{Type}
adamc@530 278 }
adamc@530 279 \quad \infer{\Gamma \vdash x \; ? \: \kappa \to \tau :: \mt{Type}}{
adamc@530 280 \Gamma, x :: \kappa \vdash \tau :: \mt{Type}
adamc@530 281 }
adamc@530 282 \quad \infer{\Gamma \vdash \$c :: \mt{Type}}{
adamc@530 283 \Gamma \vdash c :: \{\mt{Type}\}
adamc@530 284 }$$
adamc@530 285
adamc@530 286 $$\infer{\Gamma \vdash c_1 \; c_2 :: \kappa_2}{
adamc@530 287 \Gamma \vdash c_1 :: \kappa_1 \to \kappa_2
adamc@530 288 & \Gamma \vdash c_2 :: \kappa_1
adamc@530 289 }
adamc@530 290 \quad \infer{\Gamma \vdash \lambda x \; :: \; \kappa_1 \Rightarrow c :: \kappa_1 \to \kappa_2}{
adamc@530 291 \Gamma, x :: \kappa_1 \vdash c :: \kappa_2
adamc@530 292 }$$
adamc@530 293
adamc@530 294 $$\infer{\Gamma \vdash () :: \mt{Unit}}{}
adamc@530 295 \quad \infer{\Gamma \vdash \#X :: \mt{Name}}{}$$
adamc@530 296
adamc@530 297 $$\infer{\Gamma \vdash [\overline{c_i = c'_i}] :: \{\kappa\}}{
adamc@530 298 \forall i: \Gamma \vdash c_i : \mt{Name}
adamc@530 299 & \Gamma \vdash c'_i :: \kappa
adamc@530 300 & \forall i \neq j: \Gamma \vdash c_i \sim c_j
adamc@530 301 }
adamc@530 302 \quad \infer{\Gamma \vdash c_1 \rc c_2 :: \{\kappa\}}{
adamc@530 303 \Gamma \vdash c_1 :: \{\kappa\}
adamc@530 304 & \Gamma \vdash c_2 :: \{\kappa\}
adamc@530 305 & \Gamma \vdash c_1 \sim c_2
adamc@530 306 }$$
adamc@530 307
adamc@530 308 $$\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 309
adamc@530 310 $$\infer{\Gamma \vdash (\overline c) :: (k_1 \times \ldots \times k_n)}{
adamc@530 311 \forall i: \Gamma \vdash c_i :: k_i
adamc@530 312 }
adamc@530 313 \quad \infer{\Gamma \vdash c.i :: k_i}{
adamc@530 314 \Gamma \vdash c :: (k_1 \times \ldots \times k_n)
adamc@530 315 }$$
adamc@530 316
adamc@530 317 $$\infer{\Gamma \vdash \lambda [c_1 \sim c_2] \Rightarrow c :: \kappa}{
adamc@530 318 \Gamma \vdash c_1 :: \{\kappa'\}
adamc@530 319 & \Gamma \vdash c_2 :: \{\kappa'\}
adamc@530 320 & \Gamma, c_1 \sim c_2 \vdash c :: \kappa
adamc@530 321 }$$
adamc@530 322
adamc@531 323 \subsection{Record Disjointness}
adamc@531 324
adamc@531 325 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 326
adamc@531 327 $$\infer{\Gamma \vdash c_1 \sim c_2}{
adamc@531 328 \Gamma \vdash c_1 \hookrightarrow c'_1
adamc@531 329 & \Gamma \vdash c_2 \hookrightarrow c'_2
adamc@531 330 & \forall c''_1 \in c'_1, c''_2 \in c'_2: \Gamma \vdash c''_1 \sim c''_2
adamc@531 331 }
adamc@531 332 \quad \infer{\Gamma \vdash X \sim X'}{
adamc@531 333 X \neq X'
adamc@531 334 }$$
adamc@531 335
adamc@531 336 $$\infer{\Gamma \vdash c_1 \sim c_2}{
adamc@531 337 c'_1 \sim c'_2 \in \Gamma
adamc@531 338 & \Gamma \vdash c'_1 \hookrightarrow c''_1
adamc@531 339 & \Gamma \vdash c'_2 \hookrightarrow c''_2
adamc@531 340 & c_1 \in c''_1
adamc@531 341 & c_2 \in c''_2
adamc@531 342 }$$
adamc@531 343
adamc@531 344 $$\infer{\Gamma \vdash c \hookrightarrow \{c\}}{}
adamc@531 345 \quad \infer{\Gamma \vdash [\overline{c = c'}] \hookrightarrow \{\overline{c}\}}{}
adamc@531 346 \quad \infer{\Gamma \vdash c_1 \rc c_2 \hookrightarrow C_1 \cup C_2}{
adamc@531 347 \Gamma \vdash c_1 \hookrightarrow C_1
adamc@531 348 & \Gamma \vdash c_2 \hookrightarrow C_2
adamc@531 349 }
adamc@531 350 \quad \infer{\Gamma \vdash c \hookrightarrow C}{
adamc@531 351 \Gamma \vdash c \equiv c'
adamc@531 352 & \Gamma \vdash c' \hookrightarrow C
adamc@531 353 }
adamc@531 354 \quad \infer{\Gamma \vdash \mt{map} \; f \; c \hookrightarrow C}{
adamc@531 355 \Gamma \vdash c \hookrightarrow C
adamc@531 356 }$$
adamc@531 357
adamc@532 358 \subsection{Definitional Equality}
adamc@532 359
adamc@532 360 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 361
adamc@532 362 $$\infer{\Gamma \vdash c \equiv c}{}
adamc@532 363 \quad \infer{\Gamma \vdash c_1 \equiv c_2}{
adamc@532 364 \Gamma \vdash c_2 \equiv c_1
adamc@532 365 }
adamc@532 366 \quad \infer{\Gamma \vdash c_1 \equiv c_3}{
adamc@532 367 \Gamma \vdash c_1 \equiv c_2
adamc@532 368 & \Gamma \vdash c_2 \equiv c_3
adamc@532 369 }
adamc@532 370 \quad \infer{\Gamma \vdash \mathcal C[c_1] \equiv \mathcal C[c_2]}{
adamc@532 371 \Gamma \vdash c_1 \equiv c_2
adamc@532 372 }$$
adamc@532 373
adamc@532 374 $$\infer{\Gamma \vdash x \equiv c}{
adamc@532 375 x :: \kappa = c \in \Gamma
adamc@532 376 }
adamc@532 377 \quad \infer{\Gamma \vdash M.x \equiv c}{
adamc@537 378 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 379 & \mt{proj}(M, \overline{s}, \mt{con} \; x) = (\kappa, c)
adamc@532 380 }
adamc@532 381 \quad \infer{\Gamma \vdash (\overline c).i \equiv c_i}{}$$
adamc@532 382
adamc@532 383 $$\infer{\Gamma \vdash (\lambda x :: \kappa \Rightarrow c) \; c' \equiv [x \mapsto c'] c}{}
adamc@532 384 \quad \infer{\Gamma \vdash c_1 \rc c_2 \equiv c_2 \rc c_1}{}
adamc@532 385 \quad \infer{\Gamma \vdash c_1 \rc (c_2 \rc c_3) \equiv (c_1 \rc c_2) \rc c_3}{}$$
adamc@532 386
adamc@532 387 $$\infer{\Gamma \vdash [] \rc c \equiv c}{}
adamc@532 388 \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 389
adamc@532 390 $$\infer{\Gamma \vdash \lambda [c_1 \sim c_2] \Rightarrow c \equiv c}{
adamc@532 391 \Gamma \vdash c_1 \sim c_2
adamc@532 392 }
adamc@532 393 \quad \infer{\Gamma \vdash \mt{fold} \; f \; i \; [] \equiv i}{}
adamc@532 394 \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 395
adamc@532 396 $$\infer{\Gamma \vdash \mt{map} \; (\lambda x \Rightarrow x) \; c \equiv c}{}
adamc@532 397 \quad \infer{\Gamma \vdash \mt{fold} \; f \; i \; (\mt{map} \; f' \; c)
adamc@532 398 \equiv \mt{fold} \; (\lambda (x_1 :: \mt{Name}) (x_2 :: \kappa) \Rightarrow f \; x_1 \; (f' \; x_2)) \; i \; c}{}$$
adamc@532 399
adamc@532 400 $$\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 401
adamc@534 402 \subsection{Expression Typing}
adamc@533 403
adamc@533 404 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 405
adamc@533 406 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 407
adamc@533 408 $$\infer{\Gamma \vdash e : \tau : \tau}{
adamc@533 409 \Gamma \vdash e : \tau
adamc@533 410 }
adamc@533 411 \quad \infer{\Gamma \vdash e : \tau}{
adamc@533 412 \Gamma \vdash e : \tau'
adamc@533 413 & \Gamma \vdash \tau' \equiv \tau
adamc@533 414 }
adamc@533 415 \quad \infer{\Gamma \vdash \ell : T(\ell)}{}$$
adamc@533 416
adamc@533 417 $$\infer{\Gamma \vdash x : \mathcal I(\tau)}{
adamc@533 418 x : \tau \in \Gamma
adamc@533 419 }
adamc@533 420 \quad \infer{\Gamma \vdash M.x : \mathcal I(\tau)}{
adamc@537 421 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 422 & \mt{proj}(M, \overline{s}, \mt{val} \; x) = \tau
adamc@533 423 }
adamc@533 424 \quad \infer{\Gamma \vdash X : \mathcal I(\tau)}{
adamc@533 425 X : \tau \in \Gamma
adamc@533 426 }
adamc@533 427 \quad \infer{\Gamma \vdash M.X : \mathcal I(\tau)}{
adamc@537 428 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 429 & \mt{proj}(M, \overline{s}, \mt{val} \; X) = \tau
adamc@533 430 }$$
adamc@533 431
adamc@533 432 $$\infer{\Gamma \vdash e_1 \; e_2 : \tau_2}{
adamc@533 433 \Gamma \vdash e_1 : \tau_1 \to \tau_2
adamc@533 434 & \Gamma \vdash e_2 : \tau_1
adamc@533 435 }
adamc@533 436 \quad \infer{\Gamma \vdash \lambda x : \tau_1 \Rightarrow e : \tau_1 \to \tau_2}{
adamc@533 437 \Gamma, x : \tau_1 \vdash e : \tau_2
adamc@533 438 }$$
adamc@533 439
adamc@533 440 $$\infer{\Gamma \vdash e [c] : [x \mapsto c]\tau}{
adamc@533 441 \Gamma \vdash e : x :: \kappa \to \tau
adamc@533 442 & \Gamma \vdash c :: \kappa
adamc@533 443 }
adamc@533 444 \quad \infer{\Gamma \vdash \lambda x \; ? \; \kappa \Rightarrow e : x \; ? \; \kappa \to \tau}{
adamc@533 445 \Gamma, x :: \kappa \vdash e : \tau
adamc@533 446 }$$
adamc@533 447
adamc@533 448 $$\infer{\Gamma \vdash \{\overline{c = e}\} : \{\overline{c : \tau}\}}{
adamc@533 449 \forall i: \Gamma \vdash c_i :: \mt{Name}
adamc@533 450 & \Gamma \vdash e_i : \tau_i
adamc@533 451 & \forall i \neq j: \Gamma \vdash c_i \sim c_j
adamc@533 452 }
adamc@533 453 \quad \infer{\Gamma \vdash e.c : \tau}{
adamc@533 454 \Gamma \vdash e : \$([c = \tau] \rc c')
adamc@533 455 }
adamc@533 456 \quad \infer{\Gamma \vdash e_1 \rc e_2 : \$(c_1 \rc c_2)}{
adamc@533 457 \Gamma \vdash e_1 : \$c_1
adamc@533 458 & \Gamma \vdash e_2 : \$c_2
adamc@533 459 }$$
adamc@533 460
adamc@533 461 $$\infer{\Gamma \vdash e \rcut c : \$c'}{
adamc@533 462 \Gamma \vdash e : \$([c = \tau] \rc c')
adamc@533 463 }
adamc@533 464 \quad \infer{\Gamma \vdash e \rcutM c : \$c'}{
adamc@533 465 \Gamma \vdash e : \$(c \rc c')
adamc@533 466 }$$
adamc@533 467
adamc@533 468 $$\infer{\Gamma \vdash \mt{fold} : \begin{array}{c}
adamc@533 469 x_1 :: (\{\kappa\} \to \tau)
adamc@533 470 \to (x_2 :: \mt{Name} \to x_3 :: \kappa \to x_4 :: \{\kappa\} \to \lambda [[x_2] \sim x_4]
adamc@533 471 \Rightarrow x_1 \; x_4 \to x_1 \; ([x_2 = x_3] \rc x_4)) \\
adamc@533 472 \to x_1 \; [] \to x_5 :: \{\kappa\} \to x_1 \; x_5
adamc@533 473 \end{array}}{}$$
adamc@533 474
adamc@533 475 $$\infer{\Gamma \vdash \mt{let} \; \overline{ed} \; \mt{in} \; e \; \mt{end} : \tau}{
adamc@533 476 \Gamma \vdash \overline{ed} \leadsto \Gamma'
adamc@533 477 & \Gamma' \vdash e : \tau
adamc@533 478 }
adamc@533 479 \quad \infer{\Gamma \vdash \mt{case} \; e \; \mt{of} \; \overline{p \Rightarrow e} : \tau}{
adamc@533 480 \forall i: \Gamma \vdash p_i \leadsto \Gamma_i, \tau'
adamc@533 481 & \Gamma_i \vdash e_i : \tau
adamc@533 482 }$$
adamc@533 483
adamc@533 484 $$\infer{\Gamma \vdash [c_1 \sim c_2] \Rightarrow e : [c_1 \sim c_2] \Rightarrow \tau}{
adamc@533 485 \Gamma \vdash c_1 :: \{\kappa\}
adamc@533 486 & \Gamma \vdash c_2 :: \{\kappa\}
adamc@533 487 & \Gamma, c_1 \sim c_2 \vdash e : \tau
adamc@533 488 }$$
adamc@533 489
adamc@534 490 \subsection{Pattern Typing}
adamc@534 491
adamc@534 492 $$\infer{\Gamma \vdash \_ \leadsto \Gamma; \tau}{}
adamc@534 493 \quad \infer{\Gamma \vdash x \leadsto \Gamma, x : \tau; \tau}{}
adamc@534 494 \quad \infer{\Gamma \vdash \ell \leadsto \Gamma; T(\ell)}{}$$
adamc@534 495
adamc@534 496 $$\infer{\Gamma \vdash X \leadsto \Gamma; \overline{[x_i \mapsto \tau'_i]}\tau}{
adamc@534 497 X : \overline{x ::: \mt{Type}} \to \tau \in \Gamma
adamc@534 498 & \textrm{$\tau$ not a function type}
adamc@534 499 }
adamc@534 500 \quad \infer{\Gamma \vdash X \; p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau}{
adamc@534 501 X : \overline{x ::: \mt{Type}} \to \tau'' \to \tau \in \Gamma
adamc@534 502 & \Gamma \vdash p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau''
adamc@534 503 }$$
adamc@534 504
adamc@534 505 $$\infer{\Gamma \vdash M.X \leadsto \Gamma; \overline{[x_i \mapsto \tau'_i]}\tau}{
adamc@537 506 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 507 & \mt{proj}(M, \overline{s}, \mt{val} \; X) = \overline{x ::: \mt{Type}} \to \tau
adamc@534 508 & \textrm{$\tau$ not a function type}
adamc@534 509 }$$
adamc@534 510
adamc@534 511 $$\infer{\Gamma \vdash M.X \; p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau}{
adamc@537 512 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 513 & \mt{proj}(M, \overline{s}, \mt{val} \; X) = \overline{x ::: \mt{Type}} \to \tau'' \to \tau
adamc@534 514 & \Gamma \vdash p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau''
adamc@534 515 }$$
adamc@534 516
adamc@534 517 $$\infer{\Gamma \vdash \{\overline{x = p}\} \leadsto \Gamma_n; \{\overline{x = \tau}\}}{
adamc@534 518 \Gamma_0 = \Gamma
adamc@534 519 & \forall i: \Gamma_i \vdash p_i \leadsto \Gamma_{i+1}; \tau_i
adamc@534 520 }
adamc@534 521 \quad \infer{\Gamma \vdash \{\overline{x = p}, \ldots\} \leadsto \Gamma_n; \$([\overline{x = \tau}] \rc c)}{
adamc@534 522 \Gamma_0 = \Gamma
adamc@534 523 & \forall i: \Gamma_i \vdash p_i \leadsto \Gamma_{i+1}; \tau_i
adamc@534 524 }$$
adamc@534 525
adamc@535 526 \subsection{Declaration Typing}
adamc@535 527
adamc@535 528 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 529
adamc@535 530 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. In the compiler, a set of available type classes and their instances is maintained, and these instances are used to fill in expression wildcards.
adamc@535 531
adamc@537 532 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 533
adamc@537 534 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 535
adamc@535 536 $$\infer{\Gamma \vdash \cdot \leadsto \Gamma}{}
adamc@535 537 \quad \infer{\Gamma \vdash d, \overline{d} \leadsto \Gamma''}{
adamc@535 538 \Gamma \vdash d \leadsto \Gamma'
adamc@535 539 & \Gamma' \vdash \overline{d} \leadsto \Gamma''
adamc@535 540 }$$
adamc@535 541
adamc@535 542 $$\infer{\Gamma \vdash \mt{con} \; x :: \kappa = c \leadsto \Gamma, x :: \kappa = c}{
adamc@535 543 \Gamma \vdash c :: \kappa
adamc@535 544 }
adamc@535 545 \quad \infer{\Gamma \vdash \mt{datatype} \; x \; \overline{y} = \overline{dc} \leadsto \Gamma'}{
adamc@535 546 \overline{y}; x; \Gamma, x :: \mt{Type}^{\mt{len}(\overline y)} \to \mt{Type} \vdash \overline{dc} \leadsto \Gamma'
adamc@535 547 }$$
adamc@535 548
adamc@535 549 $$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leadsto \Gamma'}{
adamc@537 550 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 551 & \mt{proj}(M, \overline{s}, \mt{datatype} \; z) = (\overline{y}, \overline{dc})
adamc@535 552 & \overline{y}; x; \Gamma, x :: \mt{Type}^{\mt{len}(\overline y)} \to \mt{Type} = M.z \vdash \overline{dc} \leadsto \Gamma'
adamc@535 553 }$$
adamc@535 554
adamc@535 555 $$\infer{\Gamma \vdash \mt{val} \; x : \tau = e \leadsto \Gamma, x : \tau}{
adamc@535 556 \Gamma \vdash e : \tau
adamc@535 557 }$$
adamc@535 558
adamc@535 559 $$\infer{\Gamma \vdash \mt{val} \; \mt{rec} \; \overline{x : \tau = e} \leadsto \Gamma, \overline{x : \tau}}{
adamc@535 560 \forall i: \Gamma, \overline{x : \tau} \vdash e_i : \tau_i
adamc@535 561 & \textrm{$e_i$ starts with an expression $\lambda$, optionally preceded by constructor and disjointness $\lambda$s}
adamc@535 562 }$$
adamc@535 563
adamc@535 564 $$\infer{\Gamma \vdash \mt{structure} \; X : S = M \leadsto \Gamma, X : S}{
adamc@535 565 \Gamma \vdash M : S
adamc@535 566 }
adamc@537 567 \quad \infer{\Gamma \vdash \mt{signature} \; X = S \leadsto \Gamma, X = S}{
adamc@535 568 \Gamma \vdash S
adamc@535 569 }$$
adamc@535 570
adamc@537 571 $$\infer{\Gamma \vdash \mt{open} \; M \leadsto \Gamma, \mathcal O(M, \overline{s})}{
adamc@537 572 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@535 573 }$$
adamc@535 574
adamc@535 575 $$\infer{\Gamma \vdash \mt{constraint} \; c_1 \sim c_2 \leadsto \Gamma}{
adamc@535 576 \Gamma \vdash c_1 :: \{\kappa\}
adamc@535 577 & \Gamma \vdash c_2 :: \{\kappa\}
adamc@535 578 & \Gamma \vdash c_1 \sim c_2
adamc@535 579 }
adamc@537 580 \quad \infer{\Gamma \vdash \mt{open} \; \mt{constraints} \; M \leadsto \Gamma, \mathcal O_c(M, \overline{s})}{
adamc@537 581 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@535 582 }$$
adamc@535 583
adamc@535 584 $$\infer{\Gamma \vdash \mt{table} \; x : c \leadsto \Gamma, x : \mt{Basis}.\mt{sql\_table} \; c}{
adamc@535 585 \Gamma \vdash c :: \{\mt{Type}\}
adamc@535 586 }
adamc@535 587 \quad \infer{\Gamma \vdash \mt{sequence} \; x \leadsto \Gamma, x : \mt{Basis}.\mt{sql\_sequence}}{}$$
adamc@535 588
adamc@535 589 $$\infer{\Gamma \vdash \mt{cookie} \; x : \tau \leadsto \Gamma, x : \mt{Basis}.\mt{http\_cookie} \; \tau}{
adamc@535 590 \Gamma \vdash \tau :: \mt{Type}
adamc@535 591 }$$
adamc@535 592
adamc@535 593 $$\infer{\Gamma \vdash \mt{class} \; x = c \leadsto \Gamma, x :: \mt{Type} \to \mt{Type} = c}{
adamc@535 594 \Gamma \vdash c :: \mt{Type} \to \mt{Type}
adamc@535 595 }$$
adamc@535 596
adamc@535 597 $$\infer{\overline{y}; x; \Gamma \vdash \cdot \leadsto \Gamma}{}
adamc@535 598 \quad \infer{\overline{y}; x; \Gamma \vdash X \mid \overline{dc} \leadsto \Gamma', X : \overline{y ::: \mt{Type}} \to x \; \overline{y}}{
adamc@535 599 \overline{y}; x; \Gamma \vdash \overline{dc} \leadsto \Gamma'
adamc@535 600 }
adamc@535 601 \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 602 \overline{y}; x; \Gamma \vdash \overline{dc} \leadsto \Gamma'
adamc@535 603 }$$
adamc@535 604
adamc@537 605 \subsection{Signature Item Typing}
adamc@537 606
adamc@537 607 We appeal to a signature item analogue of the $\mathcal O$ function from the last subsection.
adamc@537 608
adamc@537 609 $$\infer{\Gamma \vdash \cdot \leadsto \Gamma}{}
adamc@537 610 \quad \infer{\Gamma \vdash s, \overline{s} \leadsto \Gamma''}{
adamc@537 611 \Gamma \vdash s \leadsto \Gamma'
adamc@537 612 & \Gamma' \vdash \overline{s} \leadsto \Gamma''
adamc@537 613 }$$
adamc@537 614
adamc@537 615 $$\infer{\Gamma \vdash \mt{con} \; x :: \kappa \leadsto \Gamma, x :: \kappa}{}
adamc@537 616 \quad \infer{\Gamma \vdash \mt{con} \; x :: \kappa = c \leadsto \Gamma, x :: \kappa = c}{
adamc@537 617 \Gamma \vdash c :: \kappa
adamc@537 618 }
adamc@537 619 \quad \infer{\Gamma \vdash \mt{datatype} \; x \; \overline{y} = \overline{dc} \leadsto \Gamma'}{
adamc@537 620 \overline{y}; x; \Gamma, x :: \mt{Type}^{\mt{len}(\overline y)} \to \mt{Type} \vdash \overline{dc} \leadsto \Gamma'
adamc@537 621 }$$
adamc@537 622
adamc@537 623 $$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leadsto \Gamma'}{
adamc@537 624 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 625 & \mt{proj}(M, \overline{s}, \mt{datatype} \; z) = (\overline{y}, \overline{dc})
adamc@537 626 & \overline{y}; x; \Gamma, x :: \mt{Type}^{\mt{len}(\overline y)} \to \mt{Type} = M.z \vdash \overline{dc} \leadsto \Gamma'
adamc@537 627 }$$
adamc@537 628
adamc@537 629 $$\infer{\Gamma \vdash \mt{val} \; x : \tau \leadsto \Gamma, x : \tau}{
adamc@537 630 \Gamma \vdash \tau :: \mt{Type}
adamc@537 631 }$$
adamc@537 632
adamc@537 633 $$\infer{\Gamma \vdash \mt{structure} \; X : S \leadsto \Gamma, X : S}{
adamc@537 634 \Gamma \vdash S
adamc@537 635 }
adamc@537 636 \quad \infer{\Gamma \vdash \mt{signature} \; X = S \leadsto \Gamma, X = S}{
adamc@537 637 \Gamma \vdash S
adamc@537 638 }$$
adamc@537 639
adamc@537 640 $$\infer{\Gamma \vdash \mt{include} \; S \leadsto \Gamma, \mathcal O(\overline{s})}{
adamc@537 641 \Gamma \vdash S
adamc@537 642 & \Gamma \vdash S \equiv \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 643 }$$
adamc@537 644
adamc@537 645 $$\infer{\Gamma \vdash \mt{constraint} \; c_1 \sim c_2 \leadsto \Gamma, c_1 \sim c_2}{
adamc@537 646 \Gamma \vdash c_1 :: \{\kappa\}
adamc@537 647 & \Gamma \vdash c_2 :: \{\kappa\}
adamc@537 648 }$$
adamc@537 649
adamc@537 650 $$\infer{\Gamma \vdash \mt{class} \; x = c \leadsto \Gamma, x :: \mt{Type} \to \mt{Type} = c}{
adamc@537 651 \Gamma \vdash c :: \mt{Type} \to \mt{Type}
adamc@537 652 }
adamc@537 653 \quad \infer{\Gamma \vdash \mt{class} \; x \leadsto \Gamma, x :: \mt{Type} \to \mt{Type}}{}$$
adamc@537 654
adamc@536 655 \subsection{Signature Compatibility}
adamc@536 656
adamc@537 657 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 658
adamc@537 659 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 660
adamc@536 661 $$\infer{\Gamma \vdash S \equiv S}{}
adamc@536 662 \quad \infer{\Gamma \vdash S_1 \equiv S_2}{
adamc@536 663 \Gamma \vdash S_2 \equiv S_1
adamc@536 664 }
adamc@536 665 \quad \infer{\Gamma \vdash X \equiv S}{
adamc@536 666 X = S \in \Gamma
adamc@536 667 }
adamc@536 668 \quad \infer{\Gamma \vdash M.X \equiv S}{
adamc@537 669 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 670 & \mt{proj}(M, \overline{s}, \mt{signature} \; X) = S
adamc@536 671 }$$
adamc@536 672
adamc@536 673 $$\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 674 \Gamma \vdash S \equiv \mt{sig} \; \overline{s^1} \; \mt{con} \; x :: \kappa \; \overline{s_2} \; \mt{end}
adamc@536 675 & \Gamma \vdash c :: \kappa
adamc@537 676 }
adamc@537 677 \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 678 \Gamma \vdash S \equiv \mt{sig} \; \overline{s} \; \mt{end}
adamc@536 679 }$$
adamc@536 680
adamc@536 681 $$\infer{\Gamma \vdash S_1 \leq S_2}{
adamc@536 682 \Gamma \vdash S_1 \equiv S_2
adamc@536 683 }
adamc@536 684 \quad \infer{\Gamma \vdash \mt{sig} \; \overline{s} \; \mt{end} \leq \mt{sig} \; \mt{end}}{}
adamc@537 685 \quad \infer{\Gamma \vdash \mt{sig} \; \overline{s} \; \mt{end} \leq \mt{sig} \; s' \; \overline{s'} \; \mt{end}}{
adamc@537 686 \Gamma \vdash \overline{s} \leq s'
adamc@537 687 & \Gamma \vdash s' \leadsto \Gamma'
adamc@537 688 & \Gamma' \vdash \mt{sig} \; \overline{s} \; \mt{end} \leq \mt{sig} \; \overline{s'} \; \mt{end}
adamc@537 689 }$$
adamc@537 690
adamc@537 691 $$\infer{\Gamma \vdash s \; \overline{s} \leq s'}{
adamc@537 692 \Gamma \vdash s \leq s'
adamc@537 693 }
adamc@537 694 \quad \infer{\Gamma \vdash s \; \overline{s} \leq s'}{
adamc@537 695 \Gamma \vdash s \leadsto \Gamma'
adamc@537 696 & \Gamma' \vdash \overline{s} \leq s'
adamc@536 697 }$$
adamc@536 698
adamc@536 699 $$\infer{\Gamma \vdash \mt{functor} (X : S_1) : S_2 \leq \mt{functor} (X : S'_1) : S'_2}{
adamc@536 700 \Gamma \vdash S'_1 \leq S_1
adamc@536 701 & \Gamma, X : S'_1 \vdash S_2 \leq S'_2
adamc@536 702 }$$
adamc@536 703
adamc@537 704 $$\infer{\Gamma \vdash \mt{con} \; x :: \kappa \leq \mt{con} \; x :: \kappa}{}
adamc@537 705 \quad \infer{\Gamma \vdash \mt{con} \; x :: \kappa = c \leq \mt{con} \; x :: \kappa}{}
adamc@537 706 \quad \infer{\Gamma \vdash \mt{datatype} \; x \; \overline{y} = \overline{dc} \leq \mt{con} \; x :: \mt{Type}}{}$$
adamc@537 707
adamc@537 708 $$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leq \mt{con} \; x :: \mt{Type}^{\mt{len}(y)} \to \mt{Type}}{
adamc@537 709 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 710 & \mt{proj}(M, \overline{s}, \mt{datatype} \; z) = (\overline{y}, \overline{dc})
adamc@537 711 }$$
adamc@537 712
adamc@537 713 $$\infer{\Gamma \vdash \mt{class} \; x \leq \mt{con} \; x :: \mt{Type} \to \mt{Type}}{}
adamc@537 714 \quad \infer{\Gamma \vdash \mt{class} \; x = c \leq \mt{con} \; x :: \mt{Type} \to \mt{Type}}{}$$
adamc@537 715
adamc@537 716 $$\infer{\Gamma \vdash \mt{con} \; x :: \kappa = c_1 \leq \mt{con} \; x :: \mt{\kappa} = c_2}{
adamc@537 717 \Gamma \vdash c_1 \equiv c_2
adamc@537 718 }
adamc@537 719 \quad \infer{\Gamma \vdash \mt{class} \; x = c_1 \leq \mt{con} \; x :: \mt{Type} \to \mt{Type} = c_2}{
adamc@537 720 \Gamma \vdash c_1 \equiv c_2
adamc@537 721 }$$
adamc@537 722
adamc@537 723 $$\infer{\Gamma \vdash \mt{datatype} \; x \; \overline{y} = \overline{dc} \leq \mt{datatype} \; x \; \overline{y} = \overline{dc'}}{
adamc@537 724 \Gamma, \overline{y :: \mt{Type}} \vdash \overline{dc} \leq \overline{dc'}
adamc@537 725 }$$
adamc@537 726
adamc@537 727 $$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leq \mt{datatype} \; x \; \overline{y} = \overline{dc'}}{
adamc@537 728 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 729 & \mt{proj}(M, \overline{s}, \mt{datatype} \; z) = (\overline{y}, \overline{dc})
adamc@537 730 & \Gamma, \overline{y :: \mt{Type}} \vdash \overline{dc} \leq \overline{dc'}
adamc@537 731 }$$
adamc@537 732
adamc@537 733 $$\infer{\Gamma \vdash \cdot \leq \cdot}{}
adamc@537 734 \quad \infer{\Gamma \vdash X; \overline{dc} \leq X; \overline{dc'}}{
adamc@537 735 \Gamma \vdash \overline{dc} \leq \overline{dc'}
adamc@537 736 }
adamc@537 737 \quad \infer{\Gamma \vdash X \; \mt{of} \; \tau_1; \overline{dc} \leq X \; \mt{of} \; \tau_2; \overline{dc'}}{
adamc@537 738 \Gamma \vdash \tau_1 \equiv \tau_2
adamc@537 739 & \Gamma \vdash \overline{dc} \leq \overline{dc'}
adamc@537 740 }$$
adamc@537 741
adamc@537 742 $$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leq \mt{datatype} \; x = \mt{datatype} \; M'.z'}{
adamc@537 743 \Gamma \vdash M.z \equiv M'.z'
adamc@537 744 }$$
adamc@537 745
adamc@537 746 $$\infer{\Gamma \vdash \mt{val} \; x : \tau_1 \leq \mt{val} \; x : \tau_2}{
adamc@537 747 \Gamma \vdash \tau_1 \equiv \tau_2
adamc@537 748 }
adamc@537 749 \quad \infer{\Gamma \vdash \mt{structure} \; X : S_1 \leq \mt{structure} \; X : S_2}{
adamc@537 750 \Gamma \vdash S_1 \leq S_2
adamc@537 751 }
adamc@537 752 \quad \infer{\Gamma \vdash \mt{signature} \; X = S_1 \leq \mt{signature} \; X = S_2}{
adamc@537 753 \Gamma \vdash S_1 \leq S_2
adamc@537 754 & \Gamma \vdash S_2 \leq S_1
adamc@537 755 }$$
adamc@537 756
adamc@537 757 $$\infer{\Gamma \vdash \mt{constraint} \; c_1 \sim c_2 \leq \mt{constraint} \; c'_1 \sim c'_2}{
adamc@537 758 \Gamma \vdash c_1 \equiv c'_1
adamc@537 759 & \Gamma \vdash c_2 \equiv c'_2
adamc@537 760 }$$
adamc@537 761
adamc@537 762 $$\infer{\Gamma \vdash \mt{class} \; x \leq \mt{class} \; x}{}
adamc@537 763 \quad \infer{\Gamma \vdash \mt{class} \; x = c \leq \mt{class} \; x}{}
adamc@537 764 \quad \infer{\Gamma \vdash \mt{class} \; x = c_1 \leq \mt{class} \; x = c_2}{
adamc@537 765 \Gamma \vdash c_1 \equiv c_2
adamc@537 766 }$$
adamc@537 767
adamc@538 768 \subsection{Module Typing}
adamc@538 769
adamc@538 770 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 771
adamc@538 772 $$\infer{\Gamma \vdash M : S}{
adamc@538 773 \Gamma \vdash M : S'
adamc@538 774 & \Gamma \vdash S' \leq S
adamc@538 775 }
adamc@538 776 \quad \infer{\Gamma \vdash \mt{struct} \; \overline{d} \; \mt{end} : \mt{sig} \; \mt{sigOf}(\overline{d}) \; \mt{end}}{
adamc@538 777 \Gamma \vdash \overline{d} \leadsto \Gamma'
adamc@538 778 }
adamc@538 779 \quad \infer{\Gamma \vdash X : S}{
adamc@538 780 X : S \in \Gamma
adamc@538 781 }$$
adamc@538 782
adamc@538 783 $$\infer{\Gamma \vdash M.X : S}{
adamc@538 784 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@538 785 & \mt{proj}(M, \overline{s}, \mt{structure} \; X) = S
adamc@538 786 }$$
adamc@538 787
adamc@538 788 $$\infer{\Gamma \vdash M_1(M_2) : [X \mapsto M_2]S_2}{
adamc@538 789 \Gamma \vdash M_1 : \mt{functor}(X : S_1) : S_2
adamc@538 790 & \Gamma \vdash M_2 : S_1
adamc@538 791 }
adamc@538 792 \quad \infer{\Gamma \vdash \mt{functor} (X : S_1) : S_2 = M : \mt{functor} (X : S_1) : S_2}{
adamc@538 793 \Gamma \vdash S_1
adamc@538 794 & \Gamma, X : S_1 \vdash S_2
adamc@538 795 & \Gamma, X : S_1 \vdash M : S_2
adamc@538 796 }$$
adamc@538 797
adamc@538 798 \begin{eqnarray*}
adamc@538 799 \mt{sigOf}(\cdot) &=& \cdot \\
adamc@538 800 \mt{sigOf}(s \; \overline{s'}) &=& \mt{sigOf}(s) \; \mt{sigOf}(\overline{s'}) \\
adamc@538 801 \\
adamc@538 802 \mt{sigOf}(\mt{con} \; x :: \kappa = c) &=& \mt{con} \; x :: \kappa = c \\
adamc@538 803 \mt{sigOf}(\mt{datatype} \; x \; \overline{y} = \overline{dc}) &=& \mt{datatype} \; x \; \overline{y} = \overline{dc} \\
adamc@538 804 \mt{sigOf}(\mt{datatype} \; x = \mt{datatype} \; M.z) &=& \mt{datatype} \; x = \mt{datatype} \; M.z \\
adamc@538 805 \mt{sigOf}(\mt{val} \; x : \tau = e) &=& \mt{val} \; x : \tau \\
adamc@538 806 \mt{sigOf}(\mt{val} \; \mt{rec} \; \overline{x : \tau = e}) &=& \overline{\mt{val} \; x : \tau} \\
adamc@538 807 \mt{sigOf}(\mt{structure} \; X : S = M) &=& \mt{structure} \; X : S \\
adamc@538 808 \mt{sigOf}(\mt{signature} \; X = S) &=& \mt{signature} \; X = S \\
adamc@538 809 \mt{sigOf}(\mt{open} \; M) &=& \mt{include} \; S \textrm{ (where $\Gamma \vdash M : S$)} \\
adamc@538 810 \mt{sigOf}(\mt{constraint} \; c_1 \sim c_2) &=& \mt{constraint} \; c_1 \sim c_2 \\
adamc@538 811 \mt{sigOf}(\mt{open} \; \mt{constraints} \; M) &=& \cdot \\
adamc@538 812 \mt{sigOf}(\mt{table} \; x : c) &=& \mt{table} \; x : c \\
adamc@538 813 \mt{sigOf}(\mt{sequence} \; x) &=& \mt{sequence} \; x \\
adamc@538 814 \mt{sigOf}(\mt{cookie} \; x : \tau) &=& \mt{cookie} \; x : \tau \\
adamc@538 815 \mt{sigOf}(\mt{class} \; x = c) &=& \mt{class} \; x = c \\
adamc@538 816 \end{eqnarray*}
adamc@538 817
adamc@524 818 \end{document}