Mercurial > urweb

comparison doc/manual.tex @ 530:c2f9f94ea709

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Kinding
author Adam Chlipala <adamc@hcoop.net>
date Sat, 29 Nov 2008 09:34:11 -0500
parents 4df69124e9c5
children e47eff8c9037
comparison
equal deleted inserted replaced
529:4df69124e9c5 530:c2f9f94ea709
66 \end{array}$$ 66 \end{array}$$
67 67
68 \emph{Constructors} are the main class of compile-time-only data. They include proper types and are classified by kinds. 68 \emph{Constructors} are the main class of compile-time-only data. They include proper types and are classified by kinds.
69 $$\begin{array}{rrcll} 69 $$\begin{array}{rrcll}
70 \textrm{Constructors} & c, \tau &::=& (c) :: \kappa & \textrm{kind annotation} \\ 70 \textrm{Constructors} & c, \tau &::=& (c) :: \kappa & \textrm{kind annotation} \\
71 &&& x & \textrm{constructor variable} \\ 71 &&& \hat{x} & \textrm{constructor variable} \\
72 \\ 72 \\
73 &&& \tau \to \tau & \textrm{function type} \\ 73 &&& \tau \to \tau & \textrm{function type} \\
74 &&& x \; ? \; \kappa \to \tau & \textrm{polymorphic function type} \\ 74 &&& x \; ? \; \kappa \to \tau & \textrm{polymorphic function type} \\
75 &&& \$ c & \textrm{record type} \\ 75 &&& \$ c & \textrm{record type} \\
76 \\ 76 \\
77 &&& c \; c & \textrm{type-level function application} \\ 77 &&& c \; c & \textrm{type-level function application} \\
78 &&& \lambda x \; ? \; \kappa \Rightarrow c & \textrm{type-level function abstraction} \\ 78 &&& \lambda x \; :: \; \kappa \Rightarrow c & \textrm{type-level function abstraction} \\
79 \\ 79 \\
80 &&& () & \textrm{type-level unit} \\ 80 &&& () & \textrm{type-level unit} \\
81 &&& \#X & \textrm{field name} \\ 81 &&& \#X & \textrm{field name} \\
82 \\ 82 \\
83 &&& [(c = c)^*] & \textrm{known-length type-level record} \\ 83 &&& [(c = c)^*] & \textrm{known-length type-level record} \\
89 \\ 89 \\
90 &&& \lambda [c \sim c] \Rightarrow c & \textrm{guarded constructor} \\ 90 &&& \lambda [c \sim c] \Rightarrow c & \textrm{guarded constructor} \\
91 \\ 91 \\
92 &&& \_ :: \kappa & \textrm{wildcard} \\ 92 &&& \_ :: \kappa & \textrm{wildcard} \\
93 &&& (c) & \textrm{explicit precedence} \\ 93 &&& (c) & \textrm{explicit precedence} \\
94 \\
95 \textrm{Qualified uncapitalized variables} & \hat{x} &::=& x & \textrm{not from a module} \\
96 &&& M.x & \textrm{projection from a module} \\
94 \end{array}$$ 97 \end{array}$$
95 98
96 Modules of the module system are described by \emph{signatures}. 99 Modules of the module system are described by \emph{signatures}.
97 $$\begin{array}{rrcll} 100 $$\begin{array}{rrcll}
98 \textrm{Signatures} & S &::=& \mt{sig} \; s^* \; \mt{end} & \textrm{constant} \\ 101 \textrm{Signatures} & S &::=& \mt{sig} \; s^* \; \mt{end} & \textrm{constant} \\
160 &&& \_ & \textrm{wildcard} \\ 163 &&& \_ & \textrm{wildcard} \\
161 &&& (e) & \textrm{explicit precedence} \\ 164 &&& (e) & \textrm{explicit precedence} \\
162 \\ 165 \\
163 \textrm{Local declarations} & ed &::=& \cd{val} \; x : \tau = e & \textrm{non-recursive value} \\ 166 \textrm{Local declarations} & ed &::=& \cd{val} \; x : \tau = e & \textrm{non-recursive value} \\
164 &&& \cd{val} \; \cd{rec} \; (x : \tau = e \; \cd{and})^+ & \textrm{mutually-recursive values} \\ 167 &&& \cd{val} \; \cd{rec} \; (x : \tau = e \; \cd{and})^+ & \textrm{mutually-recursive values} \\
165 \\
166 \textrm{Qualified uncapitalized variables} & \hat{x} &::=& x & \textrm{not from a module} \\
167 &&& M.x & \textrm{projection from a module} \\
168 \end{array}$$ 168 \end{array}$$
169 169
170 \emph{Declarations} primarily bring new symbols into context. 170 \emph{Declarations} primarily bring new symbols into context.
171 $$\begin{array}{rrcll} 171 $$\begin{array}{rrcll}
172 \textrm{Declarations} & d &::=& \mt{con} \; x :: \kappa = c & \textrm{constructor synonym} \\ 172 \textrm{Declarations} & d &::=& \mt{con} \; x :: \kappa = c & \textrm{constructor synonym} \\
227 227
228 There are infix operator syntaxes for a number of functions defined in the $\mt{Basis}$ module. There is $=$ for $\mt{eq}$, $\neq$ for $\mt{neq}$, $-$ for $\mt{neg}$ (as a prefix operator) and $\mt{minus}$, $+$ for $\mt{plus}$, $\times$ for $\mt{times}$, $/$ for $\mt{div}$, $\%$ for $\mt{mod}$, $<$ for $\mt{lt}$, $\leq$ for $\mt{le}$, $>$ for $\mt{gt}$, and $\geq$ for $\mt{ge}$. 228 There are infix operator syntaxes for a number of functions defined in the $\mt{Basis}$ module. There is $=$ for $\mt{eq}$, $\neq$ for $\mt{neq}$, $-$ for $\mt{neg}$ (as a prefix operator) and $\mt{minus}$, $+$ for $\mt{plus}$, $\times$ for $\mt{times}$, $/$ for $\mt{div}$, $\%$ for $\mt{mod}$, $<$ for $\mt{lt}$, $\leq$ for $\mt{le}$, $>$ for $\mt{gt}$, and $\geq$ for $\mt{ge}$.
229 229
230 A signature item $\mt{table} \; x : c$ is shorthand for $\mt{val} \; x : \mt{Basis}.\mt{sql\_table} \; c$. $\mt{sequence} \; x$ is short for $\mt{val} \; x : \mt{Basis}.\mt{sql\_sequence}$, and $\mt{cookie} \; x : \tau$ is shorthand for $\mt{val} \; x : \mt{Basis}.\mt{http\_cookie} \; \tau$. 230 A signature item $\mt{table} \; x : c$ is shorthand for $\mt{val} \; x : \mt{Basis}.\mt{sql\_table} \; c$. $\mt{sequence} \; x$ is short for $\mt{val} \; x : \mt{Basis}.\mt{sql\_sequence}$, and $\mt{cookie} \; x : \tau$ is shorthand for $\mt{val} \; x : \mt{Basis}.\mt{http\_cookie} \; \tau$.
231 231
232
233 \section{Static Semantics}
234
235 In this section, we give a declarative presentation of Ur's typing rules and related judgments. Inference is the subject of the next section; here, we assume that an oracle has filled in all wildcards with concrete values.
236
237 Since there is significant mutual recursion among the judgments, we introduce them all before beginning to give rules. We use the same variety of contexts throughout this section, implicitly introducing new sorts of context entries as needed.
238 \begin{itemize}
239 \item $\Gamma \vdash c :: \kappa$ assigns a kind to a constructor in a context.
240 \item $\Gamma \vdash c \sim c$ proves the disjointness of two record constructors; that is, that they share no field names. We overload the judgment to apply to pairs of field names as well.
241 \item $\Gamma \vdash c \hookrightarrow \overline{c}$ proves that record constructor $c$ decomposes into set $\overline{c}$ of field names and record constructors.
242 \item $\Gamma \vdash c \equiv c$ proves the computational equivalence of two constructors. This is often called a \emph{definitional equality} in the world of type theory.
243 \item $\Gamma \vdash e : \tau$ is a standard typing judgment.
244 \item $\Gamma \vdash M : S$ is the module signature checking judgment.
245 \item $\mt{proj}(M, S, V)$ is a partial function for projecting a signature item from a signature $S$, given the module $M$ that we project from. $V$ may be $\mt{con} \; x$, $\mt{val} \; x$, $\mt{signature} \; X$, or $\mt{structure} \; X$. The parameter $M$ is needed because the projected signature item may refer to other items of $S$.
246 \end{itemize}
247
248 \subsection{Kinding}
249
250 $$\infer{\Gamma \vdash (c) :: \kappa :: \kappa}{
251 \Gamma \vdash c :: \kappa
252 }
253 \quad \infer{\Gamma \vdash x :: \kappa}{
254 x :: \kappa \in \Gamma
255 }
256 \quad \infer{\Gamma \vdash x :: \kappa}{
257 x :: \kappa = c \in \Gamma
258 }$$
259
260 $$\infer{\Gamma \vdash M.x :: \kappa}{
261 \Gamma \vdash M : S
262 & \mt{proj}(M, S, \mt{con} \; x) = \kappa
263 }
264 \quad \infer{\Gamma \vdash M.x :: \kappa}{
265 \Gamma \vdash M : S
266 & \mt{proj}(M, S, \mt{con} \; x) = (\kappa, c)
267 }$$
268
269 $$\infer{\Gamma \vdash \tau_1 \to \tau_2 :: \mt{Type}}{
270 \Gamma \vdash \tau_1 :: \mt{Type}
271 & \Gamma \vdash \tau_2 :: \mt{Type}
272 }
273 \quad \infer{\Gamma \vdash x \; ? \: \kappa \to \tau :: \mt{Type}}{
274 \Gamma, x :: \kappa \vdash \tau :: \mt{Type}
275 }
276 \quad \infer{\Gamma \vdash \$c :: \mt{Type}}{
277 \Gamma \vdash c :: \{\mt{Type}\}
278 }$$
279
280 $$\infer{\Gamma \vdash c_1 \; c_2 :: \kappa_2}{
281 \Gamma \vdash c_1 :: \kappa_1 \to \kappa_2
282 & \Gamma \vdash c_2 :: \kappa_1
283 }
284 \quad \infer{\Gamma \vdash \lambda x \; :: \; \kappa_1 \Rightarrow c :: \kappa_1 \to \kappa_2}{
285 \Gamma, x :: \kappa_1 \vdash c :: \kappa_2
286 }$$
287
288 $$\infer{\Gamma \vdash () :: \mt{Unit}}{}
289 \quad \infer{\Gamma \vdash \#X :: \mt{Name}}{}$$
290
291 $$\infer{\Gamma \vdash [\overline{c_i = c'_i}] :: \{\kappa\}}{
292 \forall i: \Gamma \vdash c_i : \mt{Name}
293 & \Gamma \vdash c'_i :: \kappa
294 & \forall i \neq j: \Gamma \vdash c_i \sim c_j
295 }
296 \quad \infer{\Gamma \vdash c_1 \rc c_2 :: \{\kappa\}}{
297 \Gamma \vdash c_1 :: \{\kappa\}
298 & \Gamma \vdash c_2 :: \{\kappa\}
299 & \Gamma \vdash c_1 \sim c_2
300 }$$
301
302 $$\infer{\Gamma \vdash \mt{fold} :: ((\mt{Name} \to \kappa_1 \to \kappa_2 \to \kappa_2) \to \kappa_2 \to \{\kappa_1\} \to \kappa_2}{}$$
303
304 $$\infer{\Gamma \vdash (\overline c) :: (k_1 \times \ldots \times k_n)}{
305 \forall i: \Gamma \vdash c_i :: k_i
306 }
307 \quad \infer{\Gamma \vdash c.i :: k_i}{
308 \Gamma \vdash c :: (k_1 \times \ldots \times k_n)
309 }$$
310
311 $$\infer{\Gamma \vdash \lambda [c_1 \sim c_2] \Rightarrow c :: \kappa}{
312 \Gamma \vdash c_1 :: \{\kappa'\}
313 & \Gamma \vdash c_2 :: \{\kappa'\}
314 & \Gamma, c_1 \sim c_2 \vdash c :: \kappa
315 }$$
316
232 \end{document} 317 \end{document}