annotate doc/manual.tex @ 541:2bf2d0e0fb61

Type inference
author Adam Chlipala <adamc@hcoop.net>
date Sat, 06 Dec 2008 12:01:12 -0500
parents 9eefa0cf3219
children 31482f333362
rev   line source
adamc@524 1 \documentclass{article}
adamc@524 2 \usepackage{fullpage,amsmath,amssymb,proof}
adamc@524 3
adamc@524 4 \newcommand{\cd}[1]{\texttt{#1}}
adamc@524 5 \newcommand{\mt}[1]{\mathsf{#1}}
adamc@524 6
adamc@524 7 \newcommand{\rc}{+ \hspace{-.075in} + \;}
adamc@527 8 \newcommand{\rcut}{\; \texttt{--} \;}
adamc@527 9 \newcommand{\rcutM}{\; \texttt{---} \;}
adamc@524 10
adamc@524 11 \begin{document}
adamc@524 12
adamc@524 13 \title{The Ur/Web Manual}
adamc@524 14 \author{Adam Chlipala}
adamc@524 15
adamc@524 16 \maketitle
adamc@524 17
adamc@540 18 \tableofcontents
adamc@540 19
adamc@529 20 \section{Ur Syntax}
adamc@529 21
adamc@529 22 In this section, we describe the syntax of Ur, deferring to a later section discussion of most of the syntax specific to SQL and XML. The sole exceptions are the declaration forms for tables, sequences, and cookies.
adamc@524 23
adamc@524 24 \subsection{Lexical Conventions}
adamc@524 25
adamc@524 26 We give the Ur language definition in \LaTeX $\;$ math mode, since that is prettier than monospaced ASCII. The corresponding ASCII syntax can be read off directly. Here is the key for mapping math symbols to ASCII character sequences.
adamc@524 27
adamc@524 28 \begin{center}
adamc@524 29 \begin{tabular}{rl}
adamc@524 30 \textbf{\LaTeX} & \textbf{ASCII} \\
adamc@524 31 $\to$ & \cd{->} \\
adamc@524 32 $\times$ & \cd{*} \\
adamc@524 33 $\lambda$ & \cd{fn} \\
adamc@524 34 $\Rightarrow$ & \cd{=>} \\
adamc@529 35 $\neq$ & \cd{<>} \\
adamc@529 36 $\leq$ & \cd{<=} \\
adamc@529 37 $\geq$ & \cd{>=} \\
adamc@524 38 \\
adamc@524 39 $x$ & Normal textual identifier, not beginning with an uppercase letter \\
adamc@525 40 $X$ & Normal textual identifier, beginning with an uppercase letter \\
adamc@524 41 \end{tabular}
adamc@524 42 \end{center}
adamc@524 43
adamc@525 44 We often write syntax like $e^*$ to indicate zero or more copies of $e$, $e^+$ to indicate one or more copies, and $e,^*$ and $e,^+$ to indicate multiple copies separated by commas. Another separator may be used in place of a comma. The $e$ term may be surrounded by parentheses to indicate grouping; those parentheses should not be included in the actual ASCII.
adamc@524 45
adamc@526 46 We write $\ell$ for literals of the primitive types, for the most part following C conventions. There are $\mt{int}$, $\mt{float}$, and $\mt{string}$ literals.
adamc@526 47
adamc@527 48 This version of the manual doesn't include operator precedences; see \texttt{src/urweb.grm} for that.
adamc@527 49
adamc@524 50 \subsection{Core Syntax}
adamc@524 51
adamc@524 52 \emph{Kinds} classify types and other compile-time-only entities. Each kind in the grammar is listed with a description of the sort of data it classifies.
adamc@524 53 $$\begin{array}{rrcll}
adamc@524 54 \textrm{Kinds} & \kappa &::=& \mt{Type} & \textrm{proper types} \\
adamc@525 55 &&& \mt{Unit} & \textrm{the trivial constructor} \\
adamc@525 56 &&& \mt{Name} & \textrm{field names} \\
adamc@525 57 &&& \kappa \to \kappa & \textrm{type-level functions} \\
adamc@525 58 &&& \{\kappa\} & \textrm{type-level records} \\
adamc@525 59 &&& (\kappa\times^+) & \textrm{type-level tuples} \\
adamc@529 60 &&& \_\_ & \textrm{wildcard} \\
adamc@525 61 &&& (\kappa) & \textrm{explicit precedence} \\
adamc@524 62 \end{array}$$
adamc@524 63
adamc@524 64 Ur supports several different notions of functions that take types as arguments. These arguments can be either implicit, causing them to be inferred at use sites; or explicit, forcing them to be specified manually at use sites. There is a common explicitness annotation convention applied at the definitions of and in the types of such functions.
adamc@524 65 $$\begin{array}{rrcll}
adamc@524 66 \textrm{Explicitness} & ? &::=& :: & \textrm{explicit} \\
adamc@525 67 &&& \; ::: & \textrm{implicit}
adamc@524 68 \end{array}$$
adamc@524 69
adamc@524 70 \emph{Constructors} are the main class of compile-time-only data. They include proper types and are classified by kinds.
adamc@524 71 $$\begin{array}{rrcll}
adamc@524 72 \textrm{Constructors} & c, \tau &::=& (c) :: \kappa & \textrm{kind annotation} \\
adamc@530 73 &&& \hat{x} & \textrm{constructor variable} \\
adamc@524 74 \\
adamc@525 75 &&& \tau \to \tau & \textrm{function type} \\
adamc@525 76 &&& x \; ? \; \kappa \to \tau & \textrm{polymorphic function type} \\
adamc@525 77 &&& \$ c & \textrm{record type} \\
adamc@524 78 \\
adamc@525 79 &&& c \; c & \textrm{type-level function application} \\
adamc@530 80 &&& \lambda x \; :: \; \kappa \Rightarrow c & \textrm{type-level function abstraction} \\
adamc@524 81 \\
adamc@525 82 &&& () & \textrm{type-level unit} \\
adamc@525 83 &&& \#X & \textrm{field name} \\
adamc@524 84 \\
adamc@525 85 &&& [(c = c)^*] & \textrm{known-length type-level record} \\
adamc@525 86 &&& c \rc c & \textrm{type-level record concatenation} \\
adamc@525 87 &&& \mt{fold} & \textrm{type-level record fold} \\
adamc@524 88 \\
adamc@525 89 &&& (c^+) & \textrm{type-level tuple} \\
adamc@525 90 &&& c.n & \textrm{type-level tuple projection ($n \in \mathbb N^+$)} \\
adamc@524 91 \\
adamc@525 92 &&& \lambda [c \sim c] \Rightarrow c & \textrm{guarded constructor} \\
adamc@524 93 \\
adamc@529 94 &&& \_ :: \kappa & \textrm{wildcard} \\
adamc@525 95 &&& (c) & \textrm{explicit precedence} \\
adamc@530 96 \\
adamc@530 97 \textrm{Qualified uncapitalized variables} & \hat{x} &::=& x & \textrm{not from a module} \\
adamc@530 98 &&& M.x & \textrm{projection from a module} \\
adamc@525 99 \end{array}$$
adamc@525 100
adamc@525 101 Modules of the module system are described by \emph{signatures}.
adamc@525 102 $$\begin{array}{rrcll}
adamc@525 103 \textrm{Signatures} & S &::=& \mt{sig} \; s^* \; \mt{end} & \textrm{constant} \\
adamc@525 104 &&& X & \textrm{variable} \\
adamc@525 105 &&& \mt{functor}(X : S) : S & \textrm{functor} \\
adamc@529 106 &&& S \; \mt{where} \; \mt{con} \; x = c & \textrm{concretizing an abstract constructor} \\
adamc@525 107 &&& M.X & \textrm{projection from a module} \\
adamc@525 108 \\
adamc@525 109 \textrm{Signature items} & s &::=& \mt{con} \; x :: \kappa & \textrm{abstract constructor} \\
adamc@525 110 &&& \mt{con} \; x :: \kappa = c & \textrm{concrete constructor} \\
adamc@528 111 &&& \mt{datatype} \; x \; x^* = dc\mid^+ & \textrm{algebraic datatype definition} \\
adamc@529 112 &&& \mt{datatype} \; x = \mt{datatype} \; M.x & \textrm{algebraic datatype import} \\
adamc@525 113 &&& \mt{val} \; x : \tau & \textrm{value} \\
adamc@525 114 &&& \mt{structure} \; X : S & \textrm{sub-module} \\
adamc@525 115 &&& \mt{signature} \; X = S & \textrm{sub-signature} \\
adamc@525 116 &&& \mt{include} \; S & \textrm{signature inclusion} \\
adamc@525 117 &&& \mt{constraint} \; c \sim c & \textrm{record disjointness constraint} \\
adamc@525 118 &&& \mt{class} \; x & \textrm{abstract type class} \\
adamc@525 119 &&& \mt{class} \; x = c & \textrm{concrete type class} \\
adamc@525 120 \\
adamc@525 121 \textrm{Datatype constructors} & dc &::=& X & \textrm{nullary constructor} \\
adamc@525 122 &&& X \; \mt{of} \; \tau & \textrm{unary constructor} \\
adamc@524 123 \end{array}$$
adamc@524 124
adamc@526 125 \emph{Patterns} are used to describe structural conditions on expressions, such that expressions may be tested against patterns, generating assignments to pattern variables if successful.
adamc@526 126 $$\begin{array}{rrcll}
adamc@526 127 \textrm{Patterns} & p &::=& \_ & \textrm{wildcard} \\
adamc@526 128 &&& x & \textrm{variable} \\
adamc@526 129 &&& \ell & \textrm{constant} \\
adamc@526 130 &&& \hat{X} & \textrm{nullary constructor} \\
adamc@526 131 &&& \hat{X} \; p & \textrm{unary constructor} \\
adamc@526 132 &&& \{(x = p,)^*\} & \textrm{rigid record pattern} \\
adamc@526 133 &&& \{(x = p,)^+, \ldots\} & \textrm{flexible record pattern} \\
adamc@527 134 &&& (p) & \textrm{explicit precedence} \\
adamc@526 135 \\
adamc@529 136 \textrm{Qualified capitalized variables} & \hat{X} &::=& X & \textrm{not from a module} \\
adamc@526 137 &&& M.X & \textrm{projection from a module} \\
adamc@526 138 \end{array}$$
adamc@526 139
adamc@527 140 \emph{Expressions} are the main run-time entities, corresponding to both ``expressions'' and ``statements'' in mainstream imperative languages.
adamc@527 141 $$\begin{array}{rrcll}
adamc@527 142 \textrm{Expressions} & e &::=& e : \tau & \textrm{type annotation} \\
adamc@529 143 &&& \hat{x} & \textrm{variable} \\
adamc@529 144 &&& \hat{X} & \textrm{datatype constructor} \\
adamc@527 145 &&& \ell & \textrm{constant} \\
adamc@527 146 \\
adamc@527 147 &&& e \; e & \textrm{function application} \\
adamc@527 148 &&& \lambda x : \tau \Rightarrow e & \textrm{function abstraction} \\
adamc@527 149 &&& e [c] & \textrm{polymorphic function application} \\
adamc@527 150 &&& \lambda x \; ? \; \kappa \Rightarrow e & \textrm{polymorphic function abstraction} \\
adamc@527 151 \\
adamc@527 152 &&& \{(c = e,)^*\} & \textrm{known-length record} \\
adamc@527 153 &&& e.c & \textrm{record field projection} \\
adamc@527 154 &&& e \rc e & \textrm{record concatenation} \\
adamc@527 155 &&& e \rcut c & \textrm{removal of a single record field} \\
adamc@527 156 &&& e \rcutM c & \textrm{removal of multiple record fields} \\
adamc@527 157 &&& \mt{fold} & \textrm{fold over fields of a type-level record} \\
adamc@527 158 \\
adamc@527 159 &&& \mt{let} \; ed^* \; \mt{in} \; e \; \mt{end} & \textrm{local definitions} \\
adamc@527 160 \\
adamc@527 161 &&& \mt{case} \; e \; \mt{of} \; (p \Rightarrow e|)^+ & \textrm{pattern matching} \\
adamc@527 162 \\
adamc@527 163 &&& \lambda [c \sim c] \Rightarrow e & \textrm{guarded expression} \\
adamc@527 164 \\
adamc@527 165 &&& \_ & \textrm{wildcard} \\
adamc@527 166 &&& (e) & \textrm{explicit precedence} \\
adamc@527 167 \\
adamc@527 168 \textrm{Local declarations} & ed &::=& \cd{val} \; x : \tau = e & \textrm{non-recursive value} \\
adamc@527 169 &&& \cd{val} \; \cd{rec} \; (x : \tau = e \; \cd{and})^+ & \textrm{mutually-recursive values} \\
adamc@527 170 \end{array}$$
adamc@527 171
adamc@528 172 \emph{Declarations} primarily bring new symbols into context.
adamc@528 173 $$\begin{array}{rrcll}
adamc@528 174 \textrm{Declarations} & d &::=& \mt{con} \; x :: \kappa = c & \textrm{constructor synonym} \\
adamc@528 175 &&& \mt{datatype} \; x \; x^* = dc\mid^+ & \textrm{algebraic datatype definition} \\
adamc@529 176 &&& \mt{datatype} \; x = \mt{datatype} \; M.x & \textrm{algebraic datatype import} \\
adamc@528 177 &&& \mt{val} \; x : \tau = e & \textrm{value} \\
adamc@528 178 &&& \mt{val} \; \cd{rec} \; (x : \tau = e \; \mt{and})^+ & \textrm{mutually-recursive values} \\
adamc@528 179 &&& \mt{structure} \; X : S = M & \textrm{module definition} \\
adamc@528 180 &&& \mt{signature} \; X = S & \textrm{signature definition} \\
adamc@528 181 &&& \mt{open} \; M & \textrm{module inclusion} \\
adamc@528 182 &&& \mt{constraint} \; c \sim c & \textrm{record disjointness constraint} \\
adamc@528 183 &&& \mt{open} \; \mt{constraints} \; M & \textrm{inclusion of just the constraints from a module} \\
adamc@528 184 &&& \mt{table} \; x : c & \textrm{SQL table} \\
adamc@528 185 &&& \mt{sequence} \; x & \textrm{SQL sequence} \\
adamc@535 186 &&& \mt{cookie} \; x : \tau & \textrm{HTTP cookie} \\
adamc@528 187 &&& \mt{class} \; x = c & \textrm{concrete type class} \\
adamc@528 188 \\
adamc@529 189 \textrm{Modules} & M &::=& \mt{struct} \; d^* \; \mt{end} & \textrm{constant} \\
adamc@529 190 &&& X & \textrm{variable} \\
adamc@529 191 &&& M.X & \textrm{projection} \\
adamc@529 192 &&& M(M) & \textrm{functor application} \\
adamc@529 193 &&& \mt{functor}(X : S) : S = M & \textrm{functor abstraction} \\
adamc@528 194 \end{array}$$
adamc@528 195
adamc@528 196 There are two kinds of Ur files. A file named $M\texttt{.ur}$ is an \emph{implementation file}, and it should contain a sequence of declarations $d^*$. A file named $M\texttt{.urs}$ is an \emph{interface file}; it must always have a matching $M\texttt{.ur}$ and should contain a sequence of signature items $s^*$. When both files are present, the overall effect is the same as a monolithic declaration $\mt{structure} \; M : \mt{sig} \; s^* \; \mt{end} = \mt{struct} \; d^* \; \mt{end}$. When no interface file is included, the overall effect is similar, with a signature for module $M$ being inferred rather than just checked against an interface.
adamc@527 197
adamc@529 198 \subsection{Shorthands}
adamc@529 199
adamc@529 200 There are a variety of derived syntactic forms that elaborate into the core syntax from the last subsection. We will present the additional forms roughly following the order in which we presented the constructs that they elaborate into.
adamc@529 201
adamc@529 202 In many contexts where record fields are expected, like in a projection $e.c$, a constant field may be written as simply $X$, rather than $\#X$.
adamc@529 203
adamc@529 204 A record type may be written $\{(c = c,)^*\}$, which elaborates to $\$[(c = c,)^*]$.
adamc@529 205
adamc@533 206 The notation $[c_1, \ldots, c_n]$ is shorthand for $[c_1 = (), \ldots, c_n = ()]$.
adamc@533 207
adamc@529 208 A tuple type $(\tau_1, \ldots, \tau_n)$ expands to a record type $\{1 = \tau_1, \ldots, n = \tau_n\}$, with natural numbers as field names. A tuple pattern $(p_1, \ldots, p_n)$ expands to a rigid record pattern $\{1 = p_1, \ldots, n = p_n\}$. Positive natural numbers may be used in most places where field names would be allowed.
adamc@529 209
adamc@529 210 In general, several adjacent $\lambda$ forms may be combined into one, and kind and type annotations may be omitted, in which case they are implicitly included as wildcards. More formally, for constructor-level abstractions, we can define a new non-terminal $b ::= x \mid (x :: \kappa) \mid [c \sim c]$ and allow composite abstractions of the form $\lambda b^+ \Rightarrow c$, elaborating into the obvious sequence of one core $\lambda$ per element of $b^+$.
adamc@529 211
adamc@529 212 For any signature item or declaration that defines some entity to be equal to $A$ with classification annotation $B$ (e.g., $\mt{val} \; x : B = A$), $B$ and the preceding colon (or similar punctuation) may be omitted, in which case it is filled in as a wildcard.
adamc@529 213
adamc@529 214 A signature item or declaration $\mt{type} \; x$ or $\mt{type} \; x = \tau$ is elaborated into $\mt{con} \; x :: \mt{Type}$ or $\mt{con} \; x :: \mt{Type} = \tau$, respectively.
adamc@529 215
adamc@529 216 A signature item or declaration $\mt{class} \; x = \lambda y :: \mt{Type} \Rightarrow c$ may be abbreviated $\mt{class} \; x \; y = c$.
adamc@529 217
adamc@529 218 Handling of implicit and explicit constructor arguments may be tweaked with some prefixes to variable references. An expression $@x$ is a version of $x$ where all implicit constructor arguments have been made explicit. An expression $@@x$ achieves the same effect, additionally halting automatic resolution of type class instances. The same syntax works for variables projected out of modules and for capitalized variables (datatype constructors).
adamc@529 219
adamc@529 220 At the expression level, an analogue is available of the composite $\lambda$ form for constructors. We define the language of binders as $b ::= x \mid (x : \tau) \mid (x \; ? \; \kappa) \mid [c \sim c]$. A lone variable $x$ as a binder stands for an expression variable of unspecified type.
adamc@529 221
adamc@529 222 A $\mt{val}$ or $\mt{val} \; \mt{rec}$ declaration may include expression binders before the equal sign, following the binder grammar from the last paragraph. Such declarations are elaborated into versions that add additional $\lambda$s to the fronts of the righthand sides, as appropriate. The keyword $\mt{fun}$ is a synonym for $\mt{val} \; \mt{rec}$.
adamc@529 223
adamc@529 224 A signature item $\mt{functor} \; X_1 \; (X_2 : S_1) : S_2$ is elaborated into $\mt{structure} \; X_1 : \mt{functor}(X_2 : S_1) : S_2$. A declaration $\mt{functor} \; X_1 \; (X_2 : S_1) : S_2 = M$ is elaborated into $\mt{structure} \; X_1 : \mt{functor}(X_2 : S_1) : S_2 = \mt{functor}(X_2 : S_1) : S_2 = M$.
adamc@529 225
adamc@529 226 A declaration $\mt{table} \; x : \{(c = c,)^*\}$ is elaborated into $\mt{table} \; x : [(c = c,)^*]$
adamc@529 227
adamc@529 228 The syntax $\mt{where} \; \mt{type}$ is an alternate form of $\mt{where} \; \mt{con}$.
adamc@529 229
adamc@529 230 The syntax $\mt{if} \; e \; \mt{then} \; e_1 \; \mt{else} \; e_2$ expands to $\mt{case} \; e \; \mt{of} \; \mt{Basis}.\mt{True} \Rightarrow e_1 \mid \mt{Basis}.\mt{False} \Rightarrow e_2$.
adamc@529 231
adamc@529 232 There are infix operator syntaxes for a number of functions defined in the $\mt{Basis}$ module. There is $=$ for $\mt{eq}$, $\neq$ for $\mt{neq}$, $-$ for $\mt{neg}$ (as a prefix operator) and $\mt{minus}$, $+$ for $\mt{plus}$, $\times$ for $\mt{times}$, $/$ for $\mt{div}$, $\%$ for $\mt{mod}$, $<$ for $\mt{lt}$, $\leq$ for $\mt{le}$, $>$ for $\mt{gt}$, and $\geq$ for $\mt{ge}$.
adamc@529 233
adamc@529 234 A signature item $\mt{table} \; x : c$ is shorthand for $\mt{val} \; x : \mt{Basis}.\mt{sql\_table} \; c$. $\mt{sequence} \; x$ is short for $\mt{val} \; x : \mt{Basis}.\mt{sql\_sequence}$, and $\mt{cookie} \; x : \tau$ is shorthand for $\mt{val} \; x : \mt{Basis}.\mt{http\_cookie} \; \tau$.
adamc@529 235
adamc@530 236
adamc@530 237 \section{Static Semantics}
adamc@530 238
adamc@530 239 In this section, we give a declarative presentation of Ur's typing rules and related judgments. Inference is the subject of the next section; here, we assume that an oracle has filled in all wildcards with concrete values.
adamc@530 240
adamc@530 241 Since there is significant mutual recursion among the judgments, we introduce them all before beginning to give rules. We use the same variety of contexts throughout this section, implicitly introducing new sorts of context entries as needed.
adamc@530 242 \begin{itemize}
adamc@530 243 \item $\Gamma \vdash c :: \kappa$ assigns a kind to a constructor in a context.
adamc@530 244 \item $\Gamma \vdash c \sim c$ proves the disjointness of two record constructors; that is, that they share no field names. We overload the judgment to apply to pairs of field names as well.
adamc@531 245 \item $\Gamma \vdash c \hookrightarrow C$ proves that record constructor $c$ decomposes into set $C$ of field names and record constructors.
adamc@530 246 \item $\Gamma \vdash c \equiv c$ proves the computational equivalence of two constructors. This is often called a \emph{definitional equality} in the world of type theory.
adamc@530 247 \item $\Gamma \vdash e : \tau$ is a standard typing judgment.
adamc@534 248 \item $\Gamma \vdash p \leadsto \Gamma; \tau$ combines typing of patterns with calculation of which new variables they bind.
adamc@537 249 \item $\Gamma \vdash d \leadsto \Gamma$ expresses how a declaration modifies a context. We overload this judgment to apply to sequences of declarations, as well as to signature items and sequences of signature items.
adamc@537 250 \item $\Gamma \vdash S \equiv S$ is the signature equivalence judgment.
adamc@536 251 \item $\Gamma \vdash S \leq S$ is the signature compatibility judgment. We write $\Gamma \vdash S$ as shorthand for $\Gamma \vdash S \leq S$.
adamc@530 252 \item $\Gamma \vdash M : S$ is the module signature checking judgment.
adamc@537 253 \item $\mt{proj}(M, \overline{s}, V)$ is a partial function for projecting a signature item from $\overline{s}$, given the module $M$ that we project from. $V$ may be $\mt{con} \; x$, $\mt{datatype} \; x$, $\mt{val} \; x$, $\mt{signature} \; X$, or $\mt{structure} \; X$. The parameter $M$ is needed because the projected signature item may refer to other items from $\overline{s}$.
adamc@539 254 \item $\mt{selfify}(M, \overline{s})$ adds information to signature items $\overline{s}$ to reflect the fact that we are concerned with the particular module $M$. This function is overloaded to work over individual signature items as well.
adamc@530 255 \end{itemize}
adamc@530 256
adamc@530 257 \subsection{Kinding}
adamc@530 258
adamc@530 259 $$\infer{\Gamma \vdash (c) :: \kappa :: \kappa}{
adamc@530 260 \Gamma \vdash c :: \kappa
adamc@530 261 }
adamc@530 262 \quad \infer{\Gamma \vdash x :: \kappa}{
adamc@530 263 x :: \kappa \in \Gamma
adamc@530 264 }
adamc@530 265 \quad \infer{\Gamma \vdash x :: \kappa}{
adamc@530 266 x :: \kappa = c \in \Gamma
adamc@530 267 }$$
adamc@530 268
adamc@530 269 $$\infer{\Gamma \vdash M.x :: \kappa}{
adamc@537 270 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 271 & \mt{proj}(M, \overline{s}, \mt{con} \; x) = \kappa
adamc@530 272 }
adamc@530 273 \quad \infer{\Gamma \vdash M.x :: \kappa}{
adamc@537 274 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 275 & \mt{proj}(M, \overline{s}, \mt{con} \; x) = (\kappa, c)
adamc@530 276 }$$
adamc@530 277
adamc@530 278 $$\infer{\Gamma \vdash \tau_1 \to \tau_2 :: \mt{Type}}{
adamc@530 279 \Gamma \vdash \tau_1 :: \mt{Type}
adamc@530 280 & \Gamma \vdash \tau_2 :: \mt{Type}
adamc@530 281 }
adamc@530 282 \quad \infer{\Gamma \vdash x \; ? \: \kappa \to \tau :: \mt{Type}}{
adamc@530 283 \Gamma, x :: \kappa \vdash \tau :: \mt{Type}
adamc@530 284 }
adamc@530 285 \quad \infer{\Gamma \vdash \$c :: \mt{Type}}{
adamc@530 286 \Gamma \vdash c :: \{\mt{Type}\}
adamc@530 287 }$$
adamc@530 288
adamc@530 289 $$\infer{\Gamma \vdash c_1 \; c_2 :: \kappa_2}{
adamc@530 290 \Gamma \vdash c_1 :: \kappa_1 \to \kappa_2
adamc@530 291 & \Gamma \vdash c_2 :: \kappa_1
adamc@530 292 }
adamc@530 293 \quad \infer{\Gamma \vdash \lambda x \; :: \; \kappa_1 \Rightarrow c :: \kappa_1 \to \kappa_2}{
adamc@530 294 \Gamma, x :: \kappa_1 \vdash c :: \kappa_2
adamc@530 295 }$$
adamc@530 296
adamc@530 297 $$\infer{\Gamma \vdash () :: \mt{Unit}}{}
adamc@530 298 \quad \infer{\Gamma \vdash \#X :: \mt{Name}}{}$$
adamc@530 299
adamc@530 300 $$\infer{\Gamma \vdash [\overline{c_i = c'_i}] :: \{\kappa\}}{
adamc@530 301 \forall i: \Gamma \vdash c_i : \mt{Name}
adamc@530 302 & \Gamma \vdash c'_i :: \kappa
adamc@530 303 & \forall i \neq j: \Gamma \vdash c_i \sim c_j
adamc@530 304 }
adamc@530 305 \quad \infer{\Gamma \vdash c_1 \rc c_2 :: \{\kappa\}}{
adamc@530 306 \Gamma \vdash c_1 :: \{\kappa\}
adamc@530 307 & \Gamma \vdash c_2 :: \{\kappa\}
adamc@530 308 & \Gamma \vdash c_1 \sim c_2
adamc@530 309 }$$
adamc@530 310
adamc@530 311 $$\infer{\Gamma \vdash \mt{fold} :: ((\mt{Name} \to \kappa_1 \to \kappa_2 \to \kappa_2) \to \kappa_2 \to \{\kappa_1\} \to \kappa_2}{}$$
adamc@530 312
adamc@530 313 $$\infer{\Gamma \vdash (\overline c) :: (k_1 \times \ldots \times k_n)}{
adamc@530 314 \forall i: \Gamma \vdash c_i :: k_i
adamc@530 315 }
adamc@530 316 \quad \infer{\Gamma \vdash c.i :: k_i}{
adamc@530 317 \Gamma \vdash c :: (k_1 \times \ldots \times k_n)
adamc@530 318 }$$
adamc@530 319
adamc@530 320 $$\infer{\Gamma \vdash \lambda [c_1 \sim c_2] \Rightarrow c :: \kappa}{
adamc@530 321 \Gamma \vdash c_1 :: \{\kappa'\}
adamc@530 322 & \Gamma \vdash c_2 :: \{\kappa'\}
adamc@530 323 & \Gamma, c_1 \sim c_2 \vdash c :: \kappa
adamc@530 324 }$$
adamc@530 325
adamc@531 326 \subsection{Record Disjointness}
adamc@531 327
adamc@531 328 We will use a keyword $\mt{map}$ as a shorthand, such that, for $f$ of kind $\kappa \to \kappa'$, $\mt{map} \; f$ stands for $\mt{fold} \; (\lambda (x_1 :: \mt{Name}) (x_2 :: \kappa) (x_3 :: \{\kappa'\}) \Rightarrow [x_1 = f \; x_2] \rc x_3) \; []$.
adamc@531 329
adamc@531 330 $$\infer{\Gamma \vdash c_1 \sim c_2}{
adamc@531 331 \Gamma \vdash c_1 \hookrightarrow c'_1
adamc@531 332 & \Gamma \vdash c_2 \hookrightarrow c'_2
adamc@531 333 & \forall c''_1 \in c'_1, c''_2 \in c'_2: \Gamma \vdash c''_1 \sim c''_2
adamc@531 334 }
adamc@531 335 \quad \infer{\Gamma \vdash X \sim X'}{
adamc@531 336 X \neq X'
adamc@531 337 }$$
adamc@531 338
adamc@531 339 $$\infer{\Gamma \vdash c_1 \sim c_2}{
adamc@531 340 c'_1 \sim c'_2 \in \Gamma
adamc@531 341 & \Gamma \vdash c'_1 \hookrightarrow c''_1
adamc@531 342 & \Gamma \vdash c'_2 \hookrightarrow c''_2
adamc@531 343 & c_1 \in c''_1
adamc@531 344 & c_2 \in c''_2
adamc@531 345 }$$
adamc@531 346
adamc@531 347 $$\infer{\Gamma \vdash c \hookrightarrow \{c\}}{}
adamc@531 348 \quad \infer{\Gamma \vdash [\overline{c = c'}] \hookrightarrow \{\overline{c}\}}{}
adamc@531 349 \quad \infer{\Gamma \vdash c_1 \rc c_2 \hookrightarrow C_1 \cup C_2}{
adamc@531 350 \Gamma \vdash c_1 \hookrightarrow C_1
adamc@531 351 & \Gamma \vdash c_2 \hookrightarrow C_2
adamc@531 352 }
adamc@531 353 \quad \infer{\Gamma \vdash c \hookrightarrow C}{
adamc@531 354 \Gamma \vdash c \equiv c'
adamc@531 355 & \Gamma \vdash c' \hookrightarrow C
adamc@531 356 }
adamc@531 357 \quad \infer{\Gamma \vdash \mt{map} \; f \; c \hookrightarrow C}{
adamc@531 358 \Gamma \vdash c \hookrightarrow C
adamc@531 359 }$$
adamc@531 360
adamc@541 361 \subsection{\label{definitional}Definitional Equality}
adamc@532 362
adamc@532 363 We use $\mathcal C$ to stand for a one-hole context that, when filled, yields a constructor. The notation $\mathcal C[c]$ plugs $c$ into $\mathcal C$. We omit the standard definition of one-hole contexts. We write $[x \mapsto c_1]c_2$ for capture-avoiding substitution of $c_1$ for $x$ in $c_2$.
adamc@532 364
adamc@532 365 $$\infer{\Gamma \vdash c \equiv c}{}
adamc@532 366 \quad \infer{\Gamma \vdash c_1 \equiv c_2}{
adamc@532 367 \Gamma \vdash c_2 \equiv c_1
adamc@532 368 }
adamc@532 369 \quad \infer{\Gamma \vdash c_1 \equiv c_3}{
adamc@532 370 \Gamma \vdash c_1 \equiv c_2
adamc@532 371 & \Gamma \vdash c_2 \equiv c_3
adamc@532 372 }
adamc@532 373 \quad \infer{\Gamma \vdash \mathcal C[c_1] \equiv \mathcal C[c_2]}{
adamc@532 374 \Gamma \vdash c_1 \equiv c_2
adamc@532 375 }$$
adamc@532 376
adamc@532 377 $$\infer{\Gamma \vdash x \equiv c}{
adamc@532 378 x :: \kappa = c \in \Gamma
adamc@532 379 }
adamc@532 380 \quad \infer{\Gamma \vdash M.x \equiv c}{
adamc@537 381 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 382 & \mt{proj}(M, \overline{s}, \mt{con} \; x) = (\kappa, c)
adamc@532 383 }
adamc@532 384 \quad \infer{\Gamma \vdash (\overline c).i \equiv c_i}{}$$
adamc@532 385
adamc@532 386 $$\infer{\Gamma \vdash (\lambda x :: \kappa \Rightarrow c) \; c' \equiv [x \mapsto c'] c}{}
adamc@532 387 \quad \infer{\Gamma \vdash c_1 \rc c_2 \equiv c_2 \rc c_1}{}
adamc@532 388 \quad \infer{\Gamma \vdash c_1 \rc (c_2 \rc c_3) \equiv (c_1 \rc c_2) \rc c_3}{}$$
adamc@532 389
adamc@532 390 $$\infer{\Gamma \vdash [] \rc c \equiv c}{}
adamc@532 391 \quad \infer{\Gamma \vdash [\overline{c_1 = c'_1}] \rc [\overline{c_2 = c'_2}] \equiv [\overline{c_1 = c'_1}, \overline{c_2 = c'_2}]}{}$$
adamc@532 392
adamc@532 393 $$\infer{\Gamma \vdash \lambda [c_1 \sim c_2] \Rightarrow c \equiv c}{
adamc@532 394 \Gamma \vdash c_1 \sim c_2
adamc@532 395 }
adamc@532 396 \quad \infer{\Gamma \vdash \mt{fold} \; f \; i \; [] \equiv i}{}
adamc@532 397 \quad \infer{\Gamma \vdash \mt{fold} \; f \; i \; ([c_1 = c_2] \rc c) \equiv f \; c_1 \; c_2 \; (\mt{fold} \; f \; i \; c)}{}$$
adamc@532 398
adamc@532 399 $$\infer{\Gamma \vdash \mt{map} \; (\lambda x \Rightarrow x) \; c \equiv c}{}
adamc@532 400 \quad \infer{\Gamma \vdash \mt{fold} \; f \; i \; (\mt{map} \; f' \; c)
adamc@532 401 \equiv \mt{fold} \; (\lambda (x_1 :: \mt{Name}) (x_2 :: \kappa) \Rightarrow f \; x_1 \; (f' \; x_2)) \; i \; c}{}$$
adamc@532 402
adamc@532 403 $$\infer{\Gamma \vdash \mt{map} \; f \; (c_1 \rc c_2) \equiv \mt{map} \; f \; c_1 \rc \mt{map} \; f \; c_2}{}$$
adamc@531 404
adamc@534 405 \subsection{Expression Typing}
adamc@533 406
adamc@533 407 We assume the existence of a function $T$ assigning types to literal constants. It maps integer constants to $\mt{Basis}.\mt{int}$, float constants to $\mt{Basis}.\mt{float}$, and string constants to $\mt{Basis}.\mt{string}$.
adamc@533 408
adamc@533 409 We also refer to a function $\mathcal I$, such that $\mathcal I(\tau)$ ``uses an oracle'' to instantiate all constructor function arguments at the beginning of $\tau$ that are marked implicit; i.e., replace $x_1 ::: \kappa_1 \to \ldots \to x_n ::: \kappa_n \to \tau$ with $[x_1 \mapsto c_1]\ldots[x_n \mapsto c_n]\tau$, where the $c_i$s are inferred and $\tau$ does not start like $x ::: \kappa \to \tau'$.
adamc@533 410
adamc@533 411 $$\infer{\Gamma \vdash e : \tau : \tau}{
adamc@533 412 \Gamma \vdash e : \tau
adamc@533 413 }
adamc@533 414 \quad \infer{\Gamma \vdash e : \tau}{
adamc@533 415 \Gamma \vdash e : \tau'
adamc@533 416 & \Gamma \vdash \tau' \equiv \tau
adamc@533 417 }
adamc@533 418 \quad \infer{\Gamma \vdash \ell : T(\ell)}{}$$
adamc@533 419
adamc@533 420 $$\infer{\Gamma \vdash x : \mathcal I(\tau)}{
adamc@533 421 x : \tau \in \Gamma
adamc@533 422 }
adamc@533 423 \quad \infer{\Gamma \vdash M.x : \mathcal I(\tau)}{
adamc@537 424 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 425 & \mt{proj}(M, \overline{s}, \mt{val} \; x) = \tau
adamc@533 426 }
adamc@533 427 \quad \infer{\Gamma \vdash X : \mathcal I(\tau)}{
adamc@533 428 X : \tau \in \Gamma
adamc@533 429 }
adamc@533 430 \quad \infer{\Gamma \vdash M.X : \mathcal I(\tau)}{
adamc@537 431 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 432 & \mt{proj}(M, \overline{s}, \mt{val} \; X) = \tau
adamc@533 433 }$$
adamc@533 434
adamc@533 435 $$\infer{\Gamma \vdash e_1 \; e_2 : \tau_2}{
adamc@533 436 \Gamma \vdash e_1 : \tau_1 \to \tau_2
adamc@533 437 & \Gamma \vdash e_2 : \tau_1
adamc@533 438 }
adamc@533 439 \quad \infer{\Gamma \vdash \lambda x : \tau_1 \Rightarrow e : \tau_1 \to \tau_2}{
adamc@533 440 \Gamma, x : \tau_1 \vdash e : \tau_2
adamc@533 441 }$$
adamc@533 442
adamc@533 443 $$\infer{\Gamma \vdash e [c] : [x \mapsto c]\tau}{
adamc@533 444 \Gamma \vdash e : x :: \kappa \to \tau
adamc@533 445 & \Gamma \vdash c :: \kappa
adamc@533 446 }
adamc@533 447 \quad \infer{\Gamma \vdash \lambda x \; ? \; \kappa \Rightarrow e : x \; ? \; \kappa \to \tau}{
adamc@533 448 \Gamma, x :: \kappa \vdash e : \tau
adamc@533 449 }$$
adamc@533 450
adamc@533 451 $$\infer{\Gamma \vdash \{\overline{c = e}\} : \{\overline{c : \tau}\}}{
adamc@533 452 \forall i: \Gamma \vdash c_i :: \mt{Name}
adamc@533 453 & \Gamma \vdash e_i : \tau_i
adamc@533 454 & \forall i \neq j: \Gamma \vdash c_i \sim c_j
adamc@533 455 }
adamc@533 456 \quad \infer{\Gamma \vdash e.c : \tau}{
adamc@533 457 \Gamma \vdash e : \$([c = \tau] \rc c')
adamc@533 458 }
adamc@533 459 \quad \infer{\Gamma \vdash e_1 \rc e_2 : \$(c_1 \rc c_2)}{
adamc@533 460 \Gamma \vdash e_1 : \$c_1
adamc@533 461 & \Gamma \vdash e_2 : \$c_2
adamc@533 462 }$$
adamc@533 463
adamc@533 464 $$\infer{\Gamma \vdash e \rcut c : \$c'}{
adamc@533 465 \Gamma \vdash e : \$([c = \tau] \rc c')
adamc@533 466 }
adamc@533 467 \quad \infer{\Gamma \vdash e \rcutM c : \$c'}{
adamc@533 468 \Gamma \vdash e : \$(c \rc c')
adamc@533 469 }$$
adamc@533 470
adamc@533 471 $$\infer{\Gamma \vdash \mt{fold} : \begin{array}{c}
adamc@533 472 x_1 :: (\{\kappa\} \to \tau)
adamc@533 473 \to (x_2 :: \mt{Name} \to x_3 :: \kappa \to x_4 :: \{\kappa\} \to \lambda [[x_2] \sim x_4]
adamc@533 474 \Rightarrow x_1 \; x_4 \to x_1 \; ([x_2 = x_3] \rc x_4)) \\
adamc@533 475 \to x_1 \; [] \to x_5 :: \{\kappa\} \to x_1 \; x_5
adamc@533 476 \end{array}}{}$$
adamc@533 477
adamc@533 478 $$\infer{\Gamma \vdash \mt{let} \; \overline{ed} \; \mt{in} \; e \; \mt{end} : \tau}{
adamc@533 479 \Gamma \vdash \overline{ed} \leadsto \Gamma'
adamc@533 480 & \Gamma' \vdash e : \tau
adamc@533 481 }
adamc@533 482 \quad \infer{\Gamma \vdash \mt{case} \; e \; \mt{of} \; \overline{p \Rightarrow e} : \tau}{
adamc@533 483 \forall i: \Gamma \vdash p_i \leadsto \Gamma_i, \tau'
adamc@533 484 & \Gamma_i \vdash e_i : \tau
adamc@533 485 }$$
adamc@533 486
adamc@533 487 $$\infer{\Gamma \vdash [c_1 \sim c_2] \Rightarrow e : [c_1 \sim c_2] \Rightarrow \tau}{
adamc@533 488 \Gamma \vdash c_1 :: \{\kappa\}
adamc@533 489 & \Gamma \vdash c_2 :: \{\kappa\}
adamc@533 490 & \Gamma, c_1 \sim c_2 \vdash e : \tau
adamc@533 491 }$$
adamc@533 492
adamc@534 493 \subsection{Pattern Typing}
adamc@534 494
adamc@534 495 $$\infer{\Gamma \vdash \_ \leadsto \Gamma; \tau}{}
adamc@534 496 \quad \infer{\Gamma \vdash x \leadsto \Gamma, x : \tau; \tau}{}
adamc@534 497 \quad \infer{\Gamma \vdash \ell \leadsto \Gamma; T(\ell)}{}$$
adamc@534 498
adamc@534 499 $$\infer{\Gamma \vdash X \leadsto \Gamma; \overline{[x_i \mapsto \tau'_i]}\tau}{
adamc@534 500 X : \overline{x ::: \mt{Type}} \to \tau \in \Gamma
adamc@534 501 & \textrm{$\tau$ not a function type}
adamc@534 502 }
adamc@534 503 \quad \infer{\Gamma \vdash X \; p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau}{
adamc@534 504 X : \overline{x ::: \mt{Type}} \to \tau'' \to \tau \in \Gamma
adamc@534 505 & \Gamma \vdash p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau''
adamc@534 506 }$$
adamc@534 507
adamc@534 508 $$\infer{\Gamma \vdash M.X \leadsto \Gamma; \overline{[x_i \mapsto \tau'_i]}\tau}{
adamc@537 509 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 510 & \mt{proj}(M, \overline{s}, \mt{val} \; X) = \overline{x ::: \mt{Type}} \to \tau
adamc@534 511 & \textrm{$\tau$ not a function type}
adamc@534 512 }$$
adamc@534 513
adamc@534 514 $$\infer{\Gamma \vdash M.X \; p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau}{
adamc@537 515 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 516 & \mt{proj}(M, \overline{s}, \mt{val} \; X) = \overline{x ::: \mt{Type}} \to \tau'' \to \tau
adamc@534 517 & \Gamma \vdash p \leadsto \Gamma'; \overline{[x_i \mapsto \tau'_i]}\tau''
adamc@534 518 }$$
adamc@534 519
adamc@534 520 $$\infer{\Gamma \vdash \{\overline{x = p}\} \leadsto \Gamma_n; \{\overline{x = \tau}\}}{
adamc@534 521 \Gamma_0 = \Gamma
adamc@534 522 & \forall i: \Gamma_i \vdash p_i \leadsto \Gamma_{i+1}; \tau_i
adamc@534 523 }
adamc@534 524 \quad \infer{\Gamma \vdash \{\overline{x = p}, \ldots\} \leadsto \Gamma_n; \$([\overline{x = \tau}] \rc c)}{
adamc@534 525 \Gamma_0 = \Gamma
adamc@534 526 & \forall i: \Gamma_i \vdash p_i \leadsto \Gamma_{i+1}; \tau_i
adamc@534 527 }$$
adamc@534 528
adamc@535 529 \subsection{Declaration Typing}
adamc@535 530
adamc@535 531 We use an auxiliary judgment $\overline{y}; x; \Gamma \vdash \overline{dc} \leadsto \Gamma'$, expressing the enrichment of $\Gamma$ with the types of the datatype constructors $\overline{dc}$, when they are known to belong to datatype $x$ with type parameters $\overline{y}$.
adamc@535 532
adamc@541 533 This is the first judgment where we deal with type classes, for the $\mt{class}$ declaration form. We will omit their special handling in this formal specification. Section \ref{typeclasses} gives an informal description of how type classes influence type inference.
adamc@535 534
adamc@537 535 We presuppose the existence of a function $\mathcal O$, where $\mathcal(M, \overline{s})$ implements the $\mt{open}$ declaration by producing a context with the appropriate entry for each available component of module $M$ with signature items $\overline{s}$. Where possible, $\mathcal O$ uses ``transparent'' entries (e.g., an abstract type $M.x$ is mapped to $x :: \mt{Type} = M.x$), so that the relationship with $M$ is maintained. A related function $\mathcal O_c$ builds a context containing the disjointness constraints found in $S$.
adamc@537 536
adamc@537 537 We write $\kappa_1^n \to \kappa$ as a shorthand, where $\kappa_1^0 \to \kappa = \kappa$ and $\kappa_1^{n+1} \to \kappa_2 = \kappa_1 \to (\kappa_1^n \to \kappa_2)$. We write $\mt{len}(\overline{y})$ for the length of vector $\overline{y}$ of variables.
adamc@535 538
adamc@535 539 $$\infer{\Gamma \vdash \cdot \leadsto \Gamma}{}
adamc@535 540 \quad \infer{\Gamma \vdash d, \overline{d} \leadsto \Gamma''}{
adamc@535 541 \Gamma \vdash d \leadsto \Gamma'
adamc@535 542 & \Gamma' \vdash \overline{d} \leadsto \Gamma''
adamc@535 543 }$$
adamc@535 544
adamc@535 545 $$\infer{\Gamma \vdash \mt{con} \; x :: \kappa = c \leadsto \Gamma, x :: \kappa = c}{
adamc@535 546 \Gamma \vdash c :: \kappa
adamc@535 547 }
adamc@535 548 \quad \infer{\Gamma \vdash \mt{datatype} \; x \; \overline{y} = \overline{dc} \leadsto \Gamma'}{
adamc@535 549 \overline{y}; x; \Gamma, x :: \mt{Type}^{\mt{len}(\overline y)} \to \mt{Type} \vdash \overline{dc} \leadsto \Gamma'
adamc@535 550 }$$
adamc@535 551
adamc@535 552 $$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leadsto \Gamma'}{
adamc@537 553 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 554 & \mt{proj}(M, \overline{s}, \mt{datatype} \; z) = (\overline{y}, \overline{dc})
adamc@535 555 & \overline{y}; x; \Gamma, x :: \mt{Type}^{\mt{len}(\overline y)} \to \mt{Type} = M.z \vdash \overline{dc} \leadsto \Gamma'
adamc@535 556 }$$
adamc@535 557
adamc@535 558 $$\infer{\Gamma \vdash \mt{val} \; x : \tau = e \leadsto \Gamma, x : \tau}{
adamc@535 559 \Gamma \vdash e : \tau
adamc@535 560 }$$
adamc@535 561
adamc@535 562 $$\infer{\Gamma \vdash \mt{val} \; \mt{rec} \; \overline{x : \tau = e} \leadsto \Gamma, \overline{x : \tau}}{
adamc@535 563 \forall i: \Gamma, \overline{x : \tau} \vdash e_i : \tau_i
adamc@535 564 & \textrm{$e_i$ starts with an expression $\lambda$, optionally preceded by constructor and disjointness $\lambda$s}
adamc@535 565 }$$
adamc@535 566
adamc@535 567 $$\infer{\Gamma \vdash \mt{structure} \; X : S = M \leadsto \Gamma, X : S}{
adamc@535 568 \Gamma \vdash M : S
adamc@539 569 & \textrm{ ($M$ not a $\mt{struct} \; \ldots \; \mt{end}$)}
adamc@535 570 }
adamc@539 571 \quad \infer{\Gamma \vdash \mt{structure} \; X : S = \mt{struct} \; \overline{d} \; \mt{end} \leadsto \Gamma, X : \mt{selfify}(X, \overline{s})}{
adamc@539 572 \Gamma \vdash \mt{struct} \; \overline{d} \; \mt{end} : \mt{sig} \; \overline{s} \; \mt{end}
adamc@539 573 }$$
adamc@539 574
adamc@539 575 $$\infer{\Gamma \vdash \mt{signature} \; X = S \leadsto \Gamma, X = S}{
adamc@535 576 \Gamma \vdash S
adamc@535 577 }$$
adamc@535 578
adamc@537 579 $$\infer{\Gamma \vdash \mt{open} \; M \leadsto \Gamma, \mathcal O(M, \overline{s})}{
adamc@537 580 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@535 581 }$$
adamc@535 582
adamc@535 583 $$\infer{\Gamma \vdash \mt{constraint} \; c_1 \sim c_2 \leadsto \Gamma}{
adamc@535 584 \Gamma \vdash c_1 :: \{\kappa\}
adamc@535 585 & \Gamma \vdash c_2 :: \{\kappa\}
adamc@535 586 & \Gamma \vdash c_1 \sim c_2
adamc@535 587 }
adamc@537 588 \quad \infer{\Gamma \vdash \mt{open} \; \mt{constraints} \; M \leadsto \Gamma, \mathcal O_c(M, \overline{s})}{
adamc@537 589 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@535 590 }$$
adamc@535 591
adamc@535 592 $$\infer{\Gamma \vdash \mt{table} \; x : c \leadsto \Gamma, x : \mt{Basis}.\mt{sql\_table} \; c}{
adamc@535 593 \Gamma \vdash c :: \{\mt{Type}\}
adamc@535 594 }
adamc@535 595 \quad \infer{\Gamma \vdash \mt{sequence} \; x \leadsto \Gamma, x : \mt{Basis}.\mt{sql\_sequence}}{}$$
adamc@535 596
adamc@535 597 $$\infer{\Gamma \vdash \mt{cookie} \; x : \tau \leadsto \Gamma, x : \mt{Basis}.\mt{http\_cookie} \; \tau}{
adamc@535 598 \Gamma \vdash \tau :: \mt{Type}
adamc@535 599 }$$
adamc@535 600
adamc@535 601 $$\infer{\Gamma \vdash \mt{class} \; x = c \leadsto \Gamma, x :: \mt{Type} \to \mt{Type} = c}{
adamc@535 602 \Gamma \vdash c :: \mt{Type} \to \mt{Type}
adamc@535 603 }$$
adamc@535 604
adamc@535 605 $$\infer{\overline{y}; x; \Gamma \vdash \cdot \leadsto \Gamma}{}
adamc@535 606 \quad \infer{\overline{y}; x; \Gamma \vdash X \mid \overline{dc} \leadsto \Gamma', X : \overline{y ::: \mt{Type}} \to x \; \overline{y}}{
adamc@535 607 \overline{y}; x; \Gamma \vdash \overline{dc} \leadsto \Gamma'
adamc@535 608 }
adamc@535 609 \quad \infer{\overline{y}; x; \Gamma \vdash X \; \mt{of} \; \tau \mid \overline{dc} \leadsto \Gamma', X : \overline{y ::: \mt{Type}} \to \tau \to x \; \overline{y}}{
adamc@535 610 \overline{y}; x; \Gamma \vdash \overline{dc} \leadsto \Gamma'
adamc@535 611 }$$
adamc@535 612
adamc@537 613 \subsection{Signature Item Typing}
adamc@537 614
adamc@537 615 We appeal to a signature item analogue of the $\mathcal O$ function from the last subsection.
adamc@537 616
adamc@537 617 $$\infer{\Gamma \vdash \cdot \leadsto \Gamma}{}
adamc@537 618 \quad \infer{\Gamma \vdash s, \overline{s} \leadsto \Gamma''}{
adamc@537 619 \Gamma \vdash s \leadsto \Gamma'
adamc@537 620 & \Gamma' \vdash \overline{s} \leadsto \Gamma''
adamc@537 621 }$$
adamc@537 622
adamc@537 623 $$\infer{\Gamma \vdash \mt{con} \; x :: \kappa \leadsto \Gamma, x :: \kappa}{}
adamc@537 624 \quad \infer{\Gamma \vdash \mt{con} \; x :: \kappa = c \leadsto \Gamma, x :: \kappa = c}{
adamc@537 625 \Gamma \vdash c :: \kappa
adamc@537 626 }
adamc@537 627 \quad \infer{\Gamma \vdash \mt{datatype} \; x \; \overline{y} = \overline{dc} \leadsto \Gamma'}{
adamc@537 628 \overline{y}; x; \Gamma, x :: \mt{Type}^{\mt{len}(\overline y)} \to \mt{Type} \vdash \overline{dc} \leadsto \Gamma'
adamc@537 629 }$$
adamc@537 630
adamc@537 631 $$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leadsto \Gamma'}{
adamc@537 632 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 633 & \mt{proj}(M, \overline{s}, \mt{datatype} \; z) = (\overline{y}, \overline{dc})
adamc@537 634 & \overline{y}; x; \Gamma, x :: \mt{Type}^{\mt{len}(\overline y)} \to \mt{Type} = M.z \vdash \overline{dc} \leadsto \Gamma'
adamc@537 635 }$$
adamc@537 636
adamc@537 637 $$\infer{\Gamma \vdash \mt{val} \; x : \tau \leadsto \Gamma, x : \tau}{
adamc@537 638 \Gamma \vdash \tau :: \mt{Type}
adamc@537 639 }$$
adamc@537 640
adamc@537 641 $$\infer{\Gamma \vdash \mt{structure} \; X : S \leadsto \Gamma, X : S}{
adamc@537 642 \Gamma \vdash S
adamc@537 643 }
adamc@537 644 \quad \infer{\Gamma \vdash \mt{signature} \; X = S \leadsto \Gamma, X = S}{
adamc@537 645 \Gamma \vdash S
adamc@537 646 }$$
adamc@537 647
adamc@537 648 $$\infer{\Gamma \vdash \mt{include} \; S \leadsto \Gamma, \mathcal O(\overline{s})}{
adamc@537 649 \Gamma \vdash S
adamc@537 650 & \Gamma \vdash S \equiv \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 651 }$$
adamc@537 652
adamc@537 653 $$\infer{\Gamma \vdash \mt{constraint} \; c_1 \sim c_2 \leadsto \Gamma, c_1 \sim c_2}{
adamc@537 654 \Gamma \vdash c_1 :: \{\kappa\}
adamc@537 655 & \Gamma \vdash c_2 :: \{\kappa\}
adamc@537 656 }$$
adamc@537 657
adamc@537 658 $$\infer{\Gamma \vdash \mt{class} \; x = c \leadsto \Gamma, x :: \mt{Type} \to \mt{Type} = c}{
adamc@537 659 \Gamma \vdash c :: \mt{Type} \to \mt{Type}
adamc@537 660 }
adamc@537 661 \quad \infer{\Gamma \vdash \mt{class} \; x \leadsto \Gamma, x :: \mt{Type} \to \mt{Type}}{}$$
adamc@537 662
adamc@536 663 \subsection{Signature Compatibility}
adamc@536 664
adamc@537 665 To simplify the judgments in this section, we assume that all signatures are alpha-varied as necessary to avoid including mmultiple bindings for the same identifier. This is in addition to the usual alpha-variation of locally-bound variables.
adamc@537 666
adamc@537 667 We rely on a judgment $\Gamma \vdash \overline{s} \leq s'$, which expresses the occurrence in signature items $\overline{s}$ of an item compatible with $s'$. We also use a judgment $\Gamma \vdash \overline{dc} \leq \overline{dc}$, which expresses compatibility of datatype definitions.
adamc@537 668
adamc@536 669 $$\infer{\Gamma \vdash S \equiv S}{}
adamc@536 670 \quad \infer{\Gamma \vdash S_1 \equiv S_2}{
adamc@536 671 \Gamma \vdash S_2 \equiv S_1
adamc@536 672 }
adamc@536 673 \quad \infer{\Gamma \vdash X \equiv S}{
adamc@536 674 X = S \in \Gamma
adamc@536 675 }
adamc@536 676 \quad \infer{\Gamma \vdash M.X \equiv S}{
adamc@537 677 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 678 & \mt{proj}(M, \overline{s}, \mt{signature} \; X) = S
adamc@536 679 }$$
adamc@536 680
adamc@536 681 $$\infer{\Gamma \vdash S \; \mt{where} \; \mt{con} \; x = c \equiv \mt{sig} \; \overline{s^1} \; \mt{con} \; x :: \kappa = c \; \overline{s_2} \; \mt{end}}{
adamc@536 682 \Gamma \vdash S \equiv \mt{sig} \; \overline{s^1} \; \mt{con} \; x :: \kappa \; \overline{s_2} \; \mt{end}
adamc@536 683 & \Gamma \vdash c :: \kappa
adamc@537 684 }
adamc@537 685 \quad \infer{\Gamma \vdash \mt{sig} \; \overline{s^1} \; \mt{include} \; S \; \overline{s^2} \; \mt{end} \equiv \mt{sig} \; \overline{s^1} \; \overline{s} \; \overline{s^2} \; \mt{end}}{
adamc@537 686 \Gamma \vdash S \equiv \mt{sig} \; \overline{s} \; \mt{end}
adamc@536 687 }$$
adamc@536 688
adamc@536 689 $$\infer{\Gamma \vdash S_1 \leq S_2}{
adamc@536 690 \Gamma \vdash S_1 \equiv S_2
adamc@536 691 }
adamc@536 692 \quad \infer{\Gamma \vdash \mt{sig} \; \overline{s} \; \mt{end} \leq \mt{sig} \; \mt{end}}{}
adamc@537 693 \quad \infer{\Gamma \vdash \mt{sig} \; \overline{s} \; \mt{end} \leq \mt{sig} \; s' \; \overline{s'} \; \mt{end}}{
adamc@537 694 \Gamma \vdash \overline{s} \leq s'
adamc@537 695 & \Gamma \vdash s' \leadsto \Gamma'
adamc@537 696 & \Gamma' \vdash \mt{sig} \; \overline{s} \; \mt{end} \leq \mt{sig} \; \overline{s'} \; \mt{end}
adamc@537 697 }$$
adamc@537 698
adamc@537 699 $$\infer{\Gamma \vdash s \; \overline{s} \leq s'}{
adamc@537 700 \Gamma \vdash s \leq s'
adamc@537 701 }
adamc@537 702 \quad \infer{\Gamma \vdash s \; \overline{s} \leq s'}{
adamc@537 703 \Gamma \vdash s \leadsto \Gamma'
adamc@537 704 & \Gamma' \vdash \overline{s} \leq s'
adamc@536 705 }$$
adamc@536 706
adamc@536 707 $$\infer{\Gamma \vdash \mt{functor} (X : S_1) : S_2 \leq \mt{functor} (X : S'_1) : S'_2}{
adamc@536 708 \Gamma \vdash S'_1 \leq S_1
adamc@536 709 & \Gamma, X : S'_1 \vdash S_2 \leq S'_2
adamc@536 710 }$$
adamc@536 711
adamc@537 712 $$\infer{\Gamma \vdash \mt{con} \; x :: \kappa \leq \mt{con} \; x :: \kappa}{}
adamc@537 713 \quad \infer{\Gamma \vdash \mt{con} \; x :: \kappa = c \leq \mt{con} \; x :: \kappa}{}
adamc@537 714 \quad \infer{\Gamma \vdash \mt{datatype} \; x \; \overline{y} = \overline{dc} \leq \mt{con} \; x :: \mt{Type}}{}$$
adamc@537 715
adamc@537 716 $$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leq \mt{con} \; x :: \mt{Type}^{\mt{len}(y)} \to \mt{Type}}{
adamc@537 717 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 718 & \mt{proj}(M, \overline{s}, \mt{datatype} \; z) = (\overline{y}, \overline{dc})
adamc@537 719 }$$
adamc@537 720
adamc@537 721 $$\infer{\Gamma \vdash \mt{class} \; x \leq \mt{con} \; x :: \mt{Type} \to \mt{Type}}{}
adamc@537 722 \quad \infer{\Gamma \vdash \mt{class} \; x = c \leq \mt{con} \; x :: \mt{Type} \to \mt{Type}}{}$$
adamc@537 723
adamc@537 724 $$\infer{\Gamma \vdash \mt{con} \; x :: \kappa = c_1 \leq \mt{con} \; x :: \mt{\kappa} = c_2}{
adamc@537 725 \Gamma \vdash c_1 \equiv c_2
adamc@537 726 }
adamc@537 727 \quad \infer{\Gamma \vdash \mt{class} \; x = c_1 \leq \mt{con} \; x :: \mt{Type} \to \mt{Type} = c_2}{
adamc@537 728 \Gamma \vdash c_1 \equiv c_2
adamc@537 729 }$$
adamc@537 730
adamc@537 731 $$\infer{\Gamma \vdash \mt{datatype} \; x \; \overline{y} = \overline{dc} \leq \mt{datatype} \; x \; \overline{y} = \overline{dc'}}{
adamc@537 732 \Gamma, \overline{y :: \mt{Type}} \vdash \overline{dc} \leq \overline{dc'}
adamc@537 733 }$$
adamc@537 734
adamc@537 735 $$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leq \mt{datatype} \; x \; \overline{y} = \overline{dc'}}{
adamc@537 736 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@537 737 & \mt{proj}(M, \overline{s}, \mt{datatype} \; z) = (\overline{y}, \overline{dc})
adamc@537 738 & \Gamma, \overline{y :: \mt{Type}} \vdash \overline{dc} \leq \overline{dc'}
adamc@537 739 }$$
adamc@537 740
adamc@537 741 $$\infer{\Gamma \vdash \cdot \leq \cdot}{}
adamc@537 742 \quad \infer{\Gamma \vdash X; \overline{dc} \leq X; \overline{dc'}}{
adamc@537 743 \Gamma \vdash \overline{dc} \leq \overline{dc'}
adamc@537 744 }
adamc@537 745 \quad \infer{\Gamma \vdash X \; \mt{of} \; \tau_1; \overline{dc} \leq X \; \mt{of} \; \tau_2; \overline{dc'}}{
adamc@537 746 \Gamma \vdash \tau_1 \equiv \tau_2
adamc@537 747 & \Gamma \vdash \overline{dc} \leq \overline{dc'}
adamc@537 748 }$$
adamc@537 749
adamc@537 750 $$\infer{\Gamma \vdash \mt{datatype} \; x = \mt{datatype} \; M.z \leq \mt{datatype} \; x = \mt{datatype} \; M'.z'}{
adamc@537 751 \Gamma \vdash M.z \equiv M'.z'
adamc@537 752 }$$
adamc@537 753
adamc@537 754 $$\infer{\Gamma \vdash \mt{val} \; x : \tau_1 \leq \mt{val} \; x : \tau_2}{
adamc@537 755 \Gamma \vdash \tau_1 \equiv \tau_2
adamc@537 756 }
adamc@537 757 \quad \infer{\Gamma \vdash \mt{structure} \; X : S_1 \leq \mt{structure} \; X : S_2}{
adamc@537 758 \Gamma \vdash S_1 \leq S_2
adamc@537 759 }
adamc@537 760 \quad \infer{\Gamma \vdash \mt{signature} \; X = S_1 \leq \mt{signature} \; X = S_2}{
adamc@537 761 \Gamma \vdash S_1 \leq S_2
adamc@537 762 & \Gamma \vdash S_2 \leq S_1
adamc@537 763 }$$
adamc@537 764
adamc@537 765 $$\infer{\Gamma \vdash \mt{constraint} \; c_1 \sim c_2 \leq \mt{constraint} \; c'_1 \sim c'_2}{
adamc@537 766 \Gamma \vdash c_1 \equiv c'_1
adamc@537 767 & \Gamma \vdash c_2 \equiv c'_2
adamc@537 768 }$$
adamc@537 769
adamc@537 770 $$\infer{\Gamma \vdash \mt{class} \; x \leq \mt{class} \; x}{}
adamc@537 771 \quad \infer{\Gamma \vdash \mt{class} \; x = c \leq \mt{class} \; x}{}
adamc@537 772 \quad \infer{\Gamma \vdash \mt{class} \; x = c_1 \leq \mt{class} \; x = c_2}{
adamc@537 773 \Gamma \vdash c_1 \equiv c_2
adamc@537 774 }$$
adamc@537 775
adamc@538 776 \subsection{Module Typing}
adamc@538 777
adamc@538 778 We use a helper function $\mt{sigOf}$, which converts declarations and sequences of declarations into their principal signature items and sequences of signature items, respectively.
adamc@538 779
adamc@538 780 $$\infer{\Gamma \vdash M : S}{
adamc@538 781 \Gamma \vdash M : S'
adamc@538 782 & \Gamma \vdash S' \leq S
adamc@538 783 }
adamc@538 784 \quad \infer{\Gamma \vdash \mt{struct} \; \overline{d} \; \mt{end} : \mt{sig} \; \mt{sigOf}(\overline{d}) \; \mt{end}}{
adamc@538 785 \Gamma \vdash \overline{d} \leadsto \Gamma'
adamc@538 786 }
adamc@538 787 \quad \infer{\Gamma \vdash X : S}{
adamc@538 788 X : S \in \Gamma
adamc@538 789 }$$
adamc@538 790
adamc@538 791 $$\infer{\Gamma \vdash M.X : S}{
adamc@538 792 \Gamma \vdash M : \mt{sig} \; \overline{s} \; \mt{end}
adamc@538 793 & \mt{proj}(M, \overline{s}, \mt{structure} \; X) = S
adamc@538 794 }$$
adamc@538 795
adamc@538 796 $$\infer{\Gamma \vdash M_1(M_2) : [X \mapsto M_2]S_2}{
adamc@538 797 \Gamma \vdash M_1 : \mt{functor}(X : S_1) : S_2
adamc@538 798 & \Gamma \vdash M_2 : S_1
adamc@538 799 }
adamc@538 800 \quad \infer{\Gamma \vdash \mt{functor} (X : S_1) : S_2 = M : \mt{functor} (X : S_1) : S_2}{
adamc@538 801 \Gamma \vdash S_1
adamc@538 802 & \Gamma, X : S_1 \vdash S_2
adamc@538 803 & \Gamma, X : S_1 \vdash M : S_2
adamc@538 804 }$$
adamc@538 805
adamc@538 806 \begin{eqnarray*}
adamc@538 807 \mt{sigOf}(\cdot) &=& \cdot \\
adamc@538 808 \mt{sigOf}(s \; \overline{s'}) &=& \mt{sigOf}(s) \; \mt{sigOf}(\overline{s'}) \\
adamc@538 809 \\
adamc@538 810 \mt{sigOf}(\mt{con} \; x :: \kappa = c) &=& \mt{con} \; x :: \kappa = c \\
adamc@538 811 \mt{sigOf}(\mt{datatype} \; x \; \overline{y} = \overline{dc}) &=& \mt{datatype} \; x \; \overline{y} = \overline{dc} \\
adamc@538 812 \mt{sigOf}(\mt{datatype} \; x = \mt{datatype} \; M.z) &=& \mt{datatype} \; x = \mt{datatype} \; M.z \\
adamc@538 813 \mt{sigOf}(\mt{val} \; x : \tau = e) &=& \mt{val} \; x : \tau \\
adamc@538 814 \mt{sigOf}(\mt{val} \; \mt{rec} \; \overline{x : \tau = e}) &=& \overline{\mt{val} \; x : \tau} \\
adamc@538 815 \mt{sigOf}(\mt{structure} \; X : S = M) &=& \mt{structure} \; X : S \\
adamc@538 816 \mt{sigOf}(\mt{signature} \; X = S) &=& \mt{signature} \; X = S \\
adamc@538 817 \mt{sigOf}(\mt{open} \; M) &=& \mt{include} \; S \textrm{ (where $\Gamma \vdash M : S$)} \\
adamc@538 818 \mt{sigOf}(\mt{constraint} \; c_1 \sim c_2) &=& \mt{constraint} \; c_1 \sim c_2 \\
adamc@538 819 \mt{sigOf}(\mt{open} \; \mt{constraints} \; M) &=& \cdot \\
adamc@538 820 \mt{sigOf}(\mt{table} \; x : c) &=& \mt{table} \; x : c \\
adamc@538 821 \mt{sigOf}(\mt{sequence} \; x) &=& \mt{sequence} \; x \\
adamc@538 822 \mt{sigOf}(\mt{cookie} \; x : \tau) &=& \mt{cookie} \; x : \tau \\
adamc@538 823 \mt{sigOf}(\mt{class} \; x = c) &=& \mt{class} \; x = c \\
adamc@538 824 \end{eqnarray*}
adamc@538 825
adamc@539 826 \begin{eqnarray*}
adamc@539 827 \mt{selfify}(M, \cdot) &=& \cdot \\
adamc@539 828 \mt{selfify}(M, s \; \overline{s'}) &=& \mt{selfify}(M, \sigma, s) \; \mt{selfify}(M, \overline{s'}) \\
adamc@539 829 \\
adamc@539 830 \mt{selfify}(M, \mt{con} \; x :: \kappa) &=& \mt{con} \; x :: \kappa = M.x \\
adamc@539 831 \mt{selfify}(M, \mt{con} \; x :: \kappa = c) &=& \mt{con} \; x :: \kappa = c \\
adamc@539 832 \mt{selfify}(M, \mt{datatype} \; x \; \overline{y} = \overline{dc}) &=& \mt{datatype} \; x \; \overline{y} = \mt{datatype} \; M.x \\
adamc@539 833 \mt{selfify}(M, \mt{datatype} \; x = \mt{datatype} \; M'.z) &=& \mt{datatype} \; x = \mt{datatype} \; M'.z \\
adamc@539 834 \mt{selfify}(M, \mt{val} \; x : \tau) &=& \mt{val} \; x : \tau \\
adamc@539 835 \mt{selfify}(M, \mt{structure} \; X : S) &=& \mt{structure} \; X : \mt{selfify}(M.X, \overline{s}) \textrm{ (where $\Gamma \vdash S \equiv \mt{sig} \; \overline{s} \; \mt{end}$)} \\
adamc@539 836 \mt{selfify}(M, \mt{signature} \; X = S) &=& \mt{signature} \; X = S \\
adamc@539 837 \mt{selfify}(M, \mt{include} \; S) &=& \mt{include} \; S \\
adamc@539 838 \mt{selfify}(M, \mt{constraint} \; c_1 \sim c_2) &=& \mt{constraint} \; c_1 \sim c_2 \\
adamc@539 839 \mt{selfify}(M, \mt{class} \; x) &=& \mt{class} \; x = M.x \\
adamc@539 840 \mt{selfify}(M, \mt{class} \; x = c) &=& \mt{class} \; x = c \\
adamc@539 841 \end{eqnarray*}
adamc@539 842
adamc@540 843 \subsection{Module Projection}
adamc@540 844
adamc@540 845 \begin{eqnarray*}
adamc@540 846 \mt{proj}(M, \mt{con} \; x :: \kappa \; \overline{s}, \mt{con} \; x) &=& \kappa \\
adamc@540 847 \mt{proj}(M, \mt{con} \; x :: \kappa = c \; \overline{s}, \mt{con} \; x) &=& (\kappa, c) \\
adamc@540 848 \mt{proj}(M, \mt{datatype} \; x \; \overline{y} = \overline{dc} \; \overline{s}, \mt{con} \; x) &=& \mt{Type}^{\mt{len}(\overline{y})} \to \mt{Type} \\
adamc@540 849 \mt{proj}(M, \mt{datatype} \; x = \mt{datatype} \; M'.z \; \overline{s}, \mt{con} \; x) &=& (\mt{Type}^{\mt{len}(\overline{y})} \to \mt{Type}, M'.z) \textrm{ (where $\Gamma \vdash M' : \mt{sig} \; \overline{s'} \; \mt{end}$} \\
adamc@540 850 && \textrm{and $\mt{proj}(M', \overline{s'}, \mt{datatype} \; z) = (\overline{y}, \overline{dc})$)} \\
adamc@540 851 \mt{proj}(M, \mt{class} \; x \; \overline{s}, \mt{con} \; x) &=& \mt{Type} \to \mt{Type} \\
adamc@540 852 \mt{proj}(M, \mt{class} \; x = c \; \overline{s}, \mt{con} \; x) &=& (\mt{Type} \to \mt{Type}, c) \\
adamc@540 853 \\
adamc@540 854 \mt{proj}(M, \mt{datatype} \; x \; \overline{y} = \overline{dc} \; \overline{s}, \mt{datatype} \; x) &=& (\overline{y}, \overline{dc}) \\
adamc@540 855 \mt{proj}(M, \mt{datatype} \; x = \mt{datatype} \; M'.z \; \overline{s}, \mt{con} \; x) &=& \mt{proj}(M', \overline{s'}, \mt{datatype} \; z) \textrm{ (where $\Gamma \vdash M' : \mt{sig} \; \overline{s'} \; \mt{end}$)} \\
adamc@540 856 \\
adamc@540 857 \mt{proj}(M, \mt{val} \; x : \tau \; \overline{s}, \mt{val} \; x) &=& \tau \\
adamc@540 858 \mt{proj}(M, \mt{datatype} \; x \; \overline{y} = \overline{dc} \; \overline{s}, \mt{val} \; X) &=& \overline{y ::: \mt{Type}} \to M.x \; \overline y \textrm{ (where $X \in \overline{dc}$)} \\
adamc@540 859 \mt{proj}(M, \mt{datatype} \; x \; \overline{y} = \overline{dc} \; \overline{s}, \mt{val} \; X) &=& \overline{y ::: \mt{Type}} \to \tau \to M.x \; \overline y \textrm{ (where $X \; \mt{of} \; \tau \in \overline{dc}$)} \\
adamc@540 860 \mt{proj}(M, \mt{datatype} \; x = \mt{datatype} \; M'.z, \mt{val} \; X) &=& \overline{y ::: \mt{Type}} \to M.x \; \overline y \textrm{ (where $\Gamma \vdash M' : \mt{sig} \; \overline{s'} \; \mt{end}$} \\
adamc@540 861 && \textrm{and $\mt{proj}(M', \overline{s'}, \mt{datatype} \; z = (\overline{y}, \overline{dc})$ and $X \in \overline{dc}$)} \\
adamc@540 862 \mt{proj}(M, \mt{datatype} \; x = \mt{datatype} \; M'.z, \mt{val} \; X) &=& \overline{y ::: \mt{Type}} \to \tau \to M.x \; \overline y \textrm{ (where $\Gamma \vdash M' : \mt{sig} \; \overline{s'} \; \mt{end}$} \\
adamc@540 863 && \textrm{and $\mt{proj}(M', \overline{s'}, \mt{datatype} \; z = (\overline{y}, \overline{dc})$ and $X : \tau \in \overline{dc}$)} \\
adamc@540 864 \\
adamc@540 865 \mt{proj}(M, \mt{structure} \; X : S \; \overline{s}, \mt{structure} \; X) &=& S \\
adamc@540 866 \\
adamc@540 867 \mt{proj}(M, \mt{signature} \; X = S \; \overline{s}, \mt{signature} \; X) &=& S \\
adamc@540 868 \\
adamc@540 869 \mt{proj}(M, \mt{con} \; x :: \kappa \; \overline{s}, V) &=& [x \mapsto M.x]\mt{proj}(M, \overline{s}, V) \\
adamc@540 870 \mt{proj}(M, \mt{con} \; x :: \kappa = c \; \overline{s}, V) &=& [x \mapsto M.x]\mt{proj}(M, \overline{s}, V) \\
adamc@540 871 \mt{proj}(M, \mt{datatype} \; x \; \overline{y} = \overline{dc} \; \overline{s}, V) &=& [x \mapsto M.x]\mt{proj}(M, \overline{s}, V) \\
adamc@540 872 \mt{proj}(M, \mt{datatype} \; x = \mt{datatype} \; M'.z \; \overline{s}, V) &=& [x \mapsto M.x]\mt{proj}(M, \overline{s}, V) \\
adamc@540 873 \mt{proj}(M, \mt{val} \; x : \tau \; \overline{s}, V) &=& \mt{proj}(M, \overline{s}, V) \\
adamc@540 874 \mt{proj}(M, \mt{structure} \; X : S \; \overline{s}, V) &=& [X \mapsto M.X]\mt{proj}(M, \overline{s}, V) \\
adamc@540 875 \mt{proj}(M, \mt{signature} \; X = S \; \overline{s}, V) &=& [X \mapsto M.X]\mt{proj}(M, \overline{s}, V) \\
adamc@540 876 \mt{proj}(M, \mt{include} \; S \; \overline{s}, V) &=& \mt{proj}(M, \overline{s'} \; \overline{s}, V) \textrm{ (where $\Gamma \vdash S \equiv \mt{sig} \; \overline{s'} \; \mt{end}$)} \\
adamc@540 877 \mt{proj}(M, \mt{constraint} \; c_1 \sim c_2 \; \overline{s}, V) &=& \mt{proj}(M, \overline{s}, V) \\
adamc@540 878 \mt{proj}(M, \mt{class} \; x \; \overline{s}, V) &=& [x \mapsto M.x]\mt{proj}(M, \overline{s}, V) \\
adamc@540 879 \mt{proj}(M, \mt{class} \; x = c \; \overline{s}, V) &=& [x \mapsto M.x]\mt{proj}(M, \overline{s}, V) \\
adamc@540 880 \end{eqnarray*}
adamc@540 881
adamc@541 882
adamc@541 883 \section{Type Inference}
adamc@541 884
adamc@541 885 The Ur/Web compiler uses \emph{heuristic type inference}, with no claims of completeness with respect to the declarative specification of the last section. The rules in use seem to work well in practice. This section summarizes those rules, to help Ur programmers predict what will work and what won't.
adamc@541 886
adamc@541 887 \subsection{Basic Unification}
adamc@541 888
adamc@541 889 Type-checkers for languages based on the Hindly-Milner type discipline, like ML and Haskell, take advantage of \emph{principal typing} properties, making complete type inference relatively straightforward. Inference algorithms are traditionally implemented using type unification variables, at various points asserting equalities between types, in the process discovering the values of type variables. The Ur/Web compiler uses the same basic strategy, but the complexity of the type system rules out easy completeness.
adamc@541 890
adamc@541 891 Type-checking can require evaluating recursive functional programs, thanks to the type-level $\mt{fold}$ operator. When a unification variable appears in such a type, the next step of computation can be undetermined. The value of that variable might be determined later, but this would be ``too late'' for the unification problems generated at the first occurrence. This is the essential source of incompletness.
adamc@541 892
adamc@541 893 Nonetheless, the unification engine tends to do reasonably well. Unlike in ML, polymorphism is never inferred in definitions; it must be indicated explicitly by writing out constructor-level parameters. By writing these and other annotations, the programmer can generally get the type inference engine to do most of the type reconstruction work.
adamc@541 894
adamc@541 895 \subsection{Unifying Record Types}
adamc@541 896
adamc@541 897 The type inference engine tries to take advantage of the algebraic rules governing type-level records, as shown in Section \ref{definitional}. When two constructors of record kind are unified, they are reduce to normal forms, with like terms crossed off from each normal form until, hopefully, nothing remains. This cannot be complete, with the inclusion of unification variables. The type-checker can help you understand what goes wrong when the process fails, as it outputs the unmatched remainders of the two normal forms.
adamc@541 898
adamc@541 899 \subsection{\label{typeclasses}Type Classes}
adamc@541 900
adamc@541 901 Ur includes a type class facility inspired by Haskell's. The current version is very rudimentary, only supporting instances for particular types built up from abstract types and datatypes and type-level application.
adamc@541 902
adamc@541 903 Type classes are integrated with the module system. A type class is just a constructor of kind $\mt{Type} \to \mt{Type}$. By marking such a constructor $c$ as a type class, the programmer instructs the type inference engine to, in each scope, record all values of types $c \; \tau$ as \emph{instances}. Any function argument whose type is of such a form is treated as implicit, to be determined by examining the current instance database.
adamc@541 904
adamc@541 905 The ``dictionary encoding'' often used in Haskell implementations is made explicit in Ur. Type class instances are just properly-typed values, and they can also be considered as ``proofs'' of membership in the class. In some cases, it is useful to pass these proofs around explicitly. An underscore written where a proof is expected will also be inferred, if possible, from the current instance database.
adamc@541 906
adamc@541 907 Just as for types, type classes may be exported from modules, and they may be exported as concrete or abstract. Concrete type classes have their ``real'' definitions exposed, so that client code may add new instances freely. Abstract type classes are useful as ``predicates'' that can be used to enforce invariants, as we will see in some definitions of SQL syntax in the Ur/Web standard library.
adamc@541 908
adamc@541 909 \subsection{Reverse-Engineering Record Types}
adamc@541 910
adamc@541 911 It's useful to write Ur functions and functors that take record constructors as inputs, but these constructors can grow quite long, even though their values are often implied by other arguments. The compiler uses a simple heuristic to infer the values of unification variables that are folded over, yielding known results. Often, as in the case of $\mt{map}$-like folds, the base and recursive cases of a fold produce constructors with different top-level structure. Thus, if the result of the fold is known, examining its top-level structure reveals whether the record being folded over is empty or not. If it's empty, we're done; if it's not empty, we replace a single unification variable with a new constructor formed from three new unification variables, as in $[\alpha = \beta] \rc \gamma$. This process can often be repeated to determine a unification variable fully.
adamc@541 912
adamc@541 913 \subsection{Implicit Arguments in Functor Applications}
adamc@541 914
adamc@541 915 Constructor, constraint, and type class witness members of structures may be omitted, when those structures are used in contexts where their assigned signatures imply how to fill in those missing members. This feature combines well with reverse-engineering to allow for uses of complicated meta-programming functors with little more code than would be necessary to invoke an untyped, ad-hoc code generator.
adamc@541 916
adamc@541 917
adamc@524 918 \end{document}