Mercurial > urweb

comparison doc/manual.tex @ 531:e47eff8c9037

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Disjointness
author Adam Chlipala <adamc@hcoop.net>
date Sat, 29 Nov 2008 09:48:10 -0500
parents c2f9f94ea709
children 23718a4b23d7
comparison
equal deleted inserted replaced
530:c2f9f94ea709 531:e47eff8c9037
236 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. 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} 238 \begin{itemize}
239 \item $\Gamma \vdash c :: \kappa$ assigns a kind to a constructor in a context. 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. 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. 241 \item $\Gamma \vdash c \hookrightarrow C$ proves that record constructor $c$ decomposes into set $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. 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. 243 \item $\Gamma \vdash e : \tau$ is a standard typing judgment.
244 \item $\Gamma \vdash M : S$ is the module signature checking 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$. 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} 246 \end{itemize}
312 \Gamma \vdash c_1 :: \{\kappa'\} 312 \Gamma \vdash c_1 :: \{\kappa'\}
313 & \Gamma \vdash c_2 :: \{\kappa'\} 313 & \Gamma \vdash c_2 :: \{\kappa'\}
314 & \Gamma, c_1 \sim c_2 \vdash c :: \kappa 314 & \Gamma, c_1 \sim c_2 \vdash c :: \kappa
315 }$$ 315 }$$
316 316
317 \subsection{Record Disjointness}
318
319 We will use a keyword $\mt{map}$ as a shorthand, such that, for $f$ of kind $\kappa \to \kappa'$, $\mt{map} \; f$ stands for $\mt{fold} \; (\lambda (x_1 :: \mt{Name}) (x_2 :: \kappa) (x_3 :: \{\kappa'\}) \Rightarrow [x_1 = f \; x_2] \rc x_3) \; []$.
320
321 $$\infer{\Gamma \vdash c_1 \sim c_2}{
322 \Gamma \vdash c_1 \hookrightarrow c'_1
323 & \Gamma \vdash c_2 \hookrightarrow c'_2
324 & \forall c''_1 \in c'_1, c''_2 \in c'_2: \Gamma \vdash c''_1 \sim c''_2
325 }
326 \quad \infer{\Gamma \vdash X \sim X'}{
327 X \neq X'
328 }$$
329
330 $$\infer{\Gamma \vdash c_1 \sim c_2}{
331 c'_1 \sim c'_2 \in \Gamma
332 & \Gamma \vdash c'_1 \hookrightarrow c''_1
333 & \Gamma \vdash c'_2 \hookrightarrow c''_2
334 & c_1 \in c''_1
335 & c_2 \in c''_2
336 }$$
337
338 $$\infer{\Gamma \vdash c \hookrightarrow \{c\}}{}
339 \quad \infer{\Gamma \vdash [\overline{c = c'}] \hookrightarrow \{\overline{c}\}}{}
340 \quad \infer{\Gamma \vdash c_1 \rc c_2 \hookrightarrow C_1 \cup C_2}{
341 \Gamma \vdash c_1 \hookrightarrow C_1
342 & \Gamma \vdash c_2 \hookrightarrow C_2
343 }
344 \quad \infer{\Gamma \vdash c \hookrightarrow C}{
345 \Gamma \vdash c \equiv c'
346 & \Gamma \vdash c' \hookrightarrow C
347 }
348 \quad \infer{\Gamma \vdash \mt{map} \; f \; c \hookrightarrow C}{
349 \Gamma \vdash c \hookrightarrow C
350 }$$
351
352
317 \end{document} 353 \end{document}